new interpolation fixes; re-added fixedpoint-push/pop

src/ast/ast.cpp

@@ -1307,7 +1307,7 @@ ast_manager::ast_manager(ast_manager const & src, bool disable_proofs):
 void ast_manager::init() {
     // TODO: the following is a HACK to enable proofs in the old smt solver
     // When we stop using that solver, this hack can be removed
-    m_proof_mode = PGM_FINE;
+    // m_proof_mode = PGM_FINE;
 
     m_int_real_coercions = true;
     m_debug_ref_count = false;

src/interp/iz3checker.cpp

@@ -170,6 +170,11 @@ struct iz3checker : iz3base {
   iz3checker(ast_manager &_m)
     : iz3base(_m) {
   }
+
+  iz3checker(iz3mgr &_m)
+    : iz3base(_m) {
+  }
+
 };  
 
 template <class T>
@@ -193,6 +198,18 @@ bool iz3check(ast_manager &_m_manager,
   return chk.check(s,err,chk.cook(cnsts),to_std_vector(parents),chk.cook(interps),chk.cook(theory));
 }
 
+bool iz3check(iz3mgr &mgr,
+	      solver *s,
+	      std::ostream &err,
+	      const std::vector<iz3mgr::ast> &cnsts,
+	      const std::vector<int> &parents,
+	      const std::vector<iz3mgr::ast> &interps,
+	      const std::vector<iz3mgr::ast> &theory)
+{
+  iz3checker chk(mgr);
+  return chk.check(s,err,cnsts,parents,interps,theory);
+}
+
 bool iz3check(ast_manager &_m_manager,
 	      solver *s,
 	      std::ostream &err,

src/interp/iz3checker.h

@@ -38,4 +38,12 @@ bool iz3check(ast_manager &_m_manager,
 	      ast *tree,
 	      const ptr_vector<ast> &interps);
 
+bool iz3check(iz3mgr &mgr,
+	      solver *s,
+	      std::ostream &err,
+	      const std::vector<iz3mgr::ast> &cnsts,
+	      const std::vector<int> &parents,
+	      const std::vector<iz3mgr::ast> &interps,
+	      const ptr_vector<iz3mgr::ast> &theory);
+
 #endif

src/interp/iz3interp.cpp

@@ -304,6 +304,7 @@ public:
     fr.fix_interpolants(interps_vec);
 
     interps = interps_vec;
+
   }
 
 

src/interp/iz3mgr.cpp

@@ -476,6 +476,15 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<ast>& coeffs){
   }
 }
 
+static void abs_rat(std::vector<rational> &rats){
+  // check that they are all non-neg -- if neg, take abs val and warn!
+  for(unsigned i = 0; i < rats.size(); i++)
+    if(rats[i].is_neg()){
+      //      std::cout << "negative Farkas coeff!\n";
+      rats[i] = -rats[i];
+    }
+}
+
 void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
   symb s = sym(proof);
   int numps = s->get_num_parameters();
@@ -494,12 +503,15 @@ void iz3mgr::get_farkas_coeffs(const ast &proof, std::vector<rational>& rats){
     }
     rats[i-2] = r;
   }
+#if 0
   if(rats.size() != 0 && rats[0].is_neg()){
     for(unsigned i = 0; i < rats.size(); i++){
       assert(rats[i].is_neg());
       rats[i] = -rats[i];
     }
   }
+#endif
+  abs_rat(rats);
   extract_lcd(rats);
 }
 
@@ -536,6 +548,7 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& r
     }
     rats[i-1] = r;
   }
+#if 0
   if(rats[1].is_neg()){ // work around bug -- if all coeffs negative, negate them
     for(unsigned i = 1; i < rats.size(); i++){
       if(!rats[i].is_neg())
@@ -543,6 +556,8 @@ void iz3mgr::get_assign_bounds_coeffs(const ast &proof, std::vector<rational>& r
       rats[i] = -rats[i];
     }
   }
+#endif
+  abs_rat(rats);
   extract_lcd(rats);
 }
 

src/interp/iz3proof_itp.cpp

