diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index d837ebb22..eb15910bc 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/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, diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp index 74c909c02..a90d420cb 100644 --- a/src/muz/base/dl_context.cpp +++ b/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(get_engine() != DUALITY_ENGINE) - throw default_exception("operation is not supported by engine"); + if (m_engine.get() && get_engine() != DUALITY_ENGINE) { + throw default_exception("pop operation is only supported by duality engine"); } m_trail.pop_scope(1); } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index e05bed9a7..fbff2e583 100644 --- a/src/qe/nlqsat.cpp +++ b/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
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])) { diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 74b1101fe..e09f87e5f 100644 --- a/src/qe/qsat.cpp +++ b/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; diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 764176ea0..0d7f6a3a6 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -1856,6 +1856,7 @@ namespace smt { ptr_vector m_used_enodes; unsigned m_curr_used_enodes_size; ptr_vector 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 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. - 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 min, max generation of the enodes in m_pattern_instances. - // Return the max generation of the enodes in m_pattern_instances. - unsigned get_max_top_generation() const { + void get_min_max_top_generation(unsigned& min, unsigned& max) { SASSERT(!m_pattern_instances.empty()); - unsigned max = 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 (max < curr) - max = curr; + if (m_min_top_generation.empty()) { + min = max = m_pattern_instances[0]->get_generation(); + m_min_top_generation.push_back(min); + m_max_top_generation.push_back(max); + } + 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(); @@ -2289,8 +2290,10 @@ namespace smt { m_pc = t->get_root(); m_registers[0] = n; m_top = 0; + main_loop: + TRACE("mam_int", display_pc_info(tout);); #ifdef _PROFILE_MAM const_cast(m_pc)->m_counter++; @@ -2497,8 +2500,11 @@ namespace smt { case YIELD1: m_bindings[0] = m_registers[static_cast(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(m_pc)->m_qa, \ static_cast(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 {