diff --git a/src/math/lp/horner.cpp b/src/math/lp/horner.cpp
index 208f657d2..2d5531f18 100644
--- a/src/math/lp/horner.cpp
+++ b/src/math/lp/horner.cpp
@@ -79,7 +79,7 @@ bool horner::lemmas_on_row(const T& row) {
     SASSERT (row_is_interesting(row));
     c().clear_and_resize_active_var_set();
     create_sum_from_row(row, cn.get_nex_creator(), m_row_sum, nullptr);
-    set_active_vars_weights(); // without this call the comparisons will be incorrect
+    c().set_active_vars_weights(m_nex_creator); // without this call the comparisons will be incorrect
     nex* e =  m_nex_creator.simplify(m_row_sum.mk());
     TRACE("nla_horner", tout << "e = " << * e << "\n";);
     if (e->get_degree() < 2)
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 818f13794..99a7a7b70 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -111,7 +111,6 @@ struct statistics {
     unsigned m_horner_conflicts;
     unsigned m_cross_nested_forms;
     unsigned m_grobner_calls;
-    unsigned m_grobner_basis_computatins;
     unsigned m_grobner_conflicts;
     statistics() { reset(); }
     void reset() { memset(this, 0, sizeof(*this)); }
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index 6eaee238c..97e468956 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -200,40 +200,6 @@ u_dependency* common::get_fixed_vars_dep_from_row(const T& row, u_dependency_man
     return dep;
 }
 
-void common::set_active_vars_weights() {
-    m_nex_creator.set_number_of_vars(c().m_lar_solver.column_count());
-    for (lpvar j : c().active_var_set()) {
-        m_nex_creator.set_var_weight(j, static_cast<unsigned>(get_var_weight(j)));
-    }
-}
-
-
-
-var_weight common::get_var_weight(lpvar j) const {
-    var_weight k;
-    switch (c().m_lar_solver.get_column_type(j)) {
-        
-    case lp::column_type::fixed:
-        k = var_weight::FIXED;
-        break;
-    case lp::column_type::boxed:
-        k = var_weight::BOUNDED;
-        break;
-    case lp::column_type::lower_bound:
-    case lp::column_type::upper_bound:
-        k = var_weight::NOT_FREE;
-    case lp::column_type::free_column:
-        k = var_weight::FREE;
-        break;
-    default:
-        UNREACHABLE();
-        break;
-    }
-    if (c().is_monic_var(j)) {
-        return (var_weight)((int)k + 1);
-    }
-    return k;
-}
 
 
 }
diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h
index 9cf6dbe5a..bec56964e 100644
--- a/src/math/lp/nla_common.h
+++ b/src/math/lp/nla_common.h
@@ -121,7 +121,5 @@ struct common {
     u_dependency* create_sum_from_row(const T&, nex_creator&, nex_creator::sum_factory&, u_dependency_manager*);
     template <typename T>
     u_dependency* get_fixed_vars_dep_from_row(const T&, u_dependency_manager& dep_manager);
-    void set_active_vars_weights();
-    var_weight get_var_weight(lpvar) const;
 };
 }
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index fa257c704..43b5b4a6e 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -32,7 +32,9 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_monotone(this),
     m_intervals(this, lim),
     m_horner(this, &m_intervals),
-    m_grobner(this, &m_intervals),
+    m_nex_grobner(this, &m_intervals),
+    m_pdd_manager(0),
+    m_pdd_grobner(lim, m_pdd_manager),
     m_emons(m_evars),
     m_reslim(lim)
 {}
