(sgm v b as n) is the new value assigned to the nth variable after a single step of equality elimination using valuation v, term ⟨b, as⟩, and variable index n. If v satisfies the initial constraint set, then (v ⟨n ↦ sgm v b as n⟩) satisfies the new constraint set after equality elimination.
Equations
- omega.sgm v b as n = let a_n : ℤ := list.func.get n as, m : ℤ := a_n + 1 in (omega.symmod b m + omega.coeffs.val v (list.map (λ (x : ℤ), omega.symmod x m) as)) / m
Equations
- omega.rhs n b as = let m : ℤ := list.func.get n as + 1 in (omega.symmod b m, list.func.set (-m) (list.map (λ (x : ℤ), omega.symmod x m) as) n)
theorem
omega.rhs_correct_aux
{v : ℕ → ℤ}
{m : ℤ}
{as : list ℤ}
{k : ℕ} :
∃ (d : ℤ), m * d + omega.coeffs.val_between v (list.map (λ (x : ℤ), omega.symmod x m) as) 0 k = omega.coeffs.val_between v as 0 k
theorem
omega.rhs_correct
{v : ℕ → ℤ}
{b : ℤ}
{as : list ℤ}
(n : ℕ) :
0 < list.func.get n as → 0 = omega.term.val v (b, as) → v n = omega.term.val (omega.update n (omega.sgm v b as n) v) (omega.rhs n b as)
Equations
- omega.sym_sym m b = omega.symdiv b m + omega.symmod b m
Equations
- omega.coeffs_reduce n b as = let a : ℤ := list.func.get n as, m : ℤ := a + 1 in (omega.sym_sym m b, list.func.set (-a) (list.map (omega.sym_sym m) as) n)
theorem
omega.coeffs_reduce_correct
{v : ℕ → ℤ}
{b : ℤ}
{as : list ℤ}
{n : ℕ} :
0 < list.func.get n as → 0 = omega.term.val v (b, as) → 0 = omega.term.val (omega.update n (omega.sgm v b as n) v) (omega.coeffs_reduce n b as)
Equations
- omega.cancel m t1 t2 = (omega.term.mul (-list.func.get m t2.snd) t1).add t2
Equations
- omega.subst n t1 t2 = (omega.term.mul (list.func.get n t2.snd) t1).add (t2.fst, list.func.set 0 t2.snd n)
theorem
omega.subst_correct
{v : ℕ → ℤ}
{b : ℤ}
{as : list ℤ}
{t : omega.term}
{n : ℕ} :
0 < list.func.get n as → 0 = omega.term.val v (b, as) → omega.term.val v t = omega.term.val (omega.update n (omega.sgm v b as n) v) (omega.subst n (omega.rhs n b as) t)
Equations
- (omega.ee.cancel n).repr = "+" ++ n.repr
- (omega.ee.reduce n).repr = "≻" ++ n.repr
- omega.ee.neg.repr = "-"
- (omega.ee.factor i).repr = "/" ++ i.repr
- (omega.ee.nondiv i).repr = i.repr ++ "∤"
- omega.ee.drop.repr = "↓"
@[instance]
Equations
Apply a given sequence of equality elimination steps to a clause.
Equations
- omega.eq_elim (omega.ee.cancel m :: es) (eq :: eqs, les) = omega.eq_elim es (list.map (omega.cancel m eq) eqs, list.map (omega.cancel m eq) les)
- omega.eq_elim (omega.ee.cancel a :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.reduce n :: es) ((b, as) :: eqs, les) = ite (0 < list.func.get n as) (let eq' : omega.term := omega.coeffs_reduce n b as, r : omega.term := omega.rhs n b as, eqs' : list omega.term := list.map (omega.subst n r) eqs, les' : list omega.term := list.map (omega.subst n r) les in omega.eq_elim es (eq' :: eqs', les')) (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.reduce a :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.neg :: es) (eq :: eqs, les) = omega.eq_elim es (eq.neg :: eqs, les)
- omega.eq_elim (omega.ee.neg :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.factor i :: es) ((b, as) :: eqs, les) = ite (i ∣ b ∧ ∀ (x : ℤ), x ∈ as → i ∣ x) (omega.eq_elim es (omega.term.div i (b, as) :: eqs, les)) (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.factor a :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.nondiv i :: es) ((b, as) :: eqs, les) = ite (¬i ∣ b ∧ ∀ (x : ℤ), x ∈ as → i ∣ x) (list.nil omega.term, [(-1, list.nil ℤ)]) (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.nondiv a :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim (omega.ee.drop :: es) (eq :: eqs, les) = omega.eq_elim es (eqs, les)
- omega.eq_elim (omega.ee.drop :: _x) (list.nil omega.term, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim list.nil (_x :: _x_1, les) = (list.nil omega.term, list.nil omega.term)
- omega.eq_elim list.nil (list.nil omega.term, les) = (list.nil omega.term, les)
theorem
omega.sat_eq_elim
{es : list omega.ee}
{c : omega.clause} :
c.sat → (omega.eq_elim es c).sat
theorem
omega.unsat_of_unsat_eq_elim
(ee : list omega.ee)
(c : omega.clause) :
(omega.eq_elim ee c).unsat → c.unsat
If the result of equality elimination is unsatisfiable, the original clause is unsatisfiable.