mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-20 10:10:21 +00:00
Code Activity

small changes

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-27 10:23:44 -08:00 • committed by Lev Nachmanson
parent 11dae38ae6
commit 882dd06df9
1 changed files with 9 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/util/lp/nla_solver.cpp
View file

@ -510,19 +510,14 @@ struct solver::imp {
// here we use the fact // here we use the fact
// xy = 0 -> x = 0 or y = 0 // xy = 0 -> x = 0 or y = 0
bool basic_lemma_for_mon_zero_from_monomial_to_factor(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_zero(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
if (!vvr(rm).is_zero() ) SASSERT(vvr(rm).is_zero());
return false;
bool seen_zero = false;
for (lpvar j : f) { for (lpvar j : f) {
if (vvr(j).is_zero()) { if (vvr(j).is_zero()) {
seen_zero = true; return false;
break;
} }
} }
if (seen_zero)
return false;
SASSERT(m_lemma->empty()); SASSERT(m_lemma->empty());
@ -558,11 +553,10 @@ struct solver::imp {
print_factorization(f, out << "fact: ") << "\n"; print_factorization(f, out << "fact: ") << "\n";
} }
// x = 0 or y = 0 -> xy = 0 // x = 0 or y = 0 -> xy = 0
bool basic_lemma_for_mon_zero_from_factors_to_monomial(const rooted_mon& rm, const factorization& f) { bool basic_lemma_for_mon_non_zero(const rooted_mon& rm, const factorization& f) {
TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout);); TRACE("nla_solver", trace_print_monomial_and_factorization(rm, f, tout););
if (vvr(rm).is_zero()) SASSERT (!vvr(rm).is_zero());
return false; int zero_j = -1;
unsigned zero_j = -1;
for (lpvar j : f) { for (lpvar j : f) {
if (vvr(j).is_zero()) { if (vvr(j).is_zero()) {
zero_j = j; zero_j = j;
@ -570,7 +564,7 @@ struct solver::imp {
} }
} }
if (zero_j == static_cast<unsigned>(-1)) { if (zero_j == -1) {
return false; return false;
} }
@ -696,7 +690,7 @@ struct solver::imp {
for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) {
if (factorization.is_empty()) if (factorization.is_empty())
continue; continue;
if (basic_lemma_for_mon_zero_from_monomial_to_factor(rm, factorization) || if (basic_lemma_for_mon_zero(rm, factorization) ||
basic_lemma_for_mon_neutral(rm, factorization)) basic_lemma_for_mon_neutral(rm, factorization))
return true; return true;
} }
@ -704,7 +698,7 @@ struct solver::imp {
for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) { for (auto factorization : factorization_factory_imp(rm.m_vars, *this)) {
if (factorization.is_empty()) if (factorization.is_empty())
continue; continue;
if (basic_lemma_for_mon_zero_from_factors_to_monomial(rm, factorization) || if (basic_lemma_for_mon_non_zero(rm, factorization) ||
basic_lemma_for_mon_neutral(rm, factorization)) basic_lemma_for_mon_neutral(rm, factorization))
return true; return true;