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_Inv_of_Inv (expr : BVLogicalExpr) (aig : Sat.AIG BVBit) (assign : BVExpr.Assignment) (cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) : BVExpr.Cache.Inv assign (go aig expr cache).result.val.aig (go aig expr cache).cache

theorem Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go_eval_eq_eval (expr : BVLogicalExpr) (aig : Sat.AIG BVBit) (assign : BVExpr.Assignment) (cache : BVExpr.Cache aig) (hinv : BVExpr.Cache.Inv assign aig cache) : ⟦assign.toAIGAssignment, (go aig expr cache).result.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