如何使用未饱和核心的 z3 拆分子句并尝试再次找出未饱和核心

Question

您能告诉我如何拆分 unsat cores 的子句吗？ 这是问题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 cores。 非常感谢。

Answer 1

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

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

如果F 是一个大连词，我们想单独跟踪它的元素，我们应该提取它的元素并为每个元素创建一个答案文字。这是解决问题的完整示例。您可以通过将其包含在 Z3 发行版中的 example.cpp 文件中来对其进行测试。请注意，您必须包含#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";
    }
}