def
Reduce.populate_queue
{n m : ℕ}
(O : OBdd n m)
(i : Fin n)
(acc : List ((RawBdd.RawPointer × RawBdd.RawPointer) × Fin m))
(l : List (Fin m))
(ps : ProvedState n m)
:
Invariant O ps ↑i →
(∀ j ∈ l, ↑(↑O).heap[j].var = ↑i) →
(∀ j ∈ l, Pointer.Reachable (↑O).heap (↑O).root (Pointer.node j)) →
(∀ entry ∈ acc,
RawBdd.RawPointer.Bounded ps.state.size entry.1.1 ∧ RawBdd.RawPointer.Bounded ps.state.size entry.1.2) →
(∀ entry ∈ acc, entry.1.1 ≠ entry.1.2) →
(∀ entry ∈ acc, EntryCorrect O ps (↑i) entry) →
VarInvariant O ps →
{ p : ProvedState n m × List ((RawBdd.RawPointer × RawBdd.RawPointer) × Fin m) // Invariant O p.1 ↑i ∧ p.1.state.size = ps.state.size ∧ (AllAbove ps ↑i ∧ HeapInjective ps → AllAbove p.1 ↑i ∧ HeapInjective p.1) ∧ (∀ entry ∈ acc, entry ∈ p.2) ∧ (∀ (k : Fin m), ps.state.ids[k].isSome = true → p.1.state.ids[k].isSome = true) ∧ (∀ j ∈ l,
(∃ (key : RawBdd.RawPointer × RawBdd.RawPointer), (key, j) ∈ p.2) ∨ p.1.state.ids[j].isSome = true) ∧ (∀ entry ∈ p.2,
RawBdd.RawPointer.Bounded p.1.state.size entry.1.1 ∧ RawBdd.RawPointer.Bounded p.1.state.size entry.1.2) ∧ (∀ entry ∈ p.2, entry.1.1 ≠ entry.1.2) ∧ (∀ entry ∈ p.2, EntryCorrect O p.1 (↑i) entry) ∧ VarInvariant O p.1 }
For each node j in l: if lid = hid (redundant), set ids[j] := lid; otherwise add to accumulator.
Equations
Instances For
theorem
Reduce.push_back_lt
{n s : ℕ}
{v : Vector (RawBdd.RawNode n) s}
{N : RawBdd.RawNode n}
{hh : ∀ (k : Fin s), RawBdd.RawNode.Bounded (↑k) v[k]}
{hh' : ∀ (k : Fin (s + 1)), RawBdd.RawNode.Bounded (↑k) (v.push N)[k]}
{p : RawBdd.RawPointer}
(hp : RawBdd.RawPointer.Bounded s p)
{hp' : RawBdd.RawPointer.Bounded (s + 1) p}
(j : Fin (s + 1))
:
Pointer.Reachable (RawBdd.cook_heap (v.push N) hh') (p.cook ⋯) (Pointer.node j) →
∃ (hj : ↑j < s), Pointer.Reachable (RawBdd.cook_heap v hh) (p.cook ⋯) (Pointer.node ⟨↑j, hj⟩)
Any node reachable in the pushed heap was already reachable in the original heap,
and its index is strictly less than s (the pre-push size).