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

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : Sat.AIG BVBit) (assign : BVExpr.Assignment) : ⟦assign.toAIGAssignment, (ofBoolExprCached.go aig expr BVPred.bitblast).val⟧ = eval assign expr

theorem Std.Tactic.BVDecide.BVLogicalExpr.denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) : ⟦assign.toAIGAssignment, expr.bitblast⟧ = eval assign expr

theorem Std.Tactic.BVDecide.BVLogicalExpr.unsat_of_bitblast (expr : BVLogicalExpr) : expr.bitblast.Unsat → expr.Unsat