如何使用 unsat 核心的 z3 split 子句并尝试再次找出 unsat 核心

您能告诉我如何拆分 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))) 

关于问题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 core函数，它不能再次给出unsat core。 非常感谢。

我不确定我是否理解你的问题。看来你有一个形式的断言(and c1 (and c2 c3))，并且您想要跟踪c1, c2 and c3单独。

在 Z3 中，我们使用答案文字来跟踪断言。答案文字本质上是一个新的布尔值，用于跟踪断言。也就是说，断言是否被（Z3）使用来显示整组断言的不可满足性。例如，如果我们想跟踪断言F，我们创建一个新的布尔变量p并断言p implies F。然后，我们提供p作为 check 方法的参数。

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