emonics

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/math/lp/factorization.h

@@ -54,7 +54,7 @@ public:
 
 
 class factorization {
-    svector<factor>       m_factors;
+    svector<factor>    m_factors;
     const monic*       m_mon;
 public:
     factorization(const monic* m): m_mon(m) {
@@ -63,18 +63,14 @@ public:
                 m_factors.push_back(factor(j, factor_type::VAR));
         }
     }
-    bool is_mon() const {
+    bool is_mon() const { return m_mon != nullptr; }
-        return m_mon != nullptr;
-    }
     bool is_empty() const { return m_factors.empty(); }
     const factor& operator[](unsigned k) const { return m_factors[k]; }
     factor& operator[](unsigned k) { return m_factors[k]; }
     size_t size() const { return m_factors.size(); }
     const factor* begin() const { return m_factors.begin(); }
     const factor* end() const { return m_factors.end(); }
-    void push_back(factor const& v) {
+    void push_back(factor const& v) { m_factors.push_back(v); }
-        m_factors.push_back(v);
-    }
     const monic& mon() const { return *m_mon; }
     void set_mon(const monic* m) { m_mon = m; }
 

src/math/lp/monic.h

@@ -36,8 +36,11 @@ public:
     unsigned size() const { return m_vs.size(); }
     bool sign() const { return m_sign; }
     const svector<lp::var_index>& vars() const { return m_vs; }
-    svector<lp::var_index>& vars() { return m_vs; }
     bool empty() const { return m_vs.empty(); }
+
+protected:
+    svector<lp::var_index>& vars1() { return m_vs; }
+
 };
 
 // support the congruence    
@@ -53,7 +56,7 @@ public:
     }
     monic(bool sign, lpvar v, const svector<lpvar> &vs, unsigned idx): 
         mon_eq(sign, v, vs), m_rsign(false),  m_visited(0) {
-        std::sort(vars().begin(), vars().end());
+        std::sort(vars1().begin(), vars1().end());
     }
 
     unsigned visited() const { return m_visited; }

src/math/lp/nla_common.h

@@ -57,7 +57,6 @@ struct common {
 
     template <typename T> rational val(T const& t) const;
     rational val(lpvar) const;
-    rational rval(const monic&) const;
     template <typename T> lpvar var(T const& t) const;
     bool done() const;
     template <typename T> void explain(const T&);

src/math/lp/nla_core.cpp

@@ -87,7 +87,6 @@ svector<lpvar> core::sorted_rvars(const factor& f) const {
         svector<lpvar> r; r.push_back(map_to_root(f.var()));
         return r;
     }
-    TRACE("nla_solver", tout << "nv";);
     return m_emons[f.var()].rvars();
 }
 
@@ -799,7 +798,7 @@ void core::explain(const factorization& f, lp::explanation& exp) {
     }
 }
 
-bool core:: has_zero_factor(const factorization& factorization) const {
+bool core::has_zero_factor(const factorization& factorization) const {
     for (factor f : factorization) {
         if (val(f).is_zero())
             return true;

src/smt/theory_lra.cpp

@@ -2049,8 +2049,8 @@ public:
                     set_evidence(ev.second);
                 }
             }
-			// The call mk_bound() can set the m_infeasible_column in lar_solver
+            // The call mk_bound() can set the m_infeasible_column in lar_solver
-			// so the explanation is safer to take before this call.
+            // so the explanation is safer to take before this call.
             app_ref b = mk_bound(m_lia->get_term(), m_lia->get_offset(), !m_lia->is_upper());
             if (m.has_trace_stream()) {
                 th.log_axiom_instantiation(b);
@@ -3483,6 +3483,8 @@ public:
         if (dump_lemmas()) {
             unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
             (void)id;
+            std::cout << id << "\n";
+            SASSERT(id != 49);
         }
     }