inductive Lean.Meta.Grind.Arith.Cutsat.CaseKind : Type

In principle, we only need to support two kinds of case split.

• Disequalities.
• Cooper-Left, but we have 4 different variants of this one.

• diseq (d : DiseqCnstr) : CaseKind
• cooper (s : CooperSplitPred) (hs : Array (FVarId × UnsatProof)) (decVars : FVarIdSet) : CaseKind

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedCaseKind : Inhabited CaseKind

structure Lean.Meta.Grind.Arith.Cutsat.Case : Type

• kind : CaseKind
• fvarId : FVarId

  Decision variable used to represent the case-split. For example, suppose we are splitting on p ≠ 0. Then, we create a decision variable h : p + 1 ≤ 0

• saved : State

  Snapshot of the cutsat state for backtracking purposes. We do not use a trail stack.

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedCase : Inhabited Case

inductive Lean.Meta.Grind.Arith.Cutsat.Search.Kind : Type

• rat : Kind

  Allow variables to be assigned to rational numbers during model construction.

• int : Kind

  Variables must be assigned to integer numbers. Cooper case splits are required in this mode.

instance Lean.Meta.Grind.Arith.Cutsat.Search.instInhabitedKind : Inhabited Kind

instance Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind : BEq Kind

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

State of the model search procedure.

• cases : PArray Case

  Decision stack (aka case-split stack)

• precise : Bool

  precise := false if not all constraints were satisfied during the search.

• decVars : FVarIdSet

  Set of decision variables in cases.

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.SearchM (α : Type) : Type

def Lean.Meta.Grind.Arith.Cutsat.isApprox : SearchM Bool

Returns true if approximations are allowed.

def Lean.Meta.Grind.Arith.Cutsat.setImprecise : SearchM Unit

Sets precise to false to indicate that some constraint was not satisfied.

def Lean.Meta.Grind.Arith.Cutsat.mkCase (kind : CaseKind) : SearchM FVarId