How to get all models or all convex evaluation?

Question

I'm new to the Z3-Solver with API in C++ and want to solve a group of inequalities and find the results.

I've read the answer which written in Python and try to write it in C++, but it repeating prints one model.

5 <= x + y + z <= 16
AND -4 <= x - y <= 6
AND 1 <= y - z <= 3
AND -1 <= x - z <= 7
AND x >= 0 AND y >= 0 AND z >= 0

The inequalities were added into the solver, and have a lot of evaluations.

c is context and s is the solver.

    vector<const char*> variables {"x", "y", "z"};

    // ...

    // till here, s was added into several constraints
    while(s.check() == sat){
        model m = s.get_model();
        cout << m << "\n######\n";
        expr tmp = c.bool_val(false);
        for(int i = 0; i < variables.size(); ++ i){
            tmp = tmp || (m[c.int_const(variables[i])] != c.int_const(variables[i]));
        }
        s.add(tmp);
    }

And the result:

(define-fun z () Int
  0)
(define-fun y () Int
  2)
(define-fun x () Int
  3)
######
(define-fun z () Int
  0)
(define-fun y () Int
  2)
(define-fun x () Int
  3)
######
(define-fun z () Int
  0)
...

And it just print one model. I'm not sure where is wrong.

How can I get all models or get one or more convex sets (such as {l1 <= x <= u1 and l2 <= x - y <= u2 and ...}), but not to traverse all evaluations.

BTW, there's a lot tutorials on python(such as this), where I can learn z3 in c++ as the example and api doc. is not easy to get started.

score 0 · Accepted Answer · answered May 12 '19 at 17:40

Your "model refutation" loop isn't quite correct. Since you didn't post your whole code, it's hard to tell if there might be other issues, but this is how I would go about it:

#include<vector>
#include"z3++.h"

using namespace std;
using namespace z3;

int main(void) {
    context c;

    expr_vector variables(c);
    variables.push_back(c.int_const("x"));
    variables.push_back(c.int_const("y"));
    variables.push_back(c.int_const("z"));
    expr x = variables[0];
    expr y = variables[1];
    expr z = variables[2];

    solver s(c);

    s.add(5 <= x+y+z);
    s.add(x+y+z <= 16);
    s.add(-4 <= x-y);
    s.add(x-y <= 6);
    s.add(-1 <= x-z);
    s.add(x-z <= 7);
    s.add(x >= 0);
    s.add(y >= 0);
    s.add(z >= 0);

    while (s.check() == sat) {
        model m = s.get_model();
        cout << m << endl;
        cout << "#######" << endl;
        expr tmp = c.bool_val(false);
        for(int i = 0; i < variables.size(); ++i) {
            tmp = tmp || (variables[i] != m.eval(variables[i]));
        }
        s.add(tmp);
    }

    return 0;
}

This code runs and enumerates all the "concrete" models. From your question, I surmise you're also wondering if you can get "symbolic" models: That's not possible with an SMT solver. SMT solvers only produce concrete (i.e., all ground term) models, so if you need to generalize from them, you'll have to do that outside of the z3 boundary.

I replace the m[] with m.eval() and it works. Thanks a lot! If the solver cannot get symbolic models, can I use the solver to do some set algebra? As I have two solvers s1, s2, sharing the same variables, I need to know the models from (and s1 (not s2)). Is it possible with Z3? — Osinovsky, May 14 '19 at 01:53
I'm not quite sure what you're asking. But z3 does have set-operations, see here: https://github.com/Z3Prover/z3/blob/master/src/api/c%2B%2B/z3%2B%2B.h#L3219-L3265 — alias, May 14 '19 at 04:18

How to get all models or all convex evaluation?

1 Answers1