獲得新的不飽和度核

Question

有

我試圖從公式中提取條款，每一次改變一個條款的極性，如果解決了坐，計算模型，並把在從句中套。如果解決不了，那麼找出新的不飽和核心。但是逐漸調用不可核心函數，即使解決不了，求解器也不能給出新的不可核心函數。 的代碼如下：

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不支持開箱即用，但算法可以在其上實現。另請參閱此前的question，特別是在此給出的參考文獻（Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints），它解釋了核心最小化背後的基礎知識。