From 8a665e25ed72b5719ec33f0a2f84ba632e35b366 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Mar 2020 17:14:59 -0700
Subject: [PATCH] reverting signed mon_eq, try to rely on canonization state
 during add/pop

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/emonics.cpp             | 43 +++++++++++++-----------
 src/math/lp/emonics.h               |  4 +--
 src/math/lp/factorization.h         |  1 -
 src/math/lp/monic.h                 | 42 +++++++++++------------
 src/math/lp/nla_basics_lemmas.cpp   | 26 +++++++--------
 src/math/lp/nla_common.cpp          |  4 ++-
 src/math/lp/nla_common.h            |  2 ++
 src/math/lp/nla_core.cpp            | 13 ++++----
 src/math/lp/nla_core.h              | 10 ++++--
 src/math/lp/nla_monotone_lemmas.cpp |  2 +-
 src/math/lp/nla_order_lemmas.cpp    | 52 ++++++++++++++++-------------
 src/math/lp/nra_solver.cpp          |  2 +-
 12 files changed, 110 insertions(+), 91 deletions(-)

diff --git a/src/math/lp/emonics.cpp b/src/math/lp/emonics.cpp
index dab621bf9..9079c7c01 100644
--- a/src/math/lp/emonics.cpp
+++ b/src/math/lp/emonics.cpp
@@ -53,12 +53,15 @@ void emonics::pop(unsigned n) {
     for (unsigned j = 0; j < n; ++j) {
         unsigned old_sz = m_lim[m_lim.size() - 1];
         for (unsigned i = m_monics.size(); i-- > old_sz; ) {
+            m_ve.pop(1);
             monic & m = m_monics[i];
             TRACE("nla_solver_mons", display(tout << m << "\n"););
             remove_cg_mon(m);
             m_var2index[m.var()] = UINT_MAX;
+            do_canonize(m);
+            // variables in vs are in the same state as they were when add was called
             lpvar last_var = UINT_MAX;
-            for (lpvar v : m.vars()) {
+            for (lpvar v : m.rvars()) {
                 if (v != last_var) {
                     remove_cell(m_use_lists[v]);
                     last_var = v;
@@ -168,7 +171,7 @@ monic const* emonics::find_canonical(svector<lpvar> const& vars) const {
 
 void emonics::remove_cg(lpvar v) {
     TRACE("nla_solver_mons", tout << "remove: " << v << "\n";);
-    TRACE("nla_solver_mons", display(tout););
+//    TRACE("nla_solver_mons", display(tout););
     cell* c = m_use_lists[v].m_head;
     if (c == nullptr) {
         return;
@@ -233,7 +236,7 @@ void emonics::insert_cg(lpvar v) {
         }
     }
     while (c != first);
-    TRACE("nla_solver_mons", display(tout << "insert: " << v << "\n"););    
+    TRACE("nla_solver_mons", tout << "insert: " << v << "\n";);    
 }
 
 bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::unordered_set<lpvar>, hash_svector>& lists) const {    
@@ -248,6 +251,7 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
         }
     }
     for (auto const & m : m_monics) {
+        // bail out of invariant check
         SASSERT(is_canonized(m));
         if (!is_canonical_monic(m.var()))
             continue;
@@ -279,7 +283,7 @@ bool emonics::elists_are_consistent(std::unordered_map<unsigned_vector, std::uno
 void emonics::insert_cg_mon(monic & m) {
     do_canonize(m);
     lpvar v = m.var(), w;
-    TRACE("nla_solver_mons", tout << m << " hash: " << m_cg_hash(v) << "\n";);
+    TRACE("nla_solver_mons", tout << m << "\n";); //  hash: " << m_cg_hash(v) << "\n";);
     auto* entry = m_cg_table.insert_if_not_there2(v, unsigned_vector());
     auto& vec = entry->get_data().m_value;
     if (vec.empty()) {
@@ -323,21 +327,14 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
     SASSERT(!is_monic_var(v));
     m_ve.push();
     unsigned idx = m_monics.size();
-    bool sign = false; 
-    m_vs.reset();
-    for (unsigned i = 0; i < sz; ++i) {        
-        signed_var sv = m_ve.find(vs[i]);
-        m_vs.push_back(sv.var());
-        sign ^= sv.sign();
-    }
-    m_monics.push_back(monic(sign, v, sz, m_vs.c_ptr(), idx));
+    m_monics.push_back(monic(v, sz, vs, idx));
+    do_canonize(m_monics.back());
 
-    // variables in the new monic are sorted, 
+    // variables in m_vs are canonical and sorted, 
     // so use last_var to skip duplicates, 
     // while updating use-lists
     lpvar last_var = UINT_MAX;
-    for (lpvar w : m_monics[idx].vars()) {
-        SASSERT(w == m_ve.find(w).var());
+    for (lpvar w : m_monics.back().rvars()) {
         if (w != last_var) {
             m_use_lists.reserve(w + 1);
             insert_cell(m_use_lists[w], idx);
@@ -347,6 +344,7 @@ void emonics::add(lpvar v, unsigned sz, lpvar const* vs) {
     m_var2index.setx(v, idx, UINT_MAX);
     insert_cg_mon(m_monics[idx]);
     SASSERT(invariant());
+    m_ve.push();
 }
 
 void emonics::do_canonize(monic & m) const {
@@ -363,6 +361,12 @@ bool emonics::is_canonized(const monic & m) const {
     return mm.rvars() == m.rvars();
 }
 
+void emonics::ensure_canonized() {
+    for (auto & m : m_monics) {
+        do_canonize(m);
+    }
+}
+
 bool emonics::monics_are_canonized() const {
     for (auto & m: m_monics) {
         if (!is_canonized(m)) {
@@ -372,7 +376,6 @@ bool emonics::monics_are_canonized() const {
     return true;
 }
 
-
 bool emonics::canonize_divides(monic& m, monic & n) const {
     if (m.size() > n.size()) return false;
     unsigned ms = m.size(), ns = n.size();
@@ -398,7 +401,9 @@ bool emonics::canonize_divides(monic& m, monic & n) const {
 
 // yes, assume that monics are non-empty.
 emonics::pf_iterator::pf_iterator(emonics const& m, monic & mon, bool at_end):
-    m_em(m), m_mon(&mon), m_it(iterator(m, m.head(mon.vars()[0]), at_end)), m_end(iterator(m, m.head(mon.vars()[0]), true)) {
+    m_em(m), m_mon(&mon), 
+    m_it(iterator(m, m.head(mon.vars()[0]), at_end)), 
+    m_end(iterator(m, m.head(mon.vars()[0]), true)) {
     fast_forward();
 }
 
@@ -425,7 +430,7 @@ void emonics::merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v
 }
 
 void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed_var v1) {
-    if (m_ve.find(~r1) == m_ve.find(~r2)) { // the other sign has also been merged
+    if (m_ve.find(~r1) == m_ve.find(~r2) && r1.var() != r2.var()) { // the other sign has also been merged
         TRACE("nla_solver_mons", tout << r2 << " <- " << r1 << "\n";);
         m_use_lists.reserve(std::max(r2.var(), r1.var()) + 1);
         TRACE("nla_solver_mons", tout << "rehashing " << r1.var() << "\n";);
@@ -435,7 +440,7 @@ void emonics::after_merge_eh(signed_var r2, signed_var r1, signed_var v2, signed
 }
 
 void emonics::unmerge_eh(signed_var r2, signed_var r1) {
-    if (m_ve.find(~r1) != m_ve.find(~r2)) { // the other sign has also been unmerged
+    if (m_ve.find(~r1) != m_ve.find(~r2) && r1.var() != r2.var()) { // the other sign has also been unmerged
         TRACE("nla_solver_mons", tout << r2 << " -> " << r1 << "\n";);
         unmerge_cells(m_use_lists[r2.var()], m_use_lists[r1.var()]);            
         rehash_cg(r1.var());
diff --git a/src/math/lp/emonics.h b/src/math/lp/emonics.h
index 866ad3c73..243f65f1e 100644
--- a/src/math/lp/emonics.h
+++ b/src/math/lp/emonics.h
@@ -93,7 +93,6 @@ class emonics {
     mutable svector<head_tail>   m_use_lists;     // use list of monics where variables occur.
     hash_canonical               m_cg_hash;
     eq_canonical                 m_cg_eq;
-    unsigned_vector              m_vs;            // temporary buffer of canonized variables
     map<lpvar, unsigned_vector, hash_canonical, eq_canonical> m_cg_table; // congruence (canonical) table.
 
 
@@ -167,7 +166,8 @@ public:
     monic & operator[](lpvar v) { return m_monics[m_var2index[v]]; }
     bool is_canonized(const monic&) const;    
     bool monics_are_canonized() const;
-    
+    void ensure_canonized();
+ 
     /**
        \brief obtain the representative canonized monic 
     */
diff --git a/src/math/lp/factorization.h b/src/math/lp/factorization.h
index 1606020a9..6998389b0 100644
--- a/src/math/lp/factorization.h
+++ b/src/math/lp/factorization.h
@@ -73,7 +73,6 @@ public:
     void push_back(factor const& v) { m_factors.push_back(v); }
     const monic& mon() const { return *m_mon; }
     void set_mon(const monic* m) { m_mon = m; }
-
 };
 
 struct const_iterator_mon {
diff --git a/src/math/lp/monic.h b/src/math/lp/monic.h
index f22b7c0c1..5a2773416 100644
--- a/src/math/lp/monic.h
+++ b/src/math/lp/monic.h
@@ -2,45 +2,45 @@
   Copyright (c) 2017 Microsoft Corporation
   Author: Nikolaj Bjorner
   Lev Nachmanson
+
+
+  A mon_eq represents a definition m_v = v1*v2*...*vn, 
+  where m_vs = [v1, v2, .., vn]
       
+  A monic contains a mon_eq and variables in canonized form.
+
 */
+
 #pragma once
 #include "math/lp/lp_settings.h"
 #include "util/vector.h"
 #include "math/lp/lar_solver.h"
 #include "math/lp/nla_defs.h"
 namespace nla {
-/*
- *  represents definition m_v = v1*v2*...*vn, 
- *  where m_vs = [v1, v2, .., vn]
- */
 
 class mon_eq {
     // fields
-    bool                   m_sign;
     lp::var_index          m_v;
     svector<lp::var_index> m_vs;
 public:
     // constructors
-    mon_eq(bool sign, lp::var_index v, unsigned sz, lp::var_index const* vs):
-        m_sign(sign), m_v(v), m_vs(sz, vs) {
+    mon_eq(lp::var_index v, unsigned sz, lp::var_index const* vs):
+        m_v(v), m_vs(sz, vs) {
         std::sort(m_vs.begin(), m_vs.end());
     }
-    mon_eq(bool sign, lp::var_index v, const svector<lp::var_index> &vs):
-        m_sign(sign), m_v(v), m_vs(vs) {
+    mon_eq(lp::var_index v, const svector<lp::var_index> &vs):
+        m_v(v), m_vs(vs) {
         std::sort(m_vs.begin(), m_vs.end());
     }
-    mon_eq():m_sign(false), m_v(UINT_MAX) {}
+    mon_eq(): m_v(UINT_MAX) {}
         
     unsigned var() const { return m_v; }
     unsigned size() const { return m_vs.size(); }
-    bool sign() const { return m_sign; }
     const svector<lp::var_index>& vars() const { return m_vs; }
     bool empty() const { return m_vs.empty(); }
 
 protected:
     svector<lp::var_index>& vars1() { return m_vs; }
-
 };
 
 // support the congruence    
@@ -51,11 +51,10 @@ class monic: public mon_eq {
     mutable unsigned m_visited;
 public:
     // constructors
-    monic(bool sign, lpvar v, unsigned sz, lpvar const* vs, unsigned idx):  
-        monic(sign, v, svector<lpvar>(sz, vs), idx) {
-    }
-    monic(bool sign, lpvar v, const svector<lpvar> &vs, unsigned idx): 
-        mon_eq(sign, v, vs), m_rsign(false),  m_visited(0) {
+    monic(lpvar v, unsigned sz, lpvar const* vs, unsigned idx):  
+        monic(v, svector<lpvar>(sz, vs), idx) {}
+    monic(lpvar v, const svector<lpvar> &vs, unsigned idx): 
+        mon_eq(v, vs), m_rsign(false),  m_visited(0) {
         std::sort(vars1().begin(), vars1().end());
     }
 
@@ -63,14 +62,15 @@ public:
     void set_visited(unsigned v) { m_visited = v; }
     svector<lpvar> const& rvars() const { return m_rvars; }
     bool rsign() const { return m_rsign; }
-    void reset_rfields() { m_rsign = sign(); m_rvars.reset(); SASSERT(m_rvars.size() == 0); }
+    void reset_rfields() { m_rsign = false; m_rvars.reset(); SASSERT(m_rvars.size() == 0); }
     void push_rvar(signed_var sv) { m_rsign ^= sv.sign(); m_rvars.push_back(sv.var()); }
     void sort_rvars() { std::sort(m_rvars.begin(), m_rvars.end()); }
 };
 
- inline std::ostream& operator<<(std::ostream& out, monic const& m) {
-     return out << m.var() << " := " << (m.sign()?"- ":"") << m.vars() << " r ( " << (m.rsign()?"- ":"") << m.rvars() << ")";
- }
+inline std::ostream& operator<<(std::ostream& out, monic const& m) {
+    return out << m.var() << " := " << m.vars() 
+               << " r ( " << (m.rsign()?"- ":"") << m.rvars() << ")";
+}
 
 
 typedef std::unordered_map<lpvar, rational> variable_map_type;
diff --git a/src/math/lp/nla_basics_lemmas.cpp b/src/math/lp/nla_basics_lemmas.cpp
index 2d13a33cb..609108922 100644
--- a/src/math/lp/nla_basics_lemmas.cpp
+++ b/src/math/lp/nla_basics_lemmas.cpp
@@ -28,7 +28,7 @@ basics::basics(core * c) : common(c) {}
 // Generate a lemma if values of m.var() and n.var() are not the same up to sign
 bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) {
     const rational sign = sign_to_rat(m.rsign() ^ n.rsign());
-     if (val(m) == val(n) * sign)
+     if (var_val(m) == var_val(n) * sign)
         return false;
      TRACE("nla_solver", tout << "sign contradiction:\nm = " << pp_mon(c(), m) << "n= " << pp_mon(c(), n) << "sign: " << sign << "\n";);
     generate_sign_lemma(m, n, sign);
@@ -36,8 +36,8 @@ bool basics::basic_sign_lemma_on_two_monics(const monic& m, const monic& n) {
 }
 
 void basics::generate_zero_lemmas(const monic& m) {
-    SASSERT(!val(m).is_zero() && c().product_value(m).is_zero());
-    int sign = nla::rat_sign(val(m));
+    SASSERT(!var_val(m).is_zero() && c().product_value(m).is_zero());
+    int sign = nla::rat_sign(var_val(m));
     unsigned_vector fixed_zeros;
     lpvar zero_j = find_best_zero(m, fixed_zeros);
     SASSERT(is_set(zero_j));
@@ -105,7 +105,7 @@ bool basics::basic_sign_lemma_model_based() {
     unsigned sz = c().m_to_refine.size();
     for (unsigned i = sz; i-- > 0; ) {
         monic const& m = c().emons()[c().m_to_refine[(start + i) % sz]];
-        int mon_sign = nla::rat_sign(val(m));
+        int mon_sign = nla::rat_sign(var_val(m));
         int product_sign = c().rat_sign(m);
         if (mon_sign != product_sign) {
             basic_sign_lemma_model_based_one_mon(m, product_sign);
@@ -392,7 +392,7 @@ bool basics::basic_lemma_for_mon_neutral_derived(const monic& rm, const factoriz
 void basics::proportion_lemma_model_based(const monic& rm, const factorization& factorization) {
     if (factorization_has_real(factorization)) // todo: handle the situaiton when all factors are greater than 1,        
         return;     // or smaller than 1
-    rational rmv = abs(val(rm));
+    rational rmv = abs(var_val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
         return;
@@ -409,7 +409,7 @@ void basics::proportion_lemma_model_based(const monic& rm, const factorization&
 // x != 0 or y = 0 => |xy| >= |y|
 bool basics::proportion_lemma_derived(const monic& rm, const factorization& factorization) {
     return false;
-    rational rmv = abs(val(rm));
+    rational rmv = abs(var_val(rm));
     if (rmv.is_zero()) {
         SASSERT(c().has_zero_factor(factorization));
         return false;
@@ -459,7 +459,7 @@ void basics::generate_pl(const monic& m, const factorization& fc, int factor_ind
     }
     add_empty_lemma();
     int fi = 0;
-    rational mv = val(m);
+    rational mv = var_val(m);
     rational sm = rational(nla::rat_sign(mv));
     unsigned mon_var = var(m);
     c().mk_ineq(sm, mon_var, llc::LT);
@@ -505,7 +505,7 @@ bool basics::factorization_has_real(const factorization& f) const {
 // here we use the fact xy = 0 -> x = 0 or y = 0
 void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factorization& f) {        
     TRACE("nla_solver",  c().trace_print_monic_and_factorization(rm, f, tout););
-    SASSERT(val(rm).is_zero()&& ! c().rm_check(rm));
+    SASSERT(var_val(rm).is_zero()&& ! c().rm_check(rm));
     add_empty_lemma();
     if (!is_separated_from_zero(f)) {
         c().mk_ineq(var(rm), llc::NE);        
@@ -524,7 +524,7 @@ void basics::basic_lemma_for_mon_zero_model_based(const monic& rm, const factori
 
 void basics::basic_lemma_for_mon_model_based(const monic& rm) {
     TRACE("nla_solver_bl", tout << "rm = " << pp_mon(_(), rm) << "\n";);
-    if (val(rm).is_zero()) {
+    if (var_val(rm).is_zero()) {
         for (auto factorization : factorization_factory_imp(rm, c())) {
             if (factorization.is_empty())
                 continue;
@@ -548,7 +548,7 @@ bool basics::basic_lemma_for_mon_neutral_monic_to_factor_model_based_fm(const mo
     TRACE("nla_solver_bl", c().print_monic(m, tout););
 
     lpvar mon_var = m.var();
-    const auto mv = val(mon_var);
+    const auto mv = var_val(m);
     const auto abs_mv = abs(mv);
     if (abs_mv == rational::zero()) {
         return false;
@@ -619,7 +619,7 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based_fm(co
     }
 
     if (not_one + 1) {  // we found the only not_one
-        if (val(m) == val(not_one) * sign) {
+        if (var_val(m) == val(not_one) * sign) {
             TRACE("nla_solver", tout << "the whole equal to the factor" << std::endl;);
             return false;
         }
@@ -740,13 +740,13 @@ bool basics::basic_lemma_for_mon_neutral_from_factors_to_monic_model_based(const
 
     if (not_one + 1) {
         // we found the only not_one
-        if (val(m) == val(not_one) * sign) {
+        if (var_val(m) == val(not_one) * sign) {
             TRACE("nla_solver", tout << "the whole is equal to the factor" << std::endl;);
             return false;
         }
     } else {
         // we have +-ones only in the factorization
-        if (val(m) == sign) {
+        if (var_val(m) == sign) {
             return false;
         }
     }
diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp
index 1b930f465..4b51c577e 100644
--- a/src/math/lp/nla_common.cpp
+++ b/src/math/lp/nla_common.cpp
@@ -33,9 +33,11 @@ template void common::explain<factorization>(const factorization& t);
 void common::explain(lpvar j) { c().explain(j, c().current_expl()); }
 
 template <typename T> rational common::val(T const& t) const { return c().val(t); }
-template rational common::val<monic>(monic const& t) const;
 template rational common::val<factor>(factor const& t) const;
 rational common::val(lpvar t) const { return c().val(t); }
+rational common::var_val(monic const& m) const { return c().var_val(m); }
+rational common::mul_val(monic const& m) const { return c().mul_val(m); }
+
 template <typename T> lpvar common::var(T const& t) const { return c().var(t); }
 template lpvar common::var<factor>(factor const& t) const;
 template lpvar common::var<monic>(monic const& t) const;
diff --git a/src/math/lp/nla_common.h b/src/math/lp/nla_common.h
index 1f992e749..682b50578 100644
--- a/src/math/lp/nla_common.h
+++ b/src/math/lp/nla_common.h
@@ -57,6 +57,8 @@ struct common {
 
     template <typename T> rational val(T const& t) const;
     rational val(lpvar) const;
+    rational var_val(monic const& m) const; // value obtained from variable representing monomial
+    rational mul_val(monic const& m) const; // value obtained from multiplying variables of monomial
     template <typename T> lpvar var(T const& t) const;
     bool done() const;
     template <typename T> void explain(const T&);
diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 5b7a6cd02..ca569b977 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -101,7 +101,7 @@ bool core::canonize_sign(lpvar j) const {
 }
 
 bool core::canonize_sign_is_correct(const monic& m) const {
-    bool r = m.sign();
+    bool r = false;
     for (lpvar j : m.vars()) {
         r ^= canonize_sign(j);
     }
@@ -145,7 +145,7 @@ void core::pop(unsigned n) {
 }
 
 rational core::product_value(const monic& m) const {
-    rational r(m.sign() ? -1 : 1);
+    rational r(1);
     for (auto j : m.vars()) {
         r *= m_lar_solver.get_column_value_rational(j);
     }
@@ -609,7 +609,7 @@ int core::rat_sign(const monic& m) const {
 
 // Returns true if the monic sign is incorrect
 bool core::sign_contradiction(const monic& m) const {
-    return  nla::rat_sign(val(m)) != rat_sign(m);
+    return  nla::rat_sign(var_val(m)) != rat_sign(m);
 }
 
 /*
@@ -741,7 +741,7 @@ void core::trace_print_monic_and_factorization(const monic& rm, const factorizat
     out << "\n";
         
     out << "mon:  " << pp_mon(*this, rm.var()) << "\n";
-    out << "value: " << val(rm) << "\n";
+    out << "value: " << var_val(rm) << "\n";
     print_factorization(f, out << "fact: ") << "\n";
 }
 
@@ -842,6 +842,7 @@ void core::collect_equivs() {
             add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
         }
     }
+    m_emons.ensure_canonized();
 }
 
 
@@ -1177,7 +1178,7 @@ bool core::find_bfc_to_refine_on_monic(const monic& m, factorization & bf) {
         if (f.size() == 2) {
             auto a = f[0];
             auto b = f[1];
-            if (val(m) != val(a) * val(b)) {
+            if (var_val(m) != val(a) * val(b)) {
                 bf = f;
                 TRACE("nla_solver", tout << "found bf";
                       tout << ":m:" << pp_mon_with_vars(*this, m) << "\n";
@@ -1208,7 +1209,7 @@ bool core::find_bfc_to_refine(const monic* & m, factorization & bf){
         if (find_bfc_to_refine_on_monic(*m, bf)) {
             TRACE("nla_solver",
                   tout << "bf = "; print_factorization(bf, tout);
-                  tout << "\nval(*m) = " << val(*m) << ", should be = (val(bf[0])=" << val(bf[0]) << ")*(val(bf[1]) = " << val(bf[1]) << ") = " << val(bf[0])*val(bf[1]) << "\n";);
+                  tout << "\nval(*m) = " << var_val(*m) << ", should be = (val(bf[0])=" << val(bf[0]) << ")*(val(bf[1]) = " << val(bf[1]) << ") = " << val(bf[0])*val(bf[1]) << "\n";);
             return true;
         } 
     }
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 4acb40f21..c1e3da387 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -128,7 +128,13 @@ public:
     bool is_monic_var(lpvar j) const { return m_emons.is_monic_var(j); }
     rational val(lpvar j) const { return m_lar_solver.get_column_value_rational(j); }
 
-    rational val(const monic& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
+    rational var_val(const monic& m) const { return m_lar_solver.get_column_value_rational(m.var()); }
+
+    rational mul_val(const monic& m) const { 
+        rational r(1);
+        for (lpvar v : m.vars()) r *= m_lar_solver.get_column_value_rational(v);
+        return r;
+    }
 
     bool canonize_sign_is_correct(const monic& m) const;
 
@@ -136,7 +142,7 @@ public:
 
     rational val_rooted(const monic& m) const { return m.rsign()*val(m.var()); }
 
-    rational val(const factor& f) const {  return f.rat_sign() * (f.is_var()? val(f.var()) : val(m_emons[f.var()])); }
+    rational val(const factor& f) const {  return f.rat_sign() * (f.is_var()? val(f.var()) : var_val(m_emons[f.var()])); }
 
     rational val(const factorization&) const;
     
diff --git a/src/math/lp/nla_monotone_lemmas.cpp b/src/math/lp/nla_monotone_lemmas.cpp
index f191c02f8..f72448335 100644
--- a/src/math/lp/nla_monotone_lemmas.cpp
+++ b/src/math/lp/nla_monotone_lemmas.cpp
@@ -82,7 +82,7 @@ void monotone::monotonicity_lemma(monic const& m) {
     if (c().mon_has_zero(m.vars()))
         return;
     const rational prod_val = abs(c().product_value(m));
-    const rational m_val = abs(val(m));
+    const rational m_val = abs(var_val(m));
     if (m_val < prod_val)
         monotonicity_lemma_lt(m, prod_val);
     else if (m_val > prod_val)
diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index 1c75270ce..9da589d7b 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -68,8 +68,8 @@ void order::order_lemma_on_monic(const monic& m) {
 void order::order_lemma_on_binomial(const monic& ac) {
     TRACE("nla_solver", tout << pp_mon_with_vars(c(), ac););
     SASSERT(!check_monic(ac) && ac.size() == 2);
-    const rational mult_val = val(ac.vars()[0]) * val(ac.vars()[1]);
-    const rational acv = val(ac);
+    const rational mult_val = mul_val(ac);
+    const rational acv = var_val(ac);
     bool gt = acv > mult_val;
     bool k = false;
     do {
@@ -138,11 +138,11 @@ void order::order_lemma_on_binomial_ac_bd(const monic& ac, bool k, const monic&
           tout << "ac = " << pp_mon(_(), ac) << "a = " << pp_var(_(), a) << "c = " << pp_var(_(), c) << "\nbd = " << pp_mon(_(), bd) << "b = " << pp_fac(_(), b) << "d = " << pp_var(_(), d) << "\n";
           );
     SASSERT(_().m_evars.find(c).var() == d);
-    rational acv = val(ac);
+    rational acv = var_val(ac);
     rational av = val(a);
     rational c_sign = rrat_sign(val(c));
     rational d_sign = rrat_sign(val(d));
-    rational bdv = val(bd);
+    rational bdv = var_val(bd);
     rational bv = val(b);
     // Notice that ac/|c| = a*c_sign , and bd/|d| = b*d_sign
     auto av_c_s = av*c_sign; auto bv_d_s = bv*d_sign;
@@ -171,16 +171,9 @@ void order::generate_mon_ol(const monic& ac,
                            const rational& d_sign,
                            lpvar d,
                            llc ab_cmp) {
-    SASSERT(
-        (ab_cmp == llc::LT || ab_cmp == llc::GT) &&
-        (
-            (ab_cmp != llc::LT ||
-             (val(ac) >= val(bd) && val(a)*c_sign < val(b)*d_sign))
-            ||
-            (ab_cmp != llc::GT ||
-             (val(ac) <= val(bd) && val(a)*c_sign > val(b)*d_sign))
-         )
-            );
+    SASSERT(ab_cmp == llc::LT || ab_cmp == llc::GT);
+    SASSERT(ab_cmp != llc::LT || (var_val(ac) >= var_val(bd) && val(a)*c_sign < val(b)*d_sign));
+    SASSERT(ab_cmp != llc::GT || (var_val(ac) <= var_val(bd) && val(a)*c_sign > val(b)*d_sign));
     
     add_empty_lemma();
     mk_ineq(c_sign, c, llc::LE);
@@ -224,10 +217,10 @@ void order::order_lemma_on_factorization(const monic& m, const factorization& ab
         sign ^= _().canonize_sign(f);
     const rational rsign = sign_to_rat(sign);
     const rational fv = val(var(ab[0])) * val(var(ab[1]));
-    const rational mv = rsign * val(m);
+    const rational mv = rsign * var_val(m);
     TRACE("nla_solver",
           tout << "ab.size()=" << ab.size() << "\n";
-          tout << "we should have sign*val(m):" << mv << "=(" << rsign << ")*(" << val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";);
+          tout << "we should have sign*var_val(m):" << mv << "=(" << rsign << ")*(" << var_val(m) <<") to be equal to " << " val(var(ab[0]))*val(var(ab[1])):" << fv << "\n";);
     if (mv == fv)
         return;
     bool gt = mv > fv;
@@ -263,7 +256,7 @@ bool order::order_lemma_on_ac_explore(const monic& rm, const factorization& ac,
 }
 
 // |c_sign| = 1, and c*c_sign > 0
-// ac > bc => ac/|c| > bc/|c| => a*c_sign > b*c_sign
+// ac > bc && ac/|c| > bc/|c| => a*c_sign > b*c_sign
 void order::generate_ol(const monic& ac,                     
                        const factor& a,
                        int c_sign,
@@ -271,11 +264,22 @@ void order::generate_ol(const monic& ac,
                        const monic& bc,
                        const factor& b,
                        llc ab_cmp) {
-    add_empty_lemma();
+
     rational rc_sign = rational(c_sign);
-    mk_ineq(rc_sign * sign_to_rat(canonize_sign(c)), var(c), llc::LE);
+    rational sign_a = rc_sign * sign_to_rat(canonize_sign(a));
+    rational sign_b = rc_sign * sign_to_rat(canonize_sign(b));
+    rational sign_c = rc_sign * sign_to_rat(canonize_sign(c));
+    add_empty_lemma();
+#if 0
+    IF_VERBOSE(0, verbose_stream() << var_val(ac) << "(" << mul_val(ac) << "): " << ac 
+               << " " << ab_cmp << " " << var_val(bc) << "(" << mul_val(bc) << "): " << bc << "\n"
+               << " a " << sign_a << "*v" << var(a) << " " << val(a) << "\n"
+               << " b " << sign_b << "*v" << var(b) << " " << val(b) << "\n"
+               << " c " << sign_c << "*v" << var(c) << " " << val(c) << "\n");
+#endif    
+    mk_ineq(sign_c, var(c), llc::LE);
     mk_ineq(canonize_sign(ac), var(ac), !canonize_sign(bc), var(bc), ab_cmp);
-    mk_ineq(sign_to_rat(canonize_sign(a))*rc_sign, var(a), - sign_to_rat(canonize_sign(b))*rc_sign, var(b), negate(ab_cmp));
+    mk_ineq(sign_a, var(a), - sign_b, var(b), negate(ab_cmp));
     explain(ac);
     explain(a);
     explain(bc);
@@ -294,8 +298,8 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
     SASSERT(c_sign != 0);
     auto av_c_s = val(a)*rational(c_sign);
     auto bv_c_s = val(b)*rational(c_sign);        
-    auto acv = val(ac); 
-    auto bcv = val(bc); 
+    auto acv = var_val(ac); 
+    auto bcv = var_val(bc); 
     TRACE("nla_solver", _().trace_print_ol(ac, a, c, bc, b, tout););
     // Suppose ac >= bc, then ac/|c| >= bc/|c|.
     // Notice that ac/|c| = a*c_sign , and bc/|c| = b*c_sign, which are correspondingly av_c_s and bv_c_s
@@ -314,7 +318,7 @@ bool order::order_lemma_on_ac_and_bc_and_factors(const monic& ac,
    a < 0 & b >= value(b) => sign*ab <= value(b)*a  if value(a) < 0
 */
 void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a, lpvar b) {
-    SASSERT(sign * val(m) > val(a) * val(b));
+    SASSERT(sign * var_val(m) > val(a) * val(b));
     add_empty_lemma();
     if (val(a).is_pos()) {
         TRACE("nla_solver", tout << "a is pos\n";);
@@ -344,7 +348,7 @@ void order::order_lemma_on_ab_gt(const monic& m, const rational& sign, lpvar a,
 void order::order_lemma_on_ab_lt(const monic& m, const rational& sign, lpvar a, lpvar b) {
     TRACE("nla_solver", tout << "sign = " << sign << ", m = "; c().print_monic(m, tout) << ", a = "; c().print_var(a, tout) <<
           ", b = "; c().print_var(b, tout) << "\n";);
-    SASSERT(sign * val(m) < val(a) * val(b));
+    SASSERT(sign * var_val(m) < val(a) * val(b));
     add_empty_lemma();
     if (val(a).is_pos()) {
         //negate a > 0
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index 57e383297..e79c9b643 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -38,7 +38,7 @@ typedef nla::variable_map_type variable_map_type;
         }
 
         void add(lp::var_index v, unsigned sz, lp::var_index const* vs) {
-            m_monics.push_back(mon_eq(false, v, sz, vs));
+            m_monics.push_back(mon_eq(v, sz, vs));
         }
 
         void push() {