From 18016a710093f2e8bd06eb2b3a20984839dd1de6 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Tue, 26 May 2020 14:15:20 -0700
Subject: [PATCH] rename

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/nla_core.cpp | 8 ++++----
 src/math/lp/nla_core.h   | 4 ++--
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index a89e485b5..89b07b9ba 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1332,7 +1332,7 @@ bool core::to_refine_is_correct() const {
 }
 
 // looking for any real var to patch
-void core::patch_monomial_with_real_var(lpvar j) {    
+void core::patch_monomial(lpvar j) {    
     const monic& m = emons()[j];
     TRACE("nla_solver", tout << "m = "; print_monic(m, tout) << "\n";);
     rational v = mul_val(m);
@@ -1379,14 +1379,14 @@ void core::patch_monomial_with_real_var(lpvar j) {
     }                              
 }
 
-void core::patch_monomials_with_real_vars() {
+void core::patch_monomials() {
     auto to_refine = m_to_refine.index();
     // the rest of the function might change m_to_refine, so have to copy
     unsigned sz = to_refine.size();
     TRACE("nla_solver", tout << "sz = " << sz << "\n";);
     unsigned start = random();
     for (unsigned i = 0; i < sz; i++) {
-        patch_monomial_with_real_var(to_refine[(start + i) % sz]);
+        patch_monomial(to_refine[(start + i) % sz]);
         if (m_to_refine.size() == 0)
             break;
     }
@@ -1406,7 +1406,7 @@ lbool core::check(vector<lemma>& l_vec) {
     }
 
     init_to_refine();
-    patch_monomials_with_real_vars();
+    patch_monomials();
     if (m_to_refine.is_empty()) { return l_true; }   
     init_search();
 
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 62c026dd8..b36bd2519 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -464,8 +464,8 @@ public:
     bool influences_nl_var(lpvar) const;
     bool is_nl_var(lpvar) const;
     bool is_used_in_monic(lpvar) const;
-    void patch_monomials_with_real_vars();
-    void patch_monomial_with_real_var(lpvar);
+    void patch_monomials();
+    void patch_monomial(lpvar);
     bool var_breaks_correct_monic(lpvar) const;
     bool var_breaks_correct_monic_as_factor(lpvar, const monic&) const;
     void update_to_refine_of_var(lpvar j);