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
• id : Nat

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

• expr (h : Expr) : EqCnstrProof
• core (p₁ p₂ : Poly) (h : Expr) : EqCnstrProof
• norm (c : EqCnstr) : EqCnstrProof
• divCoeffs (c : EqCnstr) : EqCnstrProof
• subst (x : Var) (c₁ c₂ : EqCnstr) : EqCnstrProof
• ofLeGe (c₁ c₂ : LeCnstr) : EqCnstrProof

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

A divisibility constraint and its justification/proof.

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

  Unique id for caching proofs in ProofM

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

• expr (h : 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

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

An inequality constraint and its justification/proof.

• p : Poly
• h : LeCnstrProof
• id : Nat

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

• expr (h : Expr) : LeCnstrProof
• notExpr (p : Poly) (h : Expr) : LeCnstrProof
• norm (c : LeCnstr) : LeCnstrProof
• divCoeffs (c : LeCnstr) : LeCnstrProof
• combine (c₁ c₂ : LeCnstr) : 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

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

A disequality constraint and its justification/proof.

• p : Poly
• h : DiseqCnstrProof
• id : Nat

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

• expr (h : Expr) : DiseqCnstrProof
• core (p₁ p₂ : Poly) (h : Expr) : DiseqCnstrProof
• norm (c : DiseqCnstr) : DiseqCnstrProof
• divCoeffs (c : DiseqCnstr) : DiseqCnstrProof
• neg (c : DiseqCnstr) : DiseqCnstrProof
• subst (x : Var) (c₁ : EqCnstr) (c₂ : DiseqCnstr) : DiseqCnstrProof

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

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

• dvd (c : DvdCnstr) : UnsatProof
• le (c : LeCnstr) : UnsatProof
• eq (c : EqCnstr) : UnsatProof
• diseq (c : DiseqCnstr) : UnsatProof

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.expr default, id := 0 } }

@[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 ENodeKey Var

  Mapping from Expr to a variable representing it.

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

• terms : PHashMap ENodeKey Poly

  Mapping from terms (e.g., x + 2*y + 2, 3*x, 5) to polynomials representing them. These are terms used to propagate equalities between this module and the congruence closure module.

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

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

Equations

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