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)