Documentation

Std.Tactic.BVDecide.LRAT.Internal.Assignment

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
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.removePos_addPos_cancel {assignment : Assignment} (h : ¬assignment.hasPosAssignment = true) :
assignment.addPosAssignment.removePosAssignment = assignment
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬assignment.hasNegAssignment = true) :
assignment.addNegAssignment.removeNegAssignment = assignment
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_hasPos_removePos (assignment : Assignment) :
¬assignment.removePosAssignment.hasPosAssignment = true
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_hasNeg_removeNeg (assignment : Assignment) :
¬assignment.removeNegAssignment.hasNegAssignment = true
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
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPos_addNeg (assignment : Assignment) :
assignment.addNegAssignment.hasPosAssignment = assignment.hasPosAssignment
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNeg_addPos (assignment : Assignment) :
assignment.addPosAssignment.hasNegAssignment = assignment.hasNegAssignment
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPos_addNeg_eq_both (assignment : Assignment) :
assignment.addNegAssignment.addPosAssignment = both
theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNeg_addPos_eq_both (assignment : Assignment) :
assignment.addPosAssignment.addNegAssignment = both
Equations
  • One or more equations did not get rendered due to their size.