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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insertRatUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRatUnits units).fst.assignments.size = f.assignments.size

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertRatUnits_postcondition {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let assignments := (f.insertRatUnits units).fst.assignments; let_fun hsize := ⋯; let ratUnits := (f.insertRatUnits units).fst.ratUnits; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRatUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (i j : Fin (f.insertRatUnits units).fst.ratUnits.size) : i ≠ j → (f.insertRatUnits units).fst.ratUnits[i] ≠ (f.insertRatUnits units).fst.ratUnits[j]

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRat_base_case {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : let insertRat_res := f.insertRatUnits units; f.ClearInsertInductionMotive ⋯ insertRat_res.fst.ratUnits 0 insertRat_res.fst.assignments

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRat {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) : (f.insertRatUnits units).fst.clearRatUnits = f

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.formula_performRatCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHint : Nat × Array Nat) : (f.performRatCheck p ratHint).fst = f

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatCheck_fold_formula_eq {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ratHints : Array (Nat × Array Nat)) : let performRatCheck_fold_res := Array.foldl (fun (x : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool) (ratHint : Nat × Array Nat) => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true) ratHints; performRatCheck_fold_res.fst = f

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratAdd_result {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (p : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array Nat) (ratHints : Array (Nat × Array Nat)) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRatAdd : f.ReadyForRatAdd) (_pc : p ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c) (ratAddSuccess : f.performRatAdd c p rupHints ratHints = (f', true)) : f' = f.insert c