Datatypes ¶

Overview ¶

To manipulate instances of a datatype, one must first declare the datatype itself. Declaration happens in three phases. Let’s consider declaring a cons-list of integers.

First, we initialize the datatype with its name

            >>> IntList = Datatype('IntList')

           

Second, we declare constructors for the datatype, giving the constructor name and field names and sorts . Here is the empty list constructor:

            >>> IntList.declare('nil', ())

           

Here is the cons constructor:

            >>> IntList.declare('cons', ('val', IntSort()), ('tail', IntList))

           

Third, after all constructors are declared, we can create the datatype, finishing its declaration.

            >>> IntList = IntList.create()

           

Now, one has access to a number of tools for interacting with integer lists.

IntList.nil refers to the SMT term that is an empty list, and IntList.cons refers to the cons constructor.
IntList.is_nil and IntList.is_cons are testors (a.k.a., recognizers) for those constructors.
IntList.val and IntList.tail are selectors (a.k.a. accessors) for the cons constructor.

If constructor, accessor, or selector names are ambiguous (e.g., if different constructors have selectors of the same name), then see the methods on cvc5.pythonic.DatatypeSortRef to unambiguously access a specific function.

To create mutually recursive datatypes, see cvc5.pythonic.CreateDatatypes() .

To create a codataype (e.g., a possibly infinite stream of integers), pass the isCoDatatype=True argument to the cvc5.pythonic.Datatype constructor.

            >>> IntStream = Datatype('IntStream', isCoDatatype=True)

           

Declaration Utilities ¶

cvc5.pythonic. CreateDatatypes ( * ds ) ¶

Create mutually recursive SMT datatypes using 1 or more Datatype helper objects. In the following example we define a Tree-List using two mutually recursive datatypes.

              >>> TreeList = Datatype('TreeList')
>>> Tree     = Datatype('Tree')
>>> # Tree has two constructors: leaf and node
>>> Tree.declare('leaf', ('val', IntSort()))
>>> # a node contains a list of trees
>>> Tree.declare('node', ('children', TreeList))
>>> TreeList.declare('nil')
>>> TreeList.declare('cons', ('car', Tree), ('cdr', TreeList))
>>> Tree, TreeList = CreateDatatypes(Tree, TreeList)
>>> Tree.val(Tree.leaf(10))
val(leaf(10))
>>> simplify(Tree.val(Tree.leaf(10)))
10
>>> l1 = TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil))
>>> n1 = Tree.node(TreeList.cons(Tree.leaf(10), TreeList.cons(Tree.leaf(20), TreeList.nil)))
>>> n1
node(cons(leaf(10), cons(leaf(20), nil)))
>>> n2 = Tree.node(TreeList.cons(n1, TreeList.nil))
>>> simplify(n2 == n1)
False
>>> simplify(TreeList.car(Tree.children(n2)) == n1)
True

             

cvc5.pythonic. TupleSort ( name , sorts , ctx = None ) ¶

Create a named tuple sort base on a set of underlying sorts

Returns the tuple datatype, its constructor, and a list of accessors, in order.

              >>> pair, mk_pair, (first, second) = TupleSort("pair", [IntSort(), BoolSort()])
>>> b = Bool('b')
>>> i = Int('i')
>>> p = mk_pair(i, b)
>>> p
pair(i, b)
>>> solve([b != second(p)])
no solution

             

cvc5.pythonic. DisjointSum ( name , sorts , ctx = None ) ¶

Create a named tagged union sort base on a set of underlying sorts.

See this page <https://en.wikipedia.org/wiki/Tagged_union> for information about tagged unions.

Returns the created datatype and a tuple of (injector, extractor) pairs for the different variants.

              >>> sum, ((inject0, extract0), (inject1, extract1)) = DisjointSum("+", [IntSort(), BoolSort()])
>>> b = Bool('b')
>>> i, j = Ints('i j')
>>> solve([inject0(i) == inject1(b)])
no solution
>>> solve([inject0(i) == inject0(j), extract0(inject0(i)) == 5])
[i = 5, j = 5]

             

Classes ¶

class cvc5.pythonic. Datatype ( name , ctx = None , isCoDatatype = False ) ¶

Helper class for declaring datatypes.

              >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a declaration
>>> List.nil
nil
>>> List.cons(10, List.nil)
cons(10, nil)
>>> List.cons(10, List.nil).sort()
List
>>> cons = List.cons
>>> nil  = List.nil
>>> car  = List.car
>>> cdr  = List.cdr
>>> n = cons(1, cons(0, nil))
>>> n
cons(1, cons(0, nil))
>>> simplify(cdr(n))
cons(0, nil)
>>> simplify(car(n))
1

             

__init__ ( name , ctx = None , isCoDatatype = False ) ¶

__repr__ ( ) ¶: Return repr(self).

__weakref__ ¶: list of weak references to the object (if defined)

create ( ) ¶

Create an SMT datatype based on the constructors declared using the method declare() . The function CreateDatatypes() must be used to define mutually recursive datatypes.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.nil
nil
>>> List.cons(10, List.nil)
cons(10, nil)
>>> Stream = Datatype('Stream', isCoDatatype=True)
>>> Stream.declare('cons', ('car', IntSort()), ('cdr', Stream))
>>> Stream.declare('nil')
>>> Stream = Stream.create()
>>> a = Const('a', Stream)
>>> b = Const('b', Stream)
>>> s = Solver()
>>> s += a == Stream.cons(0, a)
>>> s.check()
sat
>>> s = Solver()
>>> s += a == Stream.cons(0, a)
>>> s += b == Stream.cons(0, b)
>>> s += a != b
>>> s.check()
unsat

               

