interpolation fixes

src/duality/duality.h

@@ -82,6 +82,8 @@ namespace Duality {
 
       Term SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val);
 
+      Term CloneQuantAndSimp(const expr &t, const expr &body);
+
       Term RemoveRedundancy(const Term &t);
 
       Term IneqToEq(const Term &t);

src/duality/duality_rpfp.cpp

@@ -523,6 +523,25 @@ namespace Duality {
       return foo;
   }
 
+  Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){
+    if(t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == And){
+      int nargs = body.num_args();
+      std::vector<expr> args(nargs);
+      for(int i = 0; i < nargs; i++)
+	args[i] = CloneQuantAndSimp(t, body.arg(i));
+      return ctx.make(And,args);
+    }
+    if(!t.is_quantifier_forall() && body.is_app() && body.decl().get_decl_kind() == Or){
+      int nargs = body.num_args();
+      std::vector<expr> args(nargs);
+      for(int i = 0; i < nargs; i++)
+	args[i] = CloneQuantAndSimp(t, body.arg(i));
+      return ctx.make(Or,args);
+    }
+    return clone_quantifier(t,body);
+  }
+
+
   Z3User::Term Z3User::SubstAtom(hash_map<ast, Term> &memo, const expr &t, const expr &atom, const expr &val){
     std::pair<ast,Term> foo(t,expr(ctx));
     std::pair<hash_map<ast,Term>::iterator, bool> bar = memo.insert(foo);

src/duality/duality_solver.cpp

@@ -1916,6 +1916,7 @@ namespace Duality {
 
 	stack.back().level = tree->slvr().get_scope_level();
 	bool was_sat = true;
+	int update_failures = 0;
 
 	while (true)
 	{
@@ -1954,10 +1955,14 @@ namespace Duality {
 		  heuristic->Update(node->map); // make it less likely to expand this node in future
 	      }
 	      if(update_count == 0){
-		if(was_sat)
+		if(was_sat){
-		  throw Incompleteness();
+		  update_failures++;
+		  if(update_failures > 10)
+		    throw Incompleteness();
+		}
 		reporter->Message("backtracked without learning");
 	      }
+	      else update_failures = 0;
 	    }
 	    tree->ComputeProofCore(); // need to compute the proof core before popping solver
 	    bool propagated = false;

src/interp/iz3proof_itp.cpp

@@ -369,11 +369,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
       }
       default:
 	{
-	  symb s = sym(itp2);
+	  opr o = op(itp2);
-	  if(s == sforall || s == sexists)
+	  if(o == Uninterpreted){
-	    res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
+	    symb s = sym(itp2);
-	  else
+	    if(s == sforall || s == sexists)
+	      res = make(s,arg(itp2,0),resolve_arith_rec2(memo, pivot1, conj1, arg(itp2,1)));
+	    else
+	      res = itp2;
+	  }
+	  else {
 	    res = itp2;
+	  }
 	}
       }
     }
@@ -405,11 +411,17 @@ class iz3proof_itp_impl : public iz3proof_itp {
       }
       default:
 	{
-	  symb s = sym(itp1);
+	  opr o = op(itp1);
-	  if(s == sforall || s == sexists)
+	  if(o == Uninterpreted){
-	    res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
+	    symb s = sym(itp1);
-	  else
+	    if(s == sforall || s == sexists)
+	      res = make(s,arg(itp1,0),resolve_arith_rec1(memo, neg_pivot_lit, arg(itp1,1), itp2));
+	    else
+	      res = itp1;
+	  }
+	  else {
 	    res = itp1;
+	  }
 	}
       }
     }
@@ -464,18 +476,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
     std::pair<hash_map<ast,ast>::iterator,bool> bar = subst_memo.insert(foo);
     ast &res = bar.first->second;
     if(bar.second){
-      symb g = sym(e);
+      if(op(e) == Uninterpreted){
-      if(g == rotate_sum){
+	symb g = sym(e);
-	if(var == get_placeholder(arg(e,0))){
+	if(g == rotate_sum){
-	  res = e;
+	  if(var == get_placeholder(arg(e,0))){
+	    res = e;
+	  }
+	  else 
+	    res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1)));
+	  return res;
+	}
+	if(g == concat){
+	  res = e;
+	  return res;
 	}
-	else 
-	  res = make(rotate_sum,arg(e,0),subst_term_and_simp_rec(var,t,arg(e,1)));
-	return res;
-      }
-      if(g == concat){
-	res = e;
-	return res;
       }
       int nargs = num_args(e);
       std::vector<ast> args(nargs);
@@ -794,6 +808,7 @@ class iz3proof_itp_impl : public iz3proof_itp {
      return simplify_sum(args);
   }
 
+
   ast simplify_rotate_eq2leq(const ast &pl, const ast &neg_equality, const ast &pf){
     if(pl == arg(pf,1)){
       ast cond = mk_true();
@@ -1036,6 +1051,8 @@ class iz3proof_itp_impl : public iz3proof_itp {
       ast mc = z3_simplify(chain_side_proves(LitA,pref));
       Aproves = my_and(Aproves,mc);
     }
+    if(is_true(nc))
+      return itp;
     return make_normal(itp,nc);
   }