Documentation

Std.Tactic.BVDecide.LRAT.Internal.Assignment

source
inductive Std.Tactic.BVDecide.LRAT.Internal.Assignment :
Type

The Assignment inductive datatype is used in the assignments field of default formulas (defined in Formula.Implementation.lean) to store and quickly access information about whether unit literals are contained in (or entailed by) a formula.

The elements of Assignment can be viewed as a lattice where both is top, satisfying both hasPosAssignment and hasNegAssignment, pos satisfies only the former, neg satisfies only the latter, and unassigned is bottom, satisfying neither. If one wanted to modify the default formula structure to use a BitArray rather than an Assignment Array for the assignments field, a reasonable 2-bit representation of the Assignment type would be:

  • both: 11
  • pos: 10
  • neg: 01
  • unassigned: 00

Then hasPosAssignment could simply query the first bit and hasNegAssignment could simply query the second bit.

Instances For
    source
    instance Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment :
    Inhabited Assignment
    Equations
    source
    instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqAssignment :
    DecidableEq Assignment
    Equations
    source
    instance Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment :
    BEq Assignment
    Equations
    source
    instance Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString :
    ToString Assignment
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[inline]
    def Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment (assignment : Assignment) :
    Bool
    Equations
    Instances For
      source
      @[inline]
      def Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment (assignment : Assignment) :
      Bool
      Equations
      Instances For
        source
        @[inline]
        def Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment (oldAssignment : Assignment) :
        Assignment

        Updates the old assignment of l to reflect the fact that (l, true) is now part of the formula.

        Equations
        Instances For
          source
          @[inline]
          def Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePosAssignment (oldAssignment : Assignment) :
          Assignment

          Updates the old assignment of l to reflect the fact that (l, true) is no longer part of the formula.

          Equations
          Instances For
            source
            @[inline]
            def Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment (oldAssignment : Assignment) :
            Assignment

            Updates the old assignment of l to reflect the fact that (l, false) is now part of the formula.

            Equations
            Instances For
              source
              @[inline]
              def Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNegAssignment (oldAssignment : Assignment) :
              Assignment

              Updates the old assignment of l to reflect the fact that (l, false) is no longer part of the formula.

              Equations
              Instances For
                source
                def Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment (b : Bool) :
                Assignment → Assignment
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment (b : Bool) :
                  Assignment → Assignment
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    def Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment (b : Bool) :
                    Assignment → Bool
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePos_addPos_cancel {assignment : Assignment} (h : ¬assignment.hasPosAssignment = true) :
                      assignment.addPosAssignment.removePosAssignment = assignment
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬assignment.hasNegAssignment = true) :
                      assignment.addNegAssignment.removeNegAssignment = assignment
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬hasAssignment b assignment = true) :
                      removeAssignment b (addAssignment b assignment) = assignment
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.add_both_eq_both (b : Bool) :
                      addAssignment b both = both
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_both (b : Bool) :
                      hasAssignment b both = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_add (assignment : Assignment) (b : Bool) :
                      hasAssignment b (addAssignment b assignment) = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_hasPos_removePos (assignment : Assignment) :
                      ¬assignment.removePosAssignment.hasPosAssignment = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_hasNeg_removeNeg (assignment : Assignment) :
                      ¬assignment.removeNegAssignment.hasNegAssignment = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_has_remove (assignment : Assignment) (b : Bool) :
                      ¬hasAssignment b (removeAssignment b assignment) = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_remove_irrelevant (assignment : Assignment) (b : Bool) :
                      hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned_of_has_neither (assignment : Assignment) (lacks_pos : ¬assignment.hasPosAssignment = true) (lacks_neg : ¬assignment.hasNegAssignment = true) :
                      assignment = unassigned
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPos_addNeg (assignment : Assignment) :
                      assignment.addNegAssignment.hasPosAssignment = assignment.hasPosAssignment
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNeg_addPos (assignment : Assignment) :
                      assignment.addPosAssignment.hasNegAssignment = assignment.hasNegAssignment
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_iff_has_add_complement (assignment : Assignment) (b : Bool) :
                      hasAssignment b assignment = true ↔ hasAssignment b (addAssignment (decide ¬b = true) assignment) = true
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPos_addNeg_eq_both (assignment : Assignment) :
                      assignment.addNegAssignment.addPosAssignment = both
                      source
                      theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNeg_addPos_eq_both (assignment : Assignment) :
                      assignment.addPosAssignment.addNegAssignment = both
                      source
                      instance Std.Tactic.BVDecide.LRAT.Internal.Assignment.instEntailsPosFinArray {n : Nat} :
                      Entails (PosFin n) (Array Assignment)
                      Equations
                      • One or more equations did not get rendered due to their size.