Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound

This module contains the verification of RUP-based clause adding for the default LRAT checker implementation.

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (foundContradiction : Bool) (l : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
let insertUnit_fold_res := List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; (foundContradiction = true∃ (i : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), assignments[i.val] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)insertUnit_fold_res.snd.snd = true∃ (j : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), insertUnit_fold_res.snd.fst[j.val] = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_insertUnit_fold_units {n : Nat} (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (foundContradiction : Bool) (l : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
let insertUnit_fold_res := List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; ∀ (l' : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)), l' insertUnit_fold_res.fst.toListl' l l' units.toList
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin nBool) (pf : Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p f) :
let fc := f.insertRupUnits c.negate; let confirmRupHint_fold_res := Array.foldl (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints; confirmRupHint_fold_res.snd.snd.fst = trueStd.Tactic.BVDecide.LRAT.Internal.Entails.eval p c