This module contains the verification of RAT-based clause adding for the default LRAT checker implementation.
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_necessary_assignment
{n : Nat}
{p : PosFin n → Bool}
{c : DefaultClause n}
{l : Sat.Literal (PosFin n)}
(p_entails_c : Entails.eval p c)
(p'_not_entails_c : ¬Entails.eval (fun (v : PosFin n) => if v = l.fst then l.snd else p v) c)
:
l.negate ∈ Clause.toList c
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.entails_of_irrelevant_assignment
{n : Nat}
{p : PosFin n → Bool}
{c : DefaultClause n}
{l : Sat.Literal (PosFin n)}
(p_entails_cl : Entails.eval p (c.delete l.negate))
:
Entails.eval (fun (v : PosFin n) => if v = l.fst then l.snd else p v) (c.delete l.negate)
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_insertRatUnits
{n : Nat}
(f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant)
(units : Sat.CNF.Clause (PosFin n))
:
(f.insertRatUnits units).fst.AssignmentsInvariant
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_confirmRupHint_of_insertRat_fold
{n : Nat}
(f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant)
(c : DefaultClause n)
(rupHints : Array Nat)
(p : PosFin n → Bool)
(pf : Entails.eval p f)
:
let fc := f.insertRatUnits c.negate;
let confirmRupHint_fold_res :=
Array.foldl (confirmRupHint fc.fst.clauses) (fc.fst.assignments, [], false, false) rupHints;
confirmRupHint_fold_res.snd.snd.fst = true → Entails.eval p c
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.sat_of_insertRat
{n : Nat}
(f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant)
(c : DefaultClause n)
(p : PosFin n → Bool)
(pf : Entails.eval p f)
:
(f.insertRatUnits c.negate).snd = true → Entails.eval p c
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRupCheck_insertRat
{n : Nat}
(f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant)
(c : DefaultClause n)
(rupHints : Array Nat)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_performRupCheck_of_assignmentsInvariant
{n : Nat}
(f : DefaultFormula n)
(f_AssignmentsInvariant : f.AssignmentsInvariant)
(rupHints : Array Nat)
:
(f.performRupCheck rupHints).fst.AssignmentsInvariant
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.c_without_negPivot_of_performRatCheck_success
{n : Nat}
(f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.AssignmentsInvariant)
(negPivot : Sat.Literal (PosFin n))
(ratHint : Nat × Array Nat)
(performRatCheck_success : (f.performRatCheck negPivot ratHint).snd = true)
(c : DefaultClause n)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.existsRatHint_of_ratHintsExhaustive
{n : Nat}
(f : DefaultFormula n)
(f_readyForRatAdd : f.ReadyForRatAdd)
(pivot : Sat.Literal (PosFin n))
(ratHints : Array (Nat × Array Nat))
(ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true)
(c' : DefaultClause n)
(c'_in_f : c' ∈ f.toList)
(negPivot_in_c' : pivot.negate ∈ Clause.toList c')
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck_success_of_performRatCheck_fold_success
{n : Nat}
(f : DefaultFormula n)
(hf : f.ratUnits = #[] ∧ f.assignments.size = n)
(p : Sat.Literal (PosFin n))
(ratHints : Array (Nat × Array Nat))
(i : Fin ratHints.size)
(performRatCheck_fold_success :
(Array.foldl
(fun (acc : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) =>
if acc.snd = true then acc.fst.performRatCheck p ratHint else (acc.fst, false))
(f, true) ratHints).snd = true)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.safe_insert_of_performRatCheck_fold_success
{n : Nat}
(f : DefaultFormula n)
(f_readyForRatAdd : f.ReadyForRatAdd)
(c : DefaultClause n)
(pivot : Sat.Literal (PosFin n))
(rupHints : Array Nat)
(ratHints : Array (Nat × Array Nat))
(pivot_in_c : pivot ∈ Clause.toList c)
(ratHintsExhaustive_eq_true : f.ratHintsExhaustive pivot ratHints = true)
(performRatCheck_fold_success :
(Array.foldl
(fun (x : DefaultFormula n × Bool) (ratHint : Nat × Array Nat) =>
if x.snd = true then x.fst.performRatCheck pivot.negate ratHint else (x.fst, false))
(((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints).snd = true)
:
theorem
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratAdd_sound
{n : Nat}
(f : DefaultFormula n)
(c : DefaultClause n)
(pivot : Sat.Literal (PosFin n))
(rupHints : Array Nat)
(ratHints : Array (Nat × Array Nat))
(f' : DefaultFormula n)
(f_readyForRatAdd : f.ReadyForRatAdd)
(pivot_in_c : pivot ∈ Clause.toList c)
(ratAddSuccess : f.performRatAdd c pivot rupHints ratHints = (f', true))
: