fix #3198

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

src/nlsat/nlsat_solver.cpp

@@ -2691,22 +2691,20 @@ namespace nlsat {
                     for (unsigned i = 0; i < sz; ++i) {
                         poly * po = a1.p(i);
                         m_pm.substitute(po, x, q, p, pr);
+                        change |= pr != po;
                         if (m_pm.is_zero(pr)) {
                             ps.reset();
                             even.reset();
-                            change = true;
                             break;
                         }
                         if (m_pm.is_const(pr)) {
                             if (!a1.is_even(i) && m_pm.m().is_neg(m_pm.coeff(pr, 0))) {
                                 k = atom::flip(k);
                             }
-                            change = true;
                             continue;
                         }
                         ps.push_back(pr);                                
                         even.push_back(a1.is_even(i));
-                        change |= pr != po;
                     }        
                     if (!change) continue;
                     literal l = mk_ineq_literal(k, ps.size(), ps.c_ptr(), even.c_ptr()); 

src/smt/smt_model_finder.cpp

@@ -3178,9 +3178,13 @@ namespace smt {
             throw tactic_exception(m_context->get_manager().limit().get_cancel_msg());
     }
 
-    mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) const {
+    mf::quantifier_info * model_finder::get_quantifier_info(quantifier * q) {
-        TRACE("model_finder", tout << q->get_id() << ": " << q << " " << &m_q2info << " " << mk_pp(q, m) << "\n";);
+        mf::quantifier_info* qi = nullptr;
-        return m_q2info[q];
+        if (!m_q2info.find(q, qi)) {
+            register_quantifier(q);
+            qi = m_q2info[q];
+        }
+        return qi;
     }
 
     void model_finder::set_context(context * ctx) {
@@ -3323,9 +3327,8 @@ namespace smt {
         process_auf(qs, m);
     }
 
-    quantifier * model_finder::get_flat_quantifier(quantifier * q) const {
+    quantifier * model_finder::get_flat_quantifier(quantifier * q) {
         quantifier_info * qinfo = get_quantifier_info(q);
-        SASSERT(qinfo);
         return qinfo->get_flat_q();
     }
 
@@ -3334,7 +3337,7 @@ namespace smt {
 
        \remark q is the quantifier before flattening.
     */
-    mf::instantiation_set const * model_finder::get_uvar_inst_set(quantifier * q, unsigned i) const {
+    mf::instantiation_set const * model_finder::get_uvar_inst_set(quantifier * q, unsigned i) {
         quantifier * flat_q = get_flat_quantifier(q);
         SASSERT(flat_q->get_num_decls() >= q->get_num_decls());
         instantiation_set const * r = m_auf_solver->get_uvar_inst_set(flat_q, flat_q->get_num_decls() - q->get_num_decls() + i);
@@ -3346,7 +3349,6 @@ namespace smt {
         // it must have been satisfied by "macro"/"hint".
         quantifier_info * qinfo = get_quantifier_info(q);
         SASSERT(qinfo);
-        SASSERT(qinfo->get_the_one() != nullptr);
         return qinfo->get_macro_based_inst_set(i, m_context, *(m_auf_solver.get()));        
     }
 
@@ -3357,7 +3359,7 @@ namespace smt {
 
        Store in generation the generation of the result
     */
-    expr * model_finder::get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation) const {
+    expr * model_finder::get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation) {
         instantiation_set const * s = get_uvar_inst_set(q, i);
         if (s == nullptr)
             return nullptr;

src/smt/smt_model_finder.h

@@ -93,14 +93,14 @@ namespace smt {
         expr_ref_vector                        m_new_constraints; // new constraints for fresh constants created by the model finder
 
         void restore_quantifiers(unsigned old_size);
-        quantifier_info * get_quantifier_info(quantifier * q) const;
+        quantifier_info * get_quantifier_info(quantifier * q);
         void collect_relevant_quantifiers(ptr_vector<quantifier> & qs) const;
         void cleanup_quantifier_infos(ptr_vector<quantifier> const & qs);
         void process_simple_macros(ptr_vector<quantifier> & qs, ptr_vector<quantifier> & residue, proto_model * m);
         void process_hint_macros(ptr_vector<quantifier> & qs, ptr_vector<quantifier> & residue, proto_model * m);
         void process_non_auf_macros(ptr_vector<quantifier> & qs, ptr_vector<quantifier> & residue, proto_model * m);
         void process_auf(ptr_vector<quantifier> const & qs, proto_model * m);
-        instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i) const;
+        instantiation_set const * get_uvar_inst_set(quantifier * q, unsigned i);
         void checkpoint();
 
 
@@ -116,8 +116,8 @@ namespace smt {
         void init_search_eh();
         void fix_model(proto_model * m);
 
-        quantifier * get_flat_quantifier(quantifier * q) const;
+        quantifier * get_flat_quantifier(quantifier * q);
-        expr * get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation) const;
+        expr * get_inv(quantifier * q, unsigned i, expr * val, unsigned & generation);
         bool restrict_sks_to_inst_set(context * aux_ctx, quantifier * q, expr_ref_vector const & sks);
 
         void restart_eh();

src/smt/smt_quantifier.cpp

@@ -389,6 +389,7 @@ namespace smt {
     quantifier_manager::quantifier_manager(context & ctx, smt_params & fp, params_ref const & p) {
         m_imp = alloc(imp, *this, ctx, fp, mk_default_plugin());
         m_imp->m_plugin->set_manager(*this);
+        
     }
 
     quantifier_manager::~quantifier_manager() {
@@ -399,11 +400,6 @@ namespace smt {
         return m_imp->m_context;
     }
 
-    void quantifier_manager::set_plugin(quantifier_manager_plugin * plugin) {
-        m_imp->m_plugin = plugin;
-        plugin->set_manager(*this);
-    }
-
     void quantifier_manager::add(quantifier * q, unsigned generation) {
         m_imp->add(q, generation);
     }
@@ -564,7 +560,7 @@ namespace smt {
         }
 
         void set_manager(quantifier_manager & qm) override {
-            SASSERT(m_qm == 0);
+            SASSERT(m_qm == nullptr);
             m_qm            = &qm;
             m_context       = &(qm.get_context());
             m_fparams       = &(m_context->get_fparams());
@@ -596,6 +592,7 @@ namespace smt {
            mbqi.id to be instantiated with MBQI. The default value is the
            empty string, so all quantifiers are instantiated. */
         void add(quantifier * q) override {
+            TRACE("model_finder", tout << "add " << q->get_id() << ": " << q << " " << m_fparams->m_mbqi << " " << mbqi_enabled(q) << "\n";);
             if (m_fparams->m_mbqi && mbqi_enabled(q)) {
                 m_active = true;
                 m_model_finder->register_quantifier(q);
@@ -607,26 +604,20 @@ namespace smt {
         void push() override {
             m_mam->push_scope();
             m_lazy_mam->push_scope();
-            if (m_fparams->m_mbqi) {
             m_model_finder->push_scope();            
         }
-        }
 
         void pop(unsigned num_scopes) override {
             m_mam->pop_scope(num_scopes);
             m_lazy_mam->pop_scope(num_scopes);
-            if (m_fparams->m_mbqi) {
             m_model_finder->pop_scope(num_scopes);            
         }
-        }
 
         void init_search_eh() override {
             m_lazy_matching_idx = 0;
-            if (m_fparams->m_mbqi) {
             m_model_finder->init_search_eh();
             m_model_checker->init_search_eh();            
         }
-        }
 
         void assign_eh(quantifier * q) override {
             m_active = true;

src/smt/smt_quantifier.h

@@ -41,8 +41,6 @@ namespace smt {
 
         context & get_context() const;
 
-        void set_plugin(quantifier_manager_plugin * plugin);
-
         void add(quantifier * q, unsigned generation);
         void del(quantifier * q);
         bool empty() const;