mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 04:43:39 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-07-17 11:00:11 -07:00
commit 9db636c38b
4 changed files with 16 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/euf/euf_etable.cpp
View file

@ -203,7 +203,7 @@ namespace euf {
SASSERT(n->num_args() > 0); SASSERT(n->num_args() > 0);
enode * n_prime; enode * n_prime;
void * t = get_table(n); void * t = get_table(n);
verbose_stream() << "insert " << n << "\n"; //verbose_stream() << "insert " << n << "\n";
switch (static_cast<table_kind>(GET_TAG(t))) { switch (static_cast<table_kind>(GET_TAG(t))) {
case UNARY: case UNARY:
n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n); n_prime = UNTAG(unary_table*, t)->insert_if_not_there(n);
@ -225,10 +225,10 @@ namespace euf {
SASSERT(n->num_args() > 0); SASSERT(n->num_args() > 0);
void * t = get_table(n); void * t = get_table(n);
static unsigned count = 0; static unsigned count = 0;
verbose_stream() << "erase " << (++count) << " " << n << "\n"; //verbose_stream() << "erase " << (++count) << " " << n << "\n";
if (count == 10398) { // if (count == 10398) {
verbose_stream() << "here\n"; // verbose_stream() << "here\n";
} // }
switch (static_cast<table_kind>(GET_TAG(t))) { switch (static_cast<table_kind>(GET_TAG(t))) {
case UNARY: case UNARY:
UNTAG(unary_table*, t)->erase(n); UNTAG(unary_table*, t)->erase(n);

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

@ -150,21 +150,22 @@ namespace lp {
} }
for (auto const& c : A.column(j)) { for (auto const& c : A.column(j)) {
unsigned row_index = c.var(); unsigned row_index = c.var();
unsigned i = lrac.m_r_basis[row_index]; unsigned bj = lrac.m_r_basis[row_index];
auto old_val = lia.get_value(i); auto old_val = lia.get_value(bj);
auto new_val = old_val - impq(c.coeff()*delta); auto new_val = old_val - impq(c.coeff()*delta);
if (lia.has_lower(i) && new_val < lra.get_lower_bound(i)) if (lia.has_lower(bj) && new_val < lra.get_lower_bound(bj))
return false; return false;
if (lia.has_upper(i) && new_val > lra.get_upper_bound(i)) if (lia.has_upper(bj) && new_val > lra.get_upper_bound(bj))
return false; return false;
if (old_val.is_int() && !new_val.is_int()){ if (old_val.is_int() && !new_val.is_int()){
return false; // do not waste resources on this case return false; // do not waste resources on this case
} }
lp_assert(i != v || new_val.is_int()) // if bj == v, then, because we are patching the lra.get_value(v),
// we just need to assert that the lra.get_value(v) would be integral.
lp_assert(bj != v || lra.from_model_in_impq_to_mpq(new_val).is_int());
} }
lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta)); lra.set_value_for_nbasic_column(j, lia.get_value(j) + impq(delta));
return true; return true;
} }

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

@ -619,11 +619,10 @@ namespace lp {
} }
void lar_solver::add_touched_row(unsigned rid) { void lar_solver::add_touched_row(unsigned rid) {
if (m_settings.bound_propagation())
m_touched_rows.insert(rid); m_touched_rows.insert(rid);
} }
bool lar_solver::use_tableau_costs() const { bool lar_solver::use_tableau_costs() const {
return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs; return m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs;
} }
@ -1019,7 +1018,7 @@ namespace lp {
SASSERT(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE); SASSERT(get_status() == lp_status::OPTIMAL || get_status() == lp_status::FEASIBLE);
SASSERT(m_columns_with_changed_bounds.empty()); SASSERT(m_columns_with_changed_bounds.empty());
numeric_pair<mpq> const& rp = get_column_value(j); numeric_pair<mpq> const& rp = get_column_value(j);
return rp.x + m_delta * rp.y; return from_model_in_impq_to_mpq(rp);
} }
mpq lar_solver::get_tv_value(tv const& t) const { mpq lar_solver::get_tv_value(tv const& t) const {

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

@ -497,6 +497,7 @@ class lar_solver : public column_namer {
std::ostream& display(std::ostream& out) const; std::ostream& display(std::ostream& out) const;
bool init_model() const; bool init_model() const;
mpq from_model_in_impq_to_mpq(const impq& v) const { return v.x + m_delta * v.y; }
mpq get_value(column_index const& j) const; mpq get_value(column_index const& j) const;
mpq get_tv_value(tv const& t) const; mpq get_tv_value(tv const& t) const;
const impq& get_tv_ivalue(tv const& t) const; const impq& get_tv_ivalue(tv const& t) const;