Z3证明:相当于c++ API中的Python数据类型

Question

是否有一个等效于c++的Python Datatype() API ?

例如在Python中你可以这样做:

>>> 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

如何使用c++ API声明这样的代数数据类型?

Answer 1

是。一般来说，您可以通过Python API(和其他API)完成的所有操作，都可以通过C/c++完成。我们要找的函数叫做Z3_mk_datatype。看到:

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

详情。

请注意，C/c++ api的级别要低得多，因此，尽管可能这样做，但我强烈建议不要使用这些api，除非您有强制使用C/c++的需求。