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

@[implicit_reducible]

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

def Std.Tactic.BVDecide.BVExpr.Cache.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

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

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

@[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

@[inline]

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

@[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

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

@[irreducible]

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

@[irreducible]

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

@[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