unsat core function in z3

Question

Suppose I read the SMTLIB formula using the API:

context ctx;
...
expr F = to_expr(ctx, Z3_parse_smtlib2_file(ctx,argv[1],0,0,0,0,0,0));

The expression F is a conjunction of assertions of the form:

(and (< (+ x y) 3)
     (> (- x1 x2) 0)
     (< (- x1 x2) 4)
     (not (= (- x1 x2) 1))
     (not (= (- x1 x2) 2))
     (not (= (- x1 x2) 3)))

I'd like to extract each individual assertion from this conjunction using the following code fragment from post: How to use z3 split clauses of unsat cores & try to find out unsat core again

    F = F.simplify();
    for (unsigned i = 0; i < F.num_args(); i++) {
        expr Ai = F.arg(i);
        // ... Do something with Ai, just printing in this example.
        std::cout << Ai << "\n";
    }

After utilizing the F.arg(i), the original clause (< (+ x y) 3) has been changed into (not (<= 3 (+ x y))). Here is my

a) question : How can I place the clause (not (<= 3 (+ x y))) to (< (+ x y) 3) ?

b) question : I consider the symbol <= mean to imply in this case, not mean to less than. Am I right?

c) question : Because the clause (not (<= 3 (+ x y))) model is true or false, how can I get arithmetic values such as x = 1, y = -1?

It's very grateful for any suggestion. Thank you very much.

I Tried to edit the question based on your previous messages. Questions at stackoverflow should be self contained. I hope it reflects what your real intention. This is my best guess. Please could you confirm it reflects your original question? — Leonardo de Moura

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2012-11-29T06:57:55

The expression (< (+ x y) 3) is transformed into (not (<= 3 (+ x y))) when F = F.simplify(). In the code fragment you used, the method simplify() is used to "flat" nested "and"s. That is, a formula (and (and A B) (and C (and D E))) is flattened into (and A B C D E). Then, all conjuncts can be easily traversed using the for-loop. However, the simplify() will also perform other transformations in the input formula. Keep in mind, that all transformation preserve equivalence. That is, the input and output formula are logically equivalent. If the transformations applied by simplify() are not desirable, I suggest you avoid this method. If you still want to traverse nested "and"s, you can use an auxiliary todo vector. Here is an example:

expr_vector todo(c);
todo.push_back(F);
while (!todo.empty()) {
    expr current = todo.back();
    todo.pop_back();
    if (current.decl().decl_kind() == Z3_OP_AND) {
        // it is an AND, then put children into the todo list
        for (unsigned i = 0; i < current.num_args(); i++) {
            todo.push_back(current.arg(i));
        }
    }
    else {
        // do something with current
        std::cout << current << "\n";
    }
}

unsat core function in z3

1 Answers