class
Std.Sat.AIG.LawfulVecOperator
(α : Type)
[Hashable α]
[DecidableEq α]
(β : AIG α → Nat → Type)
(f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len)
:
Instances
- Std.Sat.AIG.RefVec.instLawfulVecOperatorIfInputIte
- Std.Sat.AIG.RefVec.instLawfulVecOperatorMapTargetMap
- Std.Sat.AIG.RefVec.instLawfulVecOperatorZipTargetZip
- Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.instLawfulVecOperatorBinaryRefVecBlast
- Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift
- Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.instLawfulVecOperatorBinaryRefVecBlast
- Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift
- Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift
- Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.instLawfulVecOperatorShiftConcatInputBlastShiftConcat
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorAppendTargetBlastAppend
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastArithShiftRight
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastShiftLeft
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorArbitraryShiftTargetBlastShiftRight
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBVBitBVVarBlastVar
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastAdd
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastMul
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastSub
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUdiv
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBinaryRefVecBlastUmod
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorBitVecBlastConst
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtendTargetBlastZeroExtend
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtractTargetBlastExtract
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastNeg
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorRefVecBlastNot
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorReplicateTargetBlastReplicate
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastArithShiftRightConst
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateLeft
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastRotateRight
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastShiftLeftConst
- Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorShiftTargetBlastShiftRightConst
theorem
Std.Sat.AIG.LawfulVecOperator.isPrefix_aig
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
(aig : AIG α)
(input : β aig len)
:
theorem
Std.Sat.AIG.LawfulVecOperator.lt_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
(entry : Entrypoint α)
(input : β entry.aig len)
:
theorem
Std.Sat.AIG.LawfulVecOperator.lt_size_of_lt_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len x : Nat}
(aig : AIG α)
(input : β aig len)
(h : x < aig.decls.size)
:
theorem
Std.Sat.AIG.LawfulVecOperator.le_size_of_le_aig_size
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len x : Nat}
(aig : AIG α)
(input : β aig len)
(h : x ≤ aig.decls.size)
:
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_input_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
(entry : Entrypoint α)
{input : β entry.aig len}
{h : entry.ref.gate < (f entry.aig input).aig.decls.size}
:
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_cast_entry
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
(entry : Entrypoint α)
{input : β entry.aig len}
{h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size}
:
theorem
Std.Sat.AIG.LawfulVecOperator.denote_mem_prefix
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
{start : Nat}
{inv : Bool}
{aig : AIG α}
{input : β aig len}
(h : start < aig.decls.size)
:
@[simp]
theorem
Std.Sat.AIG.LawfulVecOperator.denote_input_vec
{α : Type}
[Hashable α]
[DecidableEq α]
{β : AIG α → Nat → Type}
{f : {len : Nat} → (aig : AIG α) → β aig len → RefVecEntry α len}
[LawfulVecOperator α β fun {len : Nat} => f]
{len : Nat}
{assign : α → Bool}
{idx : Nat}
{hidx : idx < len}
(s : RefVecEntry α len)
{input : β s.aig len}
{hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size}
: