-3

そこの

式から節を抽出し、毎回 1 つの節の極性を変更しようとしています。解決された場合は、モデルを計算し、節をセットに入れます。unsat で解決された場合は、新しい unsat コアを見つけます。しかし、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

質問が正確に何であるかは不明ですが、同じ式から複数の異なる unsat コアを抽出したいと考えています。Z3 はそのままではこれをサポートしていませんが、その上にアルゴリズムを実装できます。この前の質問と、特にそこで与えられた参照 ( Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints ) も参照してください。これは、コアの最小化の背後にある基本を説明しています。

于 2013-02-06T13:28:59.370 に答える