如何使用unsat核心&的z3 split子句尝试再次找出不饱和核 [英] How to use z3 split clauses of unsat cores & try to find out unsat core again

问题描述

您想告诉我们如何拆分unsat核心的子句吗?这是关于问题2，关于发现不饱和核之后，我将尝试再次寻求.你想告诉我怎么做吗?

Could you like to tell how to split clauses of unsat cores? And here is question 2 regarding after found out unsat cores, I will try to seek again. Would you like to tell how to do this?

非常感谢您.

如何拆分以下子句

`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))) 

关于问题2，

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核心.非常感谢.

calling the unsat core function again, it cannot give the unsat cores again. Thank you very much.

推荐答案

我不确定是否理解您的问题.似乎您有一个(和c1(和c2 c3))形式的断言，并且您想跟踪 c1 ， c2 和 c3 单独.

I'm not sure if I understood your question. It seems you have an assertion of the form (and c1 (and c2 c3)), and you want to track c1, c2 and c3 individually.

在Z3中，我们使用答案文字来跟踪断言.答案字面量本质上是用于跟踪断言的新鲜布尔值.也就是说，是否使用了断言(Z3)来显示整个断言集合的不满足性.例如，如果我们要跟踪断言 F ，则创建一个新的布尔变量 p ，然后断言 p表示F .然后，我们提供 p 作为check方法的参数.

In Z3, we use answer literals to track assertions. An answer literal is essentially a fresh Boolean that is used to track an assertion. That is, whether the assertion was used (by Z3) to show unsatisfiability of the whole set of assertions or not. For example, if we want to track assertion F, we create a fresh Boolean variable p and assert p implies F. Then, we provide p as an argument for the check method.

如果 F 是一个很大的连词，并且我们想单独跟踪其元素，则应提取其元素并为每个元素创建一个答案文字.这是完成窍门的完整示例.您可以通过将其包含在Z3发行版中的 example.cpp 文件中进行测试.请注意，您必须包含#include< vector> .

If F is a big conjunction and we want to track its elements individually, we should extract its elements and create an answer literal for each one of them. Here is the complete example that does the trick. You can test it by including it in the example.cpp file that is included in the Z3 distribution. Note that you have to include #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";
    }
}

这篇关于如何使用unsat核心&的z3 split子句尝试再次找出不饱和核的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！