comments

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

src/math/dd/dd_pdd.cpp

@@ -107,7 +107,7 @@ namespace dd {
         case pdd_add_op:
             if (is_zero(a)) return b;
             if (is_zero(b)) return a;
-            if (is_val(a) && is_val(b)) return imk_val(m_mod2_semantics ? ((val(a) + val(b)) % rational(2)) : val(a) + val(b));
+            if (is_val(a) && is_val(b)) return imk_val(val(a) + val(b));
             if (level(a) < level(b)) std::swap(a, b);
             break;
         case pdd_mul_op:
@@ -249,6 +249,7 @@ namespace dd {
     }
 
     pdd_manager::PDD pdd_manager::minus_rec(PDD a) {
+        SASSERT(!m_mod2_semantics);
         if (is_zero(a)) return zero_pdd;
         if (is_val(a)) return imk_val(-val(a));
         op_entry* e1 = pop_entry(a, a, pdd_minus_op);
@@ -299,7 +300,7 @@ namespace dd {
         if (is_val(p)) {
             if (is_val(q)) {
                 SASSERT(!val(p).is_zero());
-                return m_mod2_semantics ? imk_val(val(q)) : imk_val(-val(q)/val(p));
+                return imk_val(-val(q)/val(p));
             }     
         }   
         else if (level(p) == level(q)) {
@@ -321,7 +322,7 @@ namespace dd {
         pdd r1 = mk_val(qc);  
         for (unsigned i = q.size(); i-- > 0; ) r1 = mul(mk_var(q[i]), r1);
         r1 = mul(a, r1);
-        pdd r2 = mk_val(m_mod2_semantics ? pc : -pc);
+        pdd r2 = mk_val(-pc);
         for (unsigned i = p.size(); i-- > 0; ) r2 = mul(mk_var(p[i]), r2);
         r2 = mul(b, r2);
         return add(r1, r2);
@@ -338,6 +339,11 @@ namespace dd {
                 while (!is_val(x)) p.push_back(var(x)), x = hi(x);
                 pc = val(x);
                 qc = val(y);
+                if (!m_mod2_semantics && pc.is_int() && qc.is_int()) {
+                    rational g = gcd(pc, qc);
+                    pc /= g;
+                    qc /= g;
+                }
                 return true;
             }
             if (level(x) == level(y)) {
@@ -443,6 +449,7 @@ namespace dd {
     pdd_manager::PDD pdd_manager::imk_val(rational const& r) {
         if (r.is_zero()) return zero_pdd;
         if (r.is_one()) return one_pdd;
+        if (m_mod2_semantics) return imk_val(mod(r, rational(2)));
         const_info info;
         if (!m_mpq_table.find(r, info)) {
             init_value(info, r);

src/math/grobner/pdd_grobner.cpp

@@ -16,7 +16,7 @@
 namespace dd {
 
     /***
-        The main algorithm maintains two sets (S, A), 
+        A simple algorithm maintains two sets (S, A), 
         where S is m_processed, and A is m_to_simplify.
         Initially S is empty and A contains the initial equations.
         
@@ -29,22 +29,71 @@ namespace dd {
              add b to A
         - add a to S
         - simplify A using a
+
+        Alternate:
+
+        - Fix a variable ordering x1 > x2 > x3 > ....
+        In each step:
+          - pick a in A with *highest* variable x_i in leading term of *lowest* degree.
+          - simplify a using S
+          - simplify S using a
+          - if a does not contains x_i, put it back into A and pick again (determine whether possible)
+          - for s in S:
+               b = superpose(a, s)
+               if superposition is invertible, then remove s
+               add b to A
+          - add a to S
+          - simplify A using a
+
+
+        Apply a watch list to filter out relevant elements of S
+        Index leading_term_watch: Var -> Equation*
+        Only need to simplify equations that contain eliminated variable.
+        The watch list can be used to index into equations that are useful to simplify.
+        A Bloom filter on leading term could further speed up test whether reduction applies.
+
+        For p in A:
+            populate watch list by maxvar(p) |-> p
+        For p in S:
+            populate watch list by vars(p) |-> p
+
+        - the variable ordering should be chosen from a candidate model M, 
+          in a way that is compatible with weights that draw on the number of occurrences
+          in polynomials with violated evaluations and with the maximal slack (degree of freedom).
+         
+          weight(x) := < count { p in P | x in p, M(p) != 0 }, min_{p in P | x in p} slack(p,x) >
+
+          slack is computed from interval assignments to variables, and is an interval in which x can possibly move
+          (an over-approximation).
+
+        The alternative version maintains the following invariant:
+        - polynomials not in the watch list cannot be simplified using a
+          Justification:
+          - elements in S have all variables watched
+          - elements in A are always reduced modulo all variables above the current x_i.
+
+        Invertible rules:
+          when p, q are linear in x, e.g., is of the form p = k*x + a, q = l*x + b 
+          where k, l are constant and x is maximal, then 
+          from l*a - k*b and k*x + a we have the equality lkx+al+kb-al, which is lx+b
+          So we can throw away q after superposition without losing solutions.
+          - this corresponds to triangulating a matrix during Gauss.
+
     */
 
     grobner::grobner(reslimit& lim, pdd_manager& m) : 
         m(m),
         m_limit(lim), 
-        m_conflict(false)
+        m_conflict(nullptr)
     {}
 
-
     grobner::~grobner() {
-        del_equations(0);
+        reset();
     }
 
-    void grobner::compute_basis() {
+    void grobner::saturate() {
         try {
-            while (!done() && compute_basis_step()) {
+            while (!done() && step()) {
                 TRACE("grobner", display(tout););
                 DEBUG_CODE(invariant(););
             }
@@ -54,7 +103,7 @@ namespace dd {
         }
     }
 
-    bool grobner::compute_basis_step() {
+    bool grobner::step() {
         m_stats.m_compute_steps++;
         equation* e = pick_next();
         if (!e) return false;
@@ -66,7 +115,8 @@ namespace dd {
         if (!simplify_using(m_processed, eq)) return false;
         TRACE("grobner", tout << "eq = "; display_equation(tout, eq););
         superpose(eq);
-        toggle_processed(eq);
+        eq.set_processed(true);
+        m_processed.push_back(e);
         return simplify_using(m_to_simplify, eq);
     }
     
@@ -77,7 +127,7 @@ namespace dd {
                 eq = curr;
             }
         }
-        if (eq) m_to_simplify.erase(eq);
+        if (eq) pop_equation(eq->idx(), m_to_simplify);
         return eq;
     }
 
@@ -90,7 +140,7 @@ namespace dd {
     /*
       Use a set of equations to simplify eq
     */
-    bool grobner::simplify_using(equation& eq, equation_set const& eqs) {
+    bool grobner::simplify_using(equation& eq, equation_vector const& eqs) {
         bool simplified, changed_leading_term;
         TRACE("grobner", tout << "simplifying: "; display_equation(tout, eq); tout << "using equalities of size " << eqs.size() << "\n";);
         do {
@@ -115,31 +165,29 @@ namespace dd {
     /*
       Use the given equation to simplify equations in set
     */
-    bool grobner::simplify_using(equation_set& set, equation const& eq) {
+    bool grobner::simplify_using(equation_vector& set, equation const& eq) {
         TRACE("grobner", tout << "poly " << eq.poly() <<  "\n";);
-        ptr_buffer<equation> to_delete;
-        ptr_buffer<equation> to_move;
-        bool changed_leading_term = false;
-        for (equation* target : set) {
-            if (canceled())
-                return false;
-            if (simplify_source_target(eq, *target, changed_leading_term)) {
-                if (is_trivial(*target))
-                    to_delete.push_back(target);
-                else if (is_too_complex(*target))
-                    to_delete.push_back(target);
-                else if (check_conflict(*target))
-                    return false;
-                else if (changed_leading_term && target->is_processed()) {
-                    to_move.push_back(target);
-                }
-            }            
+        unsigned j = 0, sz = set.size();
+        for (unsigned i = 0; i < sz; ++i) {
+            equation& target = *set[i];
+            bool changed_leading_term = false;
+            bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term); 
+            if (simplified && (is_trivial(target) || is_too_complex(target))) {
+                retire(&target);
+            }
+            else if (simplified && !check_conflict(target) && changed_leading_term && target.is_processed()) {
+                target.set_index(m_to_simplify.size());
+                target.set_processed(false);
+                m_to_simplify.push_back(&target);                    
+            }
+            else {
+                set[j] = &target;
+                target.set_index(j);
+                ++j;
+            } 
         }
-        for (equation* eq : to_delete)
-            del_equation(eq);
-        for (equation* eq : to_move) 
-            toggle_processed(*eq);
-        return true;
+        set.shrink(j);
+        return !done();
     }    
 
     /*
@@ -173,70 +221,51 @@ namespace dd {
         m_stats.m_superposed++;
         if (r.is_zero()) return;
         if (is_too_complex(r)) return;
-        equation* eq = alloc(equation, r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()), m_equations.size());
-        m_equations.push_back(eq);
-        update_stats_max_degree_and_size(*eq);
-        check_conflict(*eq);
-        m_to_simplify.insert(eq);
+        add(r, m_dep_manager.mk_join(eq1.dep(), eq2.dep()));
     }
 
-    void grobner::toggle_processed(equation& eq) {
-        if (eq.is_processed()) {
-            m_to_simplify.insert(&eq);
-            m_processed.erase(&eq);
-        }
-        else {
-            m_processed.insert(&eq);
-            m_to_simplify.erase(&eq);            
-        }
-        eq.set_processed(!eq.is_processed());        
-    }
-
-    grobner::equation_set const& grobner::equations() {
+    grobner::equation_vector const& grobner::equations() {
         m_all_eqs.reset();
-        for (equation* eq : m_equations) if (eq) m_all_eqs.insert(eq);
+        for (equation* eq : m_to_simplify) m_all_eqs.push_back(eq);
+        for (equation* eq : m_processed) m_all_eqs.push_back(eq);
         return m_all_eqs;
     }
 
     void grobner::reset() {
-        del_equations(0);
-        SASSERT(m_equations.empty());    
+        for (equation* e : m_to_simplify) dealloc(e);
+        for (equation* e : m_processed) dealloc(e);
         m_processed.reset();
         m_to_simplify.reset();
         m_stats.reset();
-        m_conflict = false;
+        m_conflict = nullptr;
     }
 
     void grobner::add(pdd const& p, u_dependency * dep) {
         if (p.is_zero()) return;
-        if (p.is_val()) set_conflict();
-        equation * eq = alloc(equation, p, dep, m_equations.size());
-        m_equations.push_back(eq);
-        m_to_simplify.insert(eq);
+        equation * eq = alloc(equation, p, dep, m_to_simplify.size());
+        m_to_simplify.push_back(eq);
+        check_conflict(*eq);
+        update_stats_max_degree_and_size(*eq);
     }   
-
-    void grobner::del_equations(unsigned old_size) {
-        for (unsigned i = m_equations.size(); i-- > old_size; ) {
-            del_equation(m_equations[i]);
-        }
-        m_equations.shrink(old_size);    
-    }
-
-    void grobner::del_equation(equation* eq) {
-        if (!eq) return;
-        unsigned idx = eq->idx();
-        m_processed.erase(eq);
-        m_to_simplify.erase(eq);
-        dealloc(m_equations[idx]);
-        m_equations[idx] = nullptr;
-    }
     
     bool grobner::canceled() {
         return m_limit.get_cancel_flag();
     }
     
     bool grobner::done() {
-        return m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || canceled() || m_conflict;
+        return m_to_simplify.size() + m_processed.size() >= m_config.m_eqs_threshold || canceled() || m_conflict != nullptr;
+    }
+
+    void grobner::del_equation(equation& eq) {
+        pop_equation(eq.idx(), eq.is_processed() ? m_processed : m_to_simplify);
+        retire(&eq);
+    }
+
+    void grobner::pop_equation(unsigned idx, equation_vector& v) {
+        equation* eq2 = v.back();
+        eq2->set_index(idx);
+        v[idx] = eq2;
+        v.pop_back();            
     }
     
     void grobner::update_stats_max_degree_and_size(const equation& e) {
@@ -268,21 +297,18 @@ namespace dd {
     }
 
     void grobner::invariant() const {
+        unsigned i = 0;
         for (auto* e : m_processed) {
             SASSERT(e->is_processed());            
+            SASSERT(e->idx() == i);
+            ++i;
         }
+        i = 0;
         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));
-            }
+            SASSERT(e->idx() == i);
+            ++i;
         }
     }
-
-
 }
 

src/math/grobner/pdd_grobner.h

@@ -47,7 +47,7 @@ public:
 private:
     class equation {
         bool                       m_processed;  //!< state
-        unsigned                   m_idx;        //!< position at m_equations
+        unsigned                   m_idx;        //!< unique index
         pdd                        m_poly;       //!< polynomial in pdd form
         u_dependency *             m_dep;        //!< justification for the equality
     public:
@@ -60,15 +60,14 @@ private:
 
         const pdd& poly() const { return m_poly; }        
         u_dependency * dep() const { return m_dep; }
-        unsigned hash() const { return m_idx; }
         unsigned idx() const { return m_idx; }
         void operator=(pdd& p) { m_poly = p; }
         void operator=(u_dependency* d) { m_dep = d; }
         bool is_processed() const { return m_processed; }
         void set_processed(bool p) { m_processed = p; }
+        void set_index(unsigned idx) { m_idx = idx; }
     };
 
-    typedef obj_hashtable<equation> equation_set;
     typedef ptr_vector<equation> equation_vector;
     typedef std::function<void (u_dependency* d, std::ostream& out)> print_dep_t;
 
@@ -77,12 +76,11 @@ private:
     stats                                        m_stats;
     config                                       m_config;
     print_dep_t                                  m_print_dep;
-    equation_vector                              m_equations;
-    equation_set                                 m_processed;
-    equation_set                                 m_to_simplify;
+    equation_vector                              m_processed;
+    equation_vector                              m_to_simplify;
     mutable u_dependency_manager                 m_dep_manager;
-    equation_set                                 m_all_eqs;
-    bool                                         m_conflict;
+    equation_vector                              m_all_eqs;
+    equation const*                              m_conflict;
 public:
     grobner(reslimit& lim, pdd_manager& m);
     ~grobner();
@@ -93,9 +91,9 @@ public:
     void reset();
     void add(pdd const&, u_dependency * dep);
 
-    void compute_basis();
+    void saturate();
 
-    equation_set const& equations();
+    equation_vector const& equations();
     u_dependency_manager& dep() const { return m_dep_manager;  }
 
     void collect_statistics(statistics & st) const;
@@ -103,28 +101,27 @@ public:
     std::ostream& display(std::ostream& out) const;
 
 private:
-    bool compute_basis_step();
+    bool step();
     equation* pick_next();
     bool canceled();
     bool done();
     void superpose(equation const& eq1, equation const& eq2);
     void superpose(equation const& eq);
     bool simplify_source_target(equation const& source, equation& target, bool& changed_leading_term);
-    bool simplify_using(equation_set& set, equation const& eq);
-    bool simplify_using(equation& eq, equation_set const& eqs);
-    void toggle_processed(equation& eq);
+    bool simplify_using(equation_vector& set, equation const& eq);
+    bool simplify_using(equation& eq, equation_vector const& eqs);
 
-    bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(&eq), true); }
+    bool eliminate(equation& eq) { return is_trivial(eq) && (del_equation(eq), true); }
     bool is_trivial(equation const& eq) const { return eq.poly().is_zero(); }    
     bool is_simpler(equation const& eq1, equation const& eq2) { return eq1.poly() < eq2.poly(); }
-    bool check_conflict(equation const& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(), true); }    
-    void set_conflict() { m_conflict = true; }
+    bool check_conflict(equation const& eq) { return eq.poly().is_val() && !is_trivial(eq) && (set_conflict(eq), true); }    
+    void set_conflict(equation const& eq) { m_conflict = &eq; }
     bool is_too_complex(const equation& eq) const { return is_too_complex(eq.poly()); }
     bool is_too_complex(const pdd& p) const { return p.tree_size() > m_config.m_expr_size_limit;  }
 
-
-    void del_equations(unsigned old_size);
-    void del_equation(equation* eq);    
+    void del_equation(equation& eq);    
+    void retire(equation* eq) { dealloc(eq); }
+    void pop_equation(unsigned idx, equation_vector& v);
 
     void invariant() const;