-3

那里

我试图从公式中提取子句并每次更改一个子句的极性，如果已解决，则计算模型并将子句放入集合中。如果解决 unsat，则找出新的 unsat cores。但是增量调用 unsat 核心函数，即使解决了 unsat，求解器也无法给出新的 unsat 核心。代码如下：

context c;
expr x  = c.int_const("x");
expr y  = c.int_const("y");
solver s(c);
expr F  = x + y > 10 && x + y < 6 && y < 5 && x > 0;
assert(F.is_app());
vector<expr> qs;
if (F.decl().decl_kind() == Z3_OP_AND) {
    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);
    }
}
qs.clear();
vector<expr> f,C,M;
size_t count = 0;
for(unsigned i=0; i<F.num_args(); i++){
    f.push_back(F.arg(i));
}
while(!f.empty() && count != F.num_args()){
    C.push_back(f[0]);
    f.erase(f.begin(),f.begin() +1);
    if(M.size()){
        for(unsigned i=0; i<f.size();i++){
            s.add(f[i]);
        }
        for(unsigned j=0; j<M.size(); j++){
            s.add(M[j]);
        }
        expr notC= to_expr(c, Z3_mk_not(c,C[count]));
        s.add(notC);
    }else{  
        expr notC = to_expr(c,Z3_mk_not(c,C[count]));
        s.add(notC);
        for(unsigned i =0; i<f.size(); i++){
            s.add(f[i]);
        }
    }
    if(s.check() == sat){
        cout<<"sat"<<"\n";
        M.push_back(C[count]);
    }else if(s.check() == unsat){
        size_t i;
        i=0;
        if(f.size()){
            for(unsigned w=0; w<f.size(); w++){
                std::stringstream qname;
                expr qi = c.bool_const(qname.str().c_str());
                s.add(implies(qi,f[w]));
                qs.push_back(qi);
                i++;
            }
        }
        for(unsigned j=0; j<M.size(); j++){
            stringstream qname;
            expr qi = c.bool_const(qname.str().c_str());
            s.add(implies(qi,M[j]));
            qs.push_back(qi);
            i++;
        }
        std::stringstream qname;
        expr qi = c.bool_const(qname.str().c_str());
        expr notC = to_expr(c,Z3_mk_not(c,C[count]));
        s.add(implies(qi,notC));
        if(s.check(qs.size(),&qs[0]) == unsat){
            expr_vector core2 = s.unsat_core();
            cout<<"new cores'size  "<<core2.size()<<endl;
            cout<<"new cores  "<<core2<<endl;
        }
    }
    qs.clear();
    count++;
}
4

1 回答 1

1

目前尚不清楚问题到底是什么，但我猜你想从同一个公式中提取多个不同的未饱和核心。Z3 不支持开箱即用，但可以在其之上实现算法。另请参阅this previous question，尤其是那里给出的参考（Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints），它解释了核心最小化背后的基础知识。

于 2013-02-06T13:28:59.370 回答