Helper functions for constructing counterexamples in the linarith and cutsat modules

def Lean.Meta.Grind.Arith.pickUnusedValue (goal : Goal) (a : Std.HashMap Expr Std.Internal.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.

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

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 : Std.Internal.Rat) (a : Std.HashMap Expr Std.Internal.Rat) : Std.HashMap Expr Std.Internal.Rat

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

def Lean.Meta.Grind.Arith.finalizeModel (goal : Goal) (isTarget : ENode → MetaM Bool) (model : Std.HashMap Expr Std.Internal.Rat) : MetaM (Array (Expr × Std.Internal.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.

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

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