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