diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean index 9b8ceb0f8f..968cd1681d 100644 --- a/src/Init/Data/Int/Linear.lean +++ b/src/Init/Data/Int/Linear.lean @@ -311,6 +311,10 @@ def RelCnstr.mul (k : Int) : RelCnstr → RelCnstr | .eq p => .eq <| p.mul k | .le p => .le <| p.mul k +def RelCnstr.addConst (k : Int) : RelCnstr → RelCnstr + | .eq p => .eq <| p.addConst k + | .le p => .le <| p.addConst k + @[simp] theorem RelCnstr.denote_mul (ctx : Context) (c : RelCnstr) (k : Int) (h : k > 0) : (c.mul k).denote ctx = c.denote ctx := by cases c <;> simp [mul, denote] next => @@ -449,6 +453,9 @@ theorem Expr.denote_toPoly (ctx : Context) (e : Expr) : e.toPoly.denote ctx = e. attribute [local simp] Expr.denote_toPoly RelCnstr.denote +theorem RelCnstr.denote_norm (ctx : Context) (c : RelCnstr) : c.norm.denote ctx = c.denote ctx := by + cases c <;> simp [RelCnstr.norm] + theorem RawRelCnstr.denote_norm (ctx : Context) (c : RawRelCnstr) : c.norm.denote ctx = c.denote ctx := by cases c <;> simp · rw [Int.sub_eq_zero] @@ -502,7 +509,7 @@ theorem RawRelCnstr.eq_of_norm_eq_const (ctx : Context) (x : Var) (k : Int) (c : rw [h]; simp rw [Int.add_comm, ← Int.sub_eq_add_neg, Int.sub_eq_zero] -attribute [local simp] RelCnstr.divAll RelCnstr.div RelCnstr.mul +attribute [local simp] RelCnstr.divAll theorem RawRelCnstr.eq_of_norm_eq_mul (ctx : Context) (c : RawRelCnstr) (c' : RelCnstr) (k : Int) (hz : k > 0) (h : c.norm = c'.mul k) : c.denote ctx = c'.denote ctx := by replace h := congrArg (RelCnstr.denote ctx) h @@ -540,24 +547,29 @@ private theorem mul_add_cmod_le_iff {a k b : Int} (h : k > 0) : a*k + cmod b k simp at this assumption -theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ : RawRelCnstr) (c₂ : RelCnstr) (c₃ : RelCnstr) (k : Int) - : k > 0 → c₂.divCoeffs k → c₂.isLe → c₁.norm = c₂ → c₃ = c₂.div k → c₁.denote ctx = c₃.denote ctx := by - intro h₀ h₁ h₂ h₃ h₄ +theorem RelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ c₂ : RelCnstr) (k : Int) + : k > 0 → c₁.divCoeffs k → c₁.isLe → c₂ = c₁.div k → c₁.denote ctx = c₂.denote ctx := by + intro h₀ h₁ h₂ h₃ have hz : k ≠ 0 := Int.ne_of_gt h₀ - cases c₂ <;> simp [RelCnstr.isLe] at h₂ + cases c₁ <;> simp [RelCnstr.isLe] at h₂ clear h₂ next p => simp [RelCnstr.divCoeffs] at h₁ replace h₁ := Poly.denote_div_eq_of_divCoeffs ctx p k h₁ replace h₃ := congrArg (RelCnstr.denote ctx) h₃ - simp only [RelCnstr.denote.eq_2, ← h₁] at h₃ - replace h₄ := congrArg (RelCnstr.denote ctx) h₄ - simp only [RelCnstr.denote.eq_2, RelCnstr.div] at h₄ - rw [denote_norm] at h₃ - rw [h₃, h₄] + simp only [RelCnstr.div, RelCnstr.denote.eq_2] at h₃ + rw [h₃, denote, ← h₁]; clear h₁ h₃ apply propext apply mul_add_cmod_le_iff - exact h₀ + assumption + +theorem RawRelCnstr.eq_of_norm_eq_of_divCoeffs (ctx : Context) (c₁ : RawRelCnstr) (c₂ : RelCnstr) (c₃ : RelCnstr) (k : Int) + : k > 0 → c₂.divCoeffs k → c₂.isLe → c₁.norm = c₂ → c₃ = c₂.div k → c₁.denote ctx = c₃.denote ctx := by + intro h₀ h₁ h₂ h₃ h₄ + replace h₃ := congrArg (RelCnstr.denote ctx) h₃ + rw [denote_norm] at h₃ + rw [h₃] + apply RelCnstr.eq_of_norm_eq_of_divCoeffs _ _ _ _ h₀ h₁ h₂ h₄ /-- Certificate for normalizing the coefficients of inequality constraint with bound tightening. -/ def divByLe (c : RawRelCnstr) (c' : RelCnstr) (k : Int) : Bool := @@ -692,7 +704,7 @@ def DvdCnstr.div (k' : Int) : DvdCnstr → DvdCnstr private theorem not_dvd_of_not_mod_zero {a b : Int} (h : ¬ b % a = 0) : ¬ a ∣ b := by intro h; have := Int.emod_eq_zero_of_dvd h; contradiction -def DvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : DvdCnstr) : c.isUnsat → c.denote ctx = False := by +theorem DvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : DvdCnstr) : c.isUnsat → c.denote ctx = False := by rcases c with ⟨a, p⟩ simp [isUnsat, denote] intro h₁ h₂ @@ -700,6 +712,10 @@ def DvdCnstr.eq_false_of_isUnsat (ctx : Context) (c : DvdCnstr) : c.isUnsat → have := not_dvd_of_not_mod_zero h₁ contradiction +theorem DvdCnstr.false_of_isUnsat_of_denote (ctx : Context) (c : DvdCnstr) : c.isUnsat → c.denote ctx → False := by + intro h₁ h₂ + simp [eq_false_of_isUnsat, h₁] at h₂ + @[local simp] private theorem mul_dvd_mul_eq {a b c : Int} (hnz : a ≠ 0) : a * b ∣ a * c ↔ b ∣ c := by constructor · intro h @@ -839,7 +855,7 @@ theorem DvdCnstr.solve_elim (ctx : Context) (c₁ c₂ c : DvdCnstr) (d : Int) rw [← Int.sub_eq_add_neg] exact solveElim hd h₁ h₂ -def isNorm (c₁ c₂ : DvdCnstr) : Bool := +def DvdCnstr.isNorm (c₁ c₂ : DvdCnstr) : Bool := c₁.k == c₂.k && c₁.p.norm == c₂.p theorem DvdCnstr.of_isNorm (ctx : Context) (c₁ c₂ : DvdCnstr) @@ -853,6 +869,41 @@ theorem DvdCnstr.of_isNorm (ctx : Context) (c₁ c₂ : DvdCnstr) theorem DvdCnstr.of_isEqv (ctx : Context) (c₁ c₂ : DvdCnstr) (k : Int) (h : isEqv c₁ c₂ k) : c₁.denote' ctx → c₂.denote' ctx := by simp [DvdCnstr.denote'_eq_denote, DvdCnstr.eq_of_isEqv ctx c₁ c₂ k h] +theorem RelCnstr.of_norm_eq (ctx : Context) (c₁ c₂ : RelCnstr) (h : c₁.norm == c₂) : c₁.denote' ctx → c₂.denote' ctx := by + simp at h + replace h := congrArg (RelCnstr.denote ctx) h + simp only [RelCnstr.denote_norm] at h + simp only [RelCnstr.denote'_eq_denote, h] + intro; assumption + +def RelCnstr.divByLe (c₁ c₂ : RelCnstr) (k : Int) : Bool := + k > 0 && (c₁.isLe && (c₁.divCoeffs k && c₂ == c₁.div k)) + +theorem RelCnstr.of_divByLe (ctx : Context) (c₁ c₂ : RelCnstr) (k : Int) (h : divByLe c₁ c₂ k) : c₁.denote' ctx → c₂.denote' ctx := by + simp [divByLe] at h + rcases h with ⟨h₁, h₂, h₃, h₄⟩ + simp only [RelCnstr.denote'_eq_denote] + exact RelCnstr.eq_of_norm_eq_of_divCoeffs ctx c₁ c₂ k h₁ h₃ h₂ h₄ |>.mp + +def RelCnstr.negLe (c₁ c₂ : RelCnstr) : Bool := + c₁.isLe && c₂ == (c₁.mul (-1) |>.addConst 1) + +theorem RelCnstr.of_negLe (ctx : Context) (c₁ c₂ : RelCnstr) (h : negLe c₁ c₂) : ¬ c₁.denote' ctx → c₂.denote' ctx := by + simp [negLe] at h + rcases h with ⟨h₁, h₂⟩ + cases c₁ <;> simp [isLe] at h₁; clear h₁ + replace h₂ := congrArg (RelCnstr.denote ctx) h₂ + simp only [RelCnstr.denote'_eq_denote, h₂, RelCnstr.mul, RelCnstr.addConst] + simp + intro h + replace h : _ + 1 ≤ -0 := Int.neg_lt_neg <| Int.lt_of_not_ge h + simp at h + exact h + +theorem RelCnstr.false_of_isUnsat_of_denote (ctx : Context) (c : RelCnstr) : c.isUnsat → c.denote ctx → False := by + intro h₁ h₂ + simp [eq_false_of_isUnsat, h₁, -RelCnstr.denote] at h₂ + end Int.Linear theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index a80e489b80..e551bcd2a3 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -571,6 +571,18 @@ def mkLetValCongr (b h : Expr) : MetaM Expr := def mkLetBodyCongr (a h : Expr) : MetaM Expr := mkAppM ``let_body_congr #[a, h] +/-- Returns `@of_eq_false p h` -/ +def mkOfEqFalseCore (p : Expr) (h : Expr) : Expr := + match_expr h with + | eq_false _ h => h + | _ => mkApp2 (mkConst ``of_eq_false) p h + +/-- Returns `of_eq_false h` -/ +def mkOfEqFalse (h : Expr) : MetaM Expr := do + match_expr h with + | eq_false _ h => return h + | _ => mkAppM ``of_eq_false #[h] + /-- Returns `@of_eq_true p h` -/ def mkOfEqTrueCore (p : Expr) (h : Expr) : Expr := match_expr h with @@ -600,7 +612,9 @@ def mkEqTrue (h : Expr) : MetaM Expr := do `h` must have type definitionally equal to `¬ p` in the current reducibility setting. -/ def mkEqFalse (h : Expr) : MetaM Expr := - mkAppM ``eq_false #[h] + match_expr h with + | of_eq_false _ h => return h + | _ => mkAppM ``eq_false #[h] /-- Returns `eq_false' h` diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean index abc58519c3..419922124a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.Util.Trace import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.RelCnstr import Lean.Meta.Tactic.Grind.Arith.Cutsat.Inv import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof import Lean.Meta.Tactic.Grind.Arith.Cutsat.Types @@ -27,4 +28,7 @@ builtin_initialize registerTraceClass `grind.cutsat.dvd.solve.elim (inherited := builtin_initialize registerTraceClass `grind.cutsat.internalize builtin_initialize registerTraceClass `grind.cutsat.internalize.term (inherited := true) +builtin_initialize registerTraceClass `grind.cutsat.assert.le +builtin_initialize registerTraceClass `grind.cutsat.le + end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean index 0d07c68858..6e8ac98abb 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean @@ -37,11 +37,7 @@ partial def assertDvdCnstr (cₚ : DvdCnstrWithProof) : GoalM Unit := withIncRec if cₚ.isUnsat then trace[grind.cutsat.dvd.unsat] "{← cₚ.denoteExpr}" let hf ← withProofContext do - let h ← cₚ.toExprProof - let heq := mkApp3 (mkConst ``Int.Linear.DvdCnstr.eq_false_of_isUnsat) (← getContext) (toExpr cₚ.c) reflBoolTrue - let c ← cₚ.denoteExpr - let heq ← mkExpectedTypeHint heq (← mkEq c (← getFalseExpr)) - mkEqMP heq h + return mkApp4 (mkConst ``Int.Linear.DvdCnstr.false_of_isUnsat_of_denote) (← getContext) (toExpr cₚ.c) reflBoolTrue (← cₚ.toExprProof) closeGoal hf else if cₚ.isTrivial then trace[grind.cutsat.dvd.trivial] "{← cₚ.denoteExpr}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean index 7a0f0551bb..819989b975 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Inv.lean @@ -17,6 +17,29 @@ end Int.Linear namespace Lean.Meta.Grind.Arith.Cutsat +def checkRelCnstrs (css : PArray (PArray RelCnstrWithProof)) (isLower : Bool) : GoalM Unit := do + let mut x := 0 + for cs in css do + for { c, .. } in cs do + assert! c.isLe + assert! c.isSorted + assert! c.p.checkCoeffs + let .add a y _ := c.p | unreachable! + assert! isLower == (a < 0) + assert! x == y + x := x + 1 + return () + +def checkLowers : GoalM Unit := do + let s ← get' + assert! s.lowers.size == s.vars.size + checkRelCnstrs s.lowers (isLower := true) + +def checkUppers : GoalM Unit := do + let s ← get' + assert! s.uppers.size == s.vars.size + checkRelCnstrs s.uppers (isLower := false) + def checkDvdCnstrs : GoalM Unit := do let s ← get' assert! s.vars.size == s.dvdCnstrs.size @@ -45,5 +68,7 @@ def checkVars : GoalM Unit := do def checkInvariants : GoalM Unit := do checkVars checkDvdCnstrs + checkLowers + checkUppers end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean index 29508cd4a5..0f676d1fa0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean @@ -43,4 +43,8 @@ partial def DvdCnstrWithProof.toExprProof' (cₚ : DvdCnstrWithProof) : ProofM E partial def DvdCnstrWithProof.toExprProof (cₚ : DvdCnstrWithProof) : ProofM Expr := do mkExpectedTypeHint (← toExprProof' cₚ) (← cₚ.denoteExpr) +partial def RelCnstrWithProof.toExprProof (cₚ : RelCnstrWithProof) : ProofM Expr := do + -- TODO + mkSorry (← cₚ.denoteExpr) false + end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/RelCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/RelCnstr.lean new file mode 100644 index 0000000000..2180269ee7 --- /dev/null +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/RelCnstr.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Meta.Tactic.Simp.Arith.Int +import Lean.Meta.Tactic.Grind.PropagatorAttr +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var +import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof + +namespace Lean.Meta.Grind.Arith.Cutsat +def mkRelCnstrWithProof (c : RelCnstr) (h : RelCnstrProof) : GoalM RelCnstrWithProof := do + return { c, h, id := (← mkCnstrId) } + +abbrev RelCnstrWithProof.isUnsat (cₚ : RelCnstrWithProof) : Bool := + cₚ.c.isUnsat + +abbrev RelCnstrWithProof.isTrivial (cₚ : RelCnstrWithProof) : Bool := + cₚ.c.isTrivial + +abbrev RelCnstrWithProof.satisfied (cₚ : RelCnstrWithProof) : GoalM LBool := + cₚ.c.satisfied + +def RelCnstrWithProof.norm (cₚ : RelCnstrWithProof) : GoalM RelCnstrWithProof := do + let cₚ ← if cₚ.c.isSorted then + pure cₚ + else + mkRelCnstrWithProof cₚ.c.norm (.norm cₚ) + let k := cₚ.c.gcdCoeffs + if k != 1 then + mkRelCnstrWithProof (cₚ.c.div k) (.divCoeffs cₚ) + else + return cₚ + +def assertRelCnstr (cₚ : RelCnstrWithProof) : GoalM Unit := do + if (← isInconsistent) then return () + let cₚ ← cₚ.norm + if cₚ.isUnsat then + trace[grind.cutsat.le.unsat] "{← cₚ.denoteExpr}" + let hf ← withProofContext do + return mkApp4 (mkConst ``Int.Linear.RelCnstr.false_of_isUnsat_of_denote) (← getContext) (toExpr cₚ.c) reflBoolTrue (← cₚ.toExprProof) + closeGoal hf + else if cₚ.isTrivial then + trace[grind.cutsat.le.trivial] "{← cₚ.denoteExpr}" + return () + else + -- TODO + return () + +private def reportNonNormalized (e : Expr) : GoalM Unit := do + reportIssue! "unexpected non normalized inequality constraint found{indentExpr e}" + +private def toRelCnstr? (e : Expr) : GoalM (Option RelCnstr) := do + let_expr LE.le _ inst a b ← e | return none + unless (← isInstLEInt inst) do return none + let some k ← getIntValue? b + | reportNonNormalized e; return none + unless k == 0 do + reportNonNormalized e; return none + let p ← toPoly a + return some <| .le p + +/-- +Given an expression `e` that is in `True` (or `False` equivalence class), if `e` is an +integer inequality, asserts it to the cutsat state. +-/ +def propagateIfIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do + let some c ← toRelCnstr? e | return () + let cₚ ← if eqTrue then + mkRelCnstrWithProof c (.expr (← mkOfEqTrue (← mkEqTrueProof e))) + else + mkRelCnstrWithProof (c.mul (-1) |>.addConst 1) (.notExpr (← mkOfEqFalse (← mkEqFalseProof e))) + trace[grind.cutsat.assert.le] "{← cₚ.denoteExpr}" + assertRelCnstr cₚ + +end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean index 08ab0b29cf..12ca7c11fd 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean @@ -28,6 +28,18 @@ inductive DvdCnstrProof where | divCoeffs (c : DvdCnstrWithProof) | solveCombine (c₁ c₂ : DvdCnstrWithProof) | solveElim (c₁ c₂ : DvdCnstrWithProof) + +structure RelCnstrWithProof where + c : RelCnstr + h : RelCnstrProof + id : Nat + +inductive RelCnstrProof where + | expr (h : Expr) + | notExpr (c : Expr) + | norm (c : RelCnstrWithProof) + | divCoeffs (c : RelCnstrWithProof) + -- TODO: missing constructors end /-- State of the cutsat procedure. -/ @@ -40,8 +52,26 @@ structure State where 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. -/ dvdCnstrs : PArray (Option DvdCnstrWithProof) := {} + /-- + 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`, `c.isLe`, and `x` coefficient in `c` is negative. + -/ + lowers : PArray (PArray RelCnstrWithProof) := {} + /-- + 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`, `c.isLe`, and `x` coefficient in `c` is positive. + -/ + uppers : PArray (PArray RelCnstrWithProof) := {} + /-- Partial assignment being constructed by cutsat. -/ + assignment : PArray Int := {} /-- Next unique id for a constraint. -/ nextCnstrId : Nat := 0 + /- + TODO: support for storing + - Disjuctions: they come from conflict resolution, and disequalities. + - Disequalities. + - Linear integer terms appearing in the main module, and model-based equality propagation. + -/ deriving Inhabited end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean index 6659919d2e..25b8ce681b 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean @@ -31,6 +31,17 @@ def DvdCnstr.isTrivial (c : DvdCnstr) : Bool := | .num k' => k' % c.k == 0 | _ => c.k == 1 +def RelCnstr.p : RelCnstr → Poly + | .eq p | .le p => p + +def RelCnstr.isSorted (c : RelCnstr) : Bool := + c.p.isSorted + +def RelCnstr.isTrivial : RelCnstr → Bool + | .eq (.num 0) => true + | .le (.num k) => k ≤ 0 + | _ => false + end Int.Linear namespace Lean.Meta.Grind.Arith.Cutsat @@ -64,6 +75,10 @@ def DvdCnstrWithProof.denoteExpr (cₚ : DvdCnstrWithProof) : GoalM Expr := do let vars ← getVars cₚ.c.denoteExpr (vars[·]!) +def RelCnstrWithProof.denoteExpr (cₚ : RelCnstrWithProof) : GoalM Expr := do + let vars ← getVars + cₚ.c.denoteExpr (vars[·]!) + def toContextExpr : GoalM Expr := do let vars ← getVars if h : 0 < vars.size then @@ -97,4 +112,37 @@ abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do let h ← x ctx |>.run' {} mkLetFVars #[ctx] h +/-- +Tries to evaluate the polynomial `p` using the partial model/assignment built so far. +The result is `none` if the polynomial contains variables that have not been assigned. +-/ +def _root_.Int.Linear.Poly.eval? (p : Poly) : GoalM (Option Int) := do + let a := (← get').assignment + let rec go (v : Int) : Poly → Option Int + | .num k => some (v + k) + | .add k x p => + if _ : x < a.size then + go (v + k*a[x]) p + else + none + return go 0 p + +/-- +Returns `.true` if `c` is satisfied by the current partial model, +`.undef` if `c` contains unassigned variables, and `.false` otherwise. +-/ +def _root_.Int.Linear.DvdCnstr.satisfied (c : DvdCnstr) : GoalM LBool := do + let some v ← c.p.eval? | return .undef + return decide (c.k ∣ v) |>.toLBool + +/-- +Returns `.true` if `c` is satisfied by the current partial model, +`.undef` if `c` contains unassigned variables, and `.false` otherwise. +-/ +def _root_.Int.Linear.RelCnstr.satisfied (c : RelCnstr) : GoalM LBool := do + let some v ← c.p.eval? | return .undef + match c with + | .eq _ => return v == 0 |>.toLBool + | .le _ => return decide (v <= 0) |>.toLBool + end Lean.Meta.Grind.Arith.Cutsat diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean index 0083aa68b7..8b0b72d6d7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean @@ -19,6 +19,8 @@ def mkVar (expr : Expr) : GoalM Var := do vars := s.vars.push expr varMap := s.varMap.insert { expr } var dvdCnstrs := s.dvdCnstrs.push none + lowers := s.lowers.push {} + uppers := s.uppers.push {} } return var diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Main.lean b/src/Lean/Meta/Tactic/Grind/Arith/Main.lean index d8f90291b1..194379fd1c 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Main.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.Meta.Tactic.Grind.PropagatorAttr import Lean.Meta.Tactic.Grind.Arith.Offset +import Lean.Meta.Tactic.Grind.Arith.Cutsat.RelCnstr namespace Lean.Meta.Grind.Arith @@ -27,8 +28,10 @@ builtin_grind_propagator propagateLE ↓LE.le := fun e => do if (← isEqTrue e) then if let some c ← Offset.isCnstr? e then Offset.assertTrue c (← mkEqTrueProof e) + Cutsat.propagateIfIntLe e (eqTrue := true) if (← isEqFalse e) then if let some c ← Offset.isCnstr? e then Offset.assertFalse c (← mkEqFalseProof e) + Cutsat.propagateIfIntLe e (eqTrue := false) end Lean.Meta.Grind.Arith diff --git a/src/Lean/Meta/Tactic/Grind/Propagate.lean b/src/Lean/Meta/Tactic/Grind/Propagate.lean index fa5ed8b301..5a8c4057e3 100644 --- a/src/Lean/Meta/Tactic/Grind/Propagate.lean +++ b/src/Lean/Meta/Tactic/Grind/Propagate.lean @@ -200,7 +200,7 @@ builtin_grind_propagator propagateDIte ↑dite := fun e => do pushEq e r <| mkApp8 (mkConst ``Grind.dite_cond_eq_true' f.constLevels!) α c h a b r h₁ h₂ else if (← isEqFalse c) then let h₁ ← mkEqFalseProof c - let bh₁ := mkApp b (mkApp2 (mkConst ``of_eq_false) c h₁) + let bh₁ := mkApp b (mkOfEqFalseCore c h₁) let p ← preprocess bh₁ let r := p.expr let h₂ ← p.getProof