mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

remove debug/non-debug difference

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-13 07:52:36 -07:00
parent f09f1a7524
commit 167969d6c2
3 changed files with 31 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/smt/theory_lra.cpp
View file

@ -2712,7 +2712,6 @@ public:
if (dump_lemmas()) {
unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), false_literal);
(void)id;
//SASSERT(id != 55);
}
}
@ -2732,7 +2731,6 @@ public:
if (dump_lemmas()) {
unsigned id = ctx().display_lemma_as_smt_problem(m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), lit);
(void)id;
// SASSERT(id != 71);
}
}

28
src/util/lp/hnf_cutter.h
View file

@ -177,43 +177,41 @@ public:
bool overflow() const { return m_overflow; }
lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper
#ifdef Z3DEBUG
,
const vector<mpq> & x0
#endif
) {
lia_move create_cut(lar_term& t, mpq& k, explanation& ex, bool & upper, const vector<mpq> & x0) {
// we suppose that x0 has at least one non integer element
(void)x0;
init_matrix_A();
svector<unsigned> basis_rows;
mpq big_number = m_abs_max.expt(3);
mpq d = hnf_calc::determinant_of_rectangular_matrix(m_A, basis_rows, big_number);
// std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
//std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
// std::cout << "max = " << m_abs_max << ", d = " << d << ", d/max = " << ceil (d /m_abs_max) << std::endl;
// std::cout << "max cube " << m_abs_max * m_abs_max * m_abs_max << std::endl;
if (d >= big_number) {
return lia_move::undef;
}
if (m_settings.get_cancel_flag())
if (m_settings.get_cancel_flag()) {
return lia_move::undef;
}
if (basis_rows.size() < m_A.row_count()) {
m_A.shrink_to_rank(basis_rows);
shrink_explanation(basis_rows);
}
hnf<general_matrix> h(m_A, d);
// general_matrix A_orig = m_A;
hnf<general_matrix> h(m_A, d);
vector<mpq> b = create_b(basis_rows);
lp_assert(m_A * x0 == b);
// vector<mpq> bcopy = b;
find_h_minus_1_b(h.W(), b);
// lp_assert(bcopy == h.W().take_first_n_columns(b.size()) * b);
int cut_row = find_cut_row_index(b);
if (cut_row == -1)
if (cut_row == -1) {
return lia_move::undef;
}
// the matrix is not square - we can get
// all integers in b's projection

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

@ -577,17 +577,27 @@ lia_move int_solver::make_hnf_cut() {
return lia_move::undef;
}
settings().st().m_hnf_cutter_calls++;
TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls;);
TRACE("hnf_cut", tout << "settings().st().m_hnf_cutter_calls = " << settings().st().m_hnf_cutter_calls << "\n";
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
m_lar_solver->print_constraint(i, tout);
}
m_lar_solver->print_constraints(tout);
);
#ifdef Z3DEBUG
vector<mpq> x0 = m_hnf_cutter.transform_to_local_columns(m_lar_solver->m_mpq_lar_core_solver.m_r_x);
#else
vector<mpq> x0;
#endif
lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper
#ifdef Z3DEBUG
, x0
#endif
);
CTRACE("hnf_cut", r == lia_move::cut, tout<< "cut:"; m_lar_solver->print_term(*m_t, tout); tout << " <= " << *m_k << std::endl;);
if (r == lia_move::cut) {
lia_move r = m_hnf_cutter.create_cut(*m_t, *m_k, *m_ex, *m_upper, x0);
if (r == lia_move::cut) {
TRACE("hnf_cut",
m_lar_solver->print_term(*m_t, tout << "cut:");
tout << " <= " << *m_k << std::endl;
for (unsigned i : m_hnf_cutter.constraints_for_explanation()) {
m_lar_solver->print_constraint(i, tout);
}
);
lp_assert(current_solution_is_inf_on_cut());
settings().st().m_hnf_cuts++;
m_ex->clear();