mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 01:55:32 +00:00
Code Activity

rename

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-05-26 14:15:20 -07:00
parent c424165d94
commit 18016a7100
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/nla_core.cpp
View file

@ -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();

4
src/math/lp/nla_core.h
View file

@ -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);