@@ -1282,9 +1284,26 @@ lbool core::incremental_linearization(bool constraint_derived) {
 lbool core::inner_check(bool constraint_derived) {
     if (constraint_derived) {
         if (need_to_call_algebraic_methods())
-            if (!(m_nla_settings.run_horner() && m_horner.horner_lemmas())) {
-                if (m_nla_settings.run_grobner() == nla_settings::NEX_GROBNER || m_nla_settings.run_grobner() == nla_settings::BOTH_GROBNER)
-                    m_grobner.grobner_lemmas();
+            if (m_horner.horner_lemmas()) {
+                switch( m_nla_settings.run_grobner()) {                    
+                case nla_settings::BOTH_GROBNER:
+                    init_nex_grobner(m_nex_grobner.get_nex_creator());
+                    m_nex_grobner.grobner_lemmas();
+                    run_pdd_grobner();
+                    break;
+                case nla_settings::NEX_GROBNER:
+                    init_nex_grobner(m_nex_grobner.get_nex_creator());
+                    m_nex_grobner.grobner_lemmas();
+                    break;
+                case nla_settings::PDD_GROBNER:
+                    run_pdd_grobner();
+                    break;
+                case nla_settings::NO_GROBNER:
+                    break;
+                default:
+                    UNREACHABLE();
+                    break;
+                }
             }
         if (done()) {
             return l_false;
@@ -1361,42 +1380,6 @@ lbool core::test_check(
     return check(l);
 }
 
-// nla_expr<rational> core::mk_expr(lpvar j)  const {
-//     return nla_expr<rational>::var(j);
-// }
-
-// nla_expr<rational> core::mk_expr(const rational &a, lpvar j)  const {
-//     if (a == 1)
-//         return mk_expr(j);
-//     nla_expr<rational> r(expr_type::MUL);
-//     r.add_child(nla_expr<rational>::scalar(a));
-//     r.add_child(nla_expr<rational>::var(j));
-//     return r;            
-// }
-
-// nla_expr<rational> core::mk_expr(const rational &a, const svector<lpvar>& vs) const {
-//     nla_expr<rational> r(expr_type::MUL);
-//     r.add_child(nla_expr<rational>::scalar(a));
-//     for (lpvar j : vs)
-//         r.add_child(nla_expr<rational>::var(j));
-//     return r;            
-// }
-// nla_expr<rational> core::mk_expr(const lp::lar_term& t) const {
-//     auto coeffs = t.coeffs_as_vector();
-//     if (coeffs.size() == 1) {
-//         return mk_expr(coeffs[0].first, coeffs[0].second);
-//     }
-//     nla_expr<rational> r(expr_type::SUM);
-//     for (const auto & p : coeffs) {
-//         lpvar j = p.second;
-//         if (is_monic_var(j))
-//             r.add_child(mk_expr(p.first, m_emons[j].vars()));
-//         else
-//             r.add_child(mk_expr(p.first, j));
-//     }
-//     return r;
-// }
-
 std::ostream& core::print_terms(std::ostream& out) const {
     for (unsigned i=0; i< m_lar_solver.m_terms.size(); i++) {
         unsigned ext = i + m_lar_solver.terms_start_index();
@@ -1424,4 +1407,136 @@ std::ostream& core::print_term( const lp::lar_term& t, std::ostream& out) const
         [this](lpvar j) { return var_str(j); },
         out);
 }
+
+void core::run_pdd_grobner() {
+    m_pdd_manager.resize(m_lar_solver.number_of_vars());
+}
+
+void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {
+    if (active_var_set_contains(j) || var_is_fixed(j)) return;
+    TRACE("grobner", tout << "j = " << j << ", "; print_var(j, tout) << "\n";);
+    const auto& matrix = m_lar_solver.A_r();
+    insert_to_active_var_set(j);
+    for (auto & s : matrix.m_columns[j]) {
+        unsigned row = s.var();
+        if (m_rows.contains(row)) continue;       
+        if (matrix.m_rows[row].size() > m_nla_settings.grobner_row_length_limit()) {
+            TRACE("grobner", tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); 
+            continue;
+        }
+        m_rows.insert(row);
+        for (auto& rc : matrix.m_rows[row]) {
+            add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
+        }
+    }
+
+    if (!is_monic_var(j))
+        return;
+
+    const monic& m = emons()[j];
+    for (auto fcn : factorization_factory_imp(m, *this)) {
+        for (const factor& fc: fcn) {
+            q.push_back(var(fc));
+        }
+    }            
+}
+
+void core::find_nl_cluster(nex_creator& nc) {
+    prepare_rows_and_active_vars();
+    svector<lpvar> q;
+    for (lpvar j : m_to_refine) {        
+        TRACE("grobner", print_monic(emons()[j], tout) << "\n";);
+        q.push_back(j);
+    }
+    
+    while (!q.empty()) {
+        lpvar j = q.back();        
+        q.pop_back();
+        add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
+    }
+    set_active_vars_weights(nc);
+    TRACE("grobner", display_matrix_of_m_rows(tout););
+}
+
+void core::prepare_rows_and_active_vars() {
+    m_rows.clear();
+    m_rows.resize(m_lar_solver.row_count());
+    clear_and_resize_active_var_set();
+}
+
+
+std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e ) {
+    auto ret = get_vars_of_expr(e);
+    auto & ls = m_lar_solver;
+    svector<lpvar> added;
+    for (auto j : ret) {
+        added.push_back(j);
+    }
+    for (unsigned i = 0; i < added.size(); ++i) {
+        lpvar j = added[i];
+        if (ls.column_corresponds_to_term(j)) {
+            const auto& t = m_lar_solver.get_term(ls.local_to_external(j));
+            for (auto p : t) {
+                if (ret.find(p.var()) == ret.end()) {
+                    added.push_back(p.var());
+                    ret.insert(p.var());
+                }
+            }
+        }
+    }
+    return ret;
+}
+
+void core::display_matrix_of_m_rows(std::ostream & out) const {
+    const auto& matrix = m_lar_solver.A_r();
+    out << m_rows.size() << " rows" <<"\n";
+    out << "the matrix\n";          
+    for (const auto & r : matrix.m_rows) {
+        print_term(r, out) << std::endl;
+    }
+}
+
+void core::init_nex_grobner(nex_creator & nc) {   
+    find_nl_cluster(nc);
+    clear_and_resize_active_var_set();
+    TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";);
+    for (unsigned i : m_rows) {
+        m_nex_grobner.add_row(m_lar_solver.A_r().m_rows[i]);
+    }
+}
+
+void core::set_active_vars_weights(nex_creator& nc) {
+    nc.set_number_of_vars(m_lar_solver.column_count());
+    for (lpvar j : active_var_set()) {
+        nc.set_var_weight(j, static_cast<unsigned>(get_var_weight(j)));
+    }
+}
+
+var_weight core::get_var_weight(lpvar j) const {
+    var_weight k;
+    switch (m_lar_solver.get_column_type(j)) {
+        
+    case lp::column_type::fixed:
+        k = var_weight::FIXED;
+        break;
+    case lp::column_type::boxed:
+        k = var_weight::BOUNDED;
+        break;
+    case lp::column_type::lower_bound:
+    case lp::column_type::upper_bound:
+        k = var_weight::NOT_FREE;
+    case lp::column_type::free_column:
+        k = var_weight::FREE;
+        break;
+    default:
+        UNREACHABLE();
+        break;
+    }
+    if (is_monic_var(j)) {
+        return (var_weight)((int)k + 1);
+    }
+    return k;
+}
+
+
 } // end of nla
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 9ef0d88db..9aeb66151 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -31,6 +31,8 @@
 #include "math/lp/horner.h"
 #include "math/lp/nla_grobner.h"
 #include "math/lp/nla_intervals.h"
+#include "math/grobner/pdd_grobner.h"
+
 
 namespace nla {
 
@@ -91,12 +93,17 @@ public:
     monotone                 m_monotone;
     intervals                m_intervals;                
     horner                   m_horner;
-    nla_settings             m_nla_settings;
-    grobner                  m_grobner;
+    nla_settings             m_nla_settings;    
+    grobner                  m_nex_grobner;
+    dd::pdd_manager          m_pdd_manager;
+    dd::grobner              m_pdd_grobner;
+   
 private:
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
     mutable lp::int_set      m_active_var_set;
+    lp::int_set              m_rows;
+
 public:
     reslimit                 m_reslim;
 
@@ -383,6 +390,15 @@ public:
     lpvar map_to_root(lpvar) const;
     std::ostream& print_terms(std::ostream&) const;
     std::ostream& print_term( const lp::lar_term&, std::ostream&) const;
+    void run_pdd_grobner();
+    void find_nl_cluster(nex_creator&);
+    void prepare_rows_and_active_vars();
+    void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j,  svector<lpvar>& q);
+    void init_nex_grobner(nex_creator&);
+    std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
+    void display_matrix_of_m_rows(std::ostream & out) const;
+    void set_active_vars_weights(nex_creator&);
+    var_weight get_var_weight(lpvar) const;
 };  // end of core
 
 struct pp_mon {
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index bab20d050..ddd8369d5 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -36,10 +36,13 @@ grobner::grobner(core *c, intervals *s)
 
 void grobner::grobner_lemmas() {
     c().lp_settings().stats().m_grobner_calls++;
-    init();
-    ptr_vector<grobner_core::equation> eqs;
+    m_gc.reset();
+    m_reported = 0;
     TRACE("grobner", tout << "before:\n"; display(tout););
-    compute_basis();
+    m_gc.compute_basis_loop();
+    for (grobner_core::equation* e : m_gc.equations()) {
+        check_eq(e);
+    }
     TRACE("grobner", tout << "after:\n"; display(tout););
 }
 
@@ -51,125 +54,11 @@ void grobner::check_eq(grobner_core::equation* target) {
                   c().print_var(j, tout);
               }
               tout << "\ntarget->expr() val = " << get_nex_val(target->expr(), [this](unsigned j) { return c().val(j); }) << "\n";);
-        register_report();       
+        m_reported++;       
     }
 }
 
