Sets 

Basic Set Term Builders 

cvc5.pythonic. SetSort ( s ) : Create a set sort over element sort s

cvc5.pythonic. Set ( name , elem_sort ) : Creates a symbolic set of elements

cvc5.pythonic. EmptySet ( s ) 

Create the empty set

              >>> EmptySet(IntSort())
Empty(Set(Int))

cvc5.pythonic. Singleton ( s ) 

The single element set of just e

              >>> Singleton(IntVal(1))
Singleton(1)

cvc5.pythonic. FullSet ( s ) 

Create the full set

              >>> FullSet(IntSort())
Full(Set(Int))

Set Operators 

cvc5.pythonic. SetUnion ( * args ) 

Take the union of sets

              >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetUnion(a, b)
SetUnion(a, b)

             

cvc5.pythonic. SetIntersect ( * args ) 

Take the intersection of sets

              >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetIntersect(a, b)
SetIntersect(a, b)

             

cvc5.pythonic. SetAdd ( s , e ) 

Add element e to set s

              >>> a = Const('a', SetSort(IntSort()))
>>> SetAdd(a, 1)
SetAdd(a, 1)
>>> SetAdd(a, 1).arg(0)
a

             

cvc5.pythonic. SetDel ( s , e ) 

Remove element e to set s

              >>> a = Const('a', SetSort(IntSort()))
>>> SetDel(a, 1)
SetDifference(a, Singleton(1))

             

cvc5.pythonic. SetComplement ( s ) 

The complement of set s

              >>> a = Const('a', SetSort(IntSort()))
>>> SetComplement(a)
SetComplement(a)

             

cvc5.pythonic. SetDifference ( a , b ) 

The set difference of a and b

              >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetDifference(a, b)
SetDifference(a, b)

             

cvc5.pythonic. SetMinus ( a , b ) 

The set difference of a and b

              >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> SetMinus(a, b)
SetDifference(a, b)

             

cvc5.pythonic. IsMember ( e , s ) 

Check if e is a member of set s

              >>> a = Const('a', SetSort(IntSort()))
>>> IsMember(1, a)
IsMember(1, a)

             

cvc5.pythonic. IsSubset ( a , b ) 

Check if a is a subset of b

              >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> IsSubset(a, b)
IsSubset(a, b)

             

See the following operator overload for set terms:

is member: cvc5.pythonic.SetRef.__getitem__()

Classes (with overloads) 

class cvc5.pythonic. SetSortRef ( ast , ctx = None ) 

Array sorts.

domain ( ) 

Return the domain of the set sort self .

                >>> A = SetSort(IntSort())
>>> A.domain()
Int

               

range ( ) 

Return the “range” of the set sort self . Included for compatibility with arrays.

                >>> A = SetSort(IntSort())
>>> A.range()
Bool

               

class cvc5.pythonic. SetRef ( ast , ctx = None , reverse_children = False ) 

Array expressions.

__and__ ( other ) 

Intersection

                >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> a & b
SetIntersect(a, b)

               

__getitem__ ( arg ) 

Return the SMT expression self[arg] . Included for compatibility with arrays.

                >>> a = Set('a', IntSort())
>>> i = Int('i')
>>> a[i]
IsMember(i, a)

               

__or__ ( other ) 

Union

                >>> a = Const('a', SetSort(IntSort()))
>>> b = Const('b', SetSort(IntSort()))
>>> a | b
SetUnion(a, b)

               

default ( ) 

Always returns false.

Included for compatibility with Arrays.

                >>> Set('a', IntSort()).default()
False

domain ( ) 

Shorthand for self.sort().domain() .

                >>> a = Set('a', IntSort())
>>> a.domain()
Int

               

range ( ) 

Shorthand for self.sort().range() . Included for compatibility with arrays.

                >>> a = Set('a', IntSort())
>>> a.range()
Bool

               

sort ( ) 

Return the set sort of the set expression self .

                >>> a = Set('a', IntSort())
>>> a.sort()
Set(Int)

               