instance Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean : Hashable Poly

Equations

• Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean = { hash := Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean.hash }

def Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean.hash : Poly → UInt64

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.Grind.Arith.Cutsat.instHashablePoly_lean.hash (Int.Linear.Poly.num a) = mixHash 0 (hash a)

This module implements a model-based decision procedure for linear integer arithmetic, inspired by Section 4 of "Cutting to the Chase: Solving Linear Integer Arithmetic". Our implementation includes several enhancements and modifications: Key Features:

• Extended constraint support (equality and disequality)
• Optimized encoding of Cooper-Left rule using "big"-disjunction instead of fresh variables
• Decision variable tracking for case splits (disequalities, Cooper-Left, Cooper-Right)

Constraint Types: We handle four categories of linear polynomial constraints (where p is a linear polynomial):

1. Equality: p = 0
2. Divisibility: d ∣ p
3. Inequality: p ≤ 0
4. Disequality: p ≠ 0

Implementation Details:

• Polynomials use Int.Linear.Poly with sorted linear monomials (leading monomial contains max variable)
• Equalities are eliminated eagerly
• Divisibility constraints are maintained in solved form (one constraint per variable) using Div-Solve

Model Construction: The procedure builds a model incrementally, resolving conflicts through constraint generation. For example: Given a partial model {x := 1} and constraint 3 ∣ 3*y + x + 1:

• Cannot extend to y because 3 ∣ 3*y + 2 is unsatisfiable
• Generate implied constraint 3 ∣ x + 1
• Force model update for x

Variable Assignment: When assigning a variable y, we consider:

• Best upper and lower bounds (inequalities)
• Divisibility constraint
• Disequality constraints Cooper-Left and Cooper-Right rules handle the combination of inequalities and divisibility. For unsatisfiable disequalities p ≠ 0, we generate case split: p + 1 ≤ 0 ∨ -p + 1 ≤ 0

Contradiction Handling:

• Check dependency on decision variables
• If independent, use contradiction to close current grind goal
• Otherwise, trigger backtracking

Optimization: We employ rational approximation for model construction:

• Continue with rational solutions when integer solutions aren't immediately found
• Helps identify simpler unsatisfiability proofs before full integer model construction

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

A equality constraint and its justification/proof.

• p : Poly
• h : EqCnstrProof

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

• core0 (a zero : Expr) : EqCnstrProof

  An equality a = 0 coming from the core.

• core (a b : Expr) (p₁ p₂ : Poly) : EqCnstrProof

  An equality a = b coming from the core. p₁ and p₂ are the polynomials corresponding to a and b.

• coreToInt (a b toIntThm : Expr) (lhs rhs : Int.Linear.Expr) : EqCnstrProof
• defn (e : Expr) (p : Poly) : EqCnstrProof

  e is p

