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