Documentation

Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr

This module contains the implementation of a bitblaster for BitVec expressions (BVExpr). That is, expressions that evaluate to BitVec again. Its used as a building block in bitblasting general BitVec problems with boolean substructure.

theorem Std.Tactic.BVDecide.BVExpr.bitblast.go_decl_eq {w : Nat} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val.aig.decls.size) :
(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val.aig.decls[idx] = aig.decls[idx]