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 : Std.Tactic.BVDecide.BVLogicalExpr) (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (assign : Std.Tactic.BVDecide.BVExpr.Assignment) : ⟦assign.toAIGAssignment, (Std.Tactic.BVDecide.ofBoolExprCached.go aig expr Std.Tactic.BVDecide.BVPred.bitblast).val⟧ = Std.Tactic.BVDecide.BVLogicalExpr.eval assign expr

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

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