@[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

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

Equations

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

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

Auxiliary inductive type for representing contraints 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

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

Equations

• Lean.Meta.Grind.Arith.Offset.instInhabitedToPropagate = { default := Lean.Meta.Grind.Arith.Offset.ToPropagate.eqTrue default default default default 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 ENodeKey NodeId

  Mapping from Expr to a node representing it.

• cnstrs : PHashMap ENodeKey (Cnstr NodeId)

  Mapping from Expr representing inequalites 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.

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

Equations

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

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

State for the arithmetic procedures.

• offset : Offset.State

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

Equations

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