java - Z3:解析SMTLIB2文件/字符串

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

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

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