From 673ba137e55716c4e137ec38ea2bc03219da9b3c Mon Sep 17 00:00:00 2001
From: Ken McMillan <kenmcmil@microsoft.com>
Date: Mon, 23 Dec 2013 11:17:38 -0800
Subject: [PATCH] added qe_lite preprocessing pass to duality

---
 src/duality/duality_rpfp.cpp    | 45 ++++++++++++++++++++++++++++++++-
 src/duality/duality_wrapper.cpp | 11 ++++++++
 src/duality/duality_wrapper.h   |  3 +++
 3 files changed, 58 insertions(+), 1 deletion(-)

diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 04b4d075e..036a0c86a 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -2802,7 +2802,7 @@ namespace Duality {
 
   bool Z3User::is_variable(const Term &t){
     if(!t.is_app())
-      return false;
+      return t.is_var();
     return t.decl().get_decl_kind() == Uninterpreted
       && t.num_args() == 0;
   }
@@ -2951,6 +2951,8 @@ namespace Duality {
 			    arg.decl().get_decl_kind() == Uninterpreted);
   }
 
+#define USE_QE_LITE
+
   void RPFP::FromClauses(const std::vector<Term> &unskolemized_clauses){
     hash_map<func_decl,Node *> pmap;
     func_decl fail_pred = ctx.fresh_func_decl("@Fail", ctx.bool_sort());
@@ -2958,6 +2960,7 @@ namespace Duality {
     std::vector<expr> clauses(unskolemized_clauses);
     // first, skolemize the clauses
 
+#ifndef USE_QE_LITE
     for(unsigned i = 0; i < clauses.size(); i++){
       expr &t = clauses[i];
       if (t.is_quantifier() && t.is_quantifier_forall()) {
@@ -2974,11 +2977,32 @@ namespace Duality {
 	t = SubstBound(subst,t.body());
       }
     }    
+#else
+    std::vector<hash_map<int,expr> > substs(clauses.size());
+#endif
 
     // create the nodes from the heads of the clauses
 
     for(unsigned i = 0; i < clauses.size(); i++){
       Term &clause = clauses[i];
+
+#ifdef USE_QE_LITE
+      Term &t = clause;
+      if (t.is_quantifier() && t.is_quantifier_forall()) {
+	int bound = t.get_quantifier_num_bound();
+	std::vector<sort> sorts;
+	std::vector<symbol> names;
+	for(int j = 0; j < bound; j++){
+	  sort the_sort = t.get_quantifier_bound_sort(j);
+	  symbol name = t.get_quantifier_bound_name(j);
+	  expr skolem = ctx.constant(symbol(ctx,name),sort(ctx,the_sort));
+	  substs[i][bound-1-j] = skolem;
+	}
+	clause = t.body();
+      }
+      
+#endif
+      
       if(clause.is_app() && clause.decl().get_decl_kind() == Uninterpreted)
 	clause = implies(ctx.bool_val(true),clause);
       if(!canonical_clause(clause))
@@ -3010,6 +3034,13 @@ namespace Duality {
 	  seen.insert(arg);
 	  Indparams.push_back(arg);
 	}
+#ifdef USE_QE_LITE
+	{
+	  hash_map<int,hash_map<ast,Term> > sb_memo;
+	  for(unsigned j = 0; j < Indparams.size(); j++)
+	    Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
+	}
+#endif
         Node *node = CreateNode(R(Indparams.size(),&Indparams[0]));
 	//nodes.push_back(node);
 	pmap[R] = node;
@@ -3055,6 +3086,18 @@ namespace Duality {
       body = RemoveLabels(body,lbls);
       body = body.simplify();
 
+#ifdef USE_QE_LITE
+      std::set<int> idxs;
+      for(unsigned j = 0; j < Indparams.size(); j++)
+	if(Indparams[j].is_var())
+	  idxs.insert(Indparams[j].get_index_value());
+      body = body.qe_lite(idxs,false);
+      hash_map<int,hash_map<ast,Term> > sb_memo;
+      body = SubstBoundRec(sb_memo,substs[i],0,body);
+      for(unsigned j = 0; j < Indparams.size(); j++)
+	Indparams[j] = SubstBoundRec(sb_memo, substs[i], 0, Indparams[j]);
+#endif
+
       // Create the edge
       Transformer T = CreateTransformer(Relparams,Indparams,body);
       Edge *edge = CreateEdge(Parent,T,Children);
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 51f357653..dd1828214 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -339,6 +339,17 @@ expr context::make_quant(decl_kind op, const std::vector<sort> &_sorts, const st
     return ctx().cook(result);
   }
 
+  expr expr::qe_lite(const std::set<int> &idxs, bool index_of_bound) const {
+    ::qe_lite qe(m());
+    expr_ref result(to_expr(raw()),m());
+    proof_ref pf(m());
+    uint_set uis;
+    for(std::set<int>::const_iterator it=idxs.begin(), en = idxs.end(); it != en; ++it)
+      uis.insert(*it);
+    qe(uis,index_of_bound,result);
+    return ctx().cook(result);
+  }
+
   expr clone_quantifier(const expr &q, const expr &b){
     return q.ctx().cook(q.m().update_quantifier(to_quantifier(q.raw()), to_expr(b.raw())));
   }
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 76b28a426..0b20cb08d 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -26,6 +26,7 @@ Revision History:
 #include<sstream>
 #include<vector>
 #include<list>
+#include <set>
 #include"version.h"
 #include<limits.h>
 
@@ -561,6 +562,8 @@ namespace Duality {
 	
         expr qe_lite() const;
 
+	expr qe_lite(const std::set<int> &idxs, bool index_of_bound) const;
+
 	friend expr clone_quantifier(const expr &, const expr &);
 
         friend expr clone_quantifier(const expr &q, const expr &b, const std::vector<expr> &patterns);