Z3Opt C++ API: parse smtlib2 formula from file

Question

Is there any way in Z3Opt C++ API to parse smtlib2 file? So, basically what I'm trying to do is dump Z3Opt formula to file and then read it in other program. The only function I found to parse smtlib2 files is Z3_parse_smtlib2_file. But it's not support extended smtlib2 format (with maximize, minimize and assert-soft operations), which they describe in z3opt tutorial. However, z3 console version accept that format and did not fail. It means there is some way to do what I need. So, could anyone help me, please.

Here is some example to explain what I am talking about:

#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;
}

Function dumpFormula() create a z3opt formula and dump it to the file. Here's 'output.smt2' file:

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

Function readDumpedFormula() tries to parse that file and check that formula. But all I get is errors. Here's an output of the program:

unsupported

; maximize line: 5 position: 17

Sat

It looks like the Z3 console uses a different set of methods from the user-facing C++ API. Running Z3 with GDB shows a trace through main() in main.cpp to read_smtlib2_commands() in smtlib_frontend.cpp to parse_smt2_commands() in smt2parser.cpp. This is quite different from the methods exposed in api_parsers.cpp. — Douglas B. Staple
@DouglasB.Staple Yeah. I also thought about that. I just hoped that maybe there is some way to do it in C++ API. — kivi

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2016-07-22T15:21:15

This is a somewhat recurrent question. The parser that is exposed over the API just lets you load formulas. It uses a plugin model to let the parser know which commands are registered. In the version exposed I the API, the supplied commands do not include the commands for optimization.

Seems you are really asking for a feature that takes an optimization object (symmetrically, a solver object) and populate it using assertions and objectives from a string or file.

You could approximate the file loading declaring special predicates maximize, minimize, soft-assert, respectively. Then parse the file with these as assertions. Then post-process the parsed assertions and feed them into an optimization object.

Z3Opt C++ API: parse smtlib2 formula from file

1 Answers