From 012131df73f011dec85ea5f87708e83b7ede5677 Mon Sep 17 00:00:00 2001 From: Lev Date: Thu, 27 Sep 2018 16:22:53 -0700 Subject: [PATCH] tesing factorization of monomials in nla_solver Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 59e2dc5ab..9c7dce8a3 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1055,18 +1055,22 @@ struct solver::imp { k = k_vars[0]; k_sign = 1; k_mon = -1; - } else if (!m_binary_factorizations.m_imp.find_monomial_of_vars(k_vars, m, k_sign)) { - return false; + } else { + if (!m_binary_factorizations.m_imp.find_monomial_of_vars(k_vars, m, k_sign)) { + return false; + } + k = m.var(); } - k = m.var(); if (j_vars.size() == 1) { j = j_vars[0]; j_sign = 1; - } else if (!m_binary_factorizations.m_imp.find_monomial_of_vars(j_vars, m, j_sign)) { - return false; + } else { + if (!m_binary_factorizations.m_imp.find_monomial_of_vars(j_vars, m, j_sign)) { + return false; + } + j = m.var(); } sign = j_sign * k_sign; - j = m.var(); return true; }