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_reducible]

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCaseKind = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedCaseKind.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.

@[instance_reducible]

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

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCase = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedCase.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.

@[instance_reducible]

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.instInhabitedKind.default }

@[instance_reducible]

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.instBEqKind.beq }

def Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind.beq : Kind → Kind → Bool

Equations

• Lean.Meta.Grind.Arith.Cutsat.Search.instBEqKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

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.

• steps : Nat

  Number of steps performed by the current search. Remark: we cannot use the steps counter in the cutsat state because it is rolled back when backtracking case splits.

@[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, steps := s.steps }

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

Increments the search steps counter, and returns true if the cumulative number of steps reached the liaSteps configuration threshold.

Equations

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

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

Adds the number of steps performed by the current search to the cumulative counter in the cutsat state. It must be invoked after resetDecisionStack because backtracking rolls back the cutsat state.

Equations

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

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

Equations

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