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.
def
Std.Tactic.BVDecide.BVExpr.bitblast
{w : Nat}
(aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
(expr : Std.Tactic.BVDecide.BVExpr w)
:
Equations
- Std.Tactic.BVDecide.BVExpr.bitblast aig expr = (Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr).val
Instances For
def
Std.Tactic.BVDecide.BVExpr.bitblast.go
{w : Nat}
(aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit)
(expr : Std.Tactic.BVDecide.BVExpr w)
:
aig.ExtendingRefVecEntry w
Equations
- One or more equations did not get rendered due to their size.
- Std.Tactic.BVDecide.BVExpr.bitblast.go aig (Std.Tactic.BVDecide.BVExpr.var a) = ⟨Std.Tactic.BVDecide.BVExpr.bitblast.blastVar aig { ident := a }, ⋯⟩
- Std.Tactic.BVDecide.BVExpr.bitblast.go aig (Std.Tactic.BVDecide.BVExpr.const val) = ⟨Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig val, ⋯⟩
Instances For
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]
instance
Std.Tactic.BVDecide.BVExpr.instLawfulVecOperatorBVBitBitblast :
Std.Sat.AIG.LawfulVecOperator Std.Tactic.BVDecide.BVBit
(fun (x : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (w : Nat) => Std.Tactic.BVDecide.BVExpr w) fun {len : Nat} =>
Std.Tactic.BVDecide.BVExpr.bitblast