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