名单内置符号Z3

Question

我使用Z3的SMT2-lib的接口，并试图定义如下：

(declare-const rem (set sl$REQ)) 

而得到这个错误：

(error "line 36 column 31: invalid declaration, builtin symbol rem") 

有一种获取所有预定义符号的完整列表的方法，以便我可以进行自动重命名？

谢谢！ Simon

Answer 1

是的，但它不是那么简单。根据选项和逻辑定义，预定义符号列表可能会改变。但是，您可以通过在src/ast/*_decl_plugin.cpp中输入builtin_name来获取所有可能预定义的符号的列表。例如，rem符号定义为arith_decl_plugin.cpp:540。