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 : Std.Sat.AIG α)
(target : aig.ShiftTarget w)
:
Equations
- One or more equations did not get rendered due to their size.
@[irreducible]
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight.go
{α : Type}
[Hashable α]
[DecidableEq α]
{w : Nat}
{aig : Std.Sat.AIG α}
(input : aig.RefVec w)
(distance : Nat)
(curr : Nat)
(hcurr : curr ≤ w)
(s : aig.RefVec curr)
:
aig.RefVec w
Equations
- One or more equations did not get rendered due to their size.
instance
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ShiftTarget fun {len : Nat} =>
Std.Tactic.BVDecide.BVExpr.bitblast.blastRotateRight
Equations
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight = { le_size := ⋯, decl_eq := ⋯ }