Helper functions for constructing counterexamples in the linarith and cutsat modules

def Lean.Meta.Grind.Arith.pickUnusedValue (goal : Goal) (a : Std.HashMap Expr Rat) (e : Expr) (next : Int) (alreadyUsed : Std.HashSet Int) : Int

Returns an integer value i for assigning to e s.t. adding e := i to a will not falsify any disequality and i is not in alreadyUsed.

Equations

• Lean.Meta.Grind.Arith.pickUnusedValue goal a e next alreadyUsed = Lean.Meta.Grind.Arith.pickUnusedValue.go✝ goal a e alreadyUsed next

def Lean.Meta.Grind.Arith.isInterpretedTerm (e : Expr) : Bool

Returns true if e should be treated as an interpreted value by the arithmetic modules.

def Lean.Meta.Grind.Arith.assignEqc (goal : Goal) (e : Expr) (v : Rat) (a : Std.HashMap Expr Rat) : Std.HashMap Expr Rat

Adds the assignments e' := v to a for each e' in the equivalence class os e.

Equations

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

def Lean.Meta.Grind.Arith.finalizeModel (goal : Goal) (isTarget : ENode → MetaM Bool) (model : Std.HashMap Expr Rat) : MetaM (Array (Expr × Rat))

Converts the given model into a sorted array of pairs (e, v) representing assignments e := v. isTarget is a predicate used to detect terms that must be in the model but have not been assigned a value (see: assignUnassigned) The pairs are sorted using es generation and then Expr.lt. Only terms s.t. isInterpretedTerm e = false are included into the resulting array.

Equations

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

def Lean.Meta.Grind.Arith.traceModel (traceClass : Name) (model : Array (Expr × Rat)) : MetaM Unit

If the given trace class is enabled, trace the model using the class.

Equations

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