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

• conflict : PropagateResult
• extended (assign : Assignment) : PropagateResult
• error : PropagateResult

def Std.Tactic.BVDecide.LRAT.Internal.State.propagateHints (s : State) (assign : Assignment) (hints : Array Nat) : PropagateResult

Equations

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

def Std.Tactic.BVDecide.LRAT.Internal.State.checkPropagate (s : State) (assign : Assignment) (rupHints : Array Nat) : Bool

Equations

• s.checkPropagate assign rupHints = match s.propagateHints assign rupHints with | Std.Tactic.BVDecide.LRAT.Internal.PropagateResult.conflict => true | x => false

def Std.Tactic.BVDecide.LRAT.Internal.State.checkRup (s : State) (clause : Sat.CNF.Clause Nat) (rupHints : Array Nat) : Bool

Equations

• s.checkRup clause rupHints = (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.ofClause clause with | some assignment => s.checkPropagate assignment rupHints | x => pure true).run

theorem Std.Tactic.BVDecide.LRAT.Internal.State.unsat_of_propagateHints_eq_conflict {s : State} {assign : Assignment} {hints : Array Nat} (h : s.propagateHints assign hints = PropagateResult.conflict) : (s.toCNF ++ assign.toCNF).Unsat

theorem Std.Tactic.BVDecide.LRAT.Internal.State.entails_of_propagateHints_eq_extended {s : State} {assign : Assignment} {hints : Array Nat} {newAssign : Assignment} (h : s.propagateHints assign hints = PropagateResult.extended newAssign) : (s.toCNF ++ assign.toCNF).Entails newAssign.toCNF

theorem Std.Tactic.BVDecide.LRAT.Internal.State.unsat_of_checkPropagate {s : State} {assign : Assignment} {rupHints : Array Nat} (h : s.checkPropagate assign rupHints = true) : (s.toCNF ++ assign.toCNF).Unsat

theorem Std.Tactic.BVDecide.LRAT.Internal.State.entails_clause_of_checkRup {s : State} {clause : Sat.CNF.Clause Nat} {rupHints : Array Nat} (h : s.checkRup clause rupHints = true) : s.toCNF.EntailsClause clause