mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

small changes

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-11-02 15:42:13 -07:00 committed by Lev Nachmanson
parent 9407c4e96f
commit fde1cd23d5
5 changed files with 14 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_lra.cpp
View file

@ -1973,6 +1973,7 @@ public:
}
lbool check_lia() {
TRACE("arith",);
if (m.canceled()) {
TRACE("arith", tout << "canceled\n";);
return l_undef;

2
src/util/lp/int_solver.cpp
View file

@ -619,6 +619,7 @@ bool int_solver::ext_gcd_test(const row_strip<mpq> & 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<mpq> & 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;

2
src/util/lp/lar_core_solver.h
View file

@ -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<mpq>::is_pos(m_r_solver.m_pivot_row.m_data[j]))
out << "+";

3
src/util/lp/lp_core_solver_base_def.h
View file

@ -697,6 +697,9 @@ non_basis_is_correctly_represented_in_heading() const {
template <typename T, typename X> bool lp_core_solver_base<T, X>::
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

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

@ -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();