mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 06:39:02 +00:00
Code Activity

work on nla_solver

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-03 13:03:10 -07:00 committed by Lev Nachmanson
parent 301f8d40fd
commit 6ce69233c7
1 changed files with 10 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1285,17 +1285,17 @@ struct solver::imp {
return false;
}
bool basic_lemma_for_mon_zero_from_monomial_to_factor(const signed_factorization& factorization) {
bool basic_lemma_for_mon_zero_from_monomial_to_factor(lpvar i_mon, const signed_factorization& factorization) {
SASSERT(false);
}
bool basic_lemma_for_mon_zero_from_factors_to_monomial(const signed_factorization& factorization) {
bool basic_lemma_for_mon_zero_from_factors_to_monomial(lpvar i_mon, const signed_factorization& factorization) {
SASSERT(false);
}
bool basic_lemma_for_mon_zero(const signed_factorization& factorization) {
return basic_lemma_for_mon_zero_from_monomial_to_factor(factorization) || basic_lemma_for_mon_zero_from_factors_to_monomial(factorization);
bool basic_lemma_for_mon_zero(lpvar i_mon, const signed_factorization& factorization) {
return basic_lemma_for_mon_zero_from_monomial_to_factor(i_mon, factorization) || basic_lemma_for_mon_zero_from_factors_to_monomial(i_mon, factorization);
}
bool basic_lemma_for_mon_neutral(const signed_factorization& factorization) {
@ -1313,11 +1313,12 @@ struct solver::imp {
bool basic_lemma_for_mon(unsigned i_mon) {
for (auto factorization : binary_factorizations_of_monomial(i_mon, *this)) {
if (
basic_lemma_for_mon_zero(factorization)
||
basic_lemma_for_mon_neutral(factorization)
||
basic_lemma_for_mon_proportionality(factorization))
basic_lemma_for_mon_zero(i_mon, factorization)
||
basic_lemma_for_mon_neutral(factorization)
||
basic_lemma_for_mon_proportionality(factorization)
)
return true;
}