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.

def Std.Tactic.BVDecide.BVExpr.bitblast {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) : Sat.AIG.RefVecEntry BVBit w

Equations

• Std.Tactic.BVDecide.BVExpr.bitblast aig expr = (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val

def Std.Tactic.BVDecide.BVExpr.bitblast.go {w : Nat} (aig : Sat.AIG BVBit) (expr : BVExpr w) : aig.ExtendingRefVecEntry 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) = ⟨Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig { ident := a }, ⋯⟩
• Std.Tactic.BVDecide.BVExpr.bitblast.go aig (Std.Tactic.BVDecide.BVExpr.const val) = ⟨Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig val, ⋯⟩

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

instance Std.Tactic.BVDecide.BVExpr.instLawfulVecOperatorBVBitBitblast : Sat.AIG.LawfulVecOperator BVBit (fun (x : Sat.AIG BVBit) (w : Nat) => BVExpr w) fun {len : Nat} => bitblast