declare ( name , * args ) ¶

Declare constructor named name with the given accessors args . Each accessor is a pair (name, sort) , where name is a string and sort an SMT sort or a reference to the datatypes being declared. In the following example List.declare(‘cons’, (‘car’, IntSort()), (‘cdr’, List)) declares the constructor named cons that builds a new List using an integer and a List. It also declares the accessors car and cdr . The accessor car extracts the integer of a cons cell, and cdr the list of a cons cell. After all constructors were declared, we use the method create() to create the actual datatype in SMT.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()

               

class cvc5.pythonic. DatatypeSortRef ( ast , ctx = None ) ¶

Datatype sorts.

__init__ ( ast , ctx = None ) ¶

accessor ( i , j ) ¶

In SMT, each constructor has 0 or more accessor. The number of accessors is equal to the arity of the constructor.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0)
cons
>>> num_accs = List.constructor(0).arity()
>>> num_accs
2
>>> List.accessor(0, 0)
car
>>> List.accessor(0, 1)
cdr
>>> List.constructor(1)
nil
>>> num_accs = List.constructor(1).arity()
>>> num_accs
0

               

constructor ( idx ) ¶

Return a constructor of the datatype self .

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a declaration
>>> List.num_constructors()
2
>>> List.constructor(0)
cons
>>> List.constructor(1)
nil

               

num_constructors ( ) ¶

Return the number of constructors in the given datatype.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a declaration
>>> List.num_constructors()
2

               

recognizer ( idx ) ¶

In SMT, each constructor has an associated recognizer predicate. If the constructor is named name , then the recognizer is_name .

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a SMT declaration
>>> List.num_constructors()
2
>>> List.recognizer(0)
is_cons
>>> List.recognizer(1)
is_nil
>>> simplify(List.is_nil(List.cons(10, List.nil)))
False
>>> simplify(List.is_cons(List.cons(10, List.nil)))
True
>>> l = Const('l', List)
>>> simplify(List.is_cons(l))
is_cons(l)

               

class cvc5.pythonic. DatatypeConstructorRef ( datatype , ctx = None , r = False ) ¶

__call__ ( * args ) ¶

Apply this constructor.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0)(1, List.nil)
cons(1, nil)

               

The arguments must be SMT expressions. This method assumes that the sorts of the elements in args match the sorts of the domain. Limited coercion is supported. For example, if args[0] is a Python integer, and the function expects a SMT integer, then the argument is automatically converted into a SMT integer.

__init__ ( datatype , ctx = None , r = False ) ¶

arity ( ) ¶

Return the number of arguments of a constructor.

The number of accessors is equal to the arity of the constructor.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0).arity()
2

               

domain ( i ) ¶

Return the sort of the argument i of a constructor. This method assumes that 0 <= i < self.arity() .

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0).domain(0)
Int

               

range ( ) ¶

Return the sort of the range of a function declaration. For constants, this is the sort of the constant.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> List.num_constructors()
2
>>> List.constructor(0).range()
List

               

class cvc5.pythonic. DatatypeSelectorRef ( datatype , ctx = None , r = False ) ¶

__call__ ( * args ) ¶

Apply this selector.

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> l = List.cons(1, List.nil)
>>> solve([1 != List.car(l)])
no solution

               

The arguments must be SMT expressions. This method assumes that the sorts of the elements in args match the sorts of the domain. Limited coercion is supported. For example, if args[0] is a Python integer, and the function expects a SMT integer, then the argument is automatically converted into a SMT integer.

__init__ ( datatype , ctx = None , r = False ) ¶

arity ( ) ¶: Return the number of arguments of a selector (always 1).

domain ( i ) ¶: Return the sort of the argument i of a selector. This method assumes that 0 <= i < self.arity() .

range ( ) ¶: Return the sort of the range of a function declaration. For constants, this is the sort of the constant.

class cvc5.pythonic. DatatypeRecognizerRef ( constructor , ctx = None , r = False ) ¶

__call__ ( * args ) ¶

Apply this tester (a.k.a., recognizer).

                >>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> l = List.cons(1, List.nil)
>>> solve([List.is_nil(l)])
no solution

               

The arguments must be SMT expressions. This method assumes that the sorts of the elements in args match the sorts of the domain. Limited coercion is supported. For example, if args[0] is a Python integer, and the function expects a SMT integer, then the argument is automatically converted into a SMT integer.

__init__ ( constructor , ctx = None , r = False ) ¶

arity ( ) ¶: Return the number of arguments of a selector (always 1).

domain ( i ) ¶: Return the sort of the argument i of a selector. This method assumes that 0 <= i < self.arity() .

range ( ) ¶: Return the sort of the range of a function declaration. For constants, this is the sort of the constant.

class cvc5.pythonic. DatatypeRef ( ast , ctx = None , reverse_children = False ) ¶

Datatype expressions.

sort ( ) ¶: Return the datatype sort of the datatype expression self .