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

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

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

An inequalirty 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
• denoteAsIntNonneg (rhs : Int.OfNat.Expr) (rhs' : Int.Linear.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

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

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

• nat : ForeignType

instance Lean.Meta.Grind.Arith.Cutsat.instBEqForeignType : BEq ForeignType

Equations

• Lean.Meta.Grind.Arith.Cutsat.instBEqForeignType = { beq := Lean.Meta.Grind.Arith.Cutsat.beqForeignType✝ }

instance Lean.Meta.Grind.Arith.Cutsat.instHashableForeignType : Hashable ForeignType

Equations

• Lean.Meta.Grind.Arith.Cutsat.instHashableForeignType = { hash := Lean.Meta.Grind.Arith.Cutsat.hashForeignType✝ }

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.

• foreignVarMap : PHashMap ENodeKey (Var × ForeignType)

  Mapping from foreign terms to their variable and type (e.g., Nat). They are also marked using markAsCutsatTerm.

• foreignVars : PHashMap ForeignType (PArray Expr)
• foreignDef : PHashMap ENodeKey Var

  Some foreign 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

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

Equations

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