Z3 Prover: Equivalent to Python Datatype in the C API-CodePudding

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?

CodePudding user response：

Yes. In general, everything you can do from the Python API (and other APIs), you can do from C/C . The function you're looking for is called Z3_mk_datatype. See:

https://z3prover.github.io/api/html/group__capi.html#ga34875df69093aca24de67ae71542b1b0

for details.

Note that the C/C APIs are much lower level, so while possible to do so, I'd strongly recommend against using these APIs unless you've a requirement that forces you to use C/C .