From b8a437bd8a69de54d1d0ad013bfae50ca069d337 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 29 Jul 2021 15:04:49 -0700
Subject: [PATCH] #5429

relevancy propagation applies to quantifier unfolding.
---
 src/ast/ast_ll_pp.cpp               | 30 +++++++++++++++----------
 src/ast/normal_forms/pull_quant.cpp |  6 ++---
 src/ast/recfun_decl_plugin.cpp      |  2 --
 src/sat/smt/euf_relevancy.cpp       |  3 +--
 src/sat/smt/euf_solver.cpp          | 10 ++++-----
 src/sat/smt/q_mbi.cpp               |  7 +++---
 src/sat/smt/sat_dual_solver.cpp     | 35 +++++++++++++++++++++--------
 src/sat/smt/sat_dual_solver.h       |  3 +++
 8 files changed, 60 insertions(+), 36 deletions(-)

diff --git a/src/ast/ast_ll_pp.cpp b/src/ast/ast_ll_pp.cpp
index f7ba8132f..de6efe020 100644
--- a/src/ast/ast_ll_pp.cpp
+++ b/src/ast/ast_ll_pp.cpp
@@ -248,8 +248,7 @@ public:
         }
     }
 
-    void operator()(quantifier * n) {
-        display_def_header(n);
+    void display_quantifier_header(quantifier* n) {
         m_out << "(" << (n->get_kind() == forall_k ? "forall" : (n->get_kind() == exists_k ? "exists" : "lambda")) << " ";
         unsigned num_decls = n->get_num_decls();
         m_out << "(vars ";
@@ -272,6 +271,12 @@ public:
             display_children(n->get_num_no_patterns(), n->get_no_patterns());
             m_out << ") ";
         }
+
+  }
+
+    void operator()(quantifier * n) {
+        display_def_header(n);
+        display_quantifier_header(n);
         display_child(n->get_expr());
         m_out << ")\n";
     }
@@ -281,6 +286,12 @@ public:
             m_out << "(:var " << to_var(n)->get_idx() << ")";
             return;
         }
+        if (is_quantifier(n)) {
+            display_quantifier_header(to_quantifier(n));
+            display(to_quantifier(n)->get_expr(), depth - 1);
+            m_out << ")";
+            return;
+        }
 
         if (!is_app(n) || depth == 0 || to_app(n)->get_num_args() == 0) {
             display_child(n);
@@ -304,16 +315,11 @@ public:
 
     void display_bounded(ast * n, unsigned depth) {
         if (!n)
-   	     m_out << "null";    
-        else if (is_app(n)) {
-            display(to_expr(n), depth);
-        }
-        else if (is_var(n)) {
-            m_out << "(:var " << to_var(n)->get_idx() << ")";
-        }
-        else {
-            m_out << "#" << n->get_id();
-        }
+            m_out << "null";    
+        else if (is_expr(n)) 
+            display(to_expr(n), depth);               
+        else 
+            m_out << "#" << n->get_id();        
     }
 };
 
diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp
index 209772f3b..8a94a3482 100644
--- a/src/ast/normal_forms/pull_quant.cpp
+++ b/src/ast/normal_forms/pull_quant.cpp
@@ -281,9 +281,9 @@ struct pull_quant::imp {
                     m.mk_rewrite(old_q, result);
                 return true;
             }
-            if (is_lambda(old_q)) {
-                return false;
-            }
+
+            if (is_lambda(old_q)) 
+                return false;            
 
             if (!is_forall(new_body))
                 return false;
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 04c5d0545..a702b4bfd 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -336,7 +336,6 @@ namespace recfun {
         return alloc(def, m(), m_fid, name, n, domain, range, is_generated);
     }
 
-
     void util::set_definition(replace& subst, promise_def & d, bool is_macro, unsigned n_vars, var * const * vars, expr * rhs) {
         expr_ref rhs1(rhs, m());
         if (!is_macro)
@@ -531,7 +530,6 @@ namespace recfun {
             }
             return result;
         }
