This module contains the implementation of a bitblaster for general BitVec problems with boolean substructure (BVLogicalExpr). It is the main entrypoint into the bitblasting framework.

def Std.Tactic.BVDecide.BVLogicalExpr.bitblast (expr : Std.Tactic.BVDecide.BVLogicalExpr) : Std.Sat.AIG.Entrypoint Std.Tactic.BVDecide.BVBit

Equations

• expr.bitblast = Std.Tactic.BVDecide.ofBoolExprCached expr Std.Tactic.BVDecide.BVPred.bitblast