build dependencies, invariant annotation

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

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'])

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());

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<unsigned>  m_mark;
         mutable unsigned           m_mark_level;
         mutable svector<PDD>       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; }

src/math/grobner/CMakeLists.txt

@@ -4,4 +4,5 @@ z3_add_component(grobner
     pdd_grobner.cpp
   COMPONENT_DEPENDENCIES
     ast
+    dd
 )

src/math/grobner/pdd_grobner.cpp

@@ -43,8 +43,14 @@ namespace dd {
     }
 
     void grobner::compute_basis() {
+        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";);
@@ -135,7 +144,11 @@ namespace dd {
         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());
+        m_stats.m_max_expr_size = std::max(m_stats.m_max_expr_size, e.poly().tree_size());
-        // TBD m_stats.m_max_expr_degree = std::max(m_stats.m_max_expr_degree, e.poly.degree());
+        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 {
+    void grobner::collect_statistics(statistics& st) const {
-        return out << "stats:\nsteps = " << m_stats.m_compute_steps << "\nsimplified: " <<
+        st.update("steps", m_stats.m_compute_steps);
-            m_stats.m_simplified << "\nsuperposed: " <<
+        st.update("simplified", m_stats.m_simplified);
-            m_stats.m_superposed << "\nexpr degree: " << m_stats.m_max_expr_degree <<
+        st.update("superposed", m_stats.m_superposed);
-            "\nexpr size: " << m_stats.m_max_expr_size << "\n";
+        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));
+            }
+        }
+    }
+
+
 }
 

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;
-
 };
 
 }