Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult

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

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_insertUnit {n : Nat} (units : Array (Sat.Literal (PosFin n))) (assignments : Array Assignment) (b : Bool) (l : Sat.Literal (PosFin n)) :

(insertUnit (units, assignments, b) l).snd.fst.size = assignments.size

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_insertUnit_fold {n : Nat} {units : List (Sat.Literal (PosFin n))} (unitsAcc : Array (Sat.Literal (PosFin n))) (assignments : Array Assignment) (b : Bool) :

(List.foldl insertUnit (unitsAcc, assignments, b) units).snd.fst.size = assignments.size

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : Sat.CNF.Clause (PosFin n)) :

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

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : Sat.CNF.Clause (PosFin n)) :

(f.insertRupUnits units).fst.clauses = f.clauses

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : Sat.CNF.Clause (PosFin n)) :

(f.insertRupUnits units).fst.ratUnits = f.ratUnits

source

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant {n : Nat} (original_assignments : Array Assignment) (original_assignments_size : original_assignments.size = n) (units : Array (Sat.Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n) :

Prop

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignment) (assignments0_size : assignments0.size = n) (units : Array (Sat.Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n) (foundContradiction : Bool) (l : Sat.Literal (PosFin n)) :

InsertUnitInvariant assignments0 assignments0_size units assignments assignments_size → let update_res := insertUnit (units, assignments, foundContradiction) l; let_fun update_res_size := ⋯; InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Assignment) (assignments0_size : assignments0.size = n) (rupUnits : Array (Sat.Literal (PosFin n))) (assignments : Array Assignment) (assignments_size : assignments.size = n) (b : Bool) (units : Sat.CNF.Clause (PosFin n)) :

InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_size → let update_res := List.foldl insertUnit (rupUnits, assignments, b) units; let_fun update_res_size := ⋯; InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Sat.CNF.Clause (PosFin n)) :

let assignments := (f.insertRupUnits units).fst.assignments; let_fun hsize := ⋯; let rupUnits := (f.insertRupUnits units).fst.rupUnits; InsertUnitInvariant f.assignments ⋯ rupUnits assignments hsize

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRupUnits {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Sat.CNF.Clause (PosFin n)) (i j : Fin (f.insertRupUnits units).fst.rupUnits.size) :

i ≠ j → (f.insertRupUnits units).fst.rupUnits[i] ≠ (f.insertRupUnits units).fst.rupUnits[j]

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_clearUnit {n : Nat} (assignments : Array Assignment) (l : Sat.Literal (PosFin n)) :

(clearUnit assignments l).size = assignments.size

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_clearUnit_foldl {α : Type u} (assignments : Array Assignment) (f : Array Assignment → α → Array Assignment) (f_preserves_size : ∀ (arr : Array Assignment) (a : α), (f arr a).size = arr.size) (l : List α) :

(List.foldl f assignments l).size = assignments.size

source

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ClearInsertInductionMotive {n : Nat} (f : DefaultFormula n) (assignments_size : f.assignments.size = n) (units : Array (Sat.Literal (PosFin n))) :

Nat → Array Assignment → Prop

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup_base_case {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Sat.CNF.Clause (PosFin n)) :

f.ClearInsertInductionMotive ⋯ (f.insertRupUnits units).fst.rupUnits 0 (f.insertRupUnits units).fst.assignments

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insert_inductive_case {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (units : Array (Sat.Literal (PosFin n))) (units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]) (idx : Fin units.size) (assignments : Array Assignment) (ih : f.ClearInsertInductionMotive f_assignments_size units (↑idx) assignments) :

f.ClearInsertInductionMotive f_assignments_size units (↑idx + 1) (clearUnit assignments units[idx])

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup {n : Nat} (f : DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Sat.CNF.Clause (PosFin n)) :

(f.insertRupUnits units).fst.clearRupUnits = f

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :

(f.performRupCheck rupHints).fst.clauses = f.clauses

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :

(f.performRupCheck rupHints).fst.rupUnits = f.rupUnits

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :

(f.performRupCheck rupHints).fst.ratUnits = f.ratUnits

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignemnts_confirmRupHint {n : Nat} (clauses : Array (Option (DefaultClause n))) (assignments : Array Assignment) (derivedLits : Sat.CNF.Clause (PosFin n)) (b1 b2 : Bool) (id : Nat) :

(confirmRupHint clauses (assignments, derivedLits, b1, b2) id).fst.size = assignments.size

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :

(f.performRupCheck rupHints).fst.assignments.size = f.assignments.size

source

def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.DerivedLitsInvariant {n : Nat} (f : DefaultFormula n) (fassignments_size : f.assignments.size = n) (assignments : Array Assignment) (assignments_size : assignments.size = n) (derivedLits : Sat.CNF.Clause (PosFin n)) :

Prop

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_invariant_helper {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (acc : Array Assignment × Sat.CNF.Clause (PosFin n) × Bool × Bool) (hsize : acc.fst.size = n) (l : Sat.Literal (PosFin n)) (ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst) (h : ¬Assignment.hasAssignment l.snd acc.fst[l.fst.val]! = true) :

let_fun hsize' := ⋯; f.DerivedLitsInvariant f_assignments_size (acc.fst.modify l.fst.val (Assignment.addAssignment l.snd)) hsize' (l :: acc.snd.fst)

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_confirmRupHint {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (i : Fin rupHints.size) (acc : Array Assignment × Sat.CNF.Clause (PosFin n) × Bool × Bool) (ih : ∃ (hsize : acc.fst.size = n), f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst) :

let rupHint_res := confirmRupHint f.clauses acc rupHints[i]; ∃ (hsize : rupHint_res.fst.size = n), f.DerivedLitsInvariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n) :

let rupCheckRes := f.performRupCheck rupHints; f.DerivedLitsInvariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_derivedLits {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n) (derivedLits : Sat.CNF.Clause (PosFin n)) (derivedLits_satisfies_invariant : f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits) (derivedLits_arr : Array (Sat.Literal (PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }) (i j : Fin derivedLits_arr.size) (i_ne_j : i ≠ j) :

derivedLits_arr[i] ≠ derivedLits_arr[j]

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck_base_case {rupHints : Array Nat} {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (f' : DefaultFormula n) (_f'_def : f' = (f.performRupCheck rupHints).fst) (f'_assignments_size : f'.assignments.size = n) (derivedLits : Sat.CNF.Clause (PosFin n)) (derivedLits_arr : Array (Sat.Literal (PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }) (derivedLits_satisfies_invariant : f.DerivedLitsInvariant f_assignments_size f'.assignments f'_assignments_size derivedLits) (_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]) :

f.ClearInsertInductionMotive f_assignments_size derivedLits_arr 0 f'.assignments

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck {n : Nat} (f : DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) :

restoreAssignments (f.performRupCheck rupHints).fst.assignments (f.performRupCheck rupHints).snd.fst = f.assignments

source

theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupAdd_result {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) (rupHints : Array Nat) (f' : DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (rupAddSuccess : f.performRupAdd c rupHints = (f', true)) :

f' = f.insert c