Documentation

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_fold {n : Nat} {units : List (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))} (unitsAcc : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool) :
(List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (unitsAcc, assignments, b) units).snd.fst.size = assignments.size
def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant {n : Nat} (original_assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (original_assignments_size : original_assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) :
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments0_size : assignments0.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (foundContradiction : Bool) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size units assignments assignments_sizelet update_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (units, assignments, foundContradiction) l; let_fun update_res_size := ; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
    theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertUnit_fold {n : Nat} (assignments0 : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments0_size : assignments0.size = n) (rupUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (assignments_size : assignments.size = n) (b : Bool) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
    Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size rupUnits assignments assignments_sizelet update_res := List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit (rupUnits, assignments, b) units; let_fun update_res_size := ; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant assignments0 assignments0_size update_res.fst update_res.snd.fst update_res_size
    theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnitInvariant_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
    let assignments := (f.insertRupUnits units).fst.assignments; let_fun hsize := ; let rupUnits := (f.insertRupUnits units).fst.rupUnits; Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.InsertUnitInvariant f.assignments rupUnits assignments hsize
    theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_insertRupUnits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (i : Fin (f.insertRupUnits units).fst.rupUnits.size) (j : Fin (f.insertRupUnits units).fst.rupUnits.size) :
    i j(f.insertRupUnits units).fst.rupUnits[i] (f.insertRupUnits units).fst.rupUnits[j]
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup_base_case {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
      f.ClearInsertInductionMotive (f.insertRupUnits units).fst.rupUnits 0 (f.insertRupUnits units).fst.assignments
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insert_inductive_case {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (units_nodup : ∀ (i j : Fin units.size), i junits[i] units[j]) (idx : Fin units.size) (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (ih : f.ClearInsertInductionMotive f_assignments_size units (↑idx) assignments) :
      f.ClearInsertInductionMotive f_assignments_size units (idx + 1) (Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clearUnit assignments units[idx])
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clear_insertRup {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (units : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) :
      (f.insertRupUnits units).fst.clearRupUnits = f
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) :
      (f.performRupCheck rupHints).fst.clauses = f.clauses
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) :
      (f.performRupCheck rupHints).fst.rupUnits = f.rupUnits
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) :
      (f.performRupCheck rupHints).fst.ratUnits = f.ratUnits
      theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (rupHints : Array Nat) :
      (f.performRupCheck rupHints).fst.assignments.size = f.assignments.size
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint_preserves_invariant_helper {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (acc : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool) (hsize : acc.fst.size = n) (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (ih : f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst) (h : ¬Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment l.snd acc.fst[l.fst.val]! = true) :
        let_fun hsize' := ; f.DerivedLitsInvariant f_assignments_size (acc.fst.modify l.fst.val (Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment l.snd)) hsize' (l :: acc.snd.fst)
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_confirmRupHint {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (i : Fin rupHints.size) (acc : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) × Bool × Bool) (ih : ∃ (hsize : acc.fst.size = n), f.DerivedLitsInvariant f_assignments_size acc.fst hsize acc.snd.fst) :
        let rupHint_res := Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.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
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.derivedLitsInvariant_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.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
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.nodup_derivedLits {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) (f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n) (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (derivedLits_satisfies_invariant : f.DerivedLitsInvariant f_assignments_size (f.performRupCheck rupHints).fst.assignments f'_assignments_size derivedLits) (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) (derivedLits_arr_def : derivedLits_arr = { toList := derivedLits }) (i : Fin derivedLits_arr.size) (j : Fin derivedLits_arr.size) (i_ne_j : i j) :
        derivedLits_arr[i] derivedLits_arr[j]
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck_base_case {rupHints : Array Nat} {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (_f'_def : f' = (f.performRupCheck rupHints).fst) (f'_assignments_size : f'.assignments.size = n) (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (derivedLits_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.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 jderivedLits_arr[i] derivedLits_arr[j]) :
        f.ClearInsertInductionMotive f_assignments_size derivedLits_arr 0 f'.assignments
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments_performRupCheck {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_assignments_size : f.assignments.size = n) (rupHints : Array Nat) :
        Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.restoreAssignments (f.performRupCheck rupHints).fst.assignments (f.performRupCheck rupHints).snd.fst = f.assignments
        theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupAdd_result {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) (rupHints : Array Nat) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (f_readyForRupAdd : f.ReadyForRupAdd) (rupAddSuccess : f.performRupAdd c rupHints = (f', true)) :
        f' = f.insert c