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.

• pos : Assignment
• neg : Assignment
• both : Assignment
• unassigned : Assignment

instance Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment : Inhabited Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment = { default := Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment.default }

def Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment.default : Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment.default = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos

instance Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqAssignment : DecidableEq Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instDecidableEqAssignment x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment : BEq Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment = { beq := Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment.beq }

def Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment.beq : Assignment → Assignment → Bool

Equations

• Std.Tactic.BVDecide.LRAT.Internal.instBEqAssignment.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString : ToString Assignment

Equations

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

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasPosAssignment (assignment : Assignment) : Bool

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.hasPosAssignment = true
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.hasPosAssignment = false
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.hasPosAssignment = true
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.hasPosAssignment = false

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasNegAssignment (assignment : Assignment) : Bool

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.hasNegAssignment = false
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.hasNegAssignment = true
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.hasNegAssignment = true
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.hasNegAssignment = false

@[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

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.addPosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos

@[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

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.removePosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.removePosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.removePosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.removePosAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned

@[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

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.both
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.addNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg

@[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

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos.removeNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg.removeNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.both.removeNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos
• Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned.removeNegAssignment = Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment (b : Bool) (a : Assignment) : Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.addAssignment b a = if b = true then a.addPosAssignment else a.addNegAssignment

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment (b : Bool) (a : Assignment) : Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment b a = if b = true then a.removePosAssignment else a.removeNegAssignment

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment (b : Bool) (a : Assignment) : Bool

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b a = if b = true then a.hasPosAssignment else a.hasNegAssignment

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.remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬hasAssignment b assignment = true) : removeAssignment b (addAssignment b assignment) = assignment

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.add_both_eq_both (b : Bool) : addAssignment b both = both

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_both (b : Bool) : hasAssignment b both = true

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_add (assignment : Assignment) (b : Bool) : hasAssignment b (addAssignment b assignment) = true

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.not_has_remove (assignment : Assignment) (b : Bool) : ¬hasAssignment b (removeAssignment b assignment) = true

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_remove_irrelevant (assignment : Assignment) (b : Bool) : hasAssignment b (removeAssignment (!b) assignment) = true → hasAssignment b assignment = 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.has_iff_has_add_complement (assignment : Assignment) (b : Bool) : hasAssignment b assignment = true ↔ hasAssignment b (addAssignment (decide ¬b = true) assignment) = true

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

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.