-
     }
 
     case_expansion::case_expansion(recfun::util& u, app * n) : 
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 7e9b20af7..28ac99d9a 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -48,8 +48,7 @@ namespace euf {
         if (!relevancy_enabled())
             return;
         ensure_dual_solver();
-        if (s().at_search_lvl())
-            m_dual_solver->add_root(n, lits);
+        m_dual_solver->add_root(n, lits);
     }
 
     void solver::add_aux(unsigned n, sat::literal const* lits) {
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 295216ef9..781a94c85 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -489,6 +489,8 @@ namespace euf {
         for (auto* e : m_solvers)
             e->push();
         m_egraph.push();
+        if (m_dual_solver)
+            m_dual_solver->push();
     }
 
     void solver::pop(unsigned n) {
@@ -506,20 +508,18 @@ namespace euf {
         }
         m_var_trail.shrink(sc.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
+        if (m_dual_solver)
+            m_dual_solver->pop(n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
         TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
     }
 
     void solver::user_push() {
-        push();
-        if (m_dual_solver)
-            m_dual_solver->push();        
+        push();      
     }
 
     void solver::user_pop(unsigned n) {
         pop(n);
-        if (m_dual_solver)
-            m_dual_solver->pop(n);
     }
 
     void solver::start_reinit(unsigned n) {
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 03d748236..c7ed4913a 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -66,10 +66,11 @@ namespace q {
             }
         }
         m_max_cex += ctx.get_config().m_mbqi_max_cexs;
-        for (auto p : m_instantiations) {
-            unsigned generation = std::get<2>(p);
+        for (auto [qlit, fml, generation] : m_instantiations) {
             euf::solver::scoped_generation sg(ctx, generation + 1);
-            m_qs.add_clause(~std::get<0>(p), ~ctx.mk_literal(std::get<1>(p)));
+            sat::literal lit = ctx.mk_literal(fml);
+            m_qs.add_clause(~qlit, ~lit);
+            ctx.add_root(~qlit, ~lit);
         }
         m_instantiations.reset();
         return result;
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 6676603bc..1e2068707 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -28,15 +28,28 @@ namespace sat {
         SASSERT(!m_solver.get_config().m_drat);
     }
 
-    void dual_solver::push() {
-        m_solver.user_push(); 
-        m_roots.push_scope();
-        m_tracked_vars.push_scope();
-        m_units.push_scope();
-        m_vars.push_scope();
+    void dual_solver::flush() {
+        while (m_num_scopes > 0) {
+            m_solver.user_push();
+            m_roots.push_scope();
+            m_tracked_vars.push_scope();
+            m_units.push_scope();
+            m_vars.push_scope();
+            --m_num_scopes;
+        }
     }
 
-    void dual_solver::pop(unsigned num_scopes) {
+    void dual_solver::push() {
+        ++m_num_scopes;
+    }
+
+    void dual_solver::pop(unsigned num_scopes) {        
+        if (m_num_scopes >= num_scopes) {
+            m_num_scopes -= num_scopes;
+            return;
+        }
+        num_scopes -= m_num_scopes;
+        m_num_scopes = 0;
         m_solver.user_pop(num_scopes);
         unsigned old_sz = m_tracked_vars.old_size(num_scopes);
         for (unsigned i = m_tracked_vars.size(); i-- > old_sz; )
@@ -66,6 +79,7 @@ namespace sat {
     }
 
     void dual_solver::track_relevancy(bool_var w) {
+        flush();
         bool_var v = ext2var(w);
         if (!m_is_tracked.get(v, false)) {
             m_is_tracked.setx(v, true, false);
@@ -81,7 +95,8 @@ namespace sat {
         return literal(m_var2ext[lit.var()], lit.sign());
     }
 
-    void dual_solver::add_root(unsigned sz, literal const* clause) {        
+    void dual_solver::add_root(unsigned sz, literal const* clause) {      
+        flush();
         if (sz == 1) {
             TRACE("dual", tout << "unit: " << clause[0] << "\n";);
             m_units.push_back(clause[0]);
@@ -95,6 +110,7 @@ namespace sat {
     }
 
     void dual_solver::add_aux(unsigned sz, literal const* clause) {
+        flush();
         TRACE("dual", tout << "aux: " << literal_vector(sz, clause) << "\n";);
         m_lits.reset();
         for (unsigned i = 0; i < sz; ++i) 
@@ -103,6 +119,7 @@ namespace sat {
     }
 
     void dual_solver::add_assumptions(solver const& s) {
+        flush();
         m_lits.reset();
         for (bool_var v : m_tracked_vars)
             m_lits.push_back(literal(v, l_false == s.value(m_var2ext[v])));
@@ -113,7 +130,7 @@ namespace sat {
         }
     }
 
-    bool dual_solver::operator()(solver const& s) {
+    bool dual_solver::operator()(solver const& s) {        
         m_core.reset();
         m_core.append(m_units);
         if (m_roots.empty())
diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h
index 2b040128c..9c9b2568e 100644
--- a/src/sat/smt/sat_dual_solver.h
+++ b/src/sat/smt/sat_dual_solver.h
@@ -35,6 +35,7 @@ namespace sat {
         unsigned_vector m_ext2var;
         unsigned_vector m_var2ext;
         lim_svector<unsigned> m_vars;
+        unsigned        m_num_scopes = 0;
         void add_literal(literal lit);
 
         bool_var ext2var(bool_var v);
@@ -46,6 +47,8 @@ namespace sat {
 
         std::ostream& display(solver const& s, std::ostream& out) const;
 
+        void flush();
+
     public:
         dual_solver(reslimit& l);
         void push();