From 469f6187428c11aa8408dd8651dfe7aba7a452d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 18 Dec 2019 13:48:27 -0800 Subject: [PATCH] build dependencies, invariant annotation Signed-off-by: Nikolaj Bjorner --- scripts/mk_project.py | 2 +- src/math/dd/dd_pdd.cpp | 34 ++++++++++++++++-- src/math/dd/dd_pdd.h | 21 +++++++---- src/math/grobner/CMakeLists.txt | 1 + src/math/grobner/pdd_grobner.cpp | 60 +++++++++++++++++++++++++------- src/math/grobner/pdd_grobner.h | 19 ++++++---- 6 files changed, 108 insertions(+), 29 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index ad6e3e32b..93ceab484 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -33,7 +33,7 @@ def init_project_def(): add_lib('tactic', ['ast', 'model']) add_lib('substitution', ['ast', 'rewriter'], 'ast/substitution') add_lib('parser_util', ['ast'], 'parsers/util') - add_lib('grobner', ['ast'], 'math/grobner') + add_lib('grobner', ['ast', 'dd'], 'math/grobner') add_lib('euclid', ['util'], 'math/euclid') add_lib('proofs', ['rewriter', 'util'], 'ast/proofs') add_lib('solver', ['model', 'tactic', 'proofs']) diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp index 858552ffb..6359302d5 100644 --- a/src/math/dd/dd_pdd.cpp +++ b/src/math/dd/dd_pdd.cpp @@ -35,7 +35,7 @@ namespace dd { imk_val(rational::zero()); // becomes pdd_zero imk_val(rational::one()); // becomes pdd_one for (unsigned i = 2; i <= pdd_no_op + 2; ++i) { - m_nodes.push_back(pdd_node(0,0,0)); + m_nodes.push_back(pdd_node(0,0,0,0)); m_nodes.back().m_refcount = max_rc; m_nodes.back().m_index = m_nodes.size()-1; } @@ -388,6 +388,9 @@ namespace dd { } } + double pdd_manager::tree_size(pdd const& p) const { return tree_size(p.root); } + + void pdd_manager::push(PDD b) { m_pdd_stack.push_back(b); } @@ -440,7 +443,7 @@ namespace dd { if (is_zero(h)) return l; SASSERT(is_val(l) || level(l) <= lvl); SASSERT(is_val(h) || level(h) <= lvl); - pdd_node n(lvl, l, h); + pdd_node n(lvl, l, h, tree_size(l) + tree_size(h) + 1); return insert_node(n); } @@ -500,7 +503,7 @@ namespace dd { return pdd(m_var2pdd[i], this); } - unsigned pdd_manager::pdd_size(pdd const& b) { + unsigned pdd_manager::dag_size(pdd const& b) { init_mark(); set_mark(0); set_mark(1); @@ -527,6 +530,31 @@ namespace dd { return sz; } + unsigned pdd_manager::degree(pdd const& b) { + init_mark(); + m_degree.reserve(m_nodes.size()); + m_todo.push_back(b.root); + while (!m_todo.empty()) { + PDD r = m_todo.back(); + if (is_marked(r)) { + m_todo.pop_back(); + } + else if (is_val(r)) { + m_degree[r] = 0; + set_mark(r); + } + else if (!is_marked(lo(r)) || !is_marked(hi(r))) { + m_todo.push_back(lo(r)); + m_todo.push_back(hi(r)); + } + else { + m_degree[r] = std::max(m_degree[lo(r)], m_degree[hi(r)]+1); + set_mark(r); + } + } + return m_degree[b.root]; + } + void pdd_manager::alloc_free_nodes(unsigned n) { for (unsigned i = 0; i < n; ++i) { m_free_nodes.push_back(m_nodes.size()); diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h index b148a7b75..e70c8aed2 100644 --- a/src/math/dd/dd_pdd.h +++ b/src/math/dd/dd_pdd.h @@ -56,27 +56,30 @@ namespace dd { }; struct pdd_node { - pdd_node(unsigned level, PDD lo, PDD hi): + pdd_node(unsigned level, PDD lo, PDD hi, double tree_size): m_refcount(0), m_level(level), m_lo(lo), m_hi(hi), - m_index(0) + m_index(0), + m_tree_size(tree_size) {} pdd_node(unsigned value): m_refcount(0), m_level(0), m_lo(value), m_hi(0), - m_index(0) + m_index(0), + m_tree_size(1) {} - pdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0) {} + pdd_node(): m_refcount(0), m_level(0), m_lo(0), m_hi(0), m_index(0), m_tree_size(0) {} unsigned m_refcount : 10; unsigned m_level : 22; PDD m_lo; PDD m_hi; unsigned m_index; + double m_tree_size; unsigned hash() const { return mk_mix(m_level, m_lo, m_hi); } bool is_internal() const { return m_lo == 0 && m_hi == 0; } void set_internal() { m_lo = 0; m_hi = 0; } @@ -142,6 +145,7 @@ namespace dd { mutable svector m_mark; mutable unsigned m_mark_level; mutable svector m_todo; + mutable unsigned_vector m_degree; bool m_disable_gc; bool m_is_new_node; unsigned m_max_num_pdd_nodes; @@ -186,8 +190,10 @@ namespace dd { inline void inc_ref(PDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount++; SASSERT(!m_free_nodes.contains(b)); } inline void dec_ref(PDD b) { if (m_nodes[b].m_refcount != max_rc) m_nodes[b].m_refcount--; SASSERT(!m_free_nodes.contains(b)); } inline PDD level2pdd(unsigned l) const { return m_var2pdd[m_level2var[l]]; } + inline double tree_size(PDD p) const { return m_nodes[p].m_tree_size; } - unsigned pdd_size(pdd const& b); + unsigned dag_size(pdd const& b); + unsigned degree(pdd const& p); void try_gc(); void reserve_var(unsigned v); @@ -231,6 +237,7 @@ namespace dd { bool try_spoly(pdd const& a, pdd const& b, pdd& r); bool lt(pdd const& a, pdd const& b); bool different_leading_term(pdd const& a, pdd const& b); + double tree_size(pdd const& p) const; std::ostream& display(std::ostream& out); std::ostream& display(std::ostream& out, pdd const& b); @@ -269,7 +276,9 @@ namespace dd { bool operator!=(pdd const& other) const { return root != other.root; } bool operator<(pdd const& b) const { return m->lt(*this, b); } - unsigned size() const { return m->pdd_size(*this); } + unsigned dag_size() const { return m->dag_size(*this); } + double tree_size() const { return m->tree_size(*this); } + unsigned degree() const { return m->degree(*this); } }; inline pdd operator*(rational const& r, pdd const& b) { return b * r; } diff --git a/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt index 0ec842f75..243b226e2 100644 --- a/src/math/grobner/CMakeLists.txt +++ b/src/math/grobner/CMakeLists.txt @@ -4,4 +4,5 @@ z3_add_component(grobner pdd_grobner.cpp COMPONENT_DEPENDENCIES ast + dd ) diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp index 3b961cd96..52521998c 100644 --- a/src/math/grobner/pdd_grobner.cpp +++ b/src/math/grobner/pdd_grobner.cpp @@ -43,8 +43,14 @@ namespace dd { } void grobner::compute_basis() { - while (!done() && compute_basis_step()) { - TRACE("grobner", display(tout);); + try { + while (!done() && compute_basis_step()) { + TRACE("grobner", display(tout);); + DEBUG_CODE(invariant();); + } + } + catch (pdd_manager::mem_out) { + // don't reduce further } } @@ -85,6 +91,9 @@ namespace dd { } } + /* + Use a set of equations to simplify eq + */ bool grobner::simplify_using(equation& eq, equation_set const& eqs) { bool simplified, changed_leading_term; TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of size " << eqs.size() << "\n";); @@ -134,8 +143,12 @@ namespace dd { toggle_processed(*eq); return true; } - - // return true iff simplified + + /* + simplify target using source. + return true if the target was simplified. + set changed_leading_term if the target is in the m_processed set and the leading term changed. + */ bool grobner::simplify_source_target(equation const& source, equation& target, bool& changed_leading_term) { TRACE("grobner", tout << "simplifying: " << target.poly() << "\nusing: " << source.poly() << "\n";); m_stats.m_simplified++; @@ -152,7 +165,9 @@ namespace dd { return true; } - // let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 + /* + let eq1: ab+q=0, and eq2: ac+e=0, then qc - eb = 0 + */ void grobner::superpose(equation const& eq1, equation const& eq2) { TRACE("grobner_d", tout << "eq1="; display_equation(tout, eq1) << "eq2="; display_equation(tout, eq2);); pdd r(m); @@ -226,15 +241,16 @@ namespace dd { } void grobner::update_stats_max_degree_and_size(const equation& e) { - // TBD m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().size()); - // TBD m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e.poly.degree()); + m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().tree_size()); + m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e.poly().degree()); } - std::ostream& grobner::print_stats(std::ostream & out) const { - return out << "stats:\nsteps = " << m_stats.m_compute_steps << "\nsimplified: " << - m_stats.m_simplified << "\nsuperposed: " << - m_stats.m_superposed << "\nexpr degree: " << m_stats.m_max_expr_degree << - "\nexpr size: " << m_stats.m_max_expr_size << "\n"; + void grobner::collect_statistics(statistics& st) const { + st.update("steps", m_stats.m_compute_steps); + st.update("simplified", m_stats.m_simplified); + st.update("superposed", m_stats.m_superposed); + st.update("degree", m_stats.m_max_expr_degree); + st.update("size", m_stats.m_max_expr_size); } std::ostream& grobner::display_equation(std::ostream & out, const equation & eq) const { @@ -246,8 +262,28 @@ namespace dd { std::ostream& grobner::display(std::ostream& out) const { out << "processed\n"; for (auto e : m_processed) display_equation(out, *e); out << "to_simplify\n"; for (auto e : m_to_simplify) display_equation(out, *e); + statistics st; + collect_statistics(st); + st.display(out); return out; } + void grobner::invariant() const { + for (auto* e : m_processed) { + SASSERT(e->is_processed()); + } + for (auto* e : m_to_simplify) { + SASSERT(!e->is_processed()); + } + for (auto* e : m_equations) { + if (e) { + SASSERT(!e->is_processed() || m_processed.contains(e)); + SASSERT(e->is_processed() || m_to_simplify.contains(e)); + SASSERT(!is_trivial(*e)); + } + } + } + + } diff --git a/src/math/grobner/pdd_grobner.h b/src/math/grobner/pdd_grobner.h index cf07ca548..bdf123369 100644 --- a/src/math/grobner/pdd_grobner.h +++ b/src/math/grobner/pdd_grobner.h @@ -19,11 +19,12 @@ --*/ #pragma once -#include "math/dd/dd_pdd.h" #include "util/dependency.h" #include "util/obj_hashtable.h" #include "util/region.h" #include "util/rlimit.h" +#include "util/statistics.h" +#include "math/dd/dd_pdd.h" namespace dd { @@ -31,7 +32,7 @@ class grobner { public: struct stats { unsigned m_simplified; - unsigned m_max_expr_size; + double m_max_expr_size; unsigned m_max_expr_degree; unsigned m_superposed; unsigned m_compute_steps; @@ -40,13 +41,14 @@ public: struct config { unsigned m_eqs_threshold; + unsigned m_expr_size_limit; }; private: class equation { bool m_processed; //!< state unsigned m_idx; //!< position at m_equations - pdd m_poly; // simplified expressionted monomials + pdd m_poly; //!< polynomial in pdd form u_dependency * m_dep; //!< justification for the equality public: equation(pdd const& p, u_dependency* d, unsigned idx): @@ -89,10 +91,14 @@ public: void operator=(config const& c) { m_config = c; } void reset(); - void compute_basis(); void add(pdd const&, u_dependency * dep); + + void compute_basis(); + equation_set const& equations(); u_dependency_manager& dep() const { return m_dep_manager; } + + void collect_statistics(statistics & st) const; std::ostream& display_equation(std::ostream& out, const equation& eq) const; std::ostream& display(std::ostream& out) const; @@ -117,10 +123,9 @@ private: void del_equations(unsigned old_size); void del_equation(equation* eq); + void invariant() const; + void update_stats_max_degree_and_size(const equation& e); - - std::ostream& print_stats(std::ostream&) const; - }; }