Generated Set constructors, sort-erased

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

setUnion over two or more terms.

Equations

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

def Cvc.Untyped.Term.setInsert [Ω] (elm s : Term) : Env Term

Inserts elm into s; the element comes first, as in cvc5.

Equations

• elm.setInsert s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_INSERT #[elm, s]

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

The empty set of elements of sort α.

Equations

• Cvc.Untyped.Term.setEmpty α = do let builtSrt ← pure α >>= Cvc.Srt.set Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkEmptySet builtSrt

def Cvc.Untyped.Term.setMember [Ω] (elm s : Term) : Env Term

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

Equations

• elm.setMember s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_MEMBER #[elm, s]

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

Set intersection.

Equations

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

def Cvc.Untyped.Term.setMap [Ω] (f s : Term) : Env Term

The image of a set under a function.

Equations

• f.setMap s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_MAP #[f, s]

def Cvc.Untyped.Term.setAll [Ω] (p s : Term) : Env Term

Whether every element of a set satisfies a predicate.

Equations

• p.setAll s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_ALL #[p, s]

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

The set of every element of sort α.

Equations

• Cvc.Untyped.Term.setUniverse α = do let builtSrt ← pure α >>= Cvc.Srt.set Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkUniverseSet builtSrt

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

The singleton set containing one element.

Equations

• elm.setSingleton = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_SINGLETON #[elm]

def Cvc.Untyped.Term.setFilter [Ω] (p s : Term) : Env Term

The elements of a set satisfying a predicate.

Equations

• p.setFilter s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_FILTER #[p, s]

def Cvc.Untyped.Term.setFold [Ω] (f init s : Term) : Env Term

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

Equations

• f.setFold init s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_FOLD #[f, init, s]

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

Equations

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

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

Equations

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

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

Equations

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

def Cvc.Untyped.Term.setIsEmpty [Ω] (s : Term) : Env Term

Whether s is empty.

Equations

• s.setIsEmpty = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_IS_EMPTY #[s]

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

Whether lft is a subset of rgt.

Equations

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

def Cvc.Untyped.Term.setChoose [Ω] (s : Term) : Env Term

An unspecified element of a non-empty set.

Equations

• s.setChoose = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_CHOOSE #[s]

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

Set difference.

Equations

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

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

Set union.

Equations

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

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

Equations

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

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

setMinus over two or more terms.

Equations

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

def Cvc.Untyped.Term.setComplement [Ω] (s : Term) : Env Term

Set complement, relative to the universe set of the element sort.

Equations

• s.setComplement = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_COMPLEMENT #[s]

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

setInter over two or more terms.

Equations

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

def Cvc.Untyped.Term.setIsSingleton [Ω] (s : Term) : Env Term

Whether s has exactly one element.

Equations

• s.setIsSingleton = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_IS_SINGLETON #[s]

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

Equations

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

def Cvc.Untyped.Term.setSome [Ω] (p s : Term) : Env Term

Whether some element of a set satisfies a predicate.

Equations

• p.setSome s = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_SOME #[p, s]

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

Equations

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

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

Equations

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

def Cvc.Untyped.Term.setCard [Ω] (s : Term) : Env Term

Cardinality.

Equations

• s.setCard = Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_CARD #[s]

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

Equations

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

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

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

• setMember [Ω] (elm s : Term) : View.Set

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

• setSubset [Ω] (lft rgt : Term) : View.Set

  Whether lft is a subset of rgt.

• setIsEmpty [Ω] (s : Term) : View.Set

  Whether s is empty.

• setIsSingleton [Ω] (s : Term) : View.Set

  Whether s has exactly one element.

• setSingleton [Ω] (elm : Term) : View.Set

  The singleton set containing one element.

• setInsert [Ω] (elm s : Term) : View.Set

  Inserts elm into s; the element comes first, as in cvc5.

• setUnion [Ω] (kids : Kids) : View.Set

  Set union.

  kids holds every operand, two or more.

• setInter [Ω] (kids : Kids) : View.Set

  Set intersection.

  kids holds every operand, two or more.

• setMinus [Ω] (kids : Kids) : View.Set

  Set difference.

  kids holds every operand, two or more.

• setComplement [Ω] (s : Term) : View.Set

  Set complement, relative to the universe set of the element sort.

• setCard [Ω] (s : Term) : View.Set

  Cardinality.

• setChoose [Ω] (s : Term) : View.Set

  An unspecified element of a non-empty set.

• setMap [Ω] (f s : Term) : View.Set

  The image of a set under a function.

• setFilter [Ω] (p s : Term) : View.Set

  The elements of a set satisfying a predicate.

• setFold [Ω] (f init s : Term) : View.Set

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

• setAll [Ω] (p s : Term) : View.Set

  Whether every element of a set satisfies a predicate.

• setSome [Ω] (p s : Term) : View.Set

  Whether some element of a set satisfies a predicate.

• setEmpty [Ω] : View.Set

  The empty set of elements of sort α.

• setUniverse [Ω] : View.Set

  The set of every element of sort α.

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

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

Equations

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

Values

A Cvc.Set denotes an SMT set: the empty set, with each element inserted.

def Cvc.Untyped.Term.isSetValue [Ω] (term : Term) : Bool

Whether a term is a set value: a canonical union of singletons of values, as a model answers.

A set built from constructors is generally not one, and the universe set never is.

Equations

• term.isSetValue = (Cvc.Untyped.Term.toUnsafe✝ term).isSetValue

def Cvc.Untyped.Term.getSetElems [Ω] (term : Term) : Env Terms

The elements a constant set term denotes.

Equations

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

def Cvc.Untyped.Term.mkSetValue {α : Type} [Ω] [Ord α] [ToTyp α] [ValueToTerm α] (set : Set α) : Env Term

The set term denoting a set of values.

Equations

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

def Cvc.Untyped.Term.getSetValue {α : Type} [Ω] [Ord α] [TermToValue α] (term : Term) : Env (Set α)

The set of values a constant set term denotes.

Equations

• term.getSetValue = do let elems ← term.getSetElems Array.foldlM (fun (set : Cvc.Set α) (elem : Cvc.Untyped.Term) => Std.TreeSet.insert set <$> elem.extractValue) Cvc.Set.empty elems

@[instance_reducible]

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

Equations

• Cvc.Untyped.Term.instValueToTermSet = { valueToTerm := fun [Cvc.Ω] => Cvc.Untyped.Term.mkSetValue }

@[instance_reducible]

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

Equations

• Cvc.Untyped.Term.instTermToValueSet = { termToValue := fun [Cvc.Ω] => Cvc.Untyped.Term.getSetValue }

Comprehension

{ elem | bvs. pred }, a set built by binding variables. cvc5 supports it only under sets-exp, and its reasoning about one is incomplete: even a membership in a finite comprehension can come back unknown.

def Cvc.Untyped.Term.setComprehension [Ω] (bvs : BVars) (pred elem : Term) (_nonEmpty : 0 < Array.size bvs := by (try grind) <;> fail "failed to prove a comprehension binds at least one variable") : Env Term

The set of the values elem takes, over the bindings of bvs that satisfy pred.

Equations

• Cvc.Untyped.Term.setComprehension bvs pred elem _nonEmpty = do let vars ← bvs.toTerm Cvc.runUnsafe✝ fun (tm : cvc5.TermManager) => tm.mkTerm cvc5.Kind.SET_COMPREHENSION #[vars, pred, elem]