1

unsat コアの句を分割する方法を教えてください。そして、未飽和のコアが見つかった後、もう一度シークを試みる質問 2 です。これを行う方法を教えてください。

どうもありがとうございました。

以下のように句を分割する方法

`and` (`or` (`<=_int` 1002 x1) (`<=_int` 1000 x1)) (`and` (`or` (`<=_int` 0 (`+_int` x2 (`*_int` -1003 x1))) (`<=_int` 0 (`+_int` x2 (`*_int` -1230 x1)))) (`and` (`or` (`<=_int` 0 (`+_int` x3 (`*_int` -1999 x2)))

質問２についてですが、

cout<<s.check(3,assumptions)<<endl;
    expr_vector core = s.unsat_core();
................

expr assumptions2[2] = {p1,p3};
                    cout<<"check next"<<s.check(2,assumptions2)<<endl;
                    expr_vector core1 = s.unsat_core();
                    for(unsigned int k=0;k<core1.size();++k){
                            cout<<"New core size "<<k<<endl;
                            cout<<"New unsat core "<<core1[k]<<endl;
                    }

unsat コア関数を再度呼び出しても、unsat コアを再度与えることはできません。どうもありがとうございました。

4

1 に答える 1

4

あなたの質問を理解したかどうかわかりません。フォーム のアサーションがあり、を個別(and c1 (and c2 c3))に追跡したいようです。c1c2c3

Z3 では、回答リテラルを使用してアサーションを追跡します。回答リテラルは本質的に、アサーションを追跡するために使用される新鮮なブール値です。つまり、アサーションが (Z3 によって) アサーションのセット全体の不満足を示すために使用されたかどうか。たとえば、 assertion を追跡したい場合はF、新しいブール変数pと assertを作成しますp implies F。次に、pcheck メソッドの引数として指定します。

Fが大きな結合であり、その要素を個別に追跡したい場合は、その要素を抽出し、それぞれに対して回答リテラルを作成する必要があります。トリックを行う完全な例を次に示します。example.cppZ3 ディストリビューションに含まれているファイルに含めることでテストできます。を含める必要があることに注意してください#include<vector>。

/**
   \brief Unsat core example 2
*/
void unsat_core_example2() {
    std::cout << "unsat core example 2\n";
    context c;
    // The answer literal mechanism, described in the previous example,
    // tracks assertions. An assertion can be a complicated
    // formula containing containing the conjunction of many subformulas.
    expr p1 = c.bool_const("p1");
    expr x  = c.int_const("x");
    expr y  = c.int_const("y");
    solver s(c);
    expr F  = x > 10 && y > x && y < 5 && y > 0;
    s.add(implies(p1, F));
    expr assumptions[1] = { p1 };
    std::cout << s.check(1, assumptions) << "\n";
    expr_vector core = s.unsat_core();
    std::cout << core << "\n";
    std::cout << "size: " << core.size() << "\n";
    for (unsigned i = 0; i < core.size(); i++) {
        std::cout << core[i] << "\n";
    }
    // The core is not very informative, since p1 is tracking the formula F
    // that is a conjunction of subformulas.
    // Now, we use the following piece of code to break this conjunction
    // into individual subformulas. First, we flat the conjunctions by
    // using the method simplify.
    std::vector<expr> qs; // auxiliary vector used to store new answer literals.
    assert(F.is_app()); // I'm assuming F is an application.
    if (F.decl().decl_kind() == Z3_OP_AND) {
        // F is a conjunction
        std::cout << "F num. args (before simplify): " << F.num_args() << "\n";
        F = F.simplify();
        std::cout << "F num. args (after simplify):  " << F.num_args() << "\n";
        for (unsigned i = 0; i < F.num_args(); i++) {
            std::cout << "Creating answer literal q" << i << " for " << F.arg(i) << "\n";
            std::stringstream qname; qname << "q" << i;
            expr qi = c.bool_const(qname.str().c_str()); // create a new answer literal
            s.add(implies(qi, F.arg(i)));
            qs.push_back(qi);
        }
    }
    // The solver s already contains p1 => F
    // To disable F, we add (not p1) as an additional assumption
    qs.push_back(!p1);
    std::cout << s.check(qs.size(), &qs[0]) << "\n";
    expr_vector core2 = s.unsat_core();
    std::cout << core2 << "\n";
    std::cout << "size: " << core2.size() << "\n";
    for (unsigned i = 0; i < core2.size(); i++) {
        std::cout << core2[i] << "\n";
    }
}
于 2012-11-08T15:09:51.677 に答える