1

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

4

1 回答 1

3

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

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

于 2012-10-03T17:43:18.867 回答