そこの
式から節を抽出し、毎回 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++;
}