Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddResult

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 : DefaultFormula n) (units : Sat.CNF.Clause (PosFin n)) :

(f.insertRatUnits units).fst.assignments.size = f.assignments.size

source

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

let assignments := (f.insertRatUnits units).fst.assignments; let_fun hsize := ⋯; let ratUnits := (f.insertRatUnits units).fst.ratUnits; InsertUnitInvariant f.assignments ⋯ ratUnits assignments hsize

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRatUnits {n : Nat} (f : DefaultFormula n) (hf : f.ratUnits = #[] ∧ f.assignments.size = n) (units : Sat.CNF.Clause (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]

source

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

let insertRat_res := f.insertRatUnits units; f.ClearInsertInductionMotive ⋯ insertRat_res.fst.ratUnits 0 insertRat_res.fst.assignments

source

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

(f.insertRatUnits units).fst.clearRatUnits = f

source

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

(f.performRatCheck p ratHint).fst = f

source

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

let performRatCheck_fold_res := Array.foldl (fun (x : 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

source

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

f' = f.insert c