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
This module contains the implementation of a bitblaster for BitVec
constants.