source
@[reducible, inline]
abbrev Lean.Meta.Grind.Arith.Offset.NodeId :
Type
Equations

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

Instances For

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

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

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

Auxiliary structure used for proof extraction.

- w : NodeId
- k : Int
- proof : Expr

Instances For

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

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

Instances For

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

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

source
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

Instances For

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

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

source
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

Instances For

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

Instances For

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

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

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

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

Instances For

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