@[instance_reducible]

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

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

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.Internal.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.Internal.Linear.Expr) : EqCnstrProof
• defn (e : Expr) (e' : Int.Internal.Linear.Expr) : EqCnstrProof

  e is e'

• defnNat (h : Expr) (x : Var) (e' : Int.Internal.Linear.Expr) : EqCnstrProof
• norm (c : EqCnstr) : EqCnstrProof
• divCoeffs (c : EqCnstr) : EqCnstrProof
• subst (x : Var) (c₁ c₂ : EqCnstr) : EqCnstrProof
• ofLeGe (c₁ c₂ : LeCnstr) : EqCnstrProof
• ofZeroDvd (c : DvdCnstr) : EqCnstrProof

  p = 0 derived from the divisibility constraint c of the form 0 ∣ p.

• reorder (c : EqCnstr) : EqCnstrProof
• commRingNorm (c : EqCnstr) (e : Sym.Arith.RingExpr) (p : CommRing.Poly) : EqCnstrProof
• defnCommRing (e : Expr) (e' : Int.Internal.Linear.Expr) (p : Poly) (re : Sym.Arith.RingExpr) (rp : CommRing.Poly) (p' : Poly) : EqCnstrProof
• defnNatCommRing (h : Expr) (x : Var) (e' : Int.Internal.Linear.Expr) (p : Poly) (re : Sym.Arith.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.Internal.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 : Sym.Arith.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.Internal.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 : Sym.Arith.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.Internal.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 : Sym.Arith.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_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[reducible, inline]

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

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.

• varsHistory : PArray (PArray Expr × PHashMap ExprPtr Var)

  Variable orders superseded by reorderVars, oldest first: entry i is the pair (vars, varMap) of epoch i, and the current order is epoch varsHistory.size. Justification objects created before a reordering contain polynomials in the order of their epoch, so proof generation needs every superseded order.

• 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.

• steps : Nat

  Cumulative number of steps performed by the model search. The model search is interrupted when this counter reaches the liaSteps configuration threshold, and the solver becomes incomplete.

• 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.Internal.Linear.ediv_emod
  • Int.Internal.Linear.emod_nonneg
  • Int.Internal.Linear.emod_le
• 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_reducible]

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

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