This module contains the implementation of a bitblaster for BitVec expressions (BVExpr). That is, expressions that evaluate to BitVec again. Its used as a building block in bitblasting general BitVec problems with boolean substructure.

structure Std.Tactic.BVDecide.BVExpr.Cache.Key : Type

• w : Nat
• expr : BVExpr self.w

instance Std.Tactic.BVDecide.BVExpr.Cache.instDecidableEqKey : DecidableEq Key

Equations

• Std.Tactic.BVDecide.BVExpr.Cache.instDecidableEqKey = Std.Tactic.BVDecide.BVExpr.Cache.decEqKey✝

instance Std.Tactic.BVDecide.BVExpr.instHashableKey : Hashable Cache.Key

Equations

• Std.Tactic.BVDecide.BVExpr.instHashableKey = { hash := fun (key : Std.Tactic.BVDecide.BVExpr.Cache.Key) => hash key.expr }

structure Std.Tactic.BVDecide.BVExpr.Cache (aig : Sat.AIG BVBit) : Type

• map : DHashMap Key fun (k : Key) => Vector Sat.AIG.Fanin k.w
• hbound {i : Nat} (k : Key) (h1 : k ∈ self.map) (h2 : i < k.w) : (self.map.get k h1)[i].gate < aig.decls.size

@[inline]

def Std.Tactic.BVDecide.BVExpr.Cache.empty {aig : Sat.AIG BVBit} : Cache aig

Equations

• Std.Tactic.BVDecide.BVExpr.Cache.empty = { map := ∅, hbound := ⋯ }

@[inline]

def Std.Tactic.BVDecide.BVExpr.Cache.insert {aig : Sat.AIG BVBit} {w : Nat} (cache : Cache aig) (expr : BVExpr w) (refs : aig.RefVec w) : Cache aig

Equations

• { map := map, hbound := hbound }.insert expr refs = { map := map.insert { w := w, expr := expr } refs.refs, hbound := ⋯ }

@[inline]

def Std.Tactic.BVDecide.BVExpr.Cache.get? {aig : Sat.AIG BVBit} {w : Nat} (cache : Cache aig) (expr : BVExpr w) : Option (aig.RefVec w)

Equations

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

@[inline]

def Std.Tactic.BVDecide.BVExpr.Cache.cast {aig1 aig2 : Sat.AIG BVBit} (cache : Cache aig1) (h : aig1.decls.size ≤ aig2.decls.size) : Cache aig2

Equations

• { map := map, hbound := hbound }.cast h = { map := map, hbound := ⋯ }

structure Std.Tactic.BVDecide.BVExpr.WithCache (α : Type u) (aig : Sat.AIG BVBit) : Type u

• val : α
• cache : Cache aig

structure Std.Tactic.BVDecide.BVExpr.Return (aig : Sat.AIG BVBit) (w : Nat) : Type

• result : aig.ExtendingRefVecEntry w
• cache : Cache self.result.val.aig

def Std.Tactic.BVDecide.BVExpr.bitblast {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) : Return aig w

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast aig { val := expr, cache := cache } = Std.Tactic.BVDecide.BVExpr.bitblast.goCache aig expr cache

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.goCache {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w

Equations

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

@[irreducible]

def Std.Tactic.BVDecide.BVExpr.bitblast.go {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) : Return aig w

Equations

• One or more equations did not get rendered due to their size.
• Std.Tactic.BVDecide.BVExpr.bitblast.go aig (Std.Tactic.BVDecide.BVExpr.var a) cache = { result := ⟨Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig { ident := a }, ⋯⟩, cache := cache.cast ⋯ }
• Std.Tactic.BVDecide.BVExpr.bitblast.go aig (Std.Tactic.BVDecide.BVExpr.const val) cache = { result := ⟨Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig val, ⋯⟩, cache := cache.cast ⋯ }

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.goCache_decl_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (goCache aig expr cache).result.val.aig.decls.size) : (goCache aig expr cache).result.val.aig.decls[idx] = aig.decls[idx]

@[irreducible]

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_decl_eq {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) (cache : Cache aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (go aig expr cache).result.val.aig.decls.size) : (go aig expr cache).result.val.aig.decls[idx] = aig.decls[idx]

theorem Std.Tactic.BVDecide.BVExpr.bitblast_decl_eq {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (bitblast aig input).result.val.aig.decls.size) : (bitblast aig input).result.val.aig.decls[idx] = aig.decls[idx]

theorem Std.Tactic.BVDecide.BVExpr.bitblast_le_size {w : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) : aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size

theorem Std.Tactic.BVDecide.BVExpr.bitblast_lt_size_of_lt_aig_size {w x : Nat} (aig : Sat.AIG BVBit) (input : WithCache (BVExpr w) aig) (h : x < aig.decls.size) : x < (bitblast aig input).result.val.aig.decls.size