z3 - 用户理论插件的前端？

Question

是否可以使用 smt-lib 或类似的 C/C++ API 来解析用户理论插件的输入？例如，在示例用户理论“test_user_theory.c”中，如何在输入文件中声明一个字符串变量和一个常量字符串（不将其分解为位向量）？提前致谢。

Answer 1

函数z3_parse_smtlib_string, z3_parse_smtlib_file,允许用户将任意符号与给定的排序和声明绑定z3_parse_smtlib2_string。z3_parse_smtlib2_file因此，您可以将有限数量的符号与您的理论插件中定义的声明连接起来。这不是一个完美的解决方案，因为一些理论定义了任意数量的函数/常量声明和排序。例如，算术理论定义了符号：0、1、2等。数组理论定义了“无限”数量的排序。

请注意，理论插件 API 现在已过时。Z3 源代码现已可用，Z3 定理证明器的扩展可以直接在实际代码库中实现。Z3 源代码可在http://z3.codeplex.com获得。我计划在未来的版本中删除理论插件 API。