handle eq-propagate arithetic rule

src/interp/iz3base.cpp

@@ -24,6 +24,8 @@ Revision History:
 #include <fstream>
 #include <iostream>
 #include <ostream>
+#include "solver.h"
+#include "../smt/smt_solver.h"
 
 
 #ifndef WIN32
@@ -254,16 +256,25 @@ void iz3base::check_interp(const std::vector<ast> &itps, std::vector<ast> &theor
 #endif
 }
 
-bool iz3base::is_sat(ast f){
-  assert(0 && "iz3base::is_sat() not implemented");
-#if 0
-  Z3_push(ctx);
-  Z3_assert_cnstr(ctx,f);
-  Z3_lbool res = Z3_check(ctx);
-  Z3_pop(ctx,1);
-  return res != Z3_L_FALSE;
-#endif
-  return false;
+bool iz3base::is_sat(const std::vector<ast> &q, ast &_proof){
+
+  params_ref p;
+  p.set_bool("proof", true); // this is currently useless
+  p.set_bool("model", true); 
+  p.set_bool("unsat_core", true); 
+  scoped_ptr<solver_factory> sf = mk_smt_solver_factory();
+  ::solver *m_solver = (*sf)(m(), p, true, true, true, ::symbol::null);
+  ::solver &s = *m_solver;
+
+  for(unsigned i = 0; i < q.size(); i++)
+    s.assert_expr(to_expr(q[i].raw()));
+  lbool res = s.check_sat(0,0);
+  if(res == l_false){
+    ::ast *proof = s.get_proof();
+    _proof = cook(proof);
+  }
+  dealloc(m_solver);
+  return res != l_false;
 }
 
 

src/interp/iz3base.h

@@ -103,7 +103,7 @@ class iz3base : public iz3mgr, public scopes {
   void check_interp(const std::vector<ast> &itps, std::vector<ast> &theory);
 
   /** For convenience -- is this formula SAT? */
-  bool is_sat(ast);
+  bool is_sat(const std::vector<ast> &consts, ast &_proof);
 
   /** Interpolator for clauses, to be implemented */
   virtual void interpolate_clause(std::vector<ast> &lits, std::vector<ast> &itps){

src/interp/iz3mgr.cpp

@@ -446,6 +446,17 @@ iz3mgr::ast iz3mgr::z3_simplify(const ast &e){
     return cook(result);
 }
 
+iz3mgr::ast iz3mgr::z3_really_simplify(const ast &e){
+  ::expr * a = to_expr(e.raw());
+  params_ref simp_params;
+  simp_params.set_bool(":som",true);
+  simp_params.set_bool(":sort-sums",true);
+  th_rewriter m_rw(m(), simp_params);
+  expr_ref    result(m());
+  m_rw(a, result);
+  return cook(result);
+}
+
 
 #if 0
 static rational lcm(const rational &x, const rational &y){
@@ -485,6 +496,15 @@ static void abs_rat(std::vector<rational> &rats){
     }
 }
 
+bool iz3mgr::is_farkas_coefficient_negative(const ast &proof, int n){
+  rational r;
+  symb s = sym(proof);
+  bool ok = s->get_parameter(n+2).is_rational(r);
+  if(!ok)
+    throw "Bad Farkas coefficient";
+  return r.is_neg();
+}
+
 void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
   symb s = sym(proof);
   int numps = s->get_num_parameters();

src/interp/iz3mgr.h

@@ -386,7 +386,7 @@ class iz3mgr  {
     return UnknownTheory;
   }
 
-  enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,UnknownKind};
+  enum lemma_kind {FarkasKind,Leq2EqKind,Eq2LeqKind,GCDTestKind,AssignBoundsKind,EqPropagateKind,UnknownKind};
 
   lemma_kind get_theory_lemma_kind(const ast &proof){
     symb s = sym(proof);
@@ -402,6 +402,8 @@ class iz3mgr  {
       return GCDTestKind;
     if(foo == "assign-bounds")
       return AssignBoundsKind;
+    if(foo == "eq-propagate")
+      return EqPropagateKind;
     return UnknownKind;
   }
 
@@ -417,6 +419,8 @@ class iz3mgr  {
   
   void get_assign_bounds_rule_coeffs(const ast &proof, std::vector<ast>& rats);
 
+  bool is_farkas_coefficient_negative(const ast &proof, int n);
+
   bool is_true(ast t){
     return op(t) == True;
   }
@@ -441,6 +445,10 @@ class iz3mgr  {
 
   ast z3_simplify(const ast& e);
 
+  /** Simplify, sorting sums */
+  ast z3_really_simplify(const ast &e);
+
+
   // Some constructors that simplify things
 
   ast mk_not(ast x){

src/interp/iz3translate.cpp

@@ -782,6 +782,16 @@ public:
     return thing;
   }
 
+  bool check_farkas(const std::vector<ast> &prems, const ast &con){
+    ast zero = make_int("0");
+    ast thing = make(Leq,zero,zero);
+    for(unsigned i = 0; i < prems.size(); i++)
+      linear_comb(thing,make_int(rational(1)),prems[i]);
+    linear_comb(thing,make_int(rational(-1)),con);
+    thing = simplify_ineq(thing);
+    return arg(thing,1) == make_int(rational(0));
+  }
+
   // get an inequality in the form t <= c or t < c, there t is affine and c constant
   ast normalize_inequality(const ast &ineq){
     ast zero = make_int("0");
@@ -1120,6 +1130,92 @@ public:
     }
   }
 
+  struct TermLt {
+    iz3mgr &m;
+    bool operator()(const ast &x, const ast &y){
+      unsigned xid = m.ast_id(x);
+      unsigned yid = m.ast_id(y);
+      return xid < yid;
+    }
+    TermLt(iz3mgr &_m) : m(_m) {}
+  };
+
+  void SortTerms(std::vector<ast> &terms){
+    TermLt foo(*this);
+    std::sort(terms.begin(),terms.end(),foo);
+  }
+
+  ast SortSum(const ast &t){
+    if(!(op(t) == Plus))
+      return t;
+    int nargs = num_args(t);
+    if(nargs < 2) return t;
+    std::vector<ast> args(nargs);
+    for(int i = 0; i < nargs; i++)
+      args[i] = arg(t,i);
+    SortTerms(args);
+    return make(Plus,args);
+  }
+
+  ast really_normalize_ineq(const ast &ineq){
+    ast res = normalize_inequality(ineq);
+    res = make(op(res),SortSum(arg(res,0)),arg(res,1));
+    return res;
+  }
+
+  Iproof::node reconstruct_farkas(const std::vector<ast> &prems, const std::vector<Iproof::node> &pfs, const ast &con){
+    int nprems = prems.size();
+    std::vector<ast> pcons(nprems),npcons(nprems);
+    hash_map<ast,ast> pcon_to_pf, npcon_to_pcon;
+    for(int i = 0; i < nprems; i++){
+      pcons[i] = conc(prems[i]);
+      npcons[i] = really_normalize_ineq(pcons[i]);
+      pcon_to_pf[npcons[i]] = pfs[i];
+      npcon_to_pcon[npcons[i]] = pcons[i];
+    }
+    // ast leq = make(Leq,arg(con,0),arg(con,1));
+    ast ncon = really_normalize_ineq(mk_not(con));
+    pcons.push_back(mk_not(con));
+    npcons.push_back(ncon);
+    // ast assumps = make(And,pcons);
+    ast new_proof;
+    if(is_sat(npcons,new_proof))
+      throw "Proof error!";
+    pfrule dk = pr(new_proof);
+    int nnp = num_prems(new_proof);
+    std::vector<Iproof::node> my_prems;
+    std::vector<ast> farkas_coeffs, my_pcons;
+
+    if(dk == PR_TH_LEMMA 
+       && get_theory_lemma_theory(new_proof) == ArithTheory
+       && get_theory_lemma_kind(new_proof) == FarkasKind)
+      get_farkas_coeffs(new_proof,farkas_coeffs);
+    else if(dk == PR_UNIT_RESOLUTION && nnp == 2){
+      for(int i = 0; i < nprems; i++)
+	farkas_coeffs.push_back(make_int(rational(1)));
+    }
+    else
+      throw "cannot reconstruct farkas proof";
+
+    for(int i = 0; i < nnp; i++){
+      ast p = conc(prem(new_proof,i));
+      p = really_normalize_ineq(p);
+      if(pcon_to_pf.find(p) != pcon_to_pf.end()){
+	my_prems.push_back(pcon_to_pf[p]);
+	my_pcons.push_back(npcon_to_pcon[p]);
+      }
+      else if(p == ncon){
+	my_prems.push_back(iproof->make_hypothesis(mk_not(con)));
+	my_pcons.push_back(mk_not(con));
+      }
+      else
+	throw "cannot reconstruct farkas proof";
+    }
+    Iproof::node res = iproof->make_farkas(mk_false(),my_prems,my_pcons,farkas_coeffs);
+    return res;
+  }
+
+    
   // translate a Z3 proof term into interpolating proof system
 
   Iproof::node translate_main(ast proof, bool expect_clause = true){
@@ -1255,11 +1351,11 @@ public:
 	    get_farkas_coeffs(proof,farkas_coeffs);
 	    if(nprems == 0) {// axiom, not rule
 	      int nargs = num_args(con);
-	      if(farkas_coeffs.size() != nargs){
+	      if(farkas_coeffs.size() != (unsigned)nargs){
 		pfgoto(proof);
 		throw unsupported();
 	      }
-	      for(unsigned i = 0; i < nargs; i++){
+	      for(int i = 0; i < nargs; i++){
 		ast lit = mk_not(arg(con,i));
 		prem_cons.push_back(lit);
 		args.push_back(iproof->make_hypothesis(lit));
@@ -1314,6 +1410,23 @@ public:
 	      res = AssignBounds2Farkas(proof,conc(proof));
 	    break;
 	  }
+	  case EqPropagateKind: {
+	    std::vector<ast> prems(nprems);
+	    Iproof::node fps[2];
+	    ast ineq_con[2];
+	    for(int i = 0; i < nprems; i++)
+	      prems[i] = prem(proof,i);
+	    for(int i = 0; i < 2; i++){
+	      opr o = i == 0 ? Leq : Geq;
+	      ineq_con[i] = make(o, arg(con,0), arg(con,1));
+	      fps[i] = reconstruct_farkas(prems,args,ineq_con[i]);
+	    }
+	    res = iproof->make_leq2eq(arg(con,0), arg(con,1), ineq_con[0], ineq_con[1]);
+	    std::vector<Iproof::node> dummy_clause;
+	    for(int i = 0; i < 2; i++)
+	      res = iproof->make_resolution(ineq_con[i],dummy_clause,res,fps[i]);
+	    return res;
+	  }
 	  default:
 	    throw unsupported();
 	  }