From 976f10c613c52642d8944fe3cd12c17297f2773a Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Mon, 6 Jan 2020 17:55:49 -0800
Subject: [PATCH] rebase with Z3Prover

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/CMakeLists.txt            | 2 +-
 src/math/grobner/pdd_solver.h | 4 ++--
 src/math/lp/nla_core.cpp      | 8 ++++----
 src/math/lp/nla_core.h        | 6 +++---
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index c9f9dc270..e1ca4984e 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -53,7 +53,7 @@ add_subdirectory(parsers/util)
 add_subdirectory(math/grobner)
 add_subdirectory(sat)
 add_subdirectory(nlsat)
-add_subdirectory(util/lp)
+add_subdirectory(math/lp)
 add_subdirectory(math/euclid)
 add_subdirectory(tactic/core)
 add_subdirectory(math/subpaving/tactic)
diff --git a/src/math/grobner/pdd_solver.h b/src/math/grobner/pdd_solver.h
index 9bcab5552..262e82329 100644
--- a/src/math/grobner/pdd_solver.h
+++ b/src/math/grobner/pdd_solver.h
@@ -130,8 +130,8 @@ public:
 private:
     bool step();
     equation* pick_next();
-    bool canceled() const;
-    bool done() const;
+    bool canceled();
+    bool done();
     void superpose(equation const& eq1, equation const& eq2);
     void superpose(equation const& eq);
     void simplify_using(equation& eq, equation_vector const& eqs);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 9e548e032..9b226620d 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -20,7 +20,7 @@ Revision History:
 #include "math/lp/nla_core.h"
 #include "math/lp/factorization_factory_imp.h"
 #include "math/lp/nex.h"
-#include "math/grobner/pdd_grobner.h"
+#include "math/grobner/pdd_solver.h"
 #include "math/dd/pdd_interval.h"
 #include "math/dd/pdd_eval.h"
 namespace nla {
@@ -1429,11 +1429,11 @@ void core::run_pdd_grobner() {
         tree_size = std::max(tree_size, e->poly().tree_size());
     }
     tree_size *= 10;
-    struct dd::grobner::config cfg;
+    struct dd::solver::config cfg;
     cfg.m_expr_size_limit = (unsigned)tree_size;
     cfg.m_eqs_threshold = m_pdd_grobner.equations().size()*5;
     cfg.m_max_steps = m_pdd_grobner.equations().size();
-    m_pdd_grobner = cfg;
+    m_pdd_grobner.set(cfg);
 
     m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
 
@@ -1480,7 +1480,7 @@ std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
     return out;
 }
 
-bool core::check_pdd_eq(const dd::grobner::equation* e) {
+bool core::check_pdd_eq(const dd::solver::equation* e) {
     dd::pdd_interval eval(m_pdd_manager, m_reslim);
     eval.var2interval() =
         [this](lpvar j, bool deps) {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 5cf3924f6..316f53c3a 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -30,7 +30,7 @@
 #include "math/lp/nex.h"
 #include "math/lp/horner.h"
 #include "math/lp/nla_intervals.h"
-#include "math/grobner/pdd_grobner.h"
+#include "math/grobner/pdd_solver.h"
 
 
 namespace nla {
@@ -95,7 +95,7 @@ public:
     horner                   m_horner;
     nla_settings             m_nla_settings;    
     dd::pdd_manager          m_pdd_manager;
-    dd::grobner              m_pdd_grobner;
+    dd::solver               m_pdd_grobner;
    
 private:
     emonics                  m_emons;
@@ -408,7 +408,7 @@ public:
     void set_active_vars_weights(nex_creator&);
     unsigned get_var_weight(lpvar) const;
     void add_row_to_pdd_grobner(const vector<lp::row_cell<rational>> & row);    
-    bool check_pdd_eq(const dd::grobner::equation*);
+    bool check_pdd_eq(const dd::solver::equation*);
     const rational& val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep);
     dd::pdd pdd_expr(const rational& c, lpvar j, u_dependency*&);
     void set_level2var_for_pdd_grobner();