diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 2f6d11601e..baaf483cda 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -619,7 +619,7 @@ void cmd_context::set_produce_unsat_cores(bool f) {
 }
 
 void cmd_context::set_produce_proofs(bool f) {
-    SASSERT(!has_assertions());
+    SASSERT(!has_assertions() || m_params.m_proof == f);
     if (has_manager()) 
         m().toggle_proof_mode(f ? PGM_ENABLED : PGM_DISABLED);
     m_params.m_proof = f;
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 41482f3c2a..7fb34b5a38 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -31,8 +31,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
     m_intervals(this, lim),
     m_monomial_bounds(this),
     m_horner(this),
-    m_pdd_manager(s.number_of_vars()),
-    m_pdd_grobner(lim, m_pdd_manager),
+    m_grobner(this),
     m_emons(m_evars),
     m_reslim(lim),
     m_use_nra_model(false),
@@ -1506,7 +1505,7 @@ lbool core::check(vector<lemma>& l_vec) {
         m_horner.horner_lemmas();
 
     if (l_vec.empty() && !done() && need_run_grobner()) 
-        run_grobner();                
+        m_grobner();                
 
     if (l_vec.empty() && !done()) 
         m_basics.basic_lemma(true); 
@@ -1661,51 +1660,15 @@ std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e
 }
 
 
-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, get_var_weight(j));
+bool core::is_nl_var(lpvar j) const {
+    return is_monic_var(j) || m_emons.is_used_in_monic(j);
 }
 
