Z3Opt C++ API: 从文件解析 smtlib2 公式

Question

Z3Opt C++ API 有什么方法可以解析 smtlib2 文件吗？所以，基本上我想做的是将 Z3Opt 公式转储到文件中，然后在其他程序中读取它。我发现解析 smtlib2 文件的唯一函数是 Z3_parse_smtlib2_file。但它不支持 extended smtlib2 格式（使用 maximize, minimize 和 assert-soft 操作），它们在 z3opt tutorial 中进行了描述。但是，z3 控制台版本接受该格式并且没有失败。这意味着有一些方法可以做我需要的。所以，有谁能帮助我吗？

这里有一些例子来解释我在说什么：

#include <iostream>
#include <fstream>
#include <z3/z3++.h>

void dumpFormula() {
    z3::context ctx;
    auto&& opt = z3::optimize(ctx);

    auto&& x = ctx.int_const("x");
    auto&& y = ctx.int_const("y");

    opt.add(x < 2);
    opt.add((y - x) < 1);
    opt.maximize(x + y);

    std::ofstream out("output.smt2");
    out << opt << std::endl;
    return;
}

void readDumpedFormula() {
    z3::context ctx;
    auto&& opt = z3::optimize(ctx);
    z3::set_param("timeout", 1000);


    Z3_ast a = Z3_parse_smtlib2_file(ctx, "output.smt2", 0, 0, 0, 0, 0, 0);
    z3::expr e(ctx, a);
    opt.add(e);

    auto&& res = opt.check();
    switch (res) {
        case z3::sat: std::cout << "Sat" << std::endl;break;
        case z3::unsat: std::cout << "Unsat" << std::endl;break;
        case z3::unknown: std::cout << "Unknown" << std::endl;break;
    }
    return;
}

int main() {
    dumpFormula();
    readDumpedFormula();
    return 0;
}

函数dumpFormula() 创建一个z3opt 公式并将其转储到文件中。这是 'output.smt2' 文件：

(declare-fun x () Int)
(declare-fun y () Int)
(assert (< x 2))
(assert (< (- y x) 1))
(maximize (+ x y))
(check-sat)

函数readDumpedFormula() 尝试解析该文件并检查该公式。但我得到的只是错误。这是程序的输出：

unsupported

; maximize line: 5 position: 17

Sat

Answer 1

这是一个有点反复出现的问题。通过 API 公开的解析器只允许您加载公式。它使用插件模型让解析器知道注册了哪些命令。在 API 公开的版本中，提供的命令不包括优化命令。

看来您真的是在要求采用优化对象的功能（对称地，求解器对象）并使用字符串或文件中的断言和目标填充它。

您可以近似文件加载，分别声明特殊谓词最大化、最小化、软断言。然后用这些作为断言解析文件。然后post-处理解析的断言并将它们提供给优化对象。

Z3Opt C++ API: 从文件解析 smtlib2 公式

Z3Opt C++ API: parse smtlib2 formula from file

c++

smt

z3