'Z3 Prover: Equivalent to Python Datatype in the C++ API
Is there an equivalent to the Python Datatype() API for C++?
For example in Python you can do:
>>> List = Datatype('List')
>>> List.declare('cons', ('car', IntSort()), ('cdr', List))
>>> List.declare('nil')
>>> List = List.create()
>>> # List is now a Z3 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
How to declare such algebraic datatypes using the C++ API?
Sources
This article follows the attribution requirements of Stack Overflow and is licensed under CC BY-SA 3.0.
Source: Stack Overflow
| Solution | Source |
|---|
