remove unused code

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

src/math/lp/factorization.cpp

@@ -1,3 +1,12 @@
+/*++
+Copyright (c) 2017 Microsoft Corporation
+
+Author:
+Lev Nachmanson (levnach)
+Nikolaj Bjorner (nbjorner)
+
+--*/
+
 #include "util/vector.h"
 #include "math/lp/factorization.h"
 namespace nla {
@@ -7,11 +16,10 @@ void const_iterator_mon::init_vars_by_the_mask(unsigned_vector & k_vars, unsigne
     SASSERT(m_mask.size() + 1  == m_ff->m_vars.size());
     k_vars.push_back(m_ff->m_vars.back()); 
     for (unsigned j = 0; j < m_mask.size(); j++) {
-        if (m_mask[j]) {
-            k_vars.push_back(m_ff->m_vars[j]);
-        } else {
-            j_vars.push_back(m_ff->m_vars[j]);
-        }
+        if (m_mask[j]) 
+            k_vars.push_back(m_ff->m_vars[j]);         
+        else 
+            j_vars.push_back(m_ff->m_vars[j]);        
     }
 }
 // todo : do we need the sign?
@@ -29,9 +37,9 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
         m_full_factorization_returned = true;
         return false;
     }
-    if (k_vars.size() == 1) {
-        k.set(k_vars[0], factor_type::VAR);
-    } else {
+    if (k_vars.size() == 1) 
+        k.set(k_vars[0], factor_type::VAR);     
+    else {
         unsigned i;
         if (!m_ff->find_canonical_monic_of_vars(k_vars, i)) {
             ++m_num_failures;
@@ -41,9 +49,9 @@ bool const_iterator_mon::get_factors(factor& k, factor& j, rational& sign) const
     }
     m_num_failures = 0;
 
-    if (j_vars.size() == 1) {
-        j.set(j_vars[0], factor_type::VAR);
-    } else {
+    if (j_vars.size() == 1) 
+        j.set(j_vars[0], factor_type::VAR);    
+    else {
         unsigned i;
         if (!m_ff->find_canonical_monic_of_vars(j_vars, i)) {
             ++m_num_failures;

src/math/lp/factorization.h

@@ -2,20 +2,10 @@
   /*++
   Copyright (c) 2017 Microsoft Corporation
 
-  Module Name:
-
-  <name>
-
-  Abstract:
-
-  <abstract>
-
   Author:
   Lev Nachmanson (levnach)
   Nikolaj Bjorner (nbjorner)
 
-  Revision History:
-
 
   --*/
 #pragma once

src/math/lp/nla_core.cpp

@@ -1434,45 +1434,6 @@ void core::patch_monomials_on_to_refine() {
 void core::patch_monomials() {
     m_cautious_patching = true;
     patch_monomials_on_to_refine();
-    if (m_to_refine.size() == 0 || !params().arith_nl_expensive_patching()) {
-        return;
-    }
-    NOT_IMPLEMENTED_YET();
-    m_cautious_patching = false; 
-    patch_monomials_on_to_refine();
-    lra.push();
-    save_tableau();
-    constrain_nl_in_tableau();
-    if (solve_tableau() && integrality_holds()) {
-        lra.pop(1);
-    } else {
-        lra.pop();
-        restore_tableau();
-        lra.clear_inf_heap();
-    }
-    SASSERT(lra.ax_is_correct());
-}
-
-void core::constrain_nl_in_tableau() {
-    NOT_IMPLEMENTED_YET();
-}
-
-bool core::solve_tableau() {
-    NOT_IMPLEMENTED_YET();
-    return false;
-}
-
-void core::restore_tableau() {
-    NOT_IMPLEMENTED_YET();
-}
-
-void core::save_tableau() {
-    NOT_IMPLEMENTED_YET();
-}
-
-bool core::integrality_holds() {
-    NOT_IMPLEMENTED_YET();
-    return false;
 }
 
 /**

src/math/lp/nla_core.h

@@ -424,18 +424,10 @@ class core {
     vector<nla::ineq> const& literals() const { return m_literals; }
     vector<lp::equality> const& equalities() const { return m_equalities; }
     vector<lp::fixed_equality> const& fixed_equalities() const { return m_fixed_equalities; }
-    bool check_feasible() const { return m_check_feasible; }
+    bool should_check_feasible() const { return m_check_feasible; }
 
     void add_fixed_equality(lp::lpvar v, rational const& k, lp::explanation const& e) { m_fixed_equalities.push_back({v, k, e}); }
     void add_equality(lp::lpvar i, lp::lpvar j, lp::explanation const& e) { m_equalities.push_back({i, j, e}); }
-private:
-    void restore_patched_values();
-    void constrain_nl_in_tableau();
-    bool solve_tableau();
-    void restore_tableau();
-    void save_tableau();
-    bool integrality_holds();
-
 
 };  // end of core
 

src/math/lp/nla_solver.h

@@ -53,6 +53,6 @@ namespace nla {
         vector<nla::ineq> const& literals() const;
         vector<lp::fixed_equality> const& fixed_equalities() const;
         vector<lp::equality> const& equalities() const;
-        bool check_feasible() const { return m_core->check_feasible(); }
+        bool should_check_feasible() const { return m_core->should_check_feasible(); }
     };
 }

src/sat/smt/arith_solver.cpp

@@ -1506,7 +1506,7 @@ namespace arith {
     }
 
     void solver::add_lemmas() {
-        if (m_nla->check_feasible()) {
+        if (m_nla->should_check_feasible()) {
             auto is_sat = make_feasible();
             if (l_false == is_sat) {
                 get_infeasibility_explanation_and_set_conflict();

src/smt/theory_lra.cpp

@@ -2151,7 +2151,7 @@ class theory_lra::imp {
     }
 
     void add_lemmas() {
-        if (m_nla->check_feasible()) {
+        if (m_nla->should_check_feasible()) {
             auto is_sat = make_feasible();
             if (l_false == is_sat) {
                 get_infeasibility_explanation_and_set_conflict();