z3 — API Z3Opt C ++: анализ формулы smtlib2 из файла

Есть ли способ в Z3Opt C ++ API для анализа файла smtlib2? Итак, в основном я пытаюсь сделать дамп формулы Z3Opt в файл и затем прочитать ее в другой программе. Единственная функция, которую я нашел для анализа файлов smtlib2, это Z3_parse_smtlib2_file, Но это не поддержка расширенный smtlib2 формат (с maximize, minimize а также assert-soft операции), которые они описывают в Учебник по z3opt. Однако консольная версия 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() пытается проанализировать этот файл и проверить эту формулу. Но все, что я получаю, это ошибки. Вот вывод программы:

не поддерживается

; развернуть линию: 5 позиция: 17

Суббота