-void core::set_level2var_for_grobner() {
-    unsigned n = m_lar_solver.column_count();
-    unsigned_vector sorted_vars(n), weighted_vars(n);
-    for (unsigned j = 0; j < n; j++) {
-        sorted_vars[j] = j;
-        weighted_vars[j] = get_var_weight(j);
-    }
-#if 1
-    // potential update to weights
-    for (unsigned j = 0; j < n; j++) {
-        if (is_monic_var(j) && m_to_refine.contains(j)) {
-            for (lpvar k : m_emons[j].vars()) {
-                weighted_vars[k] += 6;
-            }
-        }
-    }
-#endif
-
-    std::sort(sorted_vars.begin(), sorted_vars.end(), [&](unsigned a, unsigned b) {
-                                                      unsigned wa = weighted_vars[a];
-                                                      unsigned wb = weighted_vars[b];
-                                                      return wa < wb || (wa == wb && a < b); });
-
-    unsigned_vector l2v(n);
-    for (unsigned j = 0; j < n; j++)
-        l2v[j] = sorted_vars[j];
-
-    m_pdd_manager.reset(l2v);
-
-    TRACE("grobner",
-          for (auto v : sorted_vars)
-              tout << "j" << v << " w:" << weighted_vars[v] << " ";
-          tout << "\n");
-}
 
 unsigned core::get_var_weight(lpvar j) const {
     unsigned k;
     switch (m_lar_solver.get_column_type(j)) {
-        
+
     case lp::column_type::fixed:
         k = 0;
         break;
@@ -1725,14 +1688,17 @@ unsigned core::get_var_weight(lpvar j) const {
     }
     if (is_monic_var(j)) {
         k++;
-        if (m_to_refine.contains(j)) 
+        if (m_to_refine.contains(j))
             k++;
     }
     return k;
 }
 
-bool core::is_nl_var(lpvar j) const {
-    return is_monic_var(j) || m_emons.is_used_in_monic(j);
+
+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, get_var_weight(j));
 }
 
 bool core::influences_nl_var(lpvar j) const {
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 043a74655a..5c44f53a6e 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -18,13 +18,13 @@
 #include "math/lp/nla_basics_lemmas.h"
 #include "math/lp/nla_order_lemmas.h"
 #include "math/lp/nla_monotone_lemmas.h"
+#include "math/lp/nla_grobner.h"
 #include "math/lp/emonics.h"
 #include "math/lp/nla_settings.h"
 #include "math/lp/nex.h"
 #include "math/lp/horner.h"
 #include "math/lp/monomial_bounds.h"
 #include "math/lp/nla_intervals.h"
-#include "math/grobner/pdd_solver.h"
 #include "nlsat/nlsat_solver.h"
 
 
@@ -139,6 +139,9 @@ struct pp_factorization {
 };
 
 class core {
+    friend class new_lemma;
+    friend class grobner;
+
     struct stats {
         unsigned m_nla_explanations;
         unsigned m_nla_lemmas;
@@ -148,11 +151,11 @@ class core {
             memset(this, 0, sizeof(*this));
         }
     };
-    stats                    m_stats;
-    friend class new_lemma;
 
-    unsigned m_nlsat_delay { 50 };
-    unsigned m_nlsat_fails { 0 };
+    stats    m_stats;
+    unsigned m_nlsat_delay = 50;
+    unsigned m_nlsat_fails = 0;
+
     bool should_run_bounded_nlsat();
     lbool bounded_nlsat();
 public:
@@ -168,13 +171,12 @@ class core {
     monomial_bounds          m_monomial_bounds;
     horner                   m_horner;
     nla_settings             m_nla_settings;    
-    dd::pdd_manager          m_pdd_manager;
-    dd::solver               m_pdd_grobner;
+    grobner                  m_grobner;
 private:
     emonics                  m_emons;
     svector<lpvar>           m_add_buffer;
     mutable lp::u_set        m_active_var_set;
-    lp::u_set                m_rows;
+
     reslimit                 m_nra_lim;
 public:
     reslimit&                m_reslim;
@@ -205,6 +207,8 @@ class core {
         m_active_var_set.resize(m_lar_solver.number_of_vars());
     }
     
+    unsigned get_var_weight(lpvar) const;
+
     reslimit& reslim() { return m_reslim; }  
     emonics& emons() { return m_emons; }
     const emonics& emons() const { return m_emons; }
@@ -249,6 +253,9 @@ class core {
     bool need_run_grobner() const { 
         return m_nla_settings.run_grobner && lp_settings().stats().m_nla_calls % m_nla_settings.grobner_frequency == 0; 
     }
+
+    void set_active_vars_weights(nex_creator&);
+    std::unordered_set<lpvar> get_vars_of_expr_with_opening_terms(const nex* e);
     
     void incremental_linearization(bool);
     
@@ -450,33 +457,16 @@ class core {
     lpvar map_to_root(lpvar) const;
     std::ostream& print_terms(std::ostream&) const;
     std::ostream& print_term(const lp::lar_term&, std::ostream&) const;
+
     template <typename T>
-    std::ostream& print_row(const T & row , std::ostream& out) const {
+    std::ostream& print_row(const T& row, std::ostream& out) const {
         vector<std::pair<rational, lpvar>> v;
         for (auto p : row) {
             v.push_back(std::make_pair(p.coeff(), p.var()));
         }
-        return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out);        
+        return lp::print_linear_combination_customized(v, [this](lpvar j) { return var_str(j); }, out);
     }
-
     
-    void run_grobner();
-    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);
-    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&);
-    unsigned get_var_weight(lpvar) const;
-    void add_row_to_grobner(const vector<lp::row_cell<rational>> & row);
-    void add_fixed_monic_to_grobner(unsigned j);
-    bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
-    void add_eq_to_grobner(dd::pdd& p, u_dependency* dep);
-    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_grobner();
-    void configure_grobner();
     bool influences_nl_var(lpvar) const;
     bool is_nl_var(lpvar) const;
     
diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index f674c0e01b..c5d1e7c2dc 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -20,16 +20,28 @@ Module Name:
 
 namespace nla {
 
-    void core::run_grobner() {
-        unsigned& quota = m_nla_settings.grobner_quota;
+    grobner::grobner(core* c):
+        common(c),
+        m_pdd_manager(m_core.m_lar_solver.number_of_vars()),
+        m_pdd_grobner(m_core.m_reslim, m_pdd_manager),
+        m_lar_solver(m_core.m_lar_solver)
+
+    {}
+
+    lp::lp_settings& grobner::lp_settings() {
+        return c().lp_settings();
+    }
+
+    void grobner::operator()() {
+        unsigned& quota = c().m_nla_settings.grobner_quota;
         if (quota == 1) {
             return;
         }
-        clear_and_resize_active_var_set(); 
+        c().clear_and_resize_active_var_set(); 
         find_nl_cluster();
 
-        lp_settings().stats().m_grobner_calls++;
-        configure_grobner();
+        c().lp_settings().stats().m_grobner_calls++;
+        configure();
         m_pdd_grobner.saturate();
         bool conflict = false;
         unsigned n = m_pdd_grobner.number_of_conflicts_to_report();
@@ -47,6 +59,20 @@ namespace nla {
             return;
         }
 
+        if (propagate_bounds())
+            return;
+
+        if (propagate_eqs())
+            return;
+
+        if (quota > 1)
+            quota--;
+
+
+        IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota << "\n");
+        IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
+
+
 #if 0
         // diagnostics: did we miss something
         vector<dd::pdd> eqs;
@@ -81,29 +107,33 @@ namespace nla {
             return;
 #endif
 
-        if (quota > 1)
-            quota--;
-        IF_VERBOSE(2, verbose_stream() << "grobner miss, quota " << quota <<  "\n");
-        IF_VERBOSE(4, diagnose_pdd_miss(verbose_stream()));
     
     }
 
-    void core::configure_grobner() {
+    bool grobner::propagate_bounds() {
+        return false;
+    }
+
+    bool grobner::propagate_eqs() {
+        return false;
+    }
+
+    void grobner::configure() {
         m_pdd_grobner.reset();
         try {
-            set_level2var_for_grobner();
+            set_level2var();
             TRACE("grobner",
                   tout << "base vars: ";
-                  for (lpvar j : active_var_set())
-                      if (m_lar_solver.is_base(j))
+                  for (lpvar j : c().active_var_set())
+                      if (c().m_lar_solver.is_base(j))
                           tout << "j" << j << " ";
                   tout << "\n");
-            for (lpvar j : active_var_set()) {
-                if (m_lar_solver.is_base(j))
-                    add_row_to_grobner(m_lar_solver.basic2row(j));
+            for (lpvar j : c().active_var_set()) {
+                if (c().m_lar_solver.is_base(j))
+                    add_row(c().m_lar_solver.basic2row(j));
                 
-                if (is_monic_var(j) && var_is_fixed(j))
-                    add_fixed_monic_to_grobner(j);
+                if (c().is_monic_var(j) && c().var_is_fixed(j))
+                    add_fixed_monic(j);
             }
         }
         catch (...) {
@@ -127,17 +157,17 @@ namespace nla {
    
         struct dd::solver::config cfg;
         cfg.m_max_steps = m_pdd_grobner.equations().size();
-        cfg.m_max_simplified = m_nla_settings.grobner_max_simplified;
-        cfg.m_eqs_growth = m_nla_settings.grobner_eqs_growth;
-        cfg.m_expr_size_growth = m_nla_settings.grobner_expr_size_growth;
-        cfg.m_expr_degree_growth = m_nla_settings.grobner_expr_degree_growth;
-        cfg.m_number_of_conflicts_to_report = m_nla_settings.grobner_number_of_conflicts_to_report;
+        cfg.m_max_simplified = c().m_nla_settings.grobner_max_simplified;
+        cfg.m_eqs_growth = c().m_nla_settings.grobner_eqs_growth;
+        cfg.m_expr_size_growth = c().m_nla_settings.grobner_expr_size_growth;
+        cfg.m_expr_degree_growth = c().m_nla_settings.grobner_expr_degree_growth;
+        cfg.m_number_of_conflicts_to_report = c().m_nla_settings.grobner_number_of_conflicts_to_report;
         m_pdd_grobner.set(cfg);
         m_pdd_grobner.adjust_cfg();
         m_pdd_manager.set_max_num_nodes(10000); // or something proportional to the number of initial nodes.
     }
 
-    std::ostream& core::diagnose_pdd_miss(std::ostream& out) {
+    std::ostream& grobner::diagnose_pdd_miss(std::ostream& out) {
 
         // m_pdd_grobner.display(out);
 
@@ -163,12 +193,12 @@ namespace nla {
         return out;
     }
 
-    bool core::check_pdd_eq(const dd::solver::equation* e) {
-        auto& di = m_intervals.get_dep_intervals();
+    bool grobner::check_pdd_eq(const dd::solver::equation* e) {
+        auto& di = c().m_intervals.get_dep_intervals();
         dd::pdd_interval eval(di);
         eval.var2interval() = [this](lpvar j, bool deps, scoped_dep_interval& a) {
-            if (deps) m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
-            else m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
+            if (deps) c().m_intervals.set_var_interval<dd::w_dep::with_deps>(j, a);
+            else c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
         };
         scoped_dep_interval i(di), i_wd(di);
         eval.get_interval<dd::w_dep::without_deps>(e->poly(), i);    
@@ -178,8 +208,8 @@ namespace nla {
                   tout << "separated from 0: " << di.separated_from_zero(i) << "\n";
                   for (auto j : e->poly().free_vars()) {
                       scoped_dep_interval a(di);
-                      m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
-                      m_intervals.display(tout << "j" << j << " ", a); tout << " ";
+                      c().m_intervals.set_var_interval<dd::w_dep::without_deps>(j, a);
+                      c().m_intervals.display(tout << "j" << j << " ", a); tout << " ";
                   }
                   tout << "\n");
         
@@ -187,7 +217,7 @@ namespace nla {
         }
         eval.get_interval<dd::w_dep::with_deps>(e->poly(), i_wd);  
         std::function<void (const lp::explanation&)> f = [this](const lp::explanation& e) {
-            new_lemma lemma(*this, "pdd");
+            new_lemma lemma(m_core, "pdd");
             lemma &= e;
         };
         if (di.check_interval_for_conflict_on_zero(i_wd, e->dep(), f)) {
@@ -201,18 +231,18 @@ namespace nla {
         }
     }
 
-    void core::add_var_and_its_factors_to_q_and_collect_new_rows(lpvar j, svector<lpvar> & q) {
-        if (active_var_set_contains(j))
+    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))
             return;
-        insert_to_active_var_set(j);
-        if (is_monic_var(j)) {
-            const monic& m = emons()[j];
-            for (auto fcn : factorization_factory_imp(m, *this)) 
+        c().insert_to_active_var_set(j);
+        if (c().is_monic_var(j)) {
+            const monic& m = c().emons()[j];
+            for (auto fcn : factorization_factory_imp(m, m_core)) 
                 for (const factor& fc: fcn) 
                     q.push_back(var(fc));        
         }
 
-        if (var_is_fixed(j))
+        if (c().var_is_fixed(j))
             return;
         const auto& matrix = m_lar_solver.A_r();
         for (auto & s : matrix.m_columns[j]) {
@@ -223,9 +253,9 @@ namespace nla {
             unsigned k = m_lar_solver.get_base_column_in_row(row);
             if (m_lar_solver.column_is_free(k) && k != j)
                 continue;
-            CTRACE("grobner", matrix.m_rows[row].size() > m_nla_settings.grobner_row_length_limit,
+            CTRACE("grobner", matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit,
                    tout << "ignore the row " << row << " with the size " << matrix.m_rows[row].size() << "\n";); 
-            if (matrix.m_rows[row].size() > m_nla_settings.grobner_row_length_limit) 
+            if (matrix.m_rows[row].size() > c().m_nla_settings.grobner_row_length_limit)
                 continue;
             for (auto& rc : matrix.m_rows[row]) 
                 add_var_and_its_factors_to_q_and_collect_new_rows(rc.var(), q);
@@ -234,33 +264,33 @@ namespace nla {
 
     }
 
-    const rational& core::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) {
+    const rational& grobner::val_of_fixed_var_with_deps(lpvar j, u_dependency*& dep) {
         unsigned lc, uc;
         m_lar_solver.get_bound_constraint_witnesses_for_column(j, lc, uc);
-        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(lc));
-        dep = m_intervals.mk_join(dep, m_intervals.mk_leaf(uc));
+        dep = c().m_intervals.mk_join(dep, c().m_intervals.mk_leaf(lc));
+        dep = c().m_intervals.mk_join(dep, c().m_intervals.mk_leaf(uc));
         return m_lar_solver.column_lower_bound(j).x;
     }
 
-    dd::pdd core::pdd_expr(const rational& c, lpvar j, u_dependency*& dep) {
-        dd::pdd r = m_pdd_manager.mk_val(c);
+    dd::pdd grobner::pdd_expr(const rational& coeff, lpvar j, u_dependency*& dep) {
+        dd::pdd r = m_pdd_manager.mk_val(coeff);
         sbuffer<lpvar> vars;
         vars.push_back(j);
         u_dependency* zero_dep = dep;
         while (!vars.empty()) {
             j = vars.back();
             vars.pop_back();
-            if (m_nla_settings.grobner_subs_fixed > 0 && var_is_fixed_to_zero(j)) {
+            if (c().m_nla_settings.grobner_subs_fixed > 0 && c().var_is_fixed_to_zero(j)) {
                 r = m_pdd_manager.mk_val(val_of_fixed_var_with_deps(j, zero_dep));
                 dep = zero_dep;
                 return r;
             }
-            if (m_nla_settings.grobner_subs_fixed == 1 && var_is_fixed(j))
+            if (c().m_nla_settings.grobner_subs_fixed == 1 && c().var_is_fixed(j))
                 r *= val_of_fixed_var_with_deps(j, dep);
-            else if (!is_monic_var(j))
+            else if (!c().is_monic_var(j))
                 r *= m_pdd_manager.mk_var(j);
             else
-                for (lpvar k : emons()[j].vars())
+                for (lpvar k : c().emons()[j].vars())
                     vars.push_back(k);        
         }
         return r;
@@ -277,7 +307,7 @@ namespace nla {
        we prefer to solve z == -x - y instead of x == -z - y
        because the solution -z - y has neither an upper, nor a lower bound.
     */
-    bool core::is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r) {
+    bool grobner::is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r) {
         if (!p.is_linear())
             return false;
         r = p;
@@ -325,7 +355,7 @@ namespace nla {
     /**
        \brief add an equality to grobner solver, convert it to solved form if available.
     */    
-    void core::add_eq_to_grobner(dd::pdd& p, u_dependency* dep) {
+    void grobner::add_eq(dd::pdd& p, u_dependency* dep) {
         unsigned v;
         dd::pdd q(m_pdd_manager);
         m_pdd_grobner.simplify(p, dep);
@@ -335,32 +365,32 @@ namespace nla {
             m_pdd_grobner.add(p, dep);    
     }
 
-    void core::add_fixed_monic_to_grobner(unsigned j) {
+    void grobner::add_fixed_monic(unsigned j) {
         u_dependency* dep = nullptr;
         dd::pdd r = m_pdd_manager.mk_val(rational(1));
-        for (lpvar k : emons()[j].vars()) 
+        for (lpvar k : c().emons()[j].vars())
             r *= pdd_expr(rational::one(), k, dep);
         r -= val_of_fixed_var_with_deps(j, dep);
-        add_eq_to_grobner(r, dep);
+        add_eq(r, dep);
     }
 
-    void core::add_row_to_grobner(const vector<lp::row_cell<rational>> & row) {
+    void grobner::add_row(const vector<lp::row_cell<rational>> & row) {
         u_dependency *dep = nullptr;
         rational val;
         dd::pdd sum = m_pdd_manager.mk_val(rational(0));
         for (const auto &p : row) 
             sum += pdd_expr(p.coeff(), p.var(), dep);
-        TRACE("grobner", print_row(row, tout) << " " << sum << "\n");
-        add_eq_to_grobner(sum, dep);
+        TRACE("grobner", c().print_row(row, tout) << " " << sum << "\n");
+        add_eq(sum, dep);
     }
 
 
-    void core::find_nl_cluster() {
+    void grobner::find_nl_cluster() {
         prepare_rows_and_active_vars();
         svector<lpvar> q;
-        TRACE("grobner", for (lpvar j : m_to_refine) print_monic(emons()[j], tout) << "\n";);
+        TRACE("grobner", for (lpvar j : c().m_to_refine) print_monic(c().emons()[j], tout) << "\n";);
           
-        for (lpvar j : m_to_refine) 
+        for (lpvar j : c().m_to_refine)
             q.push_back(j);
     
         while (!q.empty()) {
@@ -369,25 +399,59 @@ namespace nla {
             add_var_and_its_factors_to_q_and_collect_new_rows(j, q);
         }
         TRACE("grobner", tout << "vars in cluster: ";
-              for (lpvar j : active_var_set()) tout << "j" << j << " "; tout << "\n";
+              for (lpvar j : c().active_var_set()) tout << "j" << j << " "; tout << "\n";
               display_matrix_of_m_rows(tout);
               );
     }
 
-    void core::prepare_rows_and_active_vars() {
+    void grobner::prepare_rows_and_active_vars() {
         m_rows.clear();
         m_rows.resize(m_lar_solver.row_count());
-        clear_and_resize_active_var_set();
+        c().clear_and_resize_active_var_set();
     }
 
 
-    void core::display_matrix_of_m_rows(std::ostream & out) const {
+    void grobner::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_row(r, out) << std::endl;
+            c().print_row(r, out) << std::endl;
     }
     
+    void grobner::set_level2var() {
+        unsigned n = m_lar_solver.column_count();
+        unsigned_vector sorted_vars(n), weighted_vars(n);
+        for (unsigned j = 0; j < n; j++) {
+            sorted_vars[j] = j;
+            weighted_vars[j] = c().get_var_weight(j);
+        }
+#if 1
+        // potential update to weights
+        for (unsigned j = 0; j < n; j++) {
+            if (c().is_monic_var(j) && c().m_to_refine.contains(j)) {
+                for (lpvar k : c().m_emons[j].vars()) {
+                    weighted_vars[k] += 6;
+                }
+            }
+        }
+#endif
+
+        std::sort(sorted_vars.begin(), sorted_vars.end(), [&](unsigned a, unsigned b) {
+            unsigned wa = weighted_vars[a];
+            unsigned wb = weighted_vars[b];
+            return wa < wb || (wa == wb && a < b); });
+
+        unsigned_vector l2v(n);
+        for (unsigned j = 0; j < n; j++)
+            l2v[j] = sorted_vars[j];
+
+        m_pdd_manager.reset(l2v);
+
+        TRACE("grobner",
+            for (auto v : sorted_vars)
+                tout << "j" << v << " w:" << weighted_vars[v] << " ";
+        tout << "\n");
+    }
 
 }
diff --git a/src/math/lp/nla_grobner.h b/src/math/lp/nla_grobner.h
new file mode 100644
index 0000000000..a9b284a744
--- /dev/null
+++ b/src/math/lp/nla_grobner.h
@@ -0,0 +1,49 @@
+/*++
+  Copyright (c) 2017 Microsoft Corporation
+
+  Author:
+  Nikolaj Bjorner (nbjorner)
+  Lev Nachmanson (levnach)
+
+  --*/
+#pragma once
+
+#include "math/lp/nla_common.h"
+#include "math/lp/nla_intervals.h"
+#include "math/lp/nex.h"
+#include "math/lp/cross_nested.h"
+#include "math/lp/u_set.h"
+#include "math/grobner/pdd_solver.h"
+
+namespace nla {
+    class core;
+
+    class grobner : common {
+        dd::pdd_manager          m_pdd_manager;
+        dd::solver               m_pdd_grobner;
+        lp::lar_solver&          m_lar_solver;
+        lp::u_set                m_rows;
+
+        bool propagate_bounds();
+        bool propagate_eqs();
+        lp::lp_settings& lp_settings();
+        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 display_matrix_of_m_rows(std::ostream& out) const;        
+        void add_row(const vector<lp::row_cell<rational>>& row);
+        void add_fixed_monic(unsigned j);
+        bool is_solved(dd::pdd const& p, unsigned& v, dd::pdd& r);
+        void add_eq(dd::pdd& p, u_dependency* dep);
+        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();
+        void configure();
+        std::ostream& diagnose_pdd_miss(std::ostream& out);
+
+    public:
+        grobner(core *core);        
+        void operator()();
+    }; 
+}