class Std.Sat.AIG.LawfulVecOperator (α : Type) [Hashable α] [DecidableEq α] (β : Std.Sat.AIG α → Nat → Type) (f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len) : Prop

• le_size {len : Nat} (aig : Std.Sat.AIG α) (input : β aig len) : aig.decls.size ≤ (f aig input).aig.decls.size
• decl_eq {len : Nat} (aig : Std.Sat.AIG α) (input : β aig len) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (f aig input).aig.decls.size) : (f aig input).aig.decls[idx] = aig.decls[idx]

Instances

• Std.Sat.AIG.RefVec.instLawfulVecOperatorIfInputIte
• Std.Sat.AIG.RefVec.instLawfulVecOperatorMapTargetMap
• Std.Sat.AIG.RefVec.instLawfulVecOperatorZipTargetZip
• Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.instLawfulVecOperatorBinaryRefVec
• Std.Tactic.BVDecide.BVExpr.bitblast.blastArithShiftRight.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift
• Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.instLawfulVecOperatorBVBitBinaryRefVecBlast
• 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.instLawfulVecOperatorBVBitBinaryRefVecBlastMul
• 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.instLawfulVecOperatorExtendTargetBlastSignExtend
• 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
• Std.Tactic.BVDecide.BVExpr.instLawfulVecOperatorBVBitBitblast

theorem Std.Sat.AIG.LawfulVecOperator.isPrefix_aig {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len : Nat} (aig : Std.Sat.AIG α) (input : β aig len) : Std.Sat.AIG.IsPrefix aig.decls (f aig input).aig.decls

theorem Std.Sat.AIG.LawfulVecOperator.lt_size {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len : Nat} (entry : Std.Sat.AIG.Entrypoint α) (input : β entry.aig len) : entry.ref.gate < (f entry.aig input).aig.decls.size

theorem Std.Sat.AIG.LawfulVecOperator.lt_size_of_lt_aig_size {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len x : Nat} (aig : Std.Sat.AIG α) (input : β aig len) (h : x < aig.decls.size) : x < (f aig input).aig.decls.size

theorem Std.Sat.AIG.LawfulVecOperator.le_size_of_le_aig_size {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len x : Nat} (aig : Std.Sat.AIG α) (input : β aig len) (h : x ≤ aig.decls.size) : x ≤ (f aig input).aig.decls.size

@[simp]

theorem Std.Sat.AIG.LawfulVecOperator.denote_input_entry {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len : Nat} {assign : α → Bool} (entry : Std.Sat.AIG.Entrypoint α) {input : β entry.aig len} {h : entry.ref.gate < (f entry.aig input).aig.decls.size} : ⟦assign, { aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }⟧ = ⟦assign, entry⟧

@[simp]

theorem Std.Sat.AIG.LawfulVecOperator.denote_cast_entry {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len : Nat} {assign : α → Bool} (entry : Std.Sat.AIG.Entrypoint α) {input : β entry.aig len} {h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size} : ⟦assign, { aig := (f entry.aig input).aig, ref := entry.ref.cast h }⟧ = ⟦assign, entry⟧

theorem Std.Sat.AIG.LawfulVecOperator.denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len : Nat} {assign : α → Bool} {start : Nat} {aig : Std.Sat.AIG α} {input : β aig len} (h : start < aig.decls.size) : ⟦assign, { aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }⟧ = ⟦assign, { aig := aig, ref := { gate := start, hgate := h } }⟧

@[simp]

theorem Std.Sat.AIG.LawfulVecOperator.denote_input_vec {α : Type} [Hashable α] [DecidableEq α] {β : Std.Sat.AIG α → Nat → Type} {f : {len : Nat} → (aig : Std.Sat.AIG α) → β aig len → Std.Sat.AIG.RefVecEntry α len} [Std.Sat.AIG.LawfulVecOperator α β fun {len : Nat} => f] {len : Nat} {assign : α → Bool} {idx : Nat} {hidx : idx < len} (s : Std.Sat.AIG.RefVecEntry α len) {input : β s.aig len} {hcast : s.aig.decls.size ≤ (f s.aig input).aig.decls.size} : ⟦assign, { aig := (f s.aig input).aig, ref := (s.vec.get idx hidx).cast hcast }⟧ = ⟦assign, { aig := s.aig, ref := s.vec.get idx hidx }⟧