Documentation

Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas

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

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

    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

      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

        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
          theorem Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne_preserves_strongAssignmentsInvariant {n : Nat} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n) (id : Nat) :
          f.StrongAssignmentsInvariant(f.deleteOne id).StrongAssignmentsInvariant