From 5e737641b754ca1aa0e75ffcbdfdeac6cb8a0cdf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 Mar 2016 16:57:30 -0700
Subject: [PATCH] remove qe-lite pass in quant_tatics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qe_lite.cpp                     | 49 ++++++++++++++++++++++++--
 src/smt/proto_model/proto_model.cpp    |  1 +
 src/tactic/smtlogics/quant_tactics.cpp |  3 --
 3 files changed, 47 insertions(+), 6 deletions(-)

diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp
index 5039e4c3d..86a3fbec8 100644
--- a/src/qe/qe_lite.cpp
+++ b/src/qe/qe_lite.cpp
@@ -491,6 +491,10 @@ namespace eq {
                     m_new_args.push_back(args[i]);
                 }
             }
+            if (m_new_args.size() == num_args) {
+                r = q;
+                return;
+            }
             
             expr_ref t(m);
             if (q->is_forall()) {
@@ -771,7 +775,7 @@ namespace eq {
                 proof_ref curr_pr(m);
                 q  = to_quantifier(r);
                 reduce_quantifier1(q, r, curr_pr);
-                if (m.proofs_enabled()) {
+                if (m.proofs_enabled() && r != q) {
                     pr = m.mk_transitivity(pr, curr_pr);
                 }
             } while (q != r && is_quantifier(r));
@@ -2297,7 +2301,7 @@ public:
             }
             m_imp(indices, true, result);          
             if (is_forall(q)) {
-                result = m.mk_not(result);
+                result = push_not(result);
             }
             result = m.update_quantifier(
                 q, 
@@ -2476,6 +2480,41 @@ class qe_lite_tactic : public tactic {
             cooperate("qe-lite");
         }
         
+        void debug_diff(expr* a, expr* b) {
+            ptr_vector<expr> as, bs;
+            as.push_back(a);
+            bs.push_back(b);
+            expr* a1, *a2, *b1, *b2;
+            while (!as.empty()) {
+                a = as.back();
+                b = bs.back();
+                as.pop_back();
+                bs.pop_back();
+                if (a == b) {
+                    continue;
+                }
+                else if (is_forall(a) && is_forall(b)) {
+                    as.push_back(to_quantifier(a)->get_expr());
+                    bs.push_back(to_quantifier(b)->get_expr());
+                }
+                else if (m.is_and(a, a1, a2) && m.is_and(b, b1, b2)) {
+                    as.push_back(a1);
+                    as.push_back(a2);
+                    bs.push_back(b1);
+                    bs.push_back(b2);
+                }
+                else if (m.is_eq(a, a1, a2) && m.is_eq(b, b1, b2)) {
+                    as.push_back(a1);
+                    as.push_back(a2);
+                    bs.push_back(b1);
+                    bs.push_back(b2);
+                }
+                else {
+                    TRACE("qe", tout << mk_pp(a, m) << " != " << mk_pp(b, m) << "\n";);
+                }
+            }
+        }
+
         void operator()(goal_ref const & g, 
                         goal_ref_buffer & result, 
                         model_converter_ref & mc, 
@@ -2507,7 +2546,11 @@ class qe_lite_tactic : public tactic {
                         new_pr = g->pr(i);
                     }
                 }
-                g->update(i, new_f, new_pr, g->dep(i));                
+                if (f != new_f) {
+                    TRACE("qe", tout << mk_pp(f, m) << "\n" << new_f << "\n";);
+                    debug_diff(f, new_f);
+                    g->update(i, new_f, new_pr, g->dep(i));                
+                }
             }
             g->inc_depth();
             result.push_back(g.get());
diff --git a/src/smt/proto_model/proto_model.cpp b/src/smt/proto_model/proto_model.cpp
index cfc037a68..c4f38cc3a 100644
--- a/src/smt/proto_model/proto_model.cpp
+++ b/src/smt/proto_model/proto_model.cpp
@@ -105,6 +105,7 @@ bool proto_model::eval(expr * e, expr_ref & result, bool model_completion) {
     m_eval.set_model_completion(model_completion);
     try {
         m_eval(e, result);
+         std::cout << result << "\n";
         return true;
     }
     catch (model_evaluator_exception & ex) {
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index 8760d255e..13a790e93 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -22,8 +22,6 @@ Revision History:
 #include"solve_eqs_tactic.h"
 #include"elim_uncnstr_tactic.h"
 #include"qe_tactic.h"
-#include"qe_sat_tactic.h"
-#include"qe_lite.h"
 #include"qsat.h"
 #include"nlqsat.h"
 #include"ctx_simplify_tactic.h"
@@ -54,7 +52,6 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f
                     using_params(mk_simplify_tactic(m), pull_ite_p),
                     solve_eqs,
                     mk_elim_uncnstr_tactic(m),
-                    mk_qe_lite_tactic(m),
                     mk_simplify_tactic(m));    
 }