From 25b98f497a616286a14f2ad35fe67988e55cd7ca Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Dec 2019 11:51:04 -0800
Subject: [PATCH] adding level2var

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_pdd.cpp           |  8 ++++++++
 src/math/dd/dd_pdd.h             |  3 ++-
 src/math/grobner/pdd_grobner.cpp | 34 ++++++++++++++++++++------------
 src/test/pdd_grobner.cpp         | 19 ++++++++++++++++++
 4 files changed, 50 insertions(+), 14 deletions(-)

diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index ac6709630..75da3a775 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -544,6 +544,14 @@ namespace dd {
         reserve_var(i);
         return pdd(m_var2pdd[i], this);        
     }
+
+    void pdd_manager::set_level2var(unsigned_vector const& level2var) {
+        SASSERT(level2var.size() == m_level2var.size());
+        for (unsigned i = 0; i < level2var.size(); ++i) {
+            m_var2level[level2var[i]] = i;
+            m_level2var[i] = level2var[i];
+        }
+    }
     
     unsigned pdd_manager::dag_size(pdd const& b) {
         init_mark();
diff --git a/src/math/dd/dd_pdd.h b/src/math/dd/dd_pdd.h
index 0fd9606bb..a303da53d 100644
--- a/src/math/dd/dd_pdd.h
+++ b/src/math/dd/dd_pdd.h
@@ -225,7 +225,8 @@ namespace dd {
 
         void set_mod2_semantics() { m_mod2_semantics = true; }
         void set_max_num_nodes(unsigned n) { m_max_num_pdd_nodes = n; }
-        void set_var_order(unsigned_vector const& levels);  // TBD: set variable order (m_var2level, m_level2var) before doing anything else.        
+        void set_level2var(unsigned_vector const& level2var);  
+        unsigned_vector const& get_level2var() const { return m_level2var; }
 
         pdd mk_var(unsigned i);
         pdd mk_val(rational const& r);
diff --git a/src/math/grobner/pdd_grobner.cpp b/src/math/grobner/pdd_grobner.cpp
index 90e2a9d13..c4dc72f62 100644
--- a/src/math/grobner/pdd_grobner.cpp
+++ b/src/math/grobner/pdd_grobner.cpp
@@ -139,7 +139,6 @@ namespace dd {
         unsigned j = 0;
         for (equation* target : m_processed) {
             if (superpose(eq, *target)) {
-                // remove from watch lists
                 retire(target); 
             }
             else {
@@ -189,6 +188,11 @@ namespace dd {
                 retire(&target);
             }
             else if (simplified && !check_conflict(target) && changed_leading_term) {
+                SASSERT(target.is_processed());
+                target.set_processed(false);
+                if (is_tuned()) {
+                    m_levelp1 = std::max(m_var2level[target.poly().var()]+1, m_levelp1);
+                }
                 push_equation(target, m_to_simplify);               
             }
             else {
@@ -217,10 +221,6 @@ namespace dd {
         target = r;
         target = m_dep_manager.mk_join(target.dep(), source.dep());
         update_stats_max_degree_and_size(target);
-        if (changed_leading_term) {
-            target.set_processed(false);
-        }
-
         TRACE("grobner", tout << "simplified " << target.poly() << "\n";);
         return true;
     }
@@ -255,8 +255,13 @@ namespace dd {
     }
 
     void grobner::tuned_init() {
-        // TBD: extract free variables, order them, set pointer into variable list.
-        NOT_IMPLEMENTED_YET();
+        unsigned_vector const& l2v = m.get_level2var();
+        m_level2var.resize(l2v.size());
+        m_var2level.resize(l2v.size());
+        for (unsigned i = 0; i < l2v.size(); ++i) {
+            m_level2var[i] = l2v[i];
+            m_var2level[l2v[i]] = i;
+        }
         m_watch.reserve(m_level2var.size());
         m_levelp1 = m_level2var.size();
         for (equation* eq : m_to_simplify) add_to_watch(*eq);
@@ -278,17 +283,20 @@ namespace dd {
         for (equation* _target : watch) {
             equation& target = *_target;
             SASSERT(!target.is_processed());
+            SASSERT(target.poly().var() == v);
             bool changed_leading_term = false;
-            bool simplified = !done() && simplify_source_target(eq, target, changed_leading_term);
-            if (simplified && is_trivial(target)) {
+            if (!done()) simplify_source_target(eq, target, changed_leading_term);
+            if (is_trivial(target)) {
                 retire(&target);
             }
-            else if (simplified && !check_conflict(target) && changed_leading_term) {
-                SASSERT(!target.is_processed());
-                pop_equation(target.idx(), m_processed);
-                push_equation(target, m_to_simplify);
+            else if (check_conflict(target)) {
+                // remove from watch
+            } else if (target.poly().var() != v) {
+                // move to other watch list
+                m_watch[target.poly().var()].push_back(_target);
             }
             else {
+                // keep watching same variable
                 watch[++j] = _target;
             }
         }
diff --git a/src/test/pdd_grobner.cpp b/src/test/pdd_grobner.cpp
index f2dd444c1..c1172311a 100644
--- a/src/test/pdd_grobner.cpp
+++ b/src/test/pdd_grobner.cpp
@@ -36,6 +36,7 @@ namespace dd {
         print_eqs(gb.equations());
         gb.reset();
 
+        // stop early on contradiction
         gb.add(v1*v3*v3 + v3*v1 + 2);
         gb.add(v1*v3*v3 + v3*v1);
         gb.add(v3*v1 + v1*v2 + v2*v3);
@@ -45,6 +46,24 @@ namespace dd {
         print_eqs(gb.equations());
         gb.reset();
 
+        // result is v1 = 0, v2 = 0.
+        gb.add(v1*v3*v3 + v3*v1);
+        gb.add(v3*v1 + v1*v2 + v2*v3);
+        gb.add(v3*v1 + v1*v2 + v2*v3 + v1);
+        gb.add(v3*v1 + v1*v2 + v2*v3 + v2);
+        gb.saturate();        
+        print_eqs(gb.equations());
+        gb.reset();
+
+        // everything rewrites to a multiple of v0
+        gb.add(v3 - 2*v2);
+        gb.add(v2 - 2*v1);
+        gb.add(v1 - 2*v0);
+        gb.saturate();        
+        print_eqs(gb.equations());
+        gb.reset();
+
+        // 
     }
 }