This module contains the implementation of a bitblaster for BitVec.rotateRight
. Note that only
rotating with a known rotation distance is supported because rotateRight
takes a Nat
as distance.
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
(aig : Sat.AIG α)
(target : aig.ShiftTarget w)
:
Equations
Instances For
instance
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight
{α : Type}
[Hashable α]
[DecidableEq α]
:
Sat.AIG.LawfulVecOperator α Sat.AIG.ShiftTarget fun {len : Nat} => blastRotateRight