remove also second hash-table for ALIVE_OPT #4747

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/expr_safe_replace.cpp

@@ -27,9 +27,13 @@ Revision History:
 
 void expr_safe_replace::insert(expr* src, expr* dst) {
     SASSERT(m.get_sort(src) == m.get_sort(dst));
+#if ALIVE_OPT
+    cache_insert(src, dst);
+#else
     m_src.push_back(src);
     m_dst.push_back(dst);
     m_subst.insert(src, dst);
+#endif
 }
 
 void expr_safe_replace::operator()(expr_ref_vector& es) {
@@ -69,10 +73,12 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
         if (cache_find(a)) {
             m_todo.pop_back();
         }
+#if !ALIVE_OPT
         else if (m_subst.find(a, b)) {
             cache_insert(a, b);
             m_todo.pop_back();            
         }
+#endif
         else if (is_var(a)) {
             cache_insert(a, a);
             m_todo.pop_back();
@@ -150,6 +156,7 @@ void expr_safe_replace::reset() {
     m_src.reset();
     m_dst.reset();
     m_subst.reset();
+    m_refs.reset();
 }
 
 void expr_safe_replace::apply_substitution(expr* s, expr* def, expr_ref& t) {

src/math/lp/nla_core.cpp

@@ -1500,7 +1500,7 @@ lbool core::check(vector<lemma>& l_vec) {
 
     if (l_vec.empty() && !done() && m_nla_settings.run_nra()) {
         ret = m_nra.check();
-        m_stats.m_nra_calls ++;
+        m_stats.m_nra_calls++;
     }
     
     if (ret == l_undef && !l_vec.empty() && m_reslim.inc()) 

src/math/lp/nra_solver.cpp

@@ -85,7 +85,7 @@ struct solver::imp {
                 throw;
             }
         }
-        TRACE("arith", 
+        TRACE("nra", 
               m_nlsat->display(tout << r << "\n");
               display(tout); 
               for (auto kv : m_lp2nl) 

src/smt/qi_queue.cpp

@@ -193,6 +193,9 @@ namespace smt {
     }
 
     void qi_queue::instantiate(entry & ent) {
+        // set temporary flag to enable quantifier-specific tracing in within smt_internalizer.
+        flet<bool> _coming_from_quant(m_context.m_coming_from_quant, true);
+
         fingerprint * f          = ent.m_qb;
         quantifier * q           = static_cast<quantifier*>(f->get_data());
         unsigned generation      = ent.m_generation;
@@ -200,12 +203,14 @@ namespace smt {
         enode * const * bindings = f->get_args();
 
         ent.m_instantiated = true;
-
+        
+        std::cout << mk_pp(q, m) << "\n";
+        for (unsigned i = 0; i < num_bindings; ++i)
+            std::cout << mk_pp(bindings[i]->get_owner(), m) << " ";
+        std::cout << "\n";
+        
         TRACE("qi_queue_profile", tout << q->get_qid() << ", gen: " << generation << " " << *f << " cost: " << ent.m_cost << "\n";);
-        // NEVER remove coming_from_quant
+
-        // "coming_from_quant" allows the logging of bindings and enodes
-        // only when they come from instantiations
-        enable_trace("coming_from_quant");
         quantifier_stat * stat = m_qm.get_stat(q);
 
         if (m_checker.is_sat(q->get_expr(), num_bindings, bindings)) {
@@ -216,7 +221,6 @@ namespace smt {
             // a dummy instantiation is still an instantiation.
             // in this way smt.qi.profile=true coincides with the axiom profiler
             stat->inc_num_instances_checker_sat();
-            disable_trace("coming_from_quant");
             return;
         }
 
@@ -241,7 +245,6 @@ namespace smt {
                 m.trace_stream() << "[end-of-instance]\n";
             }
 
-            disable_trace("coming_from_quant");
             return;
         }
         TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";);
@@ -329,8 +332,6 @@ namespace smt {
         if (m.has_trace_stream())
             m.trace_stream() << "[end-of-instance]\n";
 
-        // NEVER remove coming_from_quant
-        disable_trace("coming_from_quant");
     }
 
     void qi_queue::push_scope() {

src/smt/smt_context.h

@@ -585,6 +585,12 @@ namespace smt {
             return get_bdata(v).get_theory();
         }
 
+        /** 
+         * flag to toggle quantifier tracing.
+         */
+        bool m_coming_from_quant { false };
+
+
         friend class set_var_theory_trail;
         void set_var_theory(bool_var v, theory_id tid);
 

src/smt/smt_internalizer.cpp

@@ -1014,7 +1014,7 @@ namespace smt {
                   tout << "is_true_eq: " << e->is_true_eq() << " in cg_table: " << m_cg_table.contains_ptr(e) << " is_cgr: "
                        << e->is_cgr() << "\n";
               });
-        SCTRACE("causality", is_trace_enabled("coming_from_quant"), tout << "EN: #" << e->get_owner_id() << "\n";);
+        SCTRACE("causality", m_coming_from_quant, tout << "EN: #" << e->get_owner_id() << "\n";);
 
         if (m.has_trace_stream())
             m.trace_stream() << "[attach-enode] #" << n->get_id() << " " << m_generation << "\n";