inductive Std.Tactic.BVDecide.LRAT.Internal.AssignValue : Type

The value of an atom under an Assignment.

• unassigned : AssignValue
• true : AssignValue
• false : AssignValue

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.AssignValue.ofBool : Bool → AssignValue

Equations

• Std.Tactic.BVDecide.LRAT.Internal.AssignValue.ofBool true = Std.Tactic.BVDecide.LRAT.Internal.AssignValue.true
• Std.Tactic.BVDecide.LRAT.Internal.AssignValue.ofBool false = Std.Tactic.BVDecide.LRAT.Internal.AssignValue.false

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.AssignValue.toOption : AssignValue → Option Bool

Equations

• Std.Tactic.BVDecide.LRAT.Internal.AssignValue.unassigned.toOption = none
• Std.Tactic.BVDecide.LRAT.Internal.AssignValue.true.toOption = some true
• Std.Tactic.BVDecide.LRAT.Internal.AssignValue.false.toOption = some false

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.AssignValue.toOption_ofBool {b : Bool} : (ofBool b).toOption = some b

structure Std.Tactic.BVDecide.LRAT.Internal.Assignment : Type

• assign : HashMap Nat AssignValue

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.empty : Assignment

Equations

• Std.Tactic.BVDecide.LRAT.Internal.Assignment.empty = { assign := ∅ }

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.get (a : Assignment) (atom : Nat) : AssignValue

Equations

• a.get atom = a.assign.getD atom Std.Tactic.BVDecide.LRAT.Internal.AssignValue.unassigned

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.get? (a : Assignment) (atom : Nat) : Option Bool

Equations

• a.get? atom = (a.get atom).toOption

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get?_empty {atom : Nat} : empty.get? atom = none

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.insert (a : Assignment) (atom : Nat) (b : Bool) : Assignment

Equations

• a.insert atom b = { assign := a.assign.insert atom (Std.Tactic.BVDecide.LRAT.Internal.AssignValue.ofBool b) }

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get?_insert_of_eq {atom atom' : Nat} {b : Bool} {a : Assignment} (h : atom = atom') : (a.insert atom b).get? atom' = some b

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get?_insert_of_ne {atom atom' : Nat} {b : Bool} {a : Assignment} (h : atom ≠ atom') : (a.insert atom b).get? atom' = a.get? atom'

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get_eq_unassigned_iff {atom : Nat} {a : Assignment} : a.get atom = AssignValue.unassigned ↔ a.get? atom = none

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get_eq_true_iff {atom : Nat} {a : Assignment} : a.get atom = AssignValue.true ↔ a.get? atom = some true

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get_eq_false_iff {atom : Nat} {a : Assignment} : a.get atom = AssignValue.false ↔ a.get? atom = some false

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.erase (a : Assignment) (atom : Nat) : Assignment

Equations

