This module contains the implementation of a bitblaster for BitVec.umod
. The implemented
circuit is a shift subtractor.
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Std.Sat.AIG α)
(input : aig.BinaryRefVec w)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUmod
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len : Nat} =>
Std.Tactic.BVDecide.BVExpr.bitblast.blastUmod
Equations
- ⋯ = ⋯