This module contains the implementation of a bitblaster for predicates over BitVec expressions (BVPred).

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

• result : aig.ExtendingEntrypoint
• cache : BVExpr.Cache self.result.val.aig

def Std.Tactic.BVDecide.BVPred.bitblast (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) : Return aig

Equations

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

theorem Std.Tactic.BVDecide.BVPred.bitblast_decl_eq (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred 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.BVPred.bitblast_le_size (aig : Sat.AIG BVBit) (input : BVExpr.WithCache BVPred aig) : aig.decls.size ≤ (bitblast aig input).result.val.aig.decls.size