@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Offset.NodeId : Type

Equations

• Lean.Meta.Grind.Arith.Offset.NodeId = Nat

instance Lean.Meta.Grind.Arith.Offset.instToMessageDataCnstrNodeId : ToMessageData (Cnstr NodeId)

Equations

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

structure Lean.Meta.Grind.Arith.Offset.ProofInfo : Type

Auxiliary structure used for proof extraction.

• w : NodeId
• k : Int
• proof : Expr

def Lean.Meta.Grind.Arith.Offset.instInhabitedProofInfo.default : ProofInfo

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedProofInfo.default = { w := default, k := default, proof := default }

instance Lean.Meta.Grind.Arith.Offset.instInhabitedProofInfo : Inhabited ProofInfo

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedProofInfo = { default := Lean.Meta.Grind.Arith.Offset.instInhabitedProofInfo.default }

inductive Lean.Meta.Grind.Arith.Offset.ToPropagate : Type

Auxiliary inductive type for representing constraints and equalities that should be propagated to core. Recall that we cannot compute proofs until the short-distance data-structures have been fully updated when a new edge is inserted. Thus, we store the information to be propagated into a list. See field propagate in State.

• eqTrue (e : Expr) (u v : NodeId) (k k' : Int) : ToPropagate
• eqFalse (e : Expr) (u v : NodeId) (k k' : Int) : ToPropagate
• eq (u v : NodeId) : ToPropagate

def Lean.Meta.Grind.Arith.Offset.instInhabitedToPropagate.default : ToPropagate

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedToPropagate.default = Lean.Meta.Grind.Arith.Offset.ToPropagate.eqTrue default default default default default

instance Lean.Meta.Grind.Arith.Offset.instInhabitedToPropagate : Inhabited ToPropagate

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedToPropagate = { default := Lean.Meta.Grind.Arith.Offset.instInhabitedToPropagate.default }

structure Lean.Meta.Grind.Arith.Offset.State : Type

State of the constraint offset procedure.

• nodes : PArray Expr

  Mapping from NodeId to the Expr represented by the node.

• nodeMap : PHashMap ExprPtr NodeId

  Mapping from Expr to a node representing it.

• cnstrs : PHashMap ExprPtr (Cnstr NodeId)

  Mapping from Expr representing inequalities to constraints.

• cnstrsOf : PHashMap (NodeId × NodeId) (List (Cnstr NodeId × Expr))

  Mapping from pairs (u, v) to a list of offset constraints on u and v. We use this mapping to implement exhaustive constraint propagation.

• sources : PArray (AssocList NodeId Int)

  For each node with id u, sources[u] contains pairs (v, k) s.t. there is a path from v to u with weight k.

• targets : PArray (AssocList NodeId Int)

  For each node with id u, targets[u] contains pairs (v, k) s.t. there is a path from u to v with weight k.

• proofs : PArray (AssocList NodeId ProofInfo)

  Proof reconstruction information. For each node with id u, proofs[u] contains pairs (v, { w, proof }) s.t. there is a path from u to v, and w is the penultimate node in the path, and proof is the justification for the last edge.

• propagate : List ToPropagate

  Truth values and equalities to propagate to core.

def Lean.Meta.Grind.Arith.Offset.instInhabitedState.default : State

Equations

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

instance Lean.Meta.Grind.Arith.Offset.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedState = { default := Lean.Meta.Grind.Arith.Offset.instInhabitedState.default }

opaque Lean.Meta.Grind.Arith.Offset.offsetExt : SolverExtension State