mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

add a trace statement

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-03-19 13:17:27 -07:00
parent 1971ee60e1
commit 3b67dd8288
3 changed files with 58 additions and 40 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/math/lp/int_gcd_test.cpp
View file

@ -215,6 +215,7 @@ namespace lp {
if (u1 < l1) { if (u1 < l1) {
fill_explanation_from_fixed_columns(row); fill_explanation_from_fixed_columns(row);
TRACE("gcd_test", tout << "row failed the GCD test:\n"; lia.display_row(tout, row););
return false; return false;
} }
return true; return true;

95
src/math/lp/int_solver.cpp
View file

@ -14,8 +14,8 @@
namespace lp { namespace lp {
int_solver::patcher::patcher(int_solver& lia): int_solver::patcher::patcher(int_solver& lia):
lia(lia), lia(lia),
lra(lia.lra), lra(lia.lra),
lrac(lia.lrac), lrac(lia.lrac),
m_num_nbasic_patches(0), m_num_nbasic_patches(0),
@ -23,7 +23,7 @@ int_solver::patcher::patcher(int_solver& lia):
m_next_patch(0), m_next_patch(0),
m_delay(0) m_delay(0)
{} {}
bool int_solver::patcher::should_apply() { bool int_solver::patcher::should_apply() {
#if 1 #if 1
return true; return true;
@ -35,7 +35,7 @@ bool int_solver::patcher::should_apply() {
return false; return false;
#endif #endif
} }
lia_move int_solver::patcher::operator()() { lia_move int_solver::patcher::operator()() {
return patch_nbasic_columns(); return patch_nbasic_columns();
} }
@ -70,7 +70,7 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
bool inf_l, inf_u; bool inf_l, inf_u;
impq l, u; impq l, u;
mpq m; mpq m;
bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m); bool has_free = lia.get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m);
m_patch_cost += lra.A_r().number_of_non_zeroes_in_column(j); m_patch_cost += lra.A_r().number_of_non_zeroes_in_column(j);
if (!has_free) { if (!has_free) {
return; return;
@ -113,7 +113,7 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
TRACE("patch_int", tout << "patching with 0\n";); TRACE("patch_int", tout << "patching with 0\n";);
} }
++m_num_nbasic_patches; ++m_num_nbasic_patches;
} }
int_solver::int_solver(lar_solver& lar_slv) : int_solver::int_solver(lar_solver& lar_slv) :
lra(lar_slv), lra(lar_slv),
@ -157,7 +157,7 @@ lia_move int_solver::check(lp::explanation * e) {
if (settings().get_cancel_flag()) if (settings().get_cancel_flag())
return lia_move::undef; return lia_move::undef;
++m_number_of_calls; ++m_number_of_calls;
if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher(); if (r == lia_move::undef && m_patcher.should_apply()) r = m_patcher();
if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)(); if (r == lia_move::undef && should_find_cube()) r = int_cube(*this)();
@ -174,7 +174,7 @@ std::ostream& int_solver::display_inf_rows(std::ostream& out) const {
display_column(out, v); display_column(out, v);
} }
} }
num = 0; num = 0;
for (unsigned i = 0; i < lra.A_r().row_count(); i++) { for (unsigned i = 0; i < lra.A_r().row_count(); i++) {
unsigned j = lrac.m_r_basis[i]; unsigned j = lrac.m_r_basis[i];
@ -224,12 +224,12 @@ unsigned int_solver::row_of_basic_column(unsigned j) const {
return lra.row_of_basic_column(j); return lra.row_of_basic_column(j);
} }
lp_settings& int_solver::settings() { lp_settings& int_solver::settings() {
return lra.settings(); return lra.settings();
} }
const lp_settings& int_solver::settings() const { const lp_settings& int_solver::settings() const {
return lra.settings(); return lra.settings();
} }
bool int_solver::column_is_int(column_index const& j) const { bool int_solver::column_is_int(column_index const& j) const {
@ -242,7 +242,7 @@ bool int_solver::is_real(unsigned j) const {
bool int_solver::value_is_int(unsigned j) const { bool int_solver::value_is_int(unsigned j) const {
return lra.column_value_is_int(j); return lra.column_value_is_int(j);
} }
unsigned int_solver::random() { unsigned int_solver::random() {
return settings().random_next(); return settings().random_next();
@ -260,8 +260,8 @@ bool int_solver::is_term(unsigned j) const {
return lra.column_corresponds_to_term(j); return lra.column_corresponds_to_term(j);
} }
unsigned int_solver::column_count() const { unsigned int_solver::column_count() const {
return lra.column_count(); return lra.column_count();
} }
bool int_solver::should_find_cube() { bool int_solver::should_find_cube() {
@ -325,12 +325,12 @@ static void set_upper(impq & u, bool & inf_u, impq const & v) {
} }
bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) { bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq & l, bool & inf_u, impq & u, mpq & m) {
if (lrac.m_r_heading[j] >= 0) // the basic var if (lrac.m_r_heading[j] >= 0) // the basic var
return false; return false;
TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";); TRACE("random_update", display_column(tout, j) << ", is_int = " << column_is_int(j) << "\n";);
impq const & xj = get_value(j); impq const & xj = get_value(j);
inf_l = true; inf_l = true;
inf_u = true; inf_u = true;
l = u = zero_of_type<impq>(); l = u = zero_of_type<impq>();
@ -349,18 +349,18 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
unsigned rounds = 0; unsigned rounds = 0;
for (auto c : A.column(j)) { for (auto c : A.column(j)) {
row_index = c.var(); row_index = c.var();
const mpq & a = c.coeff(); const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index]; unsigned i = lrac.m_r_basis[row_index];
TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";); TRACE("random_update", tout << "i = " << i << ", a = " << a << "\n";);
if (column_is_int(i) && !a.is_int()) if (column_is_int(i) && !a.is_int())
m = lcm(m, denominator(a)); m = lcm(m, denominator(a));
} }
TRACE("random_update", tout << "m = " << m << "\n";); TRACE("random_update", tout << "m = " << m << "\n";);
for (auto c : A.column(j)) { for (auto c : A.column(j)) {
if (!inf_l && !inf_u && l >= u) break; if (!inf_l && !inf_u && l >= u) break;
row_index = c.var(); row_index = c.var();
const mpq & a = c.coeff(); const mpq & a = c.coeff();
unsigned i = lrac.m_r_basis[row_index]; unsigned i = lrac.m_r_basis[row_index];
impq const & xi = get_value(i); impq const & xi = get_value(i);
@ -374,7 +374,7 @@ bool int_solver::get_freedom_interval_for_column(unsigned j, bool & inf_l, impq
else \ else \
{ _fn_(a, b, (y - z)/x); } \ { _fn_(a, b, (y - z)/x); } \
if (a.is_neg()) { if (a.is_neg()) {
if (has_lower(i)) { if (has_lower(i)) {
SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_lower_bounds()[i]); SET_BOUND(set_lower, l, inf_l, a, xi, lrac.m_r_lower_bounds()[i]);
@ -488,59 +488,74 @@ bool int_solver::at_upper(unsigned j) const {
} }
} }
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const { std::ostream & int_solver::display_row(std::ostream & out, lp::row_strip<rational> const & row) const {
bool first = true;
auto & rslv = lrac.m_r_solver; auto & rslv = lrac.m_r_solver;
bool first = true; for (const auto &c : row)
for (const auto &c: rslv.m_A.m_rows[row_index]) { {
if (is_fixed(c.var())) { if (is_fixed(c.var()))
if (!get_value(c.var()).is_zero()) { {
impq val = get_value(c.var())*c.coeff(); if (!get_value(c.var()).is_zero())
{
impq val = get_value(c.var()) * c.coeff();
if (!first && val.is_pos()) if (!first && val.is_pos())
out << "+"; out << "+";
if (val.y.is_zero()) if (val.y.is_zero())
out << val.x << " "; out << val.x << " ";
else else
out << val << " "; out << val << " ";
} }
first = false; first = false;
continue; continue;
} }
if (c.coeff().is_one()) { if (c.coeff().is_one())
{
if (!first) if (!first)
out << "+"; out << "+";
} }
else if (c.coeff().is_minus_one()) else if (c.coeff().is_minus_one())
out << "-"; out << "-";
else { else
if (c.coeff().is_pos()) { {
if (c.coeff().is_pos())
{
if (!first) if (!first)
out << "+"; out << "+";
} }
if (c.coeff().is_big()) { if (c.coeff().is_big())
{
out << " b*"; out << " b*";
} }
else else
out << c.coeff(); out << c.coeff();
} }
out << rslv.column_name(c.var()) << " "; out << rslv.column_name(c.var()) << " ";
first = false; first = false;
} }
out << "\n"; out << "\n";
for (const auto& c: rslv.m_A.m_rows[row_index]) { for (const auto &c : row)
{
if (is_fixed(c.var())) if (is_fixed(c.var()))
continue; continue;
rslv.print_column_info(c.var(), out); rslv.print_column_info(c.var(), out);
if (is_base(c.var())) out << "j" << c.var() << " base\n"; if (is_base(c.var()))
out << "j" << c.var() << " base\n";
} }
return out; return out;
} }
std::ostream& int_solver::display_row_info(std::ostream & out, unsigned row_index) const {
auto & rslv = lrac.m_r_solver;
auto row = rslv.m_A.m_rows[row_index];
return display_row(out, row);
}
bool int_solver::shift_var(unsigned j, unsigned range) { bool int_solver::shift_var(unsigned j, unsigned range) {
if (is_fixed(j) || is_base(j)) if (is_fixed(j) || is_base(j))
return false; return false;
if (settings().get_cancel_flag()) if (settings().get_cancel_flag())
return false; return false;
bool inf_l = false, inf_u = false; bool inf_l = false, inf_u = false;
impq l, u; impq l, u;
mpq m; mpq m;
@ -592,7 +607,7 @@ bool int_solver::shift_var(unsigned j, unsigned range) {
TRACE("int_solver", tout << "a = " << a << ", b = " << b << ", r = " << r<< ", m = " << m << "\n";); TRACE("int_solver", tout << "a = " << a << ", b = " << b << ", r = " << r<< ", m = " << m << "\n";);
if (r < mpq(range)) if (r < mpq(range))
range = static_cast<unsigned>(r.get_uint64()); range = static_cast<unsigned>(r.get_uint64());
mpq s = b + mpq(random() % (range + 1)); mpq s = b + mpq(random() % (range + 1));
impq new_val = x + m * impq(s); impq new_val = x + m * impq(s);
TRACE("int_solver", tout << "new_val = " << new_val << "\n";); TRACE("int_solver", tout << "new_val = " << new_val << "\n";);

2
src/math/lp/int_solver.h
View file

@ -117,6 +117,8 @@ public:
bool shift_var(unsigned j, unsigned range); bool shift_var(unsigned j, unsigned range);
std::ostream& display_row_info(std::ostream & out, unsigned row_index) const; std::ostream& display_row_info(std::ostream & out, unsigned row_index) const;
std::ostream & display_row(std::ostream & out, vector<row_cell<rational>> const & row) const;
private: private:
unsigned random(); unsigned random();
bool has_inf_int() const; bool has_inf_int() const;