• defnNat (h : Expr) (x : Var) (e' : Int.Linear.Expr) : EqCnstrProof
• norm (c : EqCnstr) : EqCnstrProof
• divCoeffs (c : EqCnstr) : EqCnstrProof
• subst (x : Var) (c₁ c₂ : EqCnstr) : EqCnstrProof
• ofLeGe (c₁ c₂ : LeCnstr) : EqCnstrProof
• reorder (c : EqCnstr) : EqCnstrProof
• commRingNorm (c : EqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly) : EqCnstrProof
• defnCommRing (e : Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly) : EqCnstrProof
• defnNatCommRing (h : Expr) (x : Var) (e' : Int.Linear.Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly) : EqCnstrProof
• mul (a? : Option Expr) (cs : Array (Expr × Int × EqCnstr)) : EqCnstrProof
• div (k : Int) (y? : Option Var) (c : EqCnstr) : EqCnstrProof

  Linearization proof for /

  • If ?y = some y, then it is a proof for a / b = y / k where c is a proof that b = k
  • If ?y = none, then it is a proof for a / b = a/k where c is a proof that b = k. a is a numeral in this case.
• mod (k : Int) (y? : Option Var) (c : EqCnstr) : EqCnstrProof

  Linearization proof for %

  • If ?y = some y, then it is a proof for a % b = y%k where c is a proof that b = k
  • If ?y = none, then it is a proof for a % b = a%k where c is a proof that b = k. a is a numeral in this case.
• pow (ka : Int) (ca? : Option EqCnstr) (kb : Nat) (cb? : Option EqCnstr) : EqCnstrProof

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

A divisibility constraint and its justification/proof.

• d : Int
• p : Poly
• h : DvdCnstrProof

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

The predicate of type Nat → Prop, which serves as the conclusion of the cooper_left, cooper_right, cooper_dvd_left, and cooper_dvd_right theorems.

The specific predicate used is determined as follows:

• cooper_left_split (if left is true and c₃? is none)
• cooper_right_split (if left is false and c₃? is none)
• cooper_dvd_left_split (if left is true and c₃? is some)
• cooper_dvd_right_split (if left is false and c₃? is some)

See CooperSplit

• left : Bool
• c₁ : LeCnstr
• c₂ : LeCnstr
• c₃? : Option DvdCnstr

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

An instance of the CooperSplitPred at k.

• pred : CooperSplitPred
• k : Nat
• h : CooperSplitProof

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

The cooper_left, cooper_right, cooper_dvd_left, and cooper_dvd_right theorems have a resulting type that is a big-or of the form OrOver n (cooper_*_split ...). The predicate (cooper_*_split ...) has type Nat → Prop. The cutsat procedure performs case splitting on (cooper_*_split ... (n-1)) down to (cooper_*_split ... 1). If it derives False from each case, it uses orOver_resolve and orOver_one to deduce the final case, which has type (cooper_*_split ... 0).

• dec (h : FVarId) : CooperSplitProof

  The first n-1 cases are decisions (aka case-splits).

• last (hs : Array (FVarId × UnsatProof)) (decVars : Array FVarId) : CooperSplitProof

  The last case which has type (cooper_*_split ... 0)

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

• core (e : Expr) : DvdCnstrProof

  Given e of the form k ∣ p s.t. e = True in the core.

• coreOfNat (e thm : Expr) (d : Nat) (a : Int.Linear.Expr) : DvdCnstrProof
• norm (c : DvdCnstr) : DvdCnstrProof
• divCoeffs (c : DvdCnstr) : DvdCnstrProof
• solveCombine (c₁ c₂ : DvdCnstr) : DvdCnstrProof
• solveElim (c₁ c₂ : DvdCnstr) : DvdCnstrProof
• elim (c : DvdCnstr) : DvdCnstrProof
• ofEq (x : Var) (c : EqCnstr) : DvdCnstrProof
• subst (x : Var) (c₁ : EqCnstr) (c₂ : DvdCnstr) : DvdCnstrProof
• cooper₁ (c : CooperSplit) : DvdCnstrProof
• cooper₂ (c : CooperSplit) : DvdCnstrProof

  c.c₃? must be some

• reorder (c : DvdCnstr) : DvdCnstrProof
• commRingNorm (c : DvdCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly) : DvdCnstrProof

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

An inequality constraint and its justification/proof.

• p : Poly
• h : LeCnstrProof

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

• core (e : Expr) : LeCnstrProof
• coreNeg (e : Expr) (p : Poly) : LeCnstrProof
• coreToInt (e : Expr) (pos : Bool) (toIntThm : Expr) (lhs rhs : Int.Linear.Expr) : LeCnstrProof
• ofNatNonneg (a : Expr) : LeCnstrProof
• bound (h : Expr) : LeCnstrProof
• dec (h : FVarId) : LeCnstrProof
• norm (c : LeCnstr) : LeCnstrProof
• divCoeffs (c : LeCnstr) : LeCnstrProof
• combine (c₁ c₂ : LeCnstr) : LeCnstrProof
• combineDivCoeffs (c₁ c₂ : LeCnstr) (k : Int) : LeCnstrProof
• subst (x : Var) (c₁ : EqCnstr) (c₂ : LeCnstr) : LeCnstrProof
• ofLeDiseq (c₁ : LeCnstr) (c₂ : DiseqCnstr) : LeCnstrProof
• ofDiseqSplit (c₁ : DiseqCnstr) (decVar : FVarId) (h : UnsatProof) (decVars : Array FVarId) : LeCnstrProof
• cooper (c : CooperSplit) : LeCnstrProof
• dvdTight (c₁ : DvdCnstr) (c₂ : LeCnstr) : LeCnstrProof
• negDvdTight (c₁ : DvdCnstr) (c₂ : LeCnstr) : LeCnstrProof
• reorder (c : LeCnstr) : LeCnstrProof
• commRingNorm (c : LeCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly) : LeCnstrProof

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

A disequality constraint and its justification/proof.

• p : Poly
• h : DiseqCnstrProof

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

• core0 (a zero : Expr) : DiseqCnstrProof

  An disequality a != 0 coming from the core. That is, (a = 0) = False in the core.

• core (a b : Expr) (p₁ p₂ : Poly) : DiseqCnstrProof

  An disequality a ≠ b coming from the core. That is, (a = b) = False in the core. p₁ and p₂ are the polynomials corresponding to a and b.

• coreToInt (a b toIntThm : Expr) (lhs rhs : Int.Linear.Expr) : DiseqCnstrProof
• norm (c : DiseqCnstr) : DiseqCnstrProof
• divCoeffs (c : DiseqCnstr) : DiseqCnstrProof
• neg (c : DiseqCnstr) : DiseqCnstrProof
• subst (x : Var) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof
• reorder (c : DiseqCnstr) : DiseqCnstrProof
• commRingNorm (c : DiseqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly) : DiseqCnstrProof

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

A proof of False. Remark: We will later add support for a backtracking search inside of cutsat.

• dvd (c : DvdCnstr) : UnsatProof
• le (c : LeCnstr) : UnsatProof
• eq (c : EqCnstr) : UnsatProof
• diseq (c : DiseqCnstr) : UnsatProof
• cooper (c₁ c₂ : LeCnstr) (c₃ : DvdCnstr) : UnsatProof

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedLeCnstr : Inhabited LeCnstr

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedLeCnstr = { default := { p := Int.Linear.Poly.num 0, h := Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.core default } }

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedDvdCnstr : Inhabited DvdCnstr

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedDvdCnstr = { default := { d := 0, p := Int.Linear.Poly.num 0, h := Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.core default } }

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedCooperSplitPred : Inhabited CooperSplitPred

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCooperSplitPred = { default := { left := false, c₁ := default, c₂ := default, c₃? := none } }

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedCooperSplit : Inhabited CooperSplit

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedCooperSplit = { default := { pred := default, k := 0, h := Lean.Meta.Grind.Arith.Cutsat.CooperSplitProof.dec default } }

@[reducible, inline]

abbrev Lean.Meta.Grind.Arith.Cutsat.VarSet : Type

Equations

• Lean.Meta.Grind.Arith.Cutsat.VarSet = Std.TreeSet Int.Linear.Var compare

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

State of the cutsat procedure.

• vars : PArray Expr

  Mapping from variables to their denotations.

• varMap : PHashMap ExprPtr Var

  Mapping from Expr to a variable representing it.

• vars' : PArray Expr

  vars before they were reordered. This array is empty if the variables were not reordered. We need them to generate the proof term because some justification objects contain terms using variables before the reordering.

• varMap' : PHashMap ExprPtr Var

  varMap before variables were reordered.

• natToIntMap : PHashMap ExprPtr (Expr × Expr)

  The field natToIntMap contains a mapping from a Nat-term e to the pair (e', he), where he : NatCast.natCast e = e'

• natDef : PHashMap ExprPtr Var

  Some Nat variables encode nested terms such as b+1. This is a mapping from this kind of variable to the integer variable representing natCast (b+1).

• dvds : PArray (Option DvdCnstr)

  Mapping from variables to divisibility constraints. Recall that we keep the divisibility constraint in solved form. Thus, we have at most one divisibility per variable.

• lowers : PArray (PArray LeCnstr)

  Mapping from variables to their "lower" bounds. We say a relational constraint c is a lower bound for a variable x if x is the maximal variable in c, and x coefficient in c is negative.

• uppers : PArray (PArray LeCnstr)

  Mapping from variables to their "upper" bounds. We say a relational constraint c is a upper bound for a variable x if x is the maximal variable in c, and x coefficient in c is positive.

• diseqs : PArray (PArray DiseqCnstr)

  Mapping from variables to their disequalities. We say a disequality constraint c is a disequality for a variable x if x is the maximal variable in c.

• elimEqs : PArray (Option EqCnstr)

  Mapping from variable to equation constraint used to eliminate it. solved variables should not occur in dvdCnstrs, lowers, or uppers.

• elimStack : List Var

  Elimination stack. For every variable in elimStack. If x in elimStack, then elimEqs[x] is not none.

• occurs : PArray VarSet

  Mapping from variable to occurrences. For example, an entry x ↦ {y, z} means that x may occur in dvdCnstrs, lowers, or uppers of variables y and z. If x occurs in dvdCnstrs[y], lowers[y], or uppers[y], then y is in occurs[x], but the reverse is not true. If x is in elimStack, then occurs[x] is the empty set.

• assignment : PArray Rat

  Partial assignment being constructed by cutsat.

• nextCnstrId : Nat

  Next unique id for a constraint.

• caseSplits : Bool

  caseSplits is true if cutsat is searching for model and already performed case splits. This information is used to decide whether a conflict should immediately close the current grind goal or not.

• conflict? : Option UnsatProof

  conflict? is some .. if a contradictory constraint was derived. This field is only set when caseSplits is true. Otherwise, we can convert UnsatProof into a Lean term and close the current grind goal.

• diseqSplits : PHashMap Poly FVarId

  Cache decision variables used when splitting on disequalities. This is necessary because the same disequality may be in different conflicts.

• divMod : PHashSet (Expr × Int)

  Pairs (x, n) s.t. we have expanded the theorems

  • Int.Linear.ediv_emod
  • Int.Linear.emod_nonneg
  • Int.Linear.emod_le
• toIntIds : PHashMap ExprPtr (Option Nat)

  Mapping from a type α to its corresponding ToIntInfo object idx in toInfos, which contains the information needed to embed α terms into Int terms.

• toIntInfos : PArray ToIntInfo
• toIntTermMap : PHashMap ExprPtr ToIntTermInfo

  For each type α in toIntInfos, the mapping toIntVarMap contains a mapping from a α-term e to the pair (toInt e, α).

• toIntVarMap : PHashMap ExprPtr Expr

  Mapping from a : α (where ToInt α) to toInt a that has been internalized. We use this information during model construction.

• usedCommRing : Bool

  usedCommRing is true if the CommRing has been used to normalize expressions.

• nonlinearOccs : PHashMap Var (List Var)

  Mapping from terms to variables representing nonlinear terms. For example, suppose the denotation of variable x is the nonlinear term a*b*c, and y is the nonlinear term a / d. Then the mapping contains the entries

  • a ↦ [x, y]
  • b ↦ [x]
  • c ↦ [x]
  • d ↦ [y]

instance Lean.Meta.Grind.Arith.Cutsat.instInhabitedState : Inhabited State

Equations

• Lean.Meta.Grind.Arith.Cutsat.instInhabitedState = { default := Lean.Meta.Grind.Arith.Cutsat.instInhabitedState.default }

def Lean.Meta.Grind.Arith.Cutsat.instInhabitedState.default : State

Equations

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

opaque Lean.Meta.Grind.Arith.Cutsat.cutsatExt : SolverExtension State