-void grobner::register_report() {
-    m_reported++;
-}
-
-void grobner::compute_basis(){
-    c().lp_settings().stats().m_grobner_basis_computatins++;
-    if (m_rows.size() < 2) {
-        TRACE("nla_grobner", tout << "there are only " << m_rows.size() << " rows, exiting compute_basis()\n";);
-        return;
-    }
-    m_gc.compute_basis_loop();
-
-    TRACE("grobner", display(tout););
-    for (grobner_core::equation* e : m_gc.equations()) {
-        check_eq(e);
-    }
-}
-
-void grobner::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {
-    if (c().active_var_set_contains(j) || c().var_is_fixed(j)) return;
-    TRACE("grobner", tout << "j = " << j << ", "; c().print_var(j, tout) << "\n";);
-    const auto& matrix = c().m_lar_solver.A_r();
-    c().insert_to_active_var_set(j);
-    for (auto & s : matrix.m_columns[j]) {
-        unsigned row = s.var();
-        if (m_rows.contains(row)) continue;       
-        if (matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit()) {
-            TRACE("grobner", tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); 
-            continue;
-        }
-        m_rows.insert(row);
-        for (auto& rc : matrix.m_rows[row]) {
-            add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
-        }
-    }
-
-    if (!c().is_monic_var(j))
-        return;
-
-    const monic& m = c().emons()[j];
-    for (auto fcn : factorization_factory_imp(m, c())) {
-        for (const factor& fc: fcn) {
-            q.push_back(var(fc));
-        }
-    }            
-}
-
-void grobner::find_nl_cluster() {
-    prepare_rows_and_active_vars();
-    svector<lpvar> q;
-    for (lpvar j : c().m_to_refine) {        
-        TRACE("grobner", c().print_monic(c().emons()[j], tout) << "\n";);
-        q.push_back(j);
-    }
-    
-    while (!q.empty()) {
-        lpvar j = q.back();        
-        q.pop_back();
-        add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
-    }
-    set_active_vars_weights();
-    TRACE("grobner", display(tout););
-}
-
-void grobner::prepare_rows_and_active_vars() {
-    m_rows.clear();
-    m_rows.resize(c().m_lar_solver.row_count());
-    c().clear_and_resize_active_var_set();
-}
-
-
-std::unordered_set<lpvar> grobner::get_vars_of_expr_with_opening_terms(const nex *e ) {
-    auto ret = get_vars_of_expr(e);
-    auto & ls = c().m_lar_solver;
-    svector<lpvar> added;
-    for (auto j : ret) {
-        added.push_back(j);
-    }
-    for (unsigned i = 0; i < added.size(); ++i) {
-        lpvar j = added[i];
-        if (ls.column_corresponds_to_term(j)) {
-            const auto& t = c().m_lar_solver.get_term(ls.local_to_external(j));
-            for (auto p : t) {
-                if (ret.find(p.var()) == ret.end()) {
-                    added.push_back(p.var());
-                    ret.insert(p.var());
-                }
-            }
-        }
-    }
-    return ret;
-}
-
-void grobner::display_matrix(std::ostream & out) const {
-    const auto& matrix = c().m_lar_solver.A_r();
-    out << m_rows.size() << " rows" <<"\n";
-    out << "the matrix\n";          
-    for (const auto & r : matrix.m_rows) {
-        c().print_term(r, out) << std::endl;
-    }
-}
-
-void grobner::init() {
-    m_gc.reset();
-    m_reported = 0;
-    find_nl_cluster();
-    c().clear_and_resize_active_var_set();
-    TRACE("grobner", tout << "m_rows.size() = " << m_rows.size() << "\n";);
-    for (unsigned i : m_rows) {
-        add_row(i);
-    }
-}
-
-void grobner::add_row(unsigned i) {    
-    const auto& row = c().m_lar_solver.A_r().m_rows[i];    
+void grobner::add_row(const vector<lp::row_cell<rational>> & row) {    
     TRACE("grobner", tout << "adding row to gb\n"; c().m_lar_solver.print_row(row, tout) << '\n';
           for (auto p : row) c().print_var(p.var(), tout) << "\n"; );
     nex_creator::sum_factory sf(m_nex_creator);
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
index b8896eb6e..e319ae941 100644
--- a/src/math/lp/nla_grobner.h
+++ b/src/math/lp/nla_grobner.h
@@ -205,23 +205,20 @@ private:
 class grobner : common {
     grobner_core m_gc;
     unsigned     m_reported;
-    lp::int_set  m_rows;
 public:
     grobner(core *, intervals *);
     void grobner_lemmas();
     ~grobner() {}
 private:
-    void find_nl_cluster();
     void prepare_rows_and_active_vars();
     void add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j,  svector<lpvar>& q);
     void init();
-    void compute_basis();       
     std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
     void display_matrix(std::ostream & out) const;
     std::ostream& display(std::ostream& out) const { return m_gc.display(out); }
-    void add_row(unsigned);
+public:
+    void add_row(const vector<lp::row_cell<rational>> & row);
     void check_eq(grobner_core::equation*);
-    void register_report();
-
+    nex_creator& get_nex_creator() { return m_nex_creator; }
 }; // end of grobner
 }