扎阿：ParseSMTLIB2File/String

Question

我使用 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？非常感谢。

Answer 1

这就是所有 'null' 参数的用途（其中之一是提供之前构建的类型）。

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

扎阿：ParseSMTLIB2File/String

Z3: ParseSMTLIB2File/String

java

api

z3