CODEWITHSUNDEEP
z3
Million
Million

Reputation: 124

unsat core function in z3

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.

Upvotes: 2

Views: 640

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

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

Upvotes: 2

Related Questions