From fde1cd23d5ffded42909230972f1a0cff1b93a9e Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 2 Nov 2018 15:42:13 -0700 Subject: [PATCH] small changes Signed-off-by: Lev --- src/smt/theory_lra.cpp | 1 + src/util/lp/int_solver.cpp | 2 ++ src/util/lp/lar_core_solver.h | 2 +- src/util/lp/lp_core_solver_base_def.h | 3 +++ src/util/lp/nla_solver.cpp | 14 +++++++------- 5 files changed, 14 insertions(+), 8 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 32acc3fd5..a3249e5da 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1973,6 +1973,7 @@ public: } lbool check_lia() { + TRACE("arith",); if (m.canceled()) { TRACE("arith", tout << "canceled\n";); return l_undef; diff --git a/src/util/lp/int_solver.cpp b/src/util/lp/int_solver.cpp index ef66f005b..6d5cc5437 100644 --- a/src/util/lp/int_solver.cpp +++ b/src/util/lp/int_solver.cpp @@ -619,6 +619,7 @@ bool int_solver::ext_gcd_test(const row_strip & row, mpq const & least_coeff, mpq const & lcm_den, mpq const & consts) { + TRACE("ext_gcd_test", tout << "row = "; m_lar_solver->print_row(row, tout);); mpq gcds(0); mpq l(consts); mpq u(consts); @@ -627,6 +628,7 @@ bool int_solver::ext_gcd_test(const row_strip & row, unsigned j; for (const auto & c : row) { j = c.var(); + TRACE("ext_gcd_test", tout << "col = "; m_lar_solver->m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, tout);); const mpq & a = c.coeff(); if (m_lar_solver->column_is_fixed(j)) continue; diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h index 98d0912bc..6c91850a1 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/util/lp/lar_core_solver.h @@ -100,7 +100,7 @@ public: void calculate_pivot_row(unsigned i); - void print_pivot_row(std::ostream & out, unsigned row_index) const { // remove later debug !!!! + void print_pivot_row(std::ostream & out, unsigned row_index) const { for (unsigned j : m_r_solver.m_pivot_row.m_index) { if (numeric_traits::is_pos(m_r_solver.m_pivot_row.m_data[j])) out << "+"; diff --git a/src/util/lp/lp_core_solver_base_def.h b/src/util/lp/lp_core_solver_base_def.h index 7452f6f65..7da84cfc3 100644 --- a/src/util/lp/lp_core_solver_base_def.h +++ b/src/util/lp/lp_core_solver_base_def.h @@ -697,6 +697,9 @@ non_basis_is_correctly_represented_in_heading() const { template bool lp_core_solver_base:: basis_heading_is_correct() const { + if ( m_A.column_count() > 10 ) { + return true; + } lp_assert(m_basis_heading.size() == m_A.column_count()); lp_assert(m_basis.size() == m_A.row_count()); lp_assert(m_nbasis.size() <= m_A.column_count() - m_A.row_count()); // for the dual the size of non basis can be smaller diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index abe4feb49..274842909 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -484,7 +484,7 @@ struct solver::imp { // here we use the fact // xy = 0 -> x = 0 or y = 0 bool basic_lemma_for_mon_zero_from_monomial_to_factor(unsigned i_mon, const factorization& f) { - TRACE("nla_solver", trace_print_monomial_and_factorization(i_mon, f);); + TRACE("nla_solver", trace_print_monomial_and_factorization(i_mon, f, tout);); lpvar mon_var = m_monomials[i_mon].var(); if (!vvr(mon_var).is_zero() ) return false; @@ -518,14 +518,14 @@ struct solver::imp { set_expl(e); } - void trace_print_monomial_and_factorization(unsigned i_mon, const factorization& f) const { - tout << "mon = "; - print_monomial(i_mon, tout); - tout << "\nfact = "; print_factorization(f, tout); + void trace_print_monomial_and_factorization(unsigned i_mon, const factorization& f, std::ostream& out) const { + out << "mon = "; + print_monomial(i_mon, out); + out << "\nfact = "; print_factorization(f, out); } // x = 0 or y = 0 -> xy = 0 bool basic_lemma_for_mon_zero_from_factors_to_monomial(unsigned i_mon, const factorization& f) { - TRACE("nla_solver", trace_print_monomial_and_factorization(i_mon, f);); + TRACE("nla_solver", trace_print_monomial_and_factorization(i_mon, f, tout);); if (vvr(m_monomials[i_mon].var()).is_zero()) return false; unsigned zero_j = -1; @@ -559,7 +559,7 @@ struct solver::imp { // use the fact that // |xabc| = |x| and x != 0 -> |a| = |b| = |c| = 1 bool basic_lemma_for_mon_neutral_monomial_to_factor(unsigned i_mon, const factorization& f) { - TRACE("nla_solver", trace_print_monomial_and_factorization(i_mon, f);); + TRACE("nla_solver", trace_print_monomial_and_factorization(i_mon, f, tout);); // todo : consider the case of just two factors lpvar mon_var = m_monomials[i_mon].var();