@@ -626,7 +626,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast equa = sep_cond(arg(pf,0),cond);
       if(is_equivrel_chain(equa)){
 	ast lhs,rhs; eq_from_ineq(arg(neg_equality,0),lhs,rhs); // get inequality we need to prove
-	ast ineqs= chain_ineqs(LitA,equa,lhs,rhs); // chain must be from lhs to rhs
+	ast ineqs= chain_ineqs(op(arg(neg_equality,0)),LitA,equa,lhs,rhs); // chain must be from lhs to rhs
 	cond = my_and(cond,chain_conditions(LitA,equa)); 
 	ast Bconds = chain_conditions(LitB,equa); 
 	if(is_true(Bconds) && op(ineqs) != And)
@@ -1313,7 +1313,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
 
-  ast chain_ineqs(LitType t, const ast &chain, const ast &lhs, const ast &rhs){
+  ast chain_ineqs(opr comp_op, LitType t, const ast &chain, const ast &lhs, const ast &rhs){
     if(is_true(chain)){
       if(lhs != rhs)
 	throw "bad ineq inference";
@@ -1322,9 +1322,12 @@ class iz3proof_itp_impl : public iz3proof_itp {
     ast last = chain_last(chain);
     ast rest = chain_rest(chain);
     ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
-    ast cond = chain_ineqs(t,rest,lhs,mid);
+    ast cond = chain_ineqs(comp_op,t,rest,lhs,mid);
     if(is_rewrite_side(t,last)){
-      ast foo = z3_simplify(make(Leq,make_int("0"),make(Sub,mid,rhs)));
+      ast diff;
+      if(comp_op == Leq) diff = make(Sub,rhs,mid);
+      else diff = make(Sub,mid,rhs);
+      ast foo = z3_simplify(make(Leq,make_int("0"),diff));
       if(is_true(cond))
 	cond = foo;
       else {
@@ -1351,6 +1354,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
 	std::swap(lhs,rhs);
       if(op(rhs) == Times){
 	rhs = arg(rhs,1);
+	if(op(ineq) == Leq)
+	  std::swap(lhs,rhs);
 	return;
       }
     }
@@ -1368,16 +1373,31 @@ class iz3proof_itp_impl : public iz3proof_itp {
 
   /** Make an assumption node. The given clause is assumed in the given frame. */
   virtual node make_assumption(int frame, const std::vector<ast> &assumption){
-    if(pv->in_range(frame,rng)){
-      std::vector<ast> itp_clause;
-      for(unsigned i = 0; i < assumption.size(); i++)
-	if(get_term_type(assumption[i]) != LitA)
-	  itp_clause.push_back(assumption[i]);
-      ast res = my_or(itp_clause);
-      return res;
+    if(!weak){
+      if(pv->in_range(frame,rng)){
+	std::vector<ast> itp_clause;
+	for(unsigned i = 0; i < assumption.size(); i++)
+	  if(get_term_type(assumption[i]) != LitA)
+	    itp_clause.push_back(assumption[i]);
+	ast res = my_or(itp_clause);
+	return res;
+      }
+      else {
+	return mk_true();
+      }
     }
     else {
-      return mk_true();
+      if(pv->in_range(frame,rng)){
+	return mk_false();
+      }
+      else {
+	std::vector<ast> itp_clause;
+	for(unsigned i = 0; i < assumption.size(); i++)
+	  if(get_term_type(assumption[i]) != LitB)
+	    itp_clause.push_back(assumption[i]);
+	ast res = my_or(itp_clause);
+	return mk_not(res);
+      }
     }
   }
 
@@ -1602,17 +1622,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
   virtual node make_congruence(const ast &p, const ast &con, const ast &prem1){
     ast x = arg(p,0), y = arg(p,1);
     ast itp;
+    LitType con_t = get_term_type(con);
     if(get_term_type(p) == LitA){
-      if(get_term_type(con) == LitA)
+      if(con_t == LitA)
 	itp = mk_false();
+      else if(con_t == LitB)
+	itp = p;
       else
 	itp = make_mixed_congruence(x, y, p, con, prem1);
     }
     else {
-      if(get_term_type(con) == LitA)
+      if(con_t == LitA)
 	itp = mk_not(p);
       else{
-	if(get_term_type(con) == LitB)
+	if(con_t == LitB)
 	  itp = mk_true();
 	else
 	  itp = make_mixed_congruence(x, y, p, con, prem1);
@@ -2047,30 +2070,58 @@ public:
   {
     pv = p;
     rng = r;
-    weak = w;
+    weak = false ; //w;
     type boolintbooldom[3] = {bool_type(),int_type(),bool_type()};
     type booldom[1] = {bool_type()};
     type boolbooldom[2] = {bool_type(),bool_type()};
     type boolboolbooldom[3] = {bool_type(),bool_type(),bool_type()};
     type intbooldom[2] = {int_type(),bool_type()};
     contra = function("@contra",2,boolbooldom,bool_type());
+    m().inc_ref(contra);
     sum = function("@sum",3,boolintbooldom,bool_type());
+    m().inc_ref(sum);
     rotate_sum = function("@rotsum",2,boolbooldom,bool_type());
+    m().inc_ref(rotate_sum);
     leq2eq = function("@leq2eq",3,boolboolbooldom,bool_type());
+    m().inc_ref(leq2eq);
     eq2leq = function("@eq2leq",2,boolbooldom,bool_type());
+    m().inc_ref(eq2leq);
     cong = function("@cong",3,boolintbooldom,bool_type());
+    m().inc_ref(cong);
     exmid = function("@exmid",3,boolboolbooldom,bool_type());
+    m().inc_ref(exmid);
     symm = function("@symm",1,booldom,bool_type());
+    m().inc_ref(symm);
     epsilon = make_var("@eps",int_type());
     modpon = function("@mp",3,boolboolbooldom,bool_type());
+    m().inc_ref(modpon);
     no_proof = make_var("@nop",bool_type());
     concat = function("@concat",2,boolbooldom,bool_type());
+    m().inc_ref(concat);
     top_pos = make_var("@top_pos",bool_type());
     add_pos = function("@add_pos",2,intbooldom,bool_type());
+    m().inc_ref(add_pos);
     rewrite_A = function("@rewrite_A",3,boolboolbooldom,bool_type());
+    m().inc_ref(rewrite_A);
     rewrite_B = function("@rewrite_B",3,boolboolbooldom,bool_type());
+    m().inc_ref(rewrite_B);
   }
 
+  ~iz3proof_itp_impl(){
+    m().dec_ref(contra);
+    m().dec_ref(sum);
+    m().dec_ref(rotate_sum);
+    m().dec_ref(leq2eq);
+    m().dec_ref(eq2leq);
+    m().dec_ref(cong);
+    m().dec_ref(exmid);
+    m().dec_ref(symm);
+    m().dec_ref(modpon);
+    m().dec_ref(concat);
+    m().dec_ref(add_pos);
+    m().dec_ref(rewrite_A);
+    m().dec_ref(rewrite_B);
+  }
 };
 
 iz3proof_itp *iz3proof_itp::create(prover *p, const prover::range &r, bool w){

src/interp/iz3translate.cpp

@@ -881,11 +881,11 @@ public:
     std::vector<Iproof::node>  my_prems;
     std::vector<ast>  my_coeffs;
     std::vector<Iproof::node>  my_prem_cons;
-    for(unsigned i = 0; i < coeffs.size(); i++){
+    for(unsigned i = pol ? 0 : 1; i < coeffs.size(); i+= 2){
       rational &c = coeffs[i];
-      if(pol ? c.is_pos() : c.is_neg()){
+      if(c.is_pos()){
 	my_prems.push_back(prems[i]);
-	my_coeffs.push_back(pol ? make_int(c) : make_int(-c));
+	my_coeffs.push_back(make_int(c));
 	my_prem_cons.push_back(conc(prem(proof,i)));
       }
     }

src/muz/base/dl_context.cpp

@@ -187,6 +187,10 @@ namespace datalog {
         if (m_trail.get_num_scopes() == 0) {
             throw default_exception("there are no backtracking points to pop to");
         }
+	if(m_engine.get()){
+	  if(get_engine() != DUALITY_ENGINE)
+	    throw default_exception("operation is not supported by engine");
+	}
         m_trail.pop_scope(1); 
     }
 

src/muz/duality/duality_dl_interface.cpp

@@ -82,6 +82,7 @@ dl_interface::dl_interface(datalog::context& dl_ctx) :
 
 {
   _d = 0;
+  dl_ctx.get_manager().toggle_proof_mode(PGM_FINE);
 }
 
 

src/muz/fp/dl_cmds.cpp

@@ -454,6 +454,44 @@ public:
     }
 };
 
+/**
+   \brief fixedpoint-push command.
+*/
+class dl_push_cmd : public cmd {
+    ref<dl_context> m_dl_ctx;
+public:
+    dl_push_cmd(dl_context * dl_ctx):
+      cmd("fixedpoint-push"),
+      m_dl_ctx(dl_ctx)
+    {}
+
+    virtual char const * get_usage() const { return ""; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "push the fixedpoint context"; }
+    virtual unsigned get_arity() const { return 0; }
+    virtual void execute(cmd_context & ctx) {
+        m_dl_ctx->push();
+    }
+};
+
+/**
+   \brief fixedpoint-pop command.
+*/
+class dl_pop_cmd : public cmd {
+    ref<dl_context> m_dl_ctx;
+public:
+    dl_pop_cmd(dl_context * dl_ctx):
+      cmd("fixedpoint-pop"),
+      m_dl_ctx(dl_ctx)
+    {}
+
+    virtual char const * get_usage() const { return ""; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "pop the fixedpoint context"; }
+    virtual unsigned get_arity() const { return 0; }
+    virtual void execute(cmd_context & ctx) {
+        m_dl_ctx->pop();
+    }
+};
+
 
 static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) {
     dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds);
@@ -463,7 +501,7 @@ static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_c
     ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
     // #ifndef _EXTERNAL_RELEASE
     // TODO: we need these!
-#if 0
+#if 1
     ctx.insert(alloc(dl_push_cmd, dl_ctx)); // not exposed to keep command-extensions simple.
     ctx.insert(alloc(dl_pop_cmd, dl_ctx));
 #endif