This module contains the implementation of a bitblaster for BitVec constants.
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Sat.AIG α)
(val : BitVec w)
:
aig.RefVec w
Equations
Instances For
@[irreducible]
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Sat.AIG α)
(val : BitVec w)
(curr : Nat)
(s : aig.RefVec curr)
(hcurr : curr ≤ w)
:
aig.RefVec w
Equations
- One or more equations did not get rendered due to their size.