How to use z3 incrementally and model without prop

问题:

Could you please tell me how to use the solver Z3 incrementally? Moreover, When I use v.name(), how can I get the model without propositional value? Such as, After call the program cout<<v.name()<<m.get_const_interp(v);, we can get the model x = 3, p = true, y = 4, because I don't need p = true, can I delete from the set of models?

回答1:

I have added new C++ examples that demonstrate how to do incremental solving using the Z3 C++ API. The new examples are already available online. I copied the examples in the end of the post.

Regarding the second question, in Z3, models are essentially read-only objects. You can simply ignore the values you don't care. You can also write your own wrapper for the model object that hides undesired values.

void incremental_example1() {
    std::cout << "incremental example1\n";
    context c;
    expr x = c.int_const("x");
    solver s(c);
    s.add(x > 0);
    std::cout << s.check() << "\n";
    // We can add more formulas to the solver
    s.add(x < 0);
    // and, invoke s.check() again...
    std::cout << s.check() << "\n";
}

void incremental_example2() {
    // In this example, we show how push() and pop() can be used
    // to remove formulas added to the solver.
    std::cout << "incremental example2\n";
    context c;
    expr x = c.int_const("x");
    solver s(c);
    s.add(x > 0);
    std::cout << s.check() << "\n";
    // push() creates a backtracking point (aka a snapshot).
    s.push();
    // We can add more formulas to the solver
    s.add(x < 0);
    // and, invoke s.check() again...
    std::cout << s.check() << "\n";
    // pop() will remove all formulas added between this pop() and the matching push()
    s.pop();
    // The context is satisfiable again
    std::cout << s.check() << "\n";
    // and contains only x > 0
    std::cout << s << "\n";
}

void incremental_example3() {
    // In this example, we show how to use assumptions to "remove" 
    // formulas added to a solver. Actually, we disable them.
    std::cout << "incremental example3\n";
    context c;
    expr x = c.int_const("x");
    solver s(c);
    s.add(x > 0);
    std::cout << s.check() << "\n";
    // Now, suppose we want to add x < 0 to the solver, but we also want
    // to be able to disable it later.
    // To do that, we create an auxiliary Boolean variable
    expr b = c.bool_const("b");
    // and, assert (b implies x < 0)
    s.add(implies(b, x < 0));
    // Now, we check whether s is satisfiable under the assumption "b" is true.
    expr_vector a1(c);
    a1.push_back(b);
    std::cout << s.check(a1) << "\n";
    // To "disable" (x > 0), we may just ask with the assumption "not b" or not provide any assumption.
    std::cout << s.check() << "\n";
    expr_vector a2(c);
    a2.push_back(!b);
    std::cout << s.check(a2) << "\n";
}