mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 19:02:02 +00:00
Code Activity

remove tracking of bounds

Browse source
This commit is contained in:
Lev Nachmanson 2023-08-20 10:10:48 -07:00
parent 610313946d
commit 9b672bc5cc
2 changed files with 4 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/math/lp/nla_core.cpp
View file

@ -1504,51 +1504,16 @@ void core::check_bounded_divisions(vector<lemma>& l_vec) {
m_lemma_vec = &l_vec; m_lemma_vec = &l_vec;
m_divisions.check_bounded_divisions(); m_divisions.check_bounded_divisions();
} }
// looking for a free variable inside of a monic to split
bool core::can_add_bound(unsigned j, u_map<unsigned>& bounds) {
unsigned count = 1;
if (bounds.find(j, count)) {
if (count >= 2)
return false;
++count;
}
bounds.insert(j, count);
struct decrement : public trail {
u_map<unsigned>& bounds;
unsigned j;
decrement(u_map<unsigned>& bounds, unsigned j):
bounds(bounds),
j(j)
{}
void undo() override {
--bounds[j];
}
};
trail().push(decrement(bounds, j));
return true;
}
void core::add_bounds() { void core::add_bounds() {
unsigned r = random(), sz = m_to_refine.size(); unsigned r = random(), sz = m_to_refine.size();
for (unsigned k = 0; k < sz; k++) { for (unsigned k = 0; k < sz; k++) {
lpvar i = m_to_refine[(k + r) % sz]; lpvar i = m_to_refine[(k + r) % sz];
auto const& m = m_emons[i]; auto const& m = m_emons[i];
for (lpvar j : m.vars()) { for (lpvar j : m.vars()) {
//m_lar_solver.print_column_info(j, verbose_stream() << "check variable " << j << " ") << "\n"; if (!var_is_free(j)) continue;
if (var_is_free(j)) // split the free variable (j <= 0, or j > 0), and return
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero())); m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::EQ, rational::zero()));
#if 0
else if (has_lower_bound(j) && can_add_bound(j, m_lower_bounds_added)) {
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::LE, get_lower_bound(j)));
std::cout << "called lower\n";
}
else if (has_upper_bound(j) && can_add_bound(j, m_upper_bounds_added)) {
m_literal_vec->push_back(ineq(j, lp::lconstraint_kind::GE, get_upper_bound(j)));
std::cout << "called upper\n";
}
#endif
else
continue;
++lp_settings().stats().m_nla_bounds; ++lp_settings().stats().m_nla_bounds;
return; return;
} }

4
src/math/lp/nla_core.h
View file

@ -110,11 +110,7 @@ class core {
monic const* m_patched_monic = nullptr; monic const* m_patched_monic = nullptr;
void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks); void check_weighted(unsigned sz, std::pair<unsigned, std::function<void(void)>>* checks);
u_map<unsigned> m_lower_bounds_added, m_upper_bounds_added;
bool can_add_bound(unsigned j, u_map<unsigned>& bounds);
void add_bounds(); void add_bounds();
public: public:
// constructor // constructor
core(lp::lar_solver& s, params_ref const& p, reslimit&); core(lp::lar_solver& s, params_ref const& p, reslimit&);