From 64acd9cac05ccb307da4cd73314a40f446340524 Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Mon, 17 Jun 2013 18:04:23 -0700
Subject: [PATCH] fixed some bugs with quantifiers in rule bodies

---
 src/duality/duality_rpfp.cpp    | 12 ++++++++++--
 src/duality/duality_wrapper.cpp | 24 ++++++++++++++++++++++++
 src/duality/duality_wrapper.h   |  4 ++++
 3 files changed, 38 insertions(+), 2 deletions(-)

diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 71a5d47e0..330799796 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -217,8 +217,12 @@ namespace Duality {
       }
     else if (t.is_quantifier())
       {
+	std::vector<expr> pats;
+	t.get_patterns(pats);
+	for(unsigned i = 0; i < pats.size(); i++)
+	  pats[i] = LocalizeRec(e,memo,pats[i]);
 	Term body = LocalizeRec(e,memo,t.body());
-	res = CloneQuantifier(t,body);
+	res = clone_quantifier(t, body, pats);
       }
     else res = t;
     return res;
@@ -1853,7 +1857,11 @@ namespace Duality {
       }
     else if (t.is_quantifier()){
       int bound = t.get_quantifier_num_bound();
-      res = CloneQuantifier(t,SubstBoundRec(memo, subst, level + bound, t.body()));
+      std::vector<expr> pats;
+      t.get_patterns(pats);
+      for(unsigned i = 0; i < pats.size(); i++)
+	pats[i] = SubstBoundRec(memo, subst, level + bound, pats[i]);
+      res = clone_quantifier(t, SubstBoundRec(memo, subst, level + bound, t.body()), pats);
     }
     else if (t.is_var()) {
       int idx = t.get_index_value();
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index fcb637a84..67768d3c8 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -326,6 +326,26 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
   }
 
+  expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns){
+    quantifier *thing = to_quantifier(q.raw());
+    bool is_forall = thing->is_forall();
+    unsigned num_patterns = patterns.size();
+    std::vector< ::expr *> _patterns(num_patterns);
+    for(unsigned i = 0; i < num_patterns; i++)
+      _patterns[i] = to_expr(patterns[i].raw());
+    return q.ctx().cook(q.m().update_quantifier(thing, is_forall, num_patterns, &_patterns[0], 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();
+    :: expr * const *it = thing->get_patterns();
+    pats.resize(num_patterns);
+    for(unsigned i = 0; i < num_patterns; i++)
+      pats[i] = expr(ctx(),it[i]);
+  }
+
+
   func_decl context::fresh_func_decl(char const * prefix, const std::vector<sort> &domain, sort const & range){
     std::vector < ::sort * > _domain(domain.size());
     for(unsigned i = 0; i < domain.size(); i++)
@@ -547,6 +567,10 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     a.show();
   }
 
+  void show_ast(::ast *a, ast_manager &m) {
+    std::cout << mk_pp(a, m) << std::endl;
+  }
+
   bool expr::is_label (bool &pos,std::vector<symbol> &names) const {
     buffer< ::symbol> _names;
     bool res = m().is_label(to_expr(raw()),pos,_names);
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 4a6d32695..18fcc3e9f 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -556,11 +556,15 @@ namespace Duality {
 	
 	friend expr clone_quantifier(const expr &, const expr &);
 
+        friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);
+
         friend std::ostream & operator<<(std::ostream & out, expr const & m){
 	  m.ctx().print_expr(out,m);
 	  return out;
 	}
 
+	void get_patterns(std::vector<expr> &pats) const ;
+
 	unsigned get_quantifier_num_bound() const {
 	  return to_quantifier(raw())->get_num_decls();
 	}