mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

make lp_bound_propagator a field of theory_lra::imp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-06-09 11:20:40 -07:00
parent dd30b5e3af
commit b3bdce7837
3 changed files with 43 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -299,7 +299,7 @@ public:
inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; } inline void backup_x() { m_backup_x = m_mpq_lar_core_solver.m_r_x; }
inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; } inline void restore_x() { m_mpq_lar_core_solver.m_r_x = m_backup_x; }
template <typename T> template <typename T>
void explain_implied_bound(implied_bound & ib, lp_bound_propagator<T> & bp) { void explain_implied_bound(const implied_bound & ib, lp_bound_propagator<T> & bp) {
unsigned i = ib.m_row_or_term_index; unsigned i = ib.m_row_or_term_index;
int bound_sign = ib.m_is_lower_bound? 1: -1; int bound_sign = ib.m_is_lower_bound? 1: -1;
int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign; int j_sign = (ib.m_coeff_before_j_is_pos ? 1 :-1) * bound_sign;

22
src/math/lp/lp_bound_propagator.h
View file

@ -67,8 +67,14 @@ class lp_bound_propagator {
std::unordered_map<unsigned, unsigned> m_improved_upper_bounds; std::unordered_map<unsigned, unsigned> m_improved_upper_bounds;
T& m_imp; T& m_imp;
impq m_zero; impq m_zero;
public:
vector<implied_bound> m_ibounds; vector<implied_bound> m_ibounds;
public:
const vector<implied_bound>& ibounds() const { return m_ibounds; }
void init() {
m_improved_upper_bounds.clear();
m_improved_lower_bounds.clear();
m_ibounds.reset();
}
lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {} lp_bound_propagator(T& imp): m_imp(imp), m_zero(impq(0)) {}
const lar_solver& lp() const { return m_imp.lp(); } const lar_solver& lp() const { return m_imp.lp(); }
column_type get_column_type(unsigned j) const { column_type get_column_type(unsigned j) const {
@ -178,9 +184,8 @@ public:
} }
} }
void clear_for_eq() { void clear_for_eq() {
// m_reported_pairs.reset();
m_visited_rows.reset(); m_visited_rows.reset();
m_visited_columns.reset(); m_visited_columns.reset();
m_offset_to_verts.reset(); m_offset_to_verts.reset();
@ -251,8 +256,9 @@ public:
void find_path_on_tree(ptr_vector<vertex> & path, vertex* u, vertex* v) const { void find_path_on_tree(ptr_vector<vertex> & path, vertex* u, vertex* v) const {
vertex* up; // u parent vertex* up; // u parent
vertex* vp; // v parent vertex* vp; // v parent
ptr_vector<vertex> v_branch;
path.push_back(u); path.push_back(u);
path.push_back(v); v_branch.push_back(v);
// equalize the levels // equalize the levels
while (u->level() > v->level()) { while (u->level() > v->level()) {
up = u->parent(); up = u->parent();
@ -264,7 +270,7 @@ public:
while (u->level() < v->level()) { while (u->level() < v->level()) {
vp = v->parent(); vp = v->parent();
if (v->row() == vp->row()) if (v->row() == vp->row())
path.push_back(vp); v_branch.push_back(vp);
v = vp; v = vp;
} }
SASSERT(u->level() == v->level()); SASSERT(u->level() == v->level());
@ -278,9 +284,13 @@ public:
if (up->row() == u->row()) if (up->row() == u->row())
path.push_back(up); path.push_back(up);
if (vp->row() == v->row()) if (vp->row() == v->row())
path.push_back(vp); v_branch.push_back(vp);
u = up; v = vp; u = up; v = vp;
} }
for (unsigned i = v_branch.size(); i--; ) {
path.push_back(v_branch[i]);
}
} }
bool tree_is_correct() const { bool tree_is_correct() const {

48
src/smt/theory_lra.cpp
View file

@ -165,11 +165,11 @@ class theory_lra::imp {
}; };
theory_lra& th; theory_lra& th;
ast_manager& m; ast_manager& m;
arith_util a; arith_util a;
arith_eq_adapter m_arith_eq_adapter; arith_eq_adapter m_arith_eq_adapter;
vector<rational> m_columns; vector<rational> m_columns;
// temporary values kept during internalization // temporary values kept during internalization
@ -309,13 +309,14 @@ class theory_lra::imp {
int_hashtable<var_value_hash, var_value_eq> m_model_eqs; int_hashtable<var_value_hash, var_value_eq> m_model_eqs;
svector<scope> m_scopes; svector<scope> m_scopes;
lp_api::stats m_stats; lp_api::stats m_stats;
arith_factory* m_factory; arith_factory* m_factory;
scoped_ptr<lp::lar_solver> m_solver; scoped_ptr<lp::lar_solver> m_solver;
resource_limit m_resource_limit; resource_limit m_resource_limit;
lp_bounds m_new_bounds; lp_bounds m_new_bounds;
symbol m_farkas; symbol m_farkas;
lp::lp_bound_propagator<imp> m_bp;
context& ctx() const { return th.get_context(); } context& ctx() const { return th.get_context(); }
theory_id get_id() const { return th.get_id(); } theory_id get_id() const { return th.get_id(); }
@ -958,7 +959,9 @@ public:
m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)), m_model_eqs(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
m_solver(nullptr), m_solver(nullptr),
m_resource_limit(*this), m_resource_limit(*this),
m_farkas("farkas") { m_farkas("farkas"),
m_bp(*this)
{
} }
~imp() { ~imp() {
@ -2351,10 +2354,9 @@ public:
void propagate_bounds_with_lp_solver() { void propagate_bounds_with_lp_solver() {
if (!should_propagate()) if (!should_propagate())
return; return;
lp::lp_bound_propagator<imp> bp(*this);
lp().propagate_bounds_for_touched_rows(bp); m_bp.init();
lp().propagate_bounds_for_touched_rows(m_bp);
if (!m.inc()) { if (!m.inc()) {
return; return;
@ -2364,8 +2366,11 @@ public:
get_infeasibility_explanation_and_set_conflict(); get_infeasibility_explanation_and_set_conflict();
} }
else { else {
for (unsigned i = 0; m.inc() && !ctx().inconsistent() && i < bp.m_ibounds.size(); ++i) { for (auto& ib : m_bp.ibounds()) {
propagate_lp_solver_bound(bp.m_ibounds[i]); m.inc();
if (ctx().inconsistent())
break;
propagate_lp_solver_bound(ib);
} }
} }
} }
@ -2386,7 +2391,7 @@ public:
} }
return false; return false;
} }
void propagate_lp_solver_bound(lp::implied_bound& be) { void propagate_lp_solver_bound(const lp::implied_bound& be) {
lpvar vi = be.m_j; lpvar vi = be.m_j;
theory_var v = lp().local_to_external(vi); theory_var v = lp().local_to_external(vi);
@ -2418,8 +2423,7 @@ public:
first = false; first = false;
reset_evidence(); reset_evidence();
m_explanation.clear(); m_explanation.clear();
lp::lp_bound_propagator<imp> bp(*this); lp().explain_implied_bound(be, m_bp);
lp().explain_implied_bound(be, bp);
} }
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";); CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1); updt_unassigned_bounds(v, -1);
@ -4045,5 +4049,5 @@ expr_ref theory_lra::mk_ge(generic_model_converter& fm, theory_var v, inf_ration
} }
template class lp::lp_bound_propagator<smt::theory_lra::imp>; template class lp::lp_bound_propagator<smt::theory_lra::imp>;
template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&); template void lp::lar_solver::propagate_bounds_for_touched_rows<smt::theory_lra::imp>(lp::lp_bound_propagator<smt::theory_lra::imp>&);
template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&); template void lp::lar_solver::explain_implied_bound<smt::theory_lra::imp>(const lp::implied_bound&, lp::lp_bound_propagator<smt::theory_lra::imp>&);
template void lp::lar_solver::calculate_implied_bounds_for_row<smt::theory_lra::imp>(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>&); template void lp::lar_solver::calculate_implied_bounds_for_row<smt::theory_lra::imp>(unsigned int, lp::lp_bound_propagator<smt::theory_lra::imp>&);