interpolation fix and improving duality quantifier handling

src/duality/duality.h

@@ -118,6 +118,8 @@ protected:
       expr FinishAndOr(const std::vector<expr> &args, bool is_and);
       expr PullCommonFactors(std::vector<expr> &args, bool is_and);
       Term IneqToEqRec(hash_map<ast, Term> &memo, const Term &t);
+      Term CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall);
+      Term PushQuantifier(const expr &t, const expr &body, bool is_forall);
 
 
 };

src/duality/duality_rpfp.cpp

@@ -548,24 +548,50 @@ 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);
+  Z3User::Term Z3User::PushQuantifier(const expr &t, const expr &body, bool is_forall){
+    if(t.get_quantifier_num_bound() == 1){
+      std::vector<expr> fmlas,free,not_free;
+      CollectConjuncts(body,fmlas, !is_forall);
+      for(unsigned i = 0; i < fmlas.size(); i++){
+	const expr &fmla = fmlas[i];
+	if(fmla.has_free(0))
+	  free.push_back(fmla);
+	else
+	  not_free.push_back(fmla);
+      }
+      decl_kind op = is_forall ? Or : And;
+      if(free.empty())
+	return SimplifyAndOr(not_free,op == And);
+      expr q = clone_quantifier(is_forall ? Forall : Exists,t, SimplifyAndOr(free, op == And));
+      if(!not_free.empty())
+	q = ctx.make(op,q,SimplifyAndOr(not_free, op == And));
+      return q;
     }
-    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(is_forall ? Forall : Exists,t,body);
+  }
+
+  Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body, bool is_forall){
+    if(body.is_app()){
+      if(body.decl().get_decl_kind() == (is_forall ? And : Or)){ // quantifier distributes
+	int nargs = body.num_args();
+	std::vector<expr> args(nargs);
+	for(int i = 0; i < nargs; i++)
+	  args[i] = CloneQuantAndSimp(t, body.arg(i), is_forall);
+	return SimplifyAndOr(args, body.decl().get_decl_kind() == And);
+      }
+      else if(body.decl().get_decl_kind() == is_forall ? And : Or){ // quantifier distributes
+	return PushQuantifier(t,body,is_forall); // may distribute partially
+      }
+      else if(body.decl().get_decl_kind() == Not){
+	return CloneQuantAndSimp(t,body.arg(0),!is_forall);
+      }
     }
     return clone_quantifier(t,body);
   }
 
+  Z3User::Term Z3User::CloneQuantAndSimp(const expr &t, const expr &body){
+    return CloneQuantAndSimp(t,body,t.is_quantifier_forall());
+  }
 
   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));
@@ -659,7 +685,7 @@ namespace Duality {
     else if (t.is_quantifier())
       {
 	Term body = RemoveRedundancyRec(memo,smemo,t.body());
-	res = clone_quantifier(t, body);
+	res = CloneQuantAndSimp(t, body);
       }
     else res = t;
     return res;

src/duality/duality_wrapper.cpp

@@ -374,6 +374,12 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], to_expr(b.raw())));
   }
 
+  expr clone_quantifier(decl_kind dk, const expr &q, const expr &b){
+    quantifier *thing = to_quantifier(q.raw());
+    bool is_forall = dk == Forall;
+    return q.ctx().cook(q.m().update_quantifier(thing, is_forall, to_expr(b.raw())));
+  }
+
   void expr::get_patterns(std::vector<expr> &pats) const {
     quantifier *thing = to_quantifier(raw());
     unsigned num_patterns = thing->get_num_patterns();

src/duality/duality_wrapper.h

@@ -466,6 +466,11 @@ namespace Duality {
 	bool is_label (bool &pos,std::vector<symbol> &names) const ;
 	bool is_ground() const {return to_app(raw())->is_ground();}
 	bool has_quantifiers() const {return to_app(raw())->has_quantifiers();}
+	bool has_free(int idx) const {
+	  used_vars proc;
+	  proc.process(to_expr(raw()));
+	  return proc.contains(idx);
+	}
 
         // operator Z3_app() const { assert(is_app()); return reinterpret_cast<Z3_app>(m_ast); }
         func_decl decl() const {return func_decl(ctx(),to_app(raw())->get_decl());}
@@ -573,6 +578,8 @@ namespace Duality {
 
         friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
 
+	friend expr clone_quantifier(decl_kind, const expr &, const expr &);
+
         friend std::ostream & operator<<(std::ostream & out, expr const & m){
 	  m.ctx().print_expr(out,m);
 	  return out;

src/interp/iz3proof_itp.cpp

@@ -814,6 +814,10 @@ 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
+	if(!rewrites_from_to(equa,lhs,rhs)){
+	  lhs = arg(arg(neg_equality,0),0); // the equality proved is ambiguous, sadly
+	  rhs = arg(arg(neg_equality,0),1);
+	}
 	LitType lhst = get_term_type(lhs), rhst = get_term_type(rhs);
 	if(lhst != LitMixed && rhst != LitMixed)
 	  return unmixed_eq2ineq(lhs, rhs, op(arg(neg_equality,0)), equa, cond);
@@ -1671,9 +1675,20 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return head;
   }
 
-  // split a rewrite chain into head and tail at last non-mixed term
+  bool has_mixed_summands(const ast &e){
+    if(op(e) == Plus){
+      int nargs = num_args(e);
+      for(int i = 0; i < nargs; i++)
+	if(has_mixed_summands(arg(e,i)))
+	  return true;
+      return false;
+    }
+    return get_term_type(e) == LitMixed;
+  }
+  
+  // split a rewrite chain into head and tail at last sum with no mixed sumands
   ast get_right_movers(const ast &chain, const ast &rhs, ast &tail, ast &mid){
-    if(is_true(chain) || get_term_type(rhs) != LitMixed){
+    if(is_true(chain) || !has_mixed_summands(rhs)){
       mid = rhs;
       tail = mk_true();
       return chain;
@@ -1686,11 +1701,11 @@ class iz3proof_itp_impl : public iz3proof_itp {
     return res;
   }
   
-  // split a rewrite chain into head and tail at first non-mixed term
+  // split a rewrite chain into head and tail at first sum with no mixed sumands
   ast get_left_movers(const ast &chain, const ast &lhs, ast &tail, ast &mid){
     if(is_true(chain)){
       mid = lhs; 
-      if(get_term_type(lhs) != LitMixed){
+      if(!has_mixed_summands(lhs)){
 	tail = mk_true();
 	return chain;
       }
@@ -1790,10 +1805,21 @@ class iz3proof_itp_impl : public iz3proof_itp {
   }
 
 
+  bool rewrites_from_to(const ast &chain, const ast &lhs, const ast &rhs){
+    if(is_true(chain))
+      return lhs == rhs;
+    ast last = chain_last(chain);
+    ast rest = chain_rest(chain);
+    ast mid = subst_in_pos(rhs,rewrite_pos(last),rewrite_lhs(last));
+    return rewrites_from_to(rest,lhs,mid);
+  }
+
+  struct bad_ineq_inference {};
+
   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";
+	throw bad_ineq_inference();
       return make(Leq,make_int(rational(0)),make_int(rational(0)));
     }
     ast last = chain_last(chain);