From 134562162a03f57eddd9433e765c6ba86f99480e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Jul 2021 13:50:21 -0700
Subject: [PATCH] #5420

---
 src/sat/smt/q_solver.cpp | 82 ++++++++++------------------------------
 1 file changed, 19 insertions(+), 63 deletions(-)

diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 524c3f1c6..23276a3f1 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -40,34 +40,25 @@ namespace q {
             return;
         quantifier* q = to_quantifier(e);
 
-        auto const& exp = expand(q);
-        if (exp.size() > 1 && is_forall(q) && !l.sign()) {
-            for (expr* e : exp) {
-                sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
-                add_clause(~l, lit);                    
-                ctx.add_aux(~l, lit);
-            }
-            return;
-        }
-        if (exp.size() > 1 && is_exists(q) && l.sign()) {
-            sat::literal_vector lits;
-            lits.push_back(~l);
-            for (expr* e : exp)
-                lits.push_back(ctx.internalize(e, l.sign(), false, false));
-            add_clause(lits);
-            ctx.add_aux(lits);
-            return;
-        }
-
         if (l.sign() == is_forall(e)) {
             sat::literal lit = skolemize(q);
             add_clause(~l, lit);
             ctx.add_root(~l, lit);
         }
         else {
-            ctx.push_vec(m_universal, l);
-            if (ctx.get_config().m_ematching)
-                m_ematch.add(q);
+            auto const& exp = expand(q);
+            if (exp.size() > 1) {
+                for (expr* e : exp) {
+                    sat::literal lit = ctx.internalize(e, l.sign(), false, false); 
+                    add_clause(~l, lit);                    
+                    ctx.add_aux(~l, lit);
+                }
+            }
+            else {
+                ctx.push_vec(m_universal, l);
+                if (ctx.get_config().m_ematching)
+                    m_ematch.add(q);
+            }
         }
         m_stats.m_num_quantifier_asserts++;
     }
@@ -146,9 +137,9 @@ namespace q {
     }
 
     /*
-    * Find initial values to instantiate quantifier with so to make it as hard as possible for solver
-    * to find values to free variables. 
-    */
+     * Find initial values to instantiate quantifier with so to make it as hard as possible for solver
+     * to find values to free variables. 
+     */
     sat::literal solver::specialize(quantifier* q) {
         std::function<expr* (quantifier*, unsigned)> mk_var = [&](quantifier* q, unsigned i) {
             return get_unit(q->get_decl_sort(i));
@@ -243,46 +234,11 @@ namespace q {
                 ctx.get_rewriter()(tmp);
                 m_expanded[i] = tmp;
             }
-            return m_expanded;
         }
-
-#if 0
-        m_expanded.reset();
-        m_expanded2.reset();
-        if (is_forall(q)) 
-            flatten_or(q->get_expr(), m_expanded2);
-        else if (is_exists(q)) 
-            flatten_and(q->get_expr(), m_expanded2);
-        else
-            UNREACHABLE();
-        for (unsigned i = m_expanded2.size(); i-- > 0; ) {
-            expr* lit = m_expanded2.get(i);
-            if (!is_ground(lit) && is_and(lit) && is_forall(q)) {
-
-                // get free vars of lit
-                // create fresh predicate over free vars
-                // replace in expanded, pack and push on m_expanded
-                
-                expr_ref p(m);
-                // TODO introduce fresh p.
-                flatten_and(lit, m_expanded);
-                for (unsigned i = m_expanded.size(); i-- > 0; ) {
-                    tmp = m.mk_or(m.mk_not(p), m_expanded.get(i));
-                    expr_ref tmp(m.update_quantifier(q, tmp), m);
-                    ctx.get_rewriter()(tmp);
-                    m_expanded[i] = tmp;
-                }
-                m_expanded2[i] = p;
-                tmp = m.mk_or(m_expanded2);
-                expr_ref tmp(m.update_quantifier(q, tmp), m);
-                ctx.get_rewriter()(tmp);                
-                m_expanded.push_back(tmp);
-                return m_expanded;
-            }
+        else {
+            m_expanded.reset();
+            m_expanded.push_back(q);
         }
-#endif
-        m_expanded.reset();
-        m_expanded.push_back(q);
         return m_expanded;
     }