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.

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

- Lean.Meta.Grind.Arith.Offset.get' = Lean.Meta.Grind.Arith.Offset.offsetExt.getState

Instances For

source
@[inline]
def Lean.Meta.Grind.Arith.Offset.modify' (f : State → State) :
GoalM Unit
Equations

- Lean.Meta.Grind.Arith.Offset.modify' f = Lean.Meta.Grind.Arith.Offset.offsetExt.modifyState f

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For

source
def Lean.Meta.Grind.Arith.Offset.processNewEq (a b : Expr) :
GoalM Unit
Equations

- One or more equations did not get rendered due to their size.

Instances For

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

- One or more equations did not get rendered due to their size.

Instances For