Получать новые ненасыщенные ядра

Question

Там

Я пытаюсь извлечь предложение из формул и изменить полярность одного предложения каждый раз, когда решается сб, вычисляя модели и помещая предложение в набор. Если это решено ненадлежащим образом, то найдите новые ненасыщенные ядра. Но постепенно вызывая функцию ядра 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++;
}

Answer 1

Непонятно, в чем конкретно вопрос, но я предполагаю, что вы хотели бы извлечь несколько разных ненасыщенных ядер из одной формулы. Z3 не поддерживает это из коробки, но алгоритмы могут быть реализованы поверх него. См. Также этот предыдущий вопрос и особенно приведенную там ссылку ( Алгоритмы вычисления минимальных неудовлетворительных подмножеств ограничений), в которых объясняются основы минимизации ядра.