Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr

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 :

w : Nat
expr : BVExpr self.w

Instances For

Std.Tactic.BVDecide.BVExpr.instHashableKey

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) :

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} :

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) :

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) :

val : α
cache : Cache aig

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

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