This module contains basic statements about the invariants that are satisfied by the LRAT checker implementation in `Implementation`.

source
def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.StrongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) :
Prop

This invariant states that if the `assignments` field of a default formula `f` indicates that `f` contains an assignment `b` at index `i`, then the unit literal `(i, b)` must be included in `f`. Default formulas are expected to satisfy this invariant at all times except during intermediate stages of unit propagation (during which, default formulas are only expected to satisfy the more lenient `AssignmentsInvariant` defined below).

Equations

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

Instances For

source
def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.AssignmentsInvariant {n : Nat} (f : DefaultFormula n) :
Prop

This invariant states that if the `assignments` field of a default formula `f` indicates that `f` contains an assignment `b` at index `i`, then the unit literal `(i, b)` is entailed by `f`. This is distinct from the `StrongAssignmentsInvariant` defined above in that the entailment described here does not require explicitly containing the literal `(i, b)`. For example, if `f` contains `(i, b) ∨ (j, b')` as well as `(i, b) ∨ (j, ¬b')`, then the `AssignmentsInvariant` would permit the `assignments` field of `f` to contain assignment `b` at index `i`, but the `StrongAssignmentsInvariant` would not.

Equations

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

Instances For

source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.assignmentsInvariant_of_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) :
f.StrongAssignmentsInvariant → f.AssignmentsInvariant
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_of_assignmentsInvariant {n : Nat} (f : DefaultFormula n) (f_AssignmentsInvariant : f.AssignmentsInvariant) :
Limplies (PosFin n) f f.assignments
source
def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReadyForRupAdd {n : Nat} (f : DefaultFormula n) :
Prop

performRupAdd adds to f.rupUnits and then clears f.rupUnits. If f begins with some units in f.rupUnits, then performRupAdd will clear more than it intended to which will break the correctness of rupAdd_result.

Equations

- f.ReadyForRupAdd = (f.rupUnits = #[] ∧ f.StrongAssignmentsInvariant)

Instances For

source
def Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReadyForRatAdd {n : Nat} (f : DefaultFormula n) :
Prop

performRatAdd adds to f.rupUnits and f.ratUnits and then clears both. If f begins with some units in either, then performRatAdd will clear more than it intended to which will break the correctness of ratAdd_result

Equations

- f.ReadyForRatAdd = (f.ratUnits = #[] ∧ f.ReadyForRupAdd)

Instances For

source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.rupUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(f.insert c).rupUnits = f.rupUnits
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratUnits_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(f.insert c).ratUnits = f.ratUnits
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_ofArray_fold_fn {n : Nat} (assignments : Array Assignment) (cOpt : Option (DefaultClause n)) :
(ofArray_fold_fn assignments cOpt).size = assignments.size
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
(ofArray arr).ReadyForRupAdd
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_ofArray {n : Nat} (arr : Array (Option (DefaultClause n))) :
(ofArray arr).ReadyForRatAdd
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert_iff {n : Nat} (f : DefaultFormula n) (c1 c2 : DefaultClause n) :
c2 ∈ (f.insert c1).toList ↔ c2 = c1 ∨ c2 ∈ f.toList
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
Limplies (PosFin n) (f.insert c) f
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.size_assignments_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
(f.insert c).assignments.size = f.assignments.size
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
f.ReadyForRupAdd → (f.insert c).ReadyForRupAdd
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_insert {n : Nat} (f : DefaultFormula n) (c : DefaultClause n) :
f.ReadyForRatAdd → (f.insert c).ReadyForRatAdd
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_insertRupUnits {n : Nat} (f : DefaultFormula n) (units : Sat.CNF.Clause (PosFin n)) (c : DefaultClause n) :
c ∈ (f.insertRupUnits units).fst.toList → c ∈ List.map Clause.unit units ∨ c ∈ f.toList
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.mem_of_insertRatUnits {n : Nat} (f : DefaultFormula n) (units : Sat.CNF.Clause (PosFin n)) (c : DefaultClause n) :
c ∈ (f.insertRatUnits units).fst.toList → c ∈ List.map Clause.unit units ∨ c ∈ f.toList
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_rupUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
(f.deleteOne id).rupUnits = f.rupUnits
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_assignments_size {n : Nat} (f : DefaultFormula n) (id : Nat) :
(f.deleteOne id).assignments.size = f.assignments.size
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : DefaultFormula n) (id : Nat) :
f.StrongAssignmentsInvariant → (f.deleteOne id).StrongAssignmentsInvariant
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRupAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
f.ReadyForRupAdd → (f.delete arr).ReadyForRupAdd
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (id : Nat) :
(f.deleteOne id).ratUnits = f.ratUnits
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.readyForRatAdd_delete {n : Nat} (f : DefaultFormula n) (arr : Array Nat) :
f.ReadyForRatAdd → (f.delete arr).ReadyForRatAdd
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_subset {n : Nat} (f : DefaultFormula n) (id : Nat) (c : DefaultClause n) :
c ∈ (f.deleteOne id).toList → c ∈ f.toList
source
theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.delete_subset {n : Nat} (f : DefaultFormula n) (arr : Array Nat) (c : DefaultClause n) :
c ∈ (f.delete arr).toList → c ∈ f.toList