canonicalize polinomals in todo_set

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

src/nlsat/levelwise.cpp

@@ -220,10 +220,10 @@ namespace nlsat {
         }
         
         /*
-          prepare the initial properties
+          prepare the initial properties:         
+          scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
         */ 
-        // Helper 1: scan input polynomials, add sgn_inv / an_del properties and collect polynomials at level m_n
+        void collect_top_level_properties(todo_set& ps_of_n_level) {
-        void collect_top_level_properties(polynomial_ref_vector & ps_of_n_level) {
             for (unsigned i = 0; i < m_P.size(); ++i) {
                 poly* p = m_P[i];
                 polynomial_ref pref(p, m_pm);
@@ -235,7 +235,7 @@ namespace nlsat {
                         m_Q[level].push(property(prop_enum::sgn_inv, prim));
                     else if (level == m_n){
                         m_Q[level].push(property(prop_enum::an_del, prim));
-                        ps_of_n_level.push_back(prim.get());
+                        ps_of_n_level.insert(f.get());
                     }
                     else {
                         UNREACHABLE();
@@ -245,8 +245,8 @@ namespace nlsat {
         }
 
         // isolate and collect algebraic roots for the given polynomials
-        void collect_roots_for_ps(polynomial_ref_vector & ps_of_n_level, std::vector<std::pair<scoped_anum, poly*>> & root_vals) {
+        void collect_roots_for_ps(todo_set const& ps_of_n_level, std::vector<std::pair<scoped_anum, poly*>> & root_vals) {
-            for (poly * p : ps_of_n_level) {
+            for (poly * p : ps_of_n_level.m_set) {
                 scoped_anum_vector roots(m_am);
                 m_am.isolate_roots(polynomial_ref(p, m_pm), undef_var_assignment(sample(), m_n), roots);
                 TRACE(lws,  
@@ -262,7 +262,7 @@ namespace nlsat {
             }
         }
 
-        // Helper 3: given collected roots (possibly unsorted), sort them, and add ord_inv(resultant(...))
+        // Given collected roots (possibly unsorted), sort them, and add ord_inv(resultant(...))
         // for adjacent roots coming from different polynomials. Avoid adding the same unordered pair twice.
         // Returns false on failure (e.g. when encountering an ambiguous zero resultant).
         bool add_adjacent_resultants(std::vector<std::pair<scoped_anum, poly*>> & root_vals) {
@@ -317,7 +317,7 @@ namespace nlsat {
           ∪ { ord_inv(resultant(p_j,p_{j+1})) for adjacent root functions }.
         */
         void init_properties() {
-            polynomial_ref_vector ps_of_n_level(m_pm);
+            todo_set ps_of_n_level(m_cache, true);
             collect_top_level_properties(ps_of_n_level);
             std::vector<std::pair<scoped_anum, poly*>> root_vals;
             collect_roots_for_ps(ps_of_n_level, root_vals);
@@ -414,25 +414,19 @@ namespace nlsat {
 
          // Part B of construct_interval: build (I, E, ≼) representation for level i
          void build_representation() {
-             // collect non-null polynomials (up to polynomial_manager equality)
+             // collect non-null polynomials (up to polynomial_manager equality and canonicalization)
-             polynomial::polynomial_ref_vector p_non_null(m_pm);
+             todo_set p_non_null(m_cache, true);
              for (auto & pr: m_Q[m_level]) {
                  if (!pr.m_poly) continue;
                  SASSERT(max_var(pr.m_poly) == m_level);
                  if (pr.m_prop_tag == prop_enum::sgn_inv
                      && !coeffs_are_zeroes_on_sample(pr.m_poly, m_pm, sample(), m_am )) {
                      TRACE(lws, tout << "adding:" << pr.m_poly.get() << "\n";);
-                     poly* new_p = pr.m_poly.get();
+                     p_non_null.insert(pr.m_poly.get());
-                     auto it = std::find_if(p_non_null.begin(), p_non_null.end(),
-                                            [this, new_p](const poly* q){
-                                                return m_pm.eq(q, new_p);
-                                            });
-                     if (it == p_non_null.end())
-                         p_non_null.push_back(new_p);
                  }
              }
 
-             collect_E(p_non_null);
+             collect_E(p_non_null.m_set);
 
              // todo: this order needs to be abstracted: it does not have to be linear.
              // We need a boolean function E_rel(a, b)
@@ -995,12 +989,10 @@ or
                  SASSERT(max_var(a) == max_var(b) && max_var(b) == m_level) ;
                  
                  polynomial_ref r(m_pm);
-                 enable_trace("lws");
                  r = resultant(polynomial_ref(a, m_pm), polynomial_ref(b, m_pm), m_level);
                  TRACE(lws, tout << "resultant of (" << pair.first << "," << pair.second << "):"; 
                        ::nlsat::display(tout, m_solver, a) << "\n";
                        ::nlsat::display(tout,m_solver, b)<< "\nresultant:"; ::nlsat::display(tout, m_solver, r) << "\n");
-                 disable_trace("lws");
                  if (m_pm.is_zero(r)) {
                      TRACE(lws, tout << "fail\n";);
                      fail();

src/nlsat/nlsat_common.cpp

@@ -18,6 +18,81 @@ Revision History:
 --*/
 #include "nlsat/nlsat_common.h"
 namespace nlsat {
+
+    todo_set::todo_set(polynomial::cache& u, bool canonicalize): m_cache(u), m_set(u.pm()), m_canonicalize(canonicalize) {}
+
+    void todo_set::reset() {
+        pmanager& pm = m_set.m();
+        unsigned sz = m_set.size();
+        for (unsigned i = 0; i < sz; i++) {
+            m_in_set[pm.id(m_set.get(i))] = false;
+        }
+        m_set.reset();
+    }
+
+    void todo_set::insert(poly* p) {
+        pmanager& pm = m_set.m();
+        if (m_canonicalize) {
+            // Canonicalize content+sign so scalar multiples share the same representative.
+            if (!pm.is_zero(p) && !pm.is_const(p)) {
+                polynomial_ref prim(pm);
+                var x = pm.max_var(p);
+                pm.primitive(p, x, prim);
+                p = prim.get();
+            }
+            p = pm.flip_sign_if_lm_neg(p);
+        }
+        p = m_cache.mk_unique(p);
+        unsigned pid = pm.id(p);
+        if (m_in_set.get(pid, false))
+            return;
+        m_in_set.setx(pid, true, false);
+        m_set.push_back(p);
+    }
+
+    bool todo_set::empty() const { return m_set.empty(); }
+
+    // Return max variable in todo_set
+    var todo_set::max_var() const {
+        pmanager& pm = m_set.m();
+        var max = null_var;
+        unsigned sz = m_set.size();
+        for (unsigned i = 0; i < sz; i++) {
+            var x = pm.max_var(m_set.get(i));
+            SASSERT(x != null_var);
+            if (max == null_var || x > max)
+                max = x;
+        }
+        return max;
+    }
+
+    /**
+       \brief Remove the maximal polynomials from the set and store
+       them in max_polys. Return the maximal variable
+     */
+    var todo_set::extract_max_polys(polynomial_ref_vector& max_polys) {
+        max_polys.reset();
+        var x = max_var();
+        pmanager& pm = m_set.m();
+        unsigned sz = m_set.size();
+        unsigned j  = 0;
+        for (unsigned i = 0; i < sz; i++) {
+            poly* p = m_set.get(i);
+            var y = pm.max_var(p);
+            SASSERT(y <= x);
+            if (y == x) {
+                max_polys.push_back(p);
+                m_in_set[pm.id(p)] = false;
+            }
+            else {
+                m_set.set(j, p);
+                j++;
+            }
+        }
+        m_set.shrink(j);
+        return x;
+    }
+
     /**
        \brief Wrapper for factorization
     */

src/nlsat/nlsat_common.h

@@ -20,6 +20,29 @@
 
 namespace nlsat {
 
+    // Lightweight set of polynomials that keeps elements unique (by cache id) and
+    // supports extracting all polynomials whose maximal variable is maximal.
+    // Optional canonicalization (primitive + sign) can be enabled per instance.
+    struct todo_set {
+        polynomial::cache&    m_cache;
+        polynomial_ref_vector m_set;
+        svector<char>         m_in_set;
+        bool                  m_canonicalize;
+
+        todo_set(polynomial::cache& u, bool canonicalize = false);
+
+        void reset();
+        void insert(poly* p);
+        bool empty() const;
+        // Return max variable in todo_set
+        var max_var() const;
+        /**
+           \brief Remove the maximal polynomials from the set and store
+           them in max_polys. Return the maximal variable
+         */
+        var extract_max_polys(polynomial_ref_vector& max_polys);
+    };
+
     inline std::ostream& display(std::ostream& out, pmanager& pm, polynomial_ref const& p, display_var_proc const& proc) {
         pm.display(out, p, proc);
         return out;