From 8a229bf684b1e2abc2276814a03182a36a8c6e96 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jan 2021 22:39:02 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- scripts/nightly.yaml | 4 ++-- src/ast/ast.h | 7 ++---- src/ast/euf/euf_egraph.cpp | 1 + src/sat/smt/q_ematch.cpp | 44 ++++++++++++++++++++++++++------------ src/sat/smt/q_ematch.h | 5 +++++ src/sat/smt/q_mam.cpp | 5 ++--- src/sat/smt/q_solver.cpp | 1 + 7 files changed, 43 insertions(+), 24 deletions(-) diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 8ef347436..1e4452b45 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -52,8 +52,8 @@ stages: ./ml_example cd .. - template: generate-doc.yml - - script: zip -r api.zip doc/api - - script: cp html.zip $(Build.ArtifactStagingDirectory)/. + - script: zip -r api.zip doc/api + - script: cp api.zip $(Build.ArtifactStagingDirectory)/. - task: PublishPipelineArtifact@0 inputs: artifactName: 'UbuntuDoc' diff --git a/src/ast/ast.h b/src/ast/ast.h index 8ca59ffb3..38b7280fd 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2597,11 +2597,8 @@ public: } void reset() { - ast * const * it = m_to_unmark.c_ptr(); - ast * const * end = it + m_to_unmark.size(); - for (; it != end; ++it) { - reset_mark(*it); - } + for (ast * a : m_to_unmark) + reset_mark(a); m_to_unmark.reset(); } diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 75b822b11..a1e83cb46 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -52,6 +52,7 @@ namespace euf { m_tmp_node->m_args[i] = args[i]; m_tmp_node->m_num_args = n; m_tmp_node->m_expr = e; + m_tmp_node->m_table_id = UINT_MAX; return m_table.find(m_tmp_node); } diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index f66756ccd..0986fcfd1 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -37,6 +37,12 @@ Todo: namespace q { + struct ematch::scoped_mark_reset { + ematch& e; + scoped_mark_reset(ematch& e): e(e) {} + ~scoped_mark_reset() { e.m_mark.reset(); } + }; + ematch::ematch(euf::solver& ctx, solver& s): ctx(ctx), m_qs(s), @@ -108,7 +114,7 @@ namespace q { void ematch::init_watch(expr* e, unsigned clause_idx) { ptr_buffer todo; - m_mark.reset(); + scoped_mark_reset _sr(*this); todo.push_back(e); while (!todo.empty()) { expr* t = todo.back(); @@ -155,17 +161,21 @@ namespace q { ctx.push(push_back_vector>(c.m_bindings)); } + std::ostream& ematch::clause::display(std::ostream& out) const { + out << "clause:\n"; + for (auto const& lit : m_lits) + out << lit.lhs << (lit.sign ? " != " : " == ") << lit.rhs << "\n"; + return out; + } + bool ematch::propagate(euf::enode* const* binding, clause& c) { + TRACE("q", c.display(tout) << "\n";); unsigned clause_idx = m_q2clauses[c.m_q]; - struct scoped_reset { - ematch& e; - scoped_reset(ematch& e): e(e) { e.m_mark.reset(); } - ~scoped_reset() { e.m_mark.reset(); } - }; - scoped_reset _sr(*this); + scoped_mark_reset _sr(*this); unsigned idx = UINT_MAX; - for (unsigned i = c.m_lits.size(); i-- > 0; ) { + unsigned sz = c.m_lits.size(); + for (unsigned i = 0; i < sz; ++i) { lit l = c.m_lits[i]; m_indirect_nodes.reset(); lbool cmp = compare(binding, l.lhs, l.rhs); @@ -185,6 +195,7 @@ namespace q { } break; case l_undef: + TRACE("q", tout << l.lhs << " ~~ " << l.rhs << " is undef\n";); if (idx == 0) { // attach bindings and indirect nodes // to watch @@ -228,6 +239,7 @@ namespace q { } lbool ematch::compare(euf::enode* const* binding, expr* s, expr* t) { + TRACE("q", tout << mk_pp(s, m) << " ~~ " << mk_pp(t, m) << "\n";); euf::enode* sn = eval(binding, s); euf::enode* tn = eval(binding, t); lbool c; @@ -284,8 +296,9 @@ namespace q { } euf::enode* ematch::eval(euf::enode* const* binding, expr* e) { + TRACE("q", tout << mk_pp(e, m) << "\n";); if (is_ground(e)) - ctx.get_egraph().find(e)->get_root(); + return ctx.get_egraph().find(e)->get_root(); if (m_mark.is_marked(e)) return m_eval[e->get_id()]; ptr_buffer todo; @@ -315,7 +328,7 @@ namespace q { args.reset(); for (expr* arg : *to_app(t)) { if (m_mark.is_marked(arg)) - args.push_back(m_eval[t->get_id()]); + args.push_back(m_eval[arg->get_id()]); else todo.push_back(arg); } @@ -333,10 +346,12 @@ namespace q { } void ematch::insert_to_propagate(unsigned node_id) { + m_node_in_queue.assure_domain(node_id); if (m_node_in_queue.contains(node_id)) return; m_node_in_queue.insert(node_id); for (unsigned idx : m_watch[node_id]) { + m_clause_in_queue.assure_domain(idx); if (!m_clause_in_queue.contains(idx)) { m_clause_in_queue.insert(idx); m_queue.push_back(idx); @@ -418,6 +433,7 @@ namespace q { }; void ematch::add(quantifier* q) { + TRACE("q", tout << "add " << mk_pp(q, m) << "\n";); clause* c = clausify(q); ensure_ground_enodes(*c); unsigned idx = m_clauses.size(); @@ -437,9 +453,9 @@ namespace q { app * mp = to_app(q->get_pattern(i)); SASSERT(m.is_pattern(mp)); bool unary = (mp->get_num_args() == 1); - TRACE("quantifier", tout << "adding:\n" << expr_ref(mp, m) << "\n";); + TRACE("q", tout << "adding:\n" << expr_ref(mp, m) << "\n";); if (!unary && j >= num_eager_multi_patterns) { - TRACE("quantifier", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";); + TRACE("q", tout << "delaying (too many multipatterns):\n" << mk_ismt2_pp(mp, m) << "\n";); if (!m_lazy_mam) m_lazy_mam = mam::mk(ctx, *this); m_lazy_mam->add_pattern(q, mp); @@ -462,8 +478,8 @@ namespace q { // // TODO: loop over pending bindings and instantiate them // - NOT_IMPLEMENTED_YET(); - return false; + // NOT_IMPLEMENTED_YET(); + return true; } } diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h index ce36383f8..a5af4e5b5 100644 --- a/src/sat/smt/q_ematch.h +++ b/src/sat/smt/q_ematch.h @@ -69,8 +69,11 @@ namespace q { ptr_vector m_bindings; ptr_vector const& bindings() { return m_bindings; } + std::ostream& display(std::ostream& out) const; + }; + struct pop_clause; euf::solver& ctx; @@ -83,6 +86,8 @@ namespace q { stats m_stats; expr_fast_mark1 m_mark; + struct scoped_mark_reset; + nat_set m_node_in_queue; nat_set m_clause_in_queue; unsigned m_qhead { 0 }; diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 813100cc5..2a4dbc19e 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -415,7 +415,7 @@ namespace q { instruction * m_root; enode_vector m_candidates; #ifdef Z3DEBUG - egraph * m_egraph; + egraph * m_egraph; ptr_vector m_patterns; #endif #ifdef _PROFILE_MAM @@ -3837,8 +3837,7 @@ namespace q { #endif unsigned min_gen = 0, max_gen = 0; m_interpreter.get_min_max_top_generation(min_gen, max_gen); - UNREACHABLE(); - // m_ematch.on_binding(qa, pat, bindings); // max_generation); // , min_gen, max_gen; + m_ematch.on_binding(qa, pat, bindings); // max_generation); // , min_gen, max_gen; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 9054a76c7..2351c1aa3 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -87,6 +87,7 @@ namespace q { } bool solver::unit_propagate() { + TRACE("q", tout << "propagate\n";); return ctx.get_config().m_ematching && m_ematch.propagate(); }