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

Instances For

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCaseKind

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCaseKind = { default := Lean.Meta.Grind.Arith.Cutsat.CaseKind.cooper default default default }

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.

Instances For

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCase

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCase = { default := { kind := default, fvarId := default, saved := default } }

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.

Instances For

• Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind
• Lean.Meta.Grind.Arith.Cutsat.Search.instInhabitedKind

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.Search.instInhabitedKind = { default := Lean.Meta.Grind.Arith.Cutsat.Search.Kind.rat }

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind = { beq := Lean.Meta.Grind.Arith.Cutsat.Search.beqKind✝ }

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.SearchM = ReaderT Lean.Meta.Grind.Arith.Cutsat.Search.Kind (StateRefT' IO.RealWorld Lean.Meta.Grind.Arith.Cutsat.Search.State Lean.Meta.Grind.GoalM)

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

Returns true if approximations are allowed.

Equations

• Lean.Meta.Grind.Arith.Cutsat.isApprox = do let __do_lift ← read pure (__do_lift == Lean.Meta.Grind.Arith.Cutsat.Search.Kind.rat)

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

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.setImprecise = modify fun (s : Lean.Meta.Grind.Arith.Cutsat.Search.State) => { cases := s.cases, precise := false, decVars := s.decVars }

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

Equations

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