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

• formula : Array (Option (Sat.CNF.Clause Nat))

def Std.Tactic.BVDecide.LRAT.Internal.State.ofCNF (cnf : Sat.CNF Nat) : State

Equations

• Std.Tactic.BVDecide.LRAT.Internal.State.ofCNF cnf = { formula := Array.map (fun (clause : Std.Sat.CNF.Clause Nat) => some clause) cnf.clauses }

def Std.Tactic.BVDecide.LRAT.Internal.State.toCNF (s : State) : Sat.CNF Nat

Equations

• s.toCNF = { clauses := Array.filterMap id s.formula }

@[simp]

theorem Std.Tactic.BVDecide.LRAT.Internal.State.ofCNF_toCNF_eq {cnf : Sat.CNF Nat} : (ofCNF cnf).toCNF = cnf

theorem Std.Tactic.BVDecide.LRAT.Internal.State.entails_ofCNF_toCNF {cnf : Sat.CNF Nat} : cnf.Entails (ofCNF cnf).toCNF

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.State.get? (s : State) (idx : Nat) : Option (Sat.CNF.Clause Nat)

Equations

• s.get? idx = s.formula.getD (idx - 1) none

@[inline]

def Std.Tactic.BVDecide.LRAT.Internal.State.all (s : State) (p : Nat → Sat.CNF.Clause Nat → Bool) : Bool

Check that p holds for all clauses of s, together with the index they are stored at.

This iterates over the underlying array instead of s.toCNF, which would have to be materialized.

Equations

• s.all p = Std.Tactic.BVDecide.LRAT.Internal.State.all.go✝ s p 0

theorem Std.Tactic.BVDecide.LRAT.Internal.State.mem_toCNF_of_eq_some {idx : Nat} {c : Sat.CNF.Clause Nat} {s : State} (h : s.get? idx = some c) : c ∈ s.toCNF

theorem Std.Tactic.BVDecide.LRAT.Internal.State.exists_getElem_eq_some_of_mem {c : Sat.CNF.Clause Nat} {s : State} (h : c ∈ s.toCNF) : ∃ (i : Nat), ∃ (hi : i < s.formula.size), s.formula[i] = some c

theorem Std.Tactic.BVDecide.LRAT.Internal.State.get?_add_one_of_getElem_eq_some {c : Sat.CNF.Clause Nat} {s : State} {i : Nat} (hi : i < s.formula.size) (h : s.formula[i] = some c) : s.get? (i + 1) = some c

theorem Std.Tactic.BVDecide.LRAT.Internal.State.exists_get?_eq_some_of_mem {c : Sat.CNF.Clause Nat} {s : State} (h : c ∈ s.toCNF) : ∃ (idx : Nat), s.get? idx = some c

theorem Std.Tactic.BVDecide.LRAT.Internal.State.all_eq_true_iff {s : State} {p : Nat → Sat.CNF.Clause Nat → Bool} : s.all p = true ↔ ∀ (j : Nat) (hj : j < s.formula.size) (c : Sat.CNF.Clause Nat), s.formula[j] = some c → p (j + 1) c = true

theorem Std.Tactic.BVDecide.LRAT.Internal.State.forall_of_all_eq_true {s : State} {p : Nat → Sat.CNF.Clause Nat → Bool} (h : s.all p = true) (c : Sat.CNF.Clause Nat) : c ∈ s.toCNF → ∃ (idx : Nat), s.get? idx = some c ∧ p idx c = true