z3 - getting new unsat cores

Question

there

I am trying to extract clause from formulas and change one clause's polarity every time, if is solved sat, computing models and put the clause in the set. If it is solved unsat, then find out new unsat cores. But incrementally calling unsat core function, even it's solved unsat, the solver cannot give the new unsat cores. The codes as below:

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() << "
";
    F = F.simplify();
    std::cout << "F num. args (after simplify):  " << F.num_args() << "
";
    for (unsigned i = 0; i < F.num_args(); i++) {
        std::cout << "Creating answer literal q" << i << " for " << F.arg(i) << "
";
        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"<<"
";
        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

It's unclear what exactly the question is, but I'm guessing you would like to extract multiple different unsat cores from the same formula. Z3 does not support this out of the box, but algorithms can be implemented on top of it. See also this previous question and especially the reference given there (Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints), which explains the basics behind core minimization.