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 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w) : Std.Sat.AIG.RefVecEntry Std.Tactic.BVDecide.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 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.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 : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val.aig.decls.size) : (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val.aig.decls[idx] = aig.decls[idx]

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