• a.erase atom = { assign := a.assign.erase atom }

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.toCNF (a : Assignment) : Sat.CNF Nat

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.sat_toCNF_iff {assign : Assignment} (a : Nat → Bool) : Sat.CNF.Sat a assign.toCNF ↔ ∀ (atom : Nat) (pol : Bool), assign.get? atom = some pol → a atom = pol

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.not_sat_of_forall_falsified {assign : Assignment} {c : Sat.CNF.Clause Nat} {a : Nat → Bool} (h1 : Sat.CNF.Sat a assign.toCNF) (h2 : ∀ (lit : Sat.Literal Nat), lit ∈ c → assign.get? lit.fst = some !lit.snd) : ¬Sat.CNF.Clause.Sat a c

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.unit_propagation {assign : Assignment} {c : Sat.CNF.Clause Nat} {unit : Sat.Literal Nat} {a : Nat → Bool} (h1 : Sat.CNF.Sat a assign.toCNF) (h2 : Sat.CNF.Clause.Sat a c) (h3 : ∀ (lit : Sat.Literal Nat), lit ∈ c → lit = unit ∨ assign.get? lit.fst = some !lit.snd) : a unit.fst = unit.snd

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.toCNF_add_entails_toCNF_insert {atom : Nat} {pol : Bool} {assignment : Assignment} : (assignment.toCNF.add (Sat.CNF.Clause.unit atom pol)).Entails (assignment.insert atom pol).toCNF

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.ofClause (clause : Sat.CNF.Clause Nat) : Option Assignment

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.ofClause_spec (clause : Sat.CNF.Clause Nat) : match ofClause clause with | none => ∃ (atom : Nat), ∃ (pol : Bool), (atom, pol) ∈ clause ∧ (atom, !pol) ∈ clause | some assignment => ∀ (lit : Sat.Literal Nat), lit ∈ clause ↔ assignment.get? lit.fst = some !lit.snd

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.exists_lit_of_ofClause_eq_none {clause : Sat.CNF.Clause Nat} (h : ofClause clause = none) : ∃ (atom : Nat), ∃ (pol : Bool), (atom, pol) ∈ clause ∧ (atom, !pol) ∈ clause

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.sat_of_ofClause_eq_none {clause : Sat.CNF.Clause Nat} (h : ofClause clause = none) (a : Nat → Bool) : Sat.CNF.Clause.Sat a clause

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.get_eq_of_ofClause_eq_some {clause : Sat.CNF.Clause Nat} {assignment : Assignment} (h : ofClause clause = some assignment) (lit : Sat.Literal Nat) : lit ∈ clause ↔ assignment.get? lit.fst = some !lit.snd

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.isNegationOf_of_ofClause_eq_some {clause : Sat.CNF.Clause Nat} {assignment : Assignment} (h1 : ofClause clause = some assignment) : assignment.toCNF.IsNegationOf clause

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.entails_clause_of_unsat_of_ofClause_eq_some {clause : Sat.CNF.Clause Nat} {assignment : Assignment} {f : Sat.CNF Nat} (h1 : ofClause clause = some assignment) (h2 : (f ++ assignment.toCNF).Unsat) : f.EntailsClause clause

def Std.Tactic.BVDecide.LRAT.Internal.Assignment.extendOfClauseWithout (assign : Assignment) (c : Sat.CNF.Clause Nat) (lit : Sat.Literal Nat) : Option Assignment

Extend assign so that it additionally falsifies every literal of c except lit.

Returns none if that is impossible, which happens exactly when assign already satisfies a literal of c besides lit, or when c contains a variable in both polarities besides lit.

Equations

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

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.extendOfClauseWithout_spec (assign : Assignment) (clause : Sat.CNF.Clause Nat) (lit : Sat.Literal Nat) : match assign.extendOfClauseWithout clause lit with | none => assign.toCNF.EntailsClause (clause.erase lit) | some newAssign => ∀ (lit' : Sat.Literal Nat), lit' ∈ clause ∧ lit' ≠ lit ∨ assign.get? lit'.fst = some !lit'.snd ↔ newAssign.get? lit'.fst = some !lit'.snd

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.mem_or_get?_eq_iff_of_extendOfClauseWithout_eq_some {a : Assignment} {clause : Sat.CNF.Clause Nat} {lit : Sat.Literal Nat} {newAssign : Assignment} (h : a.extendOfClauseWithout clause lit = some newAssign) (lit' : Sat.Literal Nat) : lit' ∈ clause ∧ lit' ≠ lit ∨ a.get? lit'.fst = some !lit'.snd ↔ newAssign.get? lit'.fst = some !lit'.snd

theorem Std.Tactic.BVDecide.LRAT.Internal.Assignment.entails_clause_of_extendOfClauseWithout_eq_none {a : Assignment} {clause : Sat.CNF.Clause Nat} {lit : Sat.Literal Nat} (h : a.extendOfClauseWithout clause lit = none) : a.toCNF.EntailsClause (clause.erase lit)