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.

source
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
source
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
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.denote_bitblast (expr : BVLogicalExpr) (assign : BVExpr.Assignment) :
⟦assign.toAIGAssignment, expr.bitblast⟧ = eval assign expr
source
theorem Std.Tactic.BVDecide.BVLogicalExpr.unsat_of_bitblast (expr : BVLogicalExpr) :
expr.bitblast.Unsat → expr.Unsat