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

remove unnecessery call

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2023-10-04 17:39:22 -07:00
parent edd1761ff3
commit 45c0ed126e
5 changed files with 11 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lar_solver.cpp
View file

@ -419,7 +419,9 @@ namespace lp {
void lar_solver::move_non_basic_columns_to_bounds(bool shift_randomly) {
auto& lcs = m_mpq_lar_core_solver;
bool change = false;
for (unsigned j : lcs.m_r_nbasis) {
for (unsigned j : m_columns_with_changed_bounds) {
if (lcs.m_r_heading[j] >= 0)
continue;
if (move_non_basic_column_to_bounds(j, shift_randomly))
change = true;
}
@ -2374,6 +2376,7 @@ namespace lp {
u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
SASSERT(bdep != nullptr);
m_crossed_bounds_deps = m_dependencies.mk_join(bdep, dep);
insert_to_columns_with_changed_bounds(j);
}
void lar_solver::collect_more_rows_for_lp_propagation(){

3
src/math/lp/lar_solver.h
View file

@ -140,7 +140,8 @@ class lar_solver : public column_namer {
bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs);
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
public:
public:
const auto& columns_with_changed_bounds() const { return m_columns_with_changed_bounds; }
void insert_to_columns_with_changed_bounds(unsigned j);
const u_dependency* crossed_bounds_deps() const { return m_crossed_bounds_deps;}
u_dependency*& crossed_bounds_deps() { return m_crossed_bounds_deps;}

10
src/math/lp/monomial_bounds.cpp
View file

@ -268,15 +268,14 @@ namespace nla {
c().lra.get_infeasibility_explanation(exp);
new_lemma lemma(c(), "propagate fixed - infeasible lra");
lemma &= exp;
return;
break;
}
if (c().m_conflicts > 0 ) {
return;
break;
}
}
}
void monomial_bounds::unit_propagate(monic & m) {
if (m.is_propagated())
return;
@ -288,9 +287,8 @@ namespace nla {
rational k = fixed_var_product(m);
lpvar w = non_fixed_var(m);
if (w == null_lpvar || k == 0) {
if (w == null_lpvar || k == 0)
propagate_fixed(m, k);
}
else
propagate_nonfixed(m, k, w);
}
@ -310,6 +308,7 @@ namespace nla {
lp::impq val(k);
c().lra.set_value_for_nbasic_column(m.var(), val);
}
TRACE("nla_solver", tout << "propagate fixed " << m << " = " << k << "\n";);
c().lra.update_column_type_and_bound(m.var(), lp::lconstraint_kind::EQ, k, dep);
// propagate fixed equality
@ -325,6 +324,7 @@ namespace nla {
lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX);
auto* dep = explain_fixed(m, k);
term_index = c().lra.map_term_index_to_column_index(term_index);
TRACE("nla_solver", tout << "propagate nonfixed " << m << " = " << k << "\n";);
c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep);
if (k == 1) {

1
src/math/lp/monomial_bounds.h
View file

@ -39,7 +39,6 @@ namespace nla {
bool is_linear(monic const& m);
rational fixed_var_product(monic const& m);
lpvar non_fixed_var(monic const& m);
public:
monomial_bounds(core* core);
void propagate();

2
src/smt/theory_lra.cpp
View file

@ -3205,8 +3205,6 @@ public:
lbool make_feasible() {
TRACE("pcs", tout << lp().constraints(););
TRACE("arith_verbose", tout << "before calling lp().find_feasible_solution()\n"; display(tout););
// todo: remove later : debug!!!!!
lp().move_non_basic_columns_to_bounds(false);
auto status = lp().find_feasible_solution();
TRACE("arith_verbose", display(tout););
if (lp().is_feasible())