model - z3 をインクリメンタルに使用し、命題のないモデルを作成するには？

Question

ソルバー Z3 をインクリメンタルに使用する方法を教えてください。また、 を使用する場合v.name()、どうすれば命題値のないモデルを取得できますか? たとえば、プログラムを呼び出した後cout<<v.name()<<m.get_const_interp(v);、モデルを取得できますが、 x = 3, p = true, y = 4必要ないため、モデルp = trueのセットから削除できますか?

Answer 1

Z3 C++ API を使用してインクリメンタル ソリューションを実行する方法を示す新しい C++ の例を追加しました。新しい例は、すでにオンラインで入手できます。投稿の最後にある例をコピーしました。

2 番目の質問についてですが、Z3 では、モデルは基本的に読み取り専用のオブジェクトです。気にしない値は単に無視できます。望ましくない値を隠すモデル オブジェクトの独自のラッパーを作成することもできます。

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