This module implements a decision procedure for offset constraints of the form:

x + k ≤ y
x ≤ y + k

where k is a numeral. Each constraint is represented as an edge in a weighted graph. The constraint x + k ≤ y is represented as a negative edge. The shortest path between two nodes in the graph corresponds to an implied inequality. When adding a new edge, the state is considered unsatisfiable if the new edge creates a negative cycle. An incremental Floyd-Warshall algorithm is used to find the shortest paths between all nodes. This module can also handle offset equalities of the form x + k = y by representing them with two edges:

x + k ≤ y
y ≤ x + k

The main advantage of this module over a full linear integer arithmetic procedure is its ability to efficiently detect all implied equalities and inequalities.

def Lean.Meta.Grind.Arith.Offset.get' : GoalM State

@[inline]

def Lean.Meta.Grind.Arith.Offset.modify' (f : State → State) : GoalM Unit

def Lean.Meta.Grind.Arith.Offset.mkNode (expr : Expr) : GoalM NodeId

def Lean.Meta.Grind.Arith.Offset.Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr

def Lean.Meta.Grind.Arith.Offset.checkInvariants : GoalM Unit

def Lean.Meta.Grind.Arith.Offset.addEdge (u v : NodeId) (k : Int) (p : Expr) : GoalM Unit

Adds an edge u --(k) --> v justified by the proof term p, and then if no negative cycle was created, updates the shortest distance of affected node pairs.

def Lean.Meta.Grind.Arith.Offset.addEdge.update (u v : NodeId) (k : Int) : GoalM Unit

def Lean.Meta.Grind.Arith.Offset.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit

@[export lean_process_new_offset_eq]

def Lean.Meta.Grind.Arith.Offset.processNewEqImpl (a b : Expr) : GoalM Unit

def Lean.Meta.Grind.Arith.Offset.traceDists : GoalM Unit