This module contains the implementation of a bitblaster for BitVec.signExtend.
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend
{α : Type}
[Hashable α]
[DecidableEq α]
{newWidth : Nat}
(aig : Std.Sat.AIG α)
(target : aig.ExtendTarget newWidth)
:
Std.Sat.AIG.RefVecEntry α newWidth
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[irreducible]
def
Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend.go
{α : Type}
[Hashable α]
[DecidableEq α]
{aig : Std.Sat.AIG α}
(w : Nat)
(hw : 0 < w)
(input : aig.RefVec w)
(newWidth : Nat)
(curr : Nat)
(hcurr : curr ≤ newWidth)
(s : aig.RefVec curr)
:
aig.RefVec newWidth
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtendTargetBlastSignExtend
{α : Type}
[Hashable α]
[DecidableEq α]
:
Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.ExtendTarget fun {len : Nat} =>
Std.Tactic.BVDecide.BVExpr.bitblast.blastSignExtend
Equations
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtendTargetBlastSignExtend = { le_size := ⋯, decl_eq := ⋯ }