mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

comment out global_max_change

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-09-27 10:12:28 -07:00 committed by Lev Nachmanson
parent 89e4f59df2
commit 5ac428fcc9
1 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/math/lp/dioph_eq.cpp
View file

@ -7,7 +7,7 @@
namespace lp { namespace lp {
// This class represents a term with an added constant number c, in form sum {x_i*a_i} + c. // This class represents a term with an added constant number c, in form sum {x_i*a_i} + c.
int global_max_change = 100000; // 9 , 10 // int global_max_change_ = 100000; // 9 , 10
class dioph_eq::imp { class dioph_eq::imp {
class term_o:public lar_term { class term_o:public lar_term {
mpq m_c; mpq m_c;
@ -339,7 +339,7 @@ namespace lp {
} }
if (!change) if (!change)
return lia_move::undef; return lia_move::undef;
std::cout << "change " << change << std::endl; // std::cout << "change " << change << std::endl;
auto st = lra.find_feasible_solution(); auto st = lra.find_feasible_solution();
if (st != lp::lp_status::FEASIBLE && st != lp::lp_status::OPTIMAL) { if (st != lp::lp_status::FEASIBLE && st != lp::lp_status::OPTIMAL) {
lra.get_infeasibility_explanation(m_infeas_explanation); lra.get_infeasibility_explanation(m_infeas_explanation);
@ -384,9 +384,9 @@ namespace lp {
bool is_strict; bool is_strict;
bool change = false; bool change = false;
u_dependency *b_dep = nullptr; u_dependency *b_dep = nullptr;
if (global_max_change <= 0) { // if (global_max_change <= 0) {
return change; // return change;
} // }
if (lra.has_upper_bound(j, b_dep, rs, is_strict)) { if (lra.has_upper_bound(j, b_dep, rs, is_strict)) {
TRACE("dioph_eq", tout << "tighten upper bound for x" << j << " with rs:" << rs << std::endl;); TRACE("dioph_eq", tout << "tighten upper bound for x" << j << " with rs:" << rs << std::endl;);
@ -397,12 +397,12 @@ namespace lp {
if (!rs.is_int() || !t.c().is_zero()) { if (!rs.is_int() || !t.c().is_zero()) {
tighten_bound_for_term(t, g, j, lra.mk_join(dep, b_dep), rs, true); tighten_bound_for_term(t, g, j, lra.mk_join(dep, b_dep), rs, true);
change = true; change = true;
global_max_change--; //global_max_change--;
} }
} }
if (global_max_change <= 0) { // if (global_max_change <= 0) {
return change; // return change;
} // }
if (lra.has_lower_bound(j, b_dep, rs, is_strict)) { if (lra.has_lower_bound(j, b_dep, rs, is_strict)) {
TRACE("dioph_eq", tout << "tighten lower bound for x" << j << " with rs:" << rs << std::endl;); TRACE("dioph_eq", tout << "tighten lower bound for x" << j << " with rs:" << rs << std::endl;);
@ -413,7 +413,7 @@ namespace lp {
if (!rs.is_int()|| !t.c().is_zero()) { if (!rs.is_int()|| !t.c().is_zero()) {
tighten_bound_for_term(t, g, j, lra.mk_join(b_dep, dep), rs, false); tighten_bound_for_term(t, g, j, lra.mk_join(b_dep, dep), rs, false);
change = true; change = true;
global_max_change--; //global_max_change--;
} }
} }
return change; return change;