there is
I try to extract the sentence from the formulas and change the polarity of each sentence every time, if solved, sits, calculates the models and puts the sentence in the set. If unsat is resolved, then find out about new unsat kernels. But phasing in the unsaturated main function, even if unsat has solved it, the solver cannot give new unsat kernels. 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() << "\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++; }
source share