diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 557f314a4..cba9e13b6 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -1935,3 +1935,6 @@ void core::collect_statistics(::statistics & st) { } // end of nla + +template void nla::intervals::set_var_interval(lpvar v, nla::intervals::interval& b); +template void nla::intervals::set_var_interval(lpvar v, nla::intervals::interval& b); diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index 9cc7b4baa..fa013c553 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -51,41 +51,38 @@ namespace q { struct remove_binding; struct insert_binding; - - binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top); - void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top); - - sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); - struct pop_clause; struct scoped_mark_reset; - euf::solver& ctx; - solver& m_qs; - ast_manager& m; - eval m_eval; - quantifier_stat_gen m_qstat_gen; - fingerprints m_fingerprints; - scoped_ptr m_tmp_binding; - unsigned m_tmp_binding_capacity { 0 }; - queue m_inst_queue; - pattern_inference_rw m_infer_patterns; - scoped_ptr m_mam, m_lazy_mam; - ptr_vector m_clauses; - obj_map m_q2clauses; - vector m_watch; // expr_id -> clause-index* - stats m_stats; - expr_fast_mark1 m_mark; - unsigned m_generation_propagation_threshold{ 3 }; + euf::solver& ctx; + solver& m_qs; + ast_manager& m; + eval m_eval; + quantifier_stat_gen m_qstat_gen; + fingerprints m_fingerprints; + scoped_ptr m_tmp_binding; + unsigned m_tmp_binding_capacity { 0 }; + queue m_inst_queue; + pattern_inference_rw m_infer_patterns; + scoped_ptr m_mam, m_lazy_mam; + ptr_vector m_clauses; + obj_map m_q2clauses; + vector m_watch; // expr_id -> clause-index* + stats m_stats; + expr_fast_mark1 m_mark; + unsigned m_generation_propagation_threshold{ 3 }; + ptr_vector m_ground; + nat_set m_node_in_queue; + nat_set m_clause_in_queue; + unsigned m_qhead { 0 }; + unsigned_vector m_clause_queue; + binding* alloc_binding(unsigned n, app* pat, unsigned max_generation, unsigned min_top, unsigned max_top); + void add_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top); - nat_set m_node_in_queue; - nat_set m_clause_in_queue; - unsigned m_qhead { 0 }; - unsigned_vector m_clause_queue; + sat::ext_justification_idx mk_justification(unsigned idx, clause& c, euf::enode* const* b); - ptr_vector m_ground; void ensure_ground_enodes(expr* e); void ensure_ground_enodes(clause const& c); @@ -126,12 +123,15 @@ namespace q { // callback from mam void on_binding(quantifier* q, app* pat, euf::enode* const* binding, unsigned max_generation, unsigned min_gen, unsigned max_gen); - // callback from queue + // callbacks from queue lbool evaluate(euf::enode* const* binding, clause& c) { return m_eval(binding, c); } + void add_instantiation(clause& c, binding& b, sat::literal lit); + bool propagate(euf::enode* const* binding, unsigned max_generation, clause& c); std::ostream& display(std::ostream& out) const; + std::ostream& display_constraint(std::ostream& out, sat::ext_constraint_idx idx) const; }; diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index efc5fa6f9..53953398f 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -497,7 +497,7 @@ namespace q { m_num_regs(num_args + 1), m_num_choices(0), m_root(nullptr) { - DEBUG_CODE(m_egraph = 0;); + DEBUG_CODE(m_egraph = nullptr;); #ifdef _PROFILE_MAM m_counter = 0; #endif @@ -566,7 +566,7 @@ namespace q { #ifdef Z3DEBUG void set_egraph(egraph * ctx) { - SASSERT(m_egraph == 0); + SASSERT(m_egraph == nullptr); m_egraph = ctx; } @@ -3772,8 +3772,7 @@ namespace q { } std::ostream& display(std::ostream& out) override { - out << "mam:\n"; - m_lbl_hasher.display(out); + m_lbl_hasher.display(out << "mam:\n"); for (auto* t : m_trees) if (t) t->display(out); @@ -3783,7 +3782,6 @@ namespace q { void propagate() override { TRACE("trigger_bug", tout << "match\n"; display(tout);); for (code_tree* t : m_to_match) { - std::cout << t << "\n"; SASSERT(t->has_candidates()); m_interpreter.execute(t); t->reset_candidates(); diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp index 61a13ea98..fc1a5249f 100644 --- a/src/sat/smt/q_queue.cpp +++ b/src/sat/smt/q_queue.cpp @@ -34,7 +34,11 @@ namespace q { m_parser(m), m_evaluator(m), m_subst(m) - {} + { + init_parser_vars(); + m_vals.resize(15, 0.0f); + setup(); + } void queue::setup() { TRACE("q", tout << "qi_cost: " << m_params.m_qi_cost << "\n";); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 5f508829c..4aa900e76 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -81,8 +81,9 @@ namespace q { } void solver::collect_statistics(statistics& st) const { - st.update("quantifier asserts", m_stats.m_num_quantifier_asserts); + st.update("q asserts", m_stats.m_num_quantifier_asserts); m_mbqi.collect_statistics(st); + m_ematch.collect_statistics(st); } euf::th_solver* solver::clone(euf::solver& ctx) {