Generated Bag constructors, sort-erased

def Cvc.Untyped.Term.bagInterMinN [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

bagInterMin over two or more terms.

Equations

• Cvc.Untyped.Term.bagInterMinN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_INTER_MIN terms

def Cvc.Untyped.Term.bagSubbag [Ω] (lft rgt : Term) : Env Term

Whether every multiplicity in lft is at most the one in rgt.

Equations

• lft.bagSubbag rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_SUBBAG #[lft, rgt]

def Cvc.Untyped.Term.bagEmpty [Ω] (α : Srt) : Env Term

The empty bag of elements of sort α.

Equations

• Cvc.Untyped.Term.bagEmpty α = do let builtSrt ← pure α >>= Cvc.Srt.bag Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkEmptyBag builtSrt

def Cvc.Untyped.Term.bagDifferenceSubtract [Ω] (lft rgt : Term) : Env Term

Difference subtracting the multiplicities.

Equations

• lft.bagDifferenceSubtract rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_DIFFERENCE_SUBTRACT #[lft, rgt]

def Cvc.Untyped.Term.bagSetof [Ω] (b : Term) : Env Term

Duplicate removal, yielding a bag whose multiplicities are all at most one.

Equations

• b.bagSetof = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_SETOF #[b]

def Cvc.Untyped.Term.bagUnionMaxN [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

bagUnionMax over two or more terms.

Equations

• Cvc.Untyped.Term.bagUnionMaxN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_UNION_MAX terms

def Cvc.Untyped.Term.bagMember [Ω] (elm b : Term) : Env Term

Whether elm is in b; the element comes first, as in cvc5.

Equations

• elm.bagMember b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_MEMBER #[elm, b]

def Cvc.Untyped.Term.bagUnionDisjoint [Ω] (lft rgt : Term) : Env Term

Union adding the multiplicities.

Equations

• lft.bagUnionDisjoint rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_UNION_DISJOINT #[lft, rgt]

def Cvc.Untyped.Term.bagFilter [Ω] (p b : Term) : Env Term

The elements of a bag satisfying a predicate, with their multiplicities.

Equations

• p.bagFilter b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_FILTER #[p, b]

def Cvc.Untyped.Term.bagCard [Ω] (b : Term) : Env Term

Cardinality, counting multiplicities.

Equations

• b.bagCard = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_CARD #[b]

def Cvc.Untyped.Term.bagChoose [Ω] (b : Term) : Env Term

An unspecified element of a non-empty bag.

Equations

• b.bagChoose = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_CHOOSE #[b]

def Cvc.Untyped.Term.bagUnionMax [Ω] (lft rgt : Term) : Env Term

Union taking the maximum of the multiplicities.

Equations

• lft.bagUnionMax rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_UNION_MAX #[lft, rgt]

def Cvc.Untyped.Term.bagMake [Ω] (elm count : Term) : Env Term

The bag holding elm count times; the element comes first, as in cvc5.

Equations

• elm.bagMake count = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_MAKE #[elm, count]

def Cvc.Untyped.Term.bagInterMin [Ω] (lft rgt : Term) : Env Term

Intersection taking the minimum of the multiplicities.

Equations

• lft.bagInterMin rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_INTER_MIN #[lft, rgt]

def Cvc.Untyped.Term.bagSome [Ω] (p b : Term) : Env Term

Whether some element of a bag satisfies a predicate.

Equations

• p.bagSome b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_SOME #[p, b]

def Cvc.Untyped.Term.bagUnionDisjointN [Ω] (terms : Terms) (atLeastTwoElements : 2 ≤ Array.size terms := by (try grind) <;> fail "failed to prove term array has at least two elements") : Env Term

bagUnionDisjoint over two or more terms.

Equations

• Cvc.Untyped.Term.bagUnionDisjointN terms atLeastTwoElements = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_UNION_DISJOINT terms

def Cvc.Untyped.Term.smtOp.binary.bagUnionDisjoint : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Cvc.Untyped.Term.bagFold [Ω] (f init b : Term) : Env Term

Folds f over the elements of b from init, in no specified order.

Equations

• f.bagFold init b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_FOLD #[f, init, b]

def Cvc.Untyped.Term.bagAll [Ω] (p b : Term) : Env Term

Whether every element of a bag satisfies a predicate.

Equations

• p.bagAll b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_ALL #[p, b]

def Cvc.Untyped.Term.bagMap [Ω] (f b : Term) : Env Term

The image of a bag under a function.

Equations

• f.bagMap b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_MAP #[f, b]

def Cvc.Untyped.Term.bagPartition [Ω] (p b : Term) : Env Term

Partitions a bag into the equivalence classes of a binary predicate.

The predicate is expected to be an equivalence relation; the result holds one bag per class.

Equations

• p.bagPartition b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_PARTITION #[p, b]

def Cvc.Untyped.Term.bagDifferenceRemove [Ω] (lft rgt : Term) : Env Term

Difference removing every element occurring on the right.

Equations

• lft.bagDifferenceRemove rgt = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_DIFFERENCE_REMOVE #[lft, rgt]

def Cvc.Untyped.Term.bagCount [Ω] (elm b : Term) : Env Term

Multiplicity of elm in b; the element comes first, as in cvc5.

Equations

• elm.bagCount b = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.BAG_COUNT #[elm, b]

def Cvc.Untyped.Term.smtOp.nary.bagUnionDisjoint : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

inductive Cvc.Untyped.View.Bag [Ω] : Type

Bag's operators, taken apart one level, sort-erased.

• bagMember [Ω] (elm b : Term) : View.Bag

  Whether elm is in b; the element comes first, as in cvc5.

• bagSubbag [Ω] (lft rgt : Term) : View.Bag

  Whether every multiplicity in lft is at most the one in rgt.

• bagMake [Ω] (elm count : Term) : View.Bag

  The bag holding elm count times; the element comes first, as in cvc5.

• bagCount [Ω] (elm b : Term) : View.Bag

  Multiplicity of elm in b; the element comes first, as in cvc5.

• bagCard [Ω] (b : Term) : View.Bag

  Cardinality, counting multiplicities.

• bagSetof [Ω] (b : Term) : View.Bag

  Duplicate removal, yielding a bag whose multiplicities are all at most one.

• bagChoose [Ω] (b : Term) : View.Bag

  An unspecified element of a non-empty bag.

• bagUnionMax [Ω] (kids : Kids) : View.Bag

  Union taking the maximum of the multiplicities.

  kids holds every operand, two or more.

• bagUnionDisjoint [Ω] (kids : Kids) : View.Bag

  Union adding the multiplicities.

  kids holds every operand, two or more.

• bagInterMin [Ω] (kids : Kids) : View.Bag

  Intersection taking the minimum of the multiplicities.

  kids holds every operand, two or more.

• bagDifferenceSubtract [Ω] (lft rgt : Term) : View.Bag

  Difference subtracting the multiplicities.

• bagDifferenceRemove [Ω] (lft rgt : Term) : View.Bag

  Difference removing every element occurring on the right.

• bagMap [Ω] (f b : Term) : View.Bag

  The image of a bag under a function.

• bagFilter [Ω] (p b : Term) : View.Bag

  The elements of a bag satisfying a predicate, with their multiplicities.

• bagFold [Ω] (f init b : Term) : View.Bag

  Folds f over the elements of b from init, in no specified order.

• bagAll [Ω] (p b : Term) : View.Bag

  Whether every element of a bag satisfies a predicate.

• bagSome [Ω] (p b : Term) : View.Bag

  Whether some element of a bag satisfies a predicate.

• bagPartition [Ω] (p b : Term) : View.Bag

  Partitions a bag into the equivalence classes of a binary predicate.

  The predicate is expected to be an equivalence relation; the result holds one bag per class.

• bagEmpty [Ω] : View.Bag

  The empty bag of elements of sort α.

def Cvc.Untyped.View.Bag.of? [Ω] (viewed : Term) : Option View.Bag

Takes a term apart one level, if Bag owns its operator.

Equations

• One or more equations did not get rendered due to their size.

Values

A Cvc.Bag denotes an SMT bag: the empty bag, unioned with one singleton bag per element, each carrying that element's multiplicity.

def Cvc.Untyped.Term.mkBagValue {α : Type} [Ω] [Ord α] [ToTyp α] [ValueToTerm α] (bag : Bag α) : Env Term

The bag term denoting a bag of values.

Equations

• One or more equations did not get rendered due to their size.

partial def Cvc.Untyped.Term.getBagValue {α : Type} [Ω] [Ord α] [TermToValue α] (term : Term) : Env (Bag α)

The bag of values a constant bag term denotes.

Works on a bag built from bagEmpty, bagMake and unions as well as on a model's answer; an intersection or a difference is refused.

@[instance_reducible]

instance Cvc.Untyped.Term.instValueToTermBag {α : Type} [Ord α] [ToTyp α] [ValueToTerm α] : ValueToTerm (Bag α)

Equations

• Cvc.Untyped.Term.instValueToTermBag = { valueToTerm := fun [Cvc.Ω] => Cvc.Untyped.Term.mkBagValue }

@[instance_reducible]

instance Cvc.Untyped.Term.instTermToValueBag {α : Type} [Ord α] [TermToValue α] : TermToValue (Bag α)

Equations

• Cvc.Untyped.Term.instTermToValueBag = { termToValue := fun [Cvc.Ω] => Cvc.Untyped.Term.getBagValue }