Fixing issue #605 rlimit responsiveness in mam

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

src/ast/datatype_decl_plugin.cpp

@@ -462,7 +462,7 @@ func_decl * datatype_decl_plugin::mk_update_field(
     }
     range = domain[0];
     func_decl_info info(m_family_id, k, num_parameters, parameters);
-    return m.mk_func_decl(symbol("update_field"), arity, domain, range, info);
+    return m.mk_func_decl(symbol("update-field"), arity, domain, range, info);
 }
 
 func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 

src/muz/base/dl_context.cpp

@@ -188,9 +188,8 @@ namespace datalog {
         if (m_trail.get_num_scopes() == 0) {
             throw default_exception("there are no backtracking points to pop to");
         }
-        if(m_engine.get()){
+        if (m_engine.get() && get_engine() != DUALITY_ENGINE) {
-            if(get_engine() != DUALITY_ENGINE)
+            throw default_exception("pop operation is only supported by duality engine");
-            throw default_exception("operation is not supported by engine");
         }
         m_trail.pop_scope(1); 
     }

src/qe/nlqsat.cpp

@@ -435,12 +435,11 @@ namespace qe {
         };
 
         class div_rewriter_cfg : public default_rewriter_cfg {
-            nlqsat&       s;
             ast_manager&  m;
             arith_util    a;
             vector<div>   m_divs;
         public:
-            div_rewriter_cfg(nlqsat& s): s(s), m(s.m), a(s.m) {}
+            div_rewriter_cfg(nlqsat& s): m(s.m), a(s.m) {}
             ~div_rewriter_cfg() {}
             br_status reduce_app(func_decl* f, unsigned sz, expr* const* args, expr_ref& result, proof_ref& pr) {
                 if (is_decl_of(f, a.get_family_id(), OP_DIV) && sz == 2 && !a.is_numeral(args[1]) && is_ground(args[0]) && is_ground(args[1])) {

src/qe/qsat.cpp

@@ -503,13 +503,11 @@ namespace qe {
     }
 
     class kernel {
-        ast_manager& m;
         smt_params   m_smtp;
         smt::kernel  m_kernel;
         
     public:
         kernel(ast_manager& m):
-            m(m),
             m_kernel(m, m_smtp)
         {
             m_smtp.m_model = true;

src/smt/mam.cpp

@@ -1856,6 +1856,7 @@ namespace smt {
         ptr_vector<enode>   m_used_enodes;
         unsigned            m_curr_used_enodes_size;
         ptr_vector<enode>   m_pattern_instances; // collect the pattern instances... used for computing min_top_generation and max_top_generation
+        unsigned_vector     m_min_top_generation, m_max_top_generation;
 
         pool<enode_vector>  m_pool;
 
@@ -2034,28 +2035,26 @@ namespace smt {
         // init(t) must be invoked before execute_core
         void execute_core(code_tree * t, enode * n);
 
-        // Return the min generation of the enodes in m_pattern_instances.
+        // Return the min, max generation of the enodes in m_pattern_instances.
-        unsigned get_min_top_generation() const {
-            SASSERT(!m_pattern_instances.empty());
-            unsigned min = m_pattern_instances[0]->get_generation();
-            for (unsigned i = 1; i < m_pattern_instances.size(); i++) {
-                unsigned curr = m_pattern_instances[i]->get_generation();
-                if (min > curr)
-                    min = curr;
-            }
-            return min;
-        }
 
-        // Return the max generation of the enodes in m_pattern_instances.
+        void get_min_max_top_generation(unsigned& min, unsigned& max) {
-        unsigned get_max_top_generation() const {
             SASSERT(!m_pattern_instances.empty());
-            unsigned max = m_pattern_instances[0]->get_generation();
+            if (m_min_top_generation.empty()) {
-            for (unsigned i = 1; i < m_pattern_instances.size(); i++) {
+                min = max = m_pattern_instances[0]->get_generation();
-                unsigned curr = m_pattern_instances[i]->get_generation();
+                m_min_top_generation.push_back(min);
-                if (max < curr)
+                m_max_top_generation.push_back(max);
-                    max = curr;
+            }
+            else {
+                min = m_min_top_generation.back();
+                max = m_max_top_generation.back();
+            }
+            for (unsigned i = m_min_top_generation.size(); i < m_pattern_instances.size(); ++i) {
+                unsigned curr = m_pattern_instances[i]->get_generation();
+                min = std::min(min, curr);
+                m_min_top_generation.push_back(min);
+                max = std::max(max, curr);
+                m_max_top_generation.push_back(max);
             }
-            return max;
         }
     };
 
@@ -2278,6 +2277,8 @@ namespace smt {
         TRACE("mam_execute_core", tout << "EXEC " << t->get_root_lbl()->get_name() << "\n";);
         SASSERT(m_context.is_relevant(n));
         m_pattern_instances.reset();
+        m_min_top_generation.reset();
+        m_max_top_generation.reset();
         m_pattern_instances.push_back(n);
         m_max_generation = n->get_generation();
 
@@ -2290,7 +2291,9 @@ namespace smt {
         m_registers[0]   = n;
         m_top            = 0;
 
+        
     main_loop:
+
         TRACE("mam_int", display_pc_info(tout););
 #ifdef _PROFILE_MAM
         const_cast<instruction*>(m_pc)->m_counter++;
@@ -2497,8 +2500,11 @@ namespace smt {
 
         case YIELD1:
             m_bindings[0] = m_registers[static_cast<const yield *>(m_pc)->m_bindings[0]];
-#define ON_MATCH(NUM)                                                                                   \
+#define ON_MATCH(NUM)                                                   \
             m_max_generation = std::max(m_max_generation, get_max_generation(NUM, m_bindings.begin())); \
+            if (m_context.get_cancel_flag()) {                          \
+                return;                                                 \
+            }                                                           \
             m_mam.on_match(static_cast<const yield *>(m_pc)->m_qa,                                      \
                            static_cast<const yield *>(m_pc)->m_pat,                                     \
                            NUM,                                                                         \
@@ -2770,9 +2776,12 @@ namespace smt {
                 if (m_app->get_num_args() == c->m_num_args && m_context.is_relevant(m_app)) {
                     // update the pattern instance
                     SASSERT(!m_pattern_instances.empty());
+                    if (m_pattern_instances.size() == m_max_top_generation.size()) {
+                        m_max_top_generation.pop_back();
+                        m_min_top_generation.pop_back();
+                    }
                     m_pattern_instances.pop_back();
                     m_pattern_instances.push_back(m_app);
-                    
                     // continue succeeded
                     update_max_generation(m_app);
                     TRACE("mam_int", tout << "continue next candidate:\n" << mk_ll_pp(m_app->get_owner(), m_ast_manager););
@@ -3932,7 +3941,9 @@ namespace smt {
                 SASSERT(bindings[i]->get_generation() <= max_generation);
             }
 #endif
-            m_context.add_instance(qa, pat, num_bindings, bindings, max_generation, m_interpreter.get_min_top_generation(), m_interpreter.get_max_top_generation(), used_enodes);
+            unsigned min_gen, max_gen;
+            m_interpreter.get_min_max_top_generation(min_gen, max_gen);
+            m_context.add_instance(qa, pat, num_bindings, bindings, max_generation, min_gen, max_gen, used_enodes);
         }
 
         virtual bool is_shared(enode * n) const {