Z3：解析SMTLIB2文件/字符串答案

【问题标题】：Z3: ParseSMTLIB2File/StringZ3：解析SMTLIB2文件/字符串
【发布时间】：2016-01-27 18:34:43
【问题描述】：

我使用 ParseSMTLIB2File 来解析一个 smt2 文件 Context.smt2，它具有数据类型、常量和函数的声明；例如

    ; Sort Declarations
    (declare-sort tla_sort_Str)
    (declare-const x tla_sort_Str)
    (declare-const y tla_sort_Str)
    (declare-const z tla_sort_Str)

然后，我使用 ParseSMTLIB2String 解析字符串“(assert (= x y))”。以下是我的代码：

     BoolExpr expr = ctx.parseSMTLIB2File("Context.smt2", null, null, null, null);
     String str = "(assert (= x y))";
     BoolExpr assert = ctx.parseSMTLIB2String(str, null, null, null, null);

很遗憾，我收到了一个错误。我猜原因是 ctx 不知道 tla_sort_Str, x 和 y 是什么。如果不是，我如何将 Context.smt2 中的信息传递给 parseSMTLIB2String？非常感谢。

【问题讨论】：

标签： java api z3

【解决方案1】：

这就是所有“空”参数的用途（其中之一是提供之前构建的排序）。

然而 parseSMTLIB2File 并不不支持 SMT2 的所有功能或任何扩展。它基本上会读取断言并忽略其他所有内容，可能包括排序声明。 SMT2 是一种交互语言，但是在 parseSMTLIB2File 范围内没有交互，因此不会执行任何命令，例如，最重要的例子是 (check-sat) 命令，它没有被执行。

【讨论】：

谢谢你，克里斯托夫。我之前应该声明新的排序和变量，然后将它们传递给 parseSMTLIB2String()。