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

Equations

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

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.

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

  e is p

• defnNat (e : Int.OfNat.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 (e : Int.OfNat.Expr) (x : Var) (e' : Int.Linear.Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly) : 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.

• coreNat (e : Expr) (d : Nat) (b : Int.OfNat.Expr) (b' : 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
• coreNat (e : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) : LeCnstrProof
• coreNatNeg (e : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) : LeCnstrProof
• coreToInt (e : Expr) (pos : Bool) (toIntThm : Expr) (lhs rhs : Int.Linear.Expr) : LeCnstrProof
• denoteAsIntNonneg (rhs : Int.OfNat.Expr) (rhs' : Int.Linear.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.

• coreNat (a b : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr) : DiseqCnstrProof
• 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 = Lean.RBTree 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

  varVap before variables were reordered.

• natVarMap : PHashMap ExprPtr Var

  Mapping from Nat terms to their variable. They are also marked using markAsCutsatTerm.

• natVars : PArray Expr
• 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
• toIntInfos : PHashMap ExprPtr (Option ToIntInfo)

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

• toIntTermMap : PHashMap ExprPtr ToIntTermInfo

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

• usedCommRing : Bool

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

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

Equations

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