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) : ((f.insertRatUnits c.negate).fst.performRupCheck rupHints).snd.snd.fst = true → Limplies (PosFin n) f (f.insert c)

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) : f.clauses[ratHint.fst]! = some c → Limplies (PosFin n) f (c.delete negPivot)

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') : ∃ (i : Fin ratHints.size), f.clauses[ratHints[i].fst]! = some 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) : (f.performRatCheck p ratHints[i]).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) : Equisat (PosFin n) f (f.insert c)

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)) : Equisat (PosFin n) f f'