From 6ce69233c7d3235be5b2938158a27ba33daa962b Mon Sep 17 00:00:00 2001 From: Lev Date: Wed, 3 Oct 2018 13:03:10 -0700 Subject: [PATCH] work on nla_solver Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 393983f10..78bbc6b90 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -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; }