mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 11:55:51 +00:00
Code Activity

Partial cleanup of util/lp/*

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-09-17 16:00:06 +01:00
parent 00651f8f21
commit d61b722b68
109 changed files with 3503 additions and 2023 deletions
Download patch file Download diff file Expand all files Collapse all files

318
src/smt/theory_lra.cpp
View file

@ -38,7 +38,7 @@ Revision History:
#include "util/nat_set.h"
#include "tactic/filter_model_converter.h"
namespace lp {
namespace lra_lp {
enum bound_kind { lower_t, upper_t };
std::ostream& operator<<(std::ostream& out, bound_kind const& k) {
@ -50,7 +50,7 @@ namespace lp {
}
class bound {
smt::bool_var m_bv;
smt::bool_var m_bv;
smt::theory_var m_var;
rational m_value;
bound_kind m_bound_kind;
@ -111,7 +111,7 @@ namespace lp {
namespace smt {
typedef ptr_vector<lp::bound> lp_bounds;
typedef ptr_vector<lra_lp::bound> lp_bounds;
class theory_lra::imp {
@ -133,7 +133,7 @@ namespace smt {
delayed_atom(unsigned b, bool t): m_bv(b), m_is_true(t) {}
};
class resource_limit : public lean::lp_resource_limit {
class resource_limit : public lp::lp_resource_limit {
imp& m_imp;
public:
resource_limit(imp& i): m_imp(i) { }
@ -198,7 +198,7 @@ namespace smt {
}
};
typedef vector<std::pair<rational, lean::var_index>> var_coeffs;
typedef vector<std::pair<rational, lp::var_index>> var_coeffs;
struct delayed_def {
vector<rational> m_coeffs;
svector<theory_var> m_vars;
@ -208,11 +208,11 @@ namespace smt {
m_coeffs(coeffs), m_vars(vars), m_coeff(r), m_var(v) {}
};
svector<lean::var_index> m_theory_var2var_index; // translate from theory variables to lar vars
svector<lp::var_index> m_theory_var2var_index; // translate from theory variables to lar vars
svector<theory_var> m_var_index2theory_var; // reverse map from lp_solver variables to theory variables
svector<theory_var> m_term_index2theory_var; // reverse map from lp_solver variables to theory variables
var_coeffs m_left_side; // constraint left side
mutable std::unordered_map<lean::var_index, rational> m_variable_values; // current model
mutable std::unordered_map<lp::var_index, rational> m_variable_values; // current model
enum constraint_source {
inequality_source,
@ -233,10 +233,10 @@ namespace smt {
expr* m_not_handled;
ptr_vector<app> m_underspecified;
unsigned_vector m_var_trail;
vector<ptr_vector<lp::bound> > m_use_list; // bounds where variables are used.
vector<ptr_vector<lra_lp::bound> > m_use_list; // bounds where variables are used.
// attributes for incremental version:
u_map<lp::bound*> m_bool_var2bound;
u_map<lra_lp::bound*> m_bool_var2bound;
vector<lp_bounds> m_bounds;
unsigned_vector m_unassigned_bounds;
unsigned_vector m_bounds_trail;
@ -258,15 +258,15 @@ namespace smt {
struct var_value_hash {
imp & m_th;
var_value_hash(imp & th):m_th(th) {}
unsigned operator()(theory_var v) const { return (unsigned)std::hash<lean::impq>()(m_th.get_ivalue(v)); }
unsigned operator()(theory_var v) const { return (unsigned)std::hash<lp::impq>()(m_th.get_ivalue(v)); }
};
int_hashtable<var_value_hash, var_value_eq> m_model_eqs;
svector<scope> m_scopes;
lp::stats m_stats;
lra_lp::stats m_stats;
arith_factory* m_factory;
scoped_ptr<lean::lar_solver> m_solver;
scoped_ptr<lp::lar_solver> m_solver;
resource_limit m_resource_limit;
lp_bounds m_new_bounds;
@ -282,10 +282,10 @@ namespace smt {
void init_solver() {
if (m_solver) return;
lp_params lp(ctx().get_params());
m_solver = alloc(lean::lar_solver);
m_solver = alloc(lp::lar_solver);
m_theory_var2var_index.reset();
m_solver->settings().set_resource_limit(m_resource_limit);
m_solver->settings().simplex_strategy() = static_cast<lean::simplex_strategy_enum>(lp.simplex_strategy());
m_solver->settings().simplex_strategy() = static_cast<lp::simplex_strategy_enum>(lp.simplex_strategy());
reset_variable_values();
m_solver->settings().bound_propagation() = BP_NONE != propagation_mode();
m_solver->set_propagate_bounds_on_pivoted_rows_mode(lp.bprop_on_pivoted_rows());
@ -487,8 +487,8 @@ namespace smt {
return v;
}
lean::var_index get_var_index(theory_var v) {
lean::var_index result = UINT_MAX;
lp::var_index get_var_index(theory_var v) {
lp::var_index result = UINT_MAX;
if (m_theory_var2var_index.size() > static_cast<unsigned>(v)) {
result = m_theory_var2var_index[v];
}
@ -537,20 +537,20 @@ namespace smt {
return true;
}
void add_eq_constraint(lean::constraint_index index, enode* n1, enode* n2) {
void add_eq_constraint(lp::constraint_index index, enode* n1, enode* n2) {
m_constraint_sources.setx(index, equality_source, null_source);
m_equalities.setx(index, enode_pair(n1, n2), enode_pair(0, 0));
++m_stats.m_add_rows;
}
void add_ineq_constraint(lean::constraint_index index, literal lit) {
void add_ineq_constraint(lp::constraint_index index, literal lit) {
m_constraint_sources.setx(index, inequality_source, null_source);
m_inequalities.setx(index, lit, null_literal);
++m_stats.m_add_rows;
TRACE("arith", m_solver->print_constraint(index, tout); tout << "\n";);
}
void add_def_constraint(lean::constraint_index index, theory_var v) {
void add_def_constraint(lp::constraint_index index, theory_var v) {
m_constraint_sources.setx(index, definition_source, null_source);
m_definitions.setx(index, v, null_theory_var);
++m_stats.m_add_rows;
@ -561,7 +561,7 @@ namespace smt {
st.vars().append(d.m_vars);
st.coeffs().append(d.m_coeffs);
init_left_side(st);
add_def_constraint(m_solver->add_constraint(m_left_side, lean::EQ, -d.m_coeff), d.m_var);
add_def_constraint(m_solver->add_constraint(m_left_side, lp::EQ, -d.m_coeff), d.m_var);
}
void internalize_eq(theory_var v1, theory_var v2) {
@ -573,7 +573,7 @@ namespace smt {
st.coeffs().push_back(rational::one());
st.coeffs().push_back(rational::minus_one());
init_left_side(st);
add_eq_constraint(m_solver->add_constraint(m_left_side, lean::EQ, rational::zero()), n1, n2);
add_eq_constraint(m_solver->add_constraint(m_left_side, lp::EQ, rational::zero()), n1, n2);
TRACE("arith",
tout << "v" << v1 << " = " << "v" << v2 << ": "
<< mk_pp(n1->get_owner(), m) << " = " << mk_pp(n2->get_owner(), m) << "\n";);
@ -583,7 +583,7 @@ namespace smt {
for (unsigned i = m_bounds_trail.size(); i > old_size; ) {
--i;
unsigned v = m_bounds_trail[i];
lp::bound* b = m_bounds[v].back();
lra_lp::bound* b = m_bounds[v].back();
// del_use_lists(b);
dealloc(b);
m_bounds[v].pop_back();
@ -626,7 +626,7 @@ namespace smt {
else {
init_left_side(st);
theory_var v = mk_var(term);
lean::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
if (vi == UINT_MAX) {
vi = m_solver->add_term(m_left_side, st.coeff());
m_theory_var2var_index.setx(v, vi, UINT_MAX);
@ -691,22 +691,22 @@ namespace smt {
ctx().set_var_theory(bv, get_id());
expr* n1, *n2;
rational r;
lp::bound_kind k;
lra_lp::bound_kind k;
theory_var v = null_theory_var;
if (a.is_le(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1));
k = lp::upper_t;
k = lra_lp::upper_t;
}
else if (a.is_ge(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1));
k = lp::lower_t;
k = lra_lp::lower_t;
}
else {
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
found_not_handled(atom);
return true;
}
lp::bound* b = alloc(lp::bound, bv, v, r, k);
lra_lp::bound* b = alloc(lra_lp::bound, bv, v, r, k);
m_bounds[v].push_back(b);
updt_unassigned_bounds(v, +1);
m_bounds_trail.push_back(v);
@ -723,23 +723,23 @@ namespace smt {
ctx().set_var_theory(bv, get_id());
expr* n1, *n2;
rational r;
lp::bound_kind k;
lra_lp::bound_kind k;
theory_var v = null_theory_var;
scoped_internalize_state st(*this);
if (a.is_le(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1), st);
k = lp::upper_t;
k = lra_lp::upper_t;
}
else if (a.is_ge(atom, n1, n2) && is_numeral(n2, r) && is_app(n1)) {
v = internalize_def(to_app(n1), st);
k = lp::lower_t;
k = lra_lp::lower_t;
}
else {
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
found_not_handled(atom);
return true;
}
lp::bound* b = alloc(lp::bound, bv, v, r, k);
lra_lp::bound* b = alloc(lra_lp::bound, bv, v, r, k);
m_bounds[v].push_back(b);
updt_unassigned_bounds(v, +1);
m_bounds_trail.push_back(v);
@ -830,7 +830,7 @@ namespace smt {
unsigned old_size = m_scopes.size() - num_scopes;
del_bounds(m_scopes[old_size].m_bounds_lim);
for (unsigned i = m_scopes[old_size].m_var_trail_lim; i < m_var_trail.size(); ++i) {
lean::var_index vi = m_theory_var2var_index[m_var_trail[i]];
lp::var_index vi = m_theory_var2var_index[m_var_trail[i]];
if (m_solver->is_term(vi)) {
unsigned ti = m_solver->adjust_term_index(vi);
m_term_index2theory_var[ti] = UINT_MAX;
@ -1023,14 +1023,14 @@ namespace smt {
return m_solver->var_is_registered(m_theory_var2var_index[v]);
}
lean::impq get_ivalue(theory_var v) const {
lean_assert(can_get_ivalue(v));
lean::var_index vi = m_theory_var2var_index[v];
lp::impq get_ivalue(theory_var v) const {
SASSERT(can_get_ivalue(v));
lp::var_index vi = m_theory_var2var_index[v];
if (!m_solver->is_term(vi))
return m_solver->get_value(vi);
const lean::lar_term& term = m_solver->get_term(vi);
lean::impq result(term.m_v);
const lp::lar_term& term = m_solver->get_term(vi);
lp::impq result(term.m_v);
for (const auto & i: term.m_coeffs) {
result += m_solver->get_value(i.first) * i.second;
}
@ -1040,12 +1040,12 @@ namespace smt {
rational get_value(theory_var v) const {
if (!can_get_value(v)) return rational::zero();
lean::var_index vi = m_theory_var2var_index[v];
lp::var_index vi = m_theory_var2var_index[v];
if (m_variable_values.count(vi) > 0) {
return m_variable_values[vi];
}
if (m_solver->is_term(vi)) {
const lean::lar_term& term = m_solver->get_term(vi);
const lp::lar_term& term = m_solver->get_term(vi);
rational result = term.m_v;
for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) {
result += m_variable_values[i->first] * i->second;
@ -1068,7 +1068,7 @@ namespace smt {
}
bool assume_eqs() {
svector<lean::var_index> vars;
svector<lp::var_index> vars;
theory_var sz = static_cast<theory_var>(th.get_num_vars());
for (theory_var v = 0; v < sz; ++v) {
if (th.is_relevant_and_shared(get_enode(v))) {
@ -1169,7 +1169,7 @@ namespace smt {
}
is_sat = make_feasible();
}
else if (m_solver->get_status() != lean::lp_status::OPTIMAL) {
else if (m_solver->get_status() != lp::lp_status::OPTIMAL) {
is_sat = make_feasible();
}
switch (is_sat) {
@ -1266,7 +1266,7 @@ namespace smt {
propagate_bound(bv, is_true, b);
#endif
if (!m_delay_constraints) {
lp::bound& b = *m_bool_var2bound.find(bv);
lra_lp::bound& b = *m_bool_var2bound.find(bv);
assert_bound(bv, is_true, b);
}
@ -1279,7 +1279,7 @@ namespace smt {
/*for (; qhead < m_asserted_atoms.size() && !ctx().inconsistent(); ++qhead) {
bool_var bv = m_asserted_atoms[qhead].m_bv;
bool is_true = m_asserted_atoms[qhead].m_is_true;
lp::bound& b = *m_bool_var2bound.find(bv);
lra_lp::bound& b = *m_bool_var2bound.find(bv);
propagate_bound_compound(bv, is_true, b);
}*/
@ -1314,7 +1314,7 @@ namespace smt {
int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
(void)new_num_of_p;
CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
if (m_solver->get_status() == lean::lp_status::INFEASIBLE) {
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
set_conflict();
}
else {
@ -1324,7 +1324,7 @@ namespace smt {
}
}
bool bound_is_interesting(unsigned vi, lean::lconstraint_kind kind, const rational & bval) const {
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
theory_var v;
if (m_solver->is_term(vi)) {
v = m_term_index2theory_var.get(m_solver->adjust_term_index(vi), null_theory_var);
@ -1341,7 +1341,7 @@ namespace smt {
}
lp_bounds const& bounds = m_bounds[v];
for (unsigned i = 0; i < bounds.size(); ++i) {
lp::bound* b = bounds[i];
lra_lp::bound* b = bounds[i];
if (ctx().get_assignment(b->get_bv()) != l_undef) {
continue;
}
@ -1354,11 +1354,11 @@ namespace smt {
return false;
}
struct local_bound_propagator: public lean::lp_bound_propagator {
struct local_bound_propagator: public lp::lp_bound_propagator {
imp & m_imp;
local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {}
bool bound_is_interesting(unsigned j, lean::lconstraint_kind kind, const rational & v) {
bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const rational & v) {
return m_imp.bound_is_interesting(j, kind, v);
}
@ -1368,10 +1368,10 @@ namespace smt {
};
void propagate_lp_solver_bound(lean::implied_bound& be) {
void propagate_lp_solver_bound(lp::implied_bound& be) {
theory_var v;
lean::var_index vi = be.m_j;
lp::var_index vi = be.m_j;
if (m_solver->is_term(vi)) {
v = m_term_index2theory_var.get(m_solver->adjust_term_index(vi), null_theory_var);
}
@ -1392,7 +1392,7 @@ namespace smt {
lp_bounds const& bounds = m_bounds[v];
bool first = true;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp::bound* b = bounds[i];
lra_lp::bound* b = bounds[i];
if (ctx().get_assignment(b->get_bv()) != l_undef) {
continue;
}
@ -1455,28 +1455,28 @@ namespace smt {
}
}
literal is_bound_implied(lean::lconstraint_kind k, rational const& value, lp::bound const& b) const {
if ((k == lean::LE || k == lean::LT) && b.get_bound_kind() == lp::upper_t && value <= b.get_value()) {
literal is_bound_implied(lp::lconstraint_kind k, rational const& value, lra_lp::bound const& b) const {
if ((k == lp::LE || k == lp::LT) && b.get_bound_kind() == lra_lp::upper_t && value <= b.get_value()) {
// v <= value <= b.get_value() => v <= b.get_value()
return literal(b.get_bv(), false);
}
if ((k == lean::GE || k == lean::GT) && b.get_bound_kind() == lp::lower_t && b.get_value() <= value) {
if ((k == lp::GE || k == lp::GT) && b.get_bound_kind() == lra_lp::lower_t && b.get_value() <= value) {
// b.get_value() <= value <= v => b.get_value() <= v
return literal(b.get_bv(), false);
}
if (k == lean::LE && b.get_bound_kind() == lp::lower_t && value < b.get_value()) {
if (k == lp::LE && b.get_bound_kind() == lra_lp::lower_t && value < b.get_value()) {
// v <= value < b.get_value() => v < b.get_value()
return literal(b.get_bv(), true);
}
if (k == lean::LT && b.get_bound_kind() == lp::lower_t && value <= b.get_value()) {
if (k == lp::LT && b.get_bound_kind() == lra_lp::lower_t && value <= b.get_value()) {
// v < value <= b.get_value() => v < b.get_value()
return literal(b.get_bv(), true);
}
if (k == lean::GE && b.get_bound_kind() == lp::upper_t && b.get_value() < value) {
if (k == lp::GE && b.get_bound_kind() == lra_lp::upper_t && b.get_value() < value) {
// b.get_value() < value <= v => b.get_value() < v
return literal(b.get_bv(), true);
}
if (k == lean::GT && b.get_bound_kind() == lp::upper_t && b.get_value() <= value) {
if (k == lp::GT && b.get_bound_kind() == lra_lp::upper_t && b.get_value() <= value) {
// b.get_value() <= value < v => b.get_value() < v
return literal(b.get_bv(), true);
}
@ -1484,7 +1484,7 @@ namespace smt {
return null_literal;
}
void mk_bound_axioms(lp::bound& b) {
void mk_bound_axioms(lra_lp::bound& b) {
if (!ctx().is_searching()) {
//
// NB. We make an assumption that user push calls propagation
@ -1495,19 +1495,19 @@ namespace smt {
return;
}
theory_var v = b.get_var();
lp::bound_kind kind1 = b.get_bound_kind();
lra_lp::bound_kind kind1 = b.get_bound_kind();
rational const& k1 = b.get_value();
lp_bounds & bounds = m_bounds[v];
lp::bound* end = 0;
lp::bound* lo_inf = end, *lo_sup = end;
lp::bound* hi_inf = end, *hi_sup = end;
lra_lp::bound* end = 0;
lra_lp::bound* lo_inf = end, *lo_sup = end;
lra_lp::bound* hi_inf = end, *hi_sup = end;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp::bound& other = *bounds[i];
lra_lp::bound& other = *bounds[i];
if (&other == &b) continue;
if (b.get_bv() == other.get_bv()) continue;
lp::bound_kind kind2 = other.get_bound_kind();
lra_lp::bound_kind kind2 = other.get_bound_kind();
rational const& k2 = other.get_value();
if (k1 == k2 && kind1 == kind2) {
// the bounds are equivalent.
@ -1515,7 +1515,7 @@ namespace smt {
}
SASSERT(k1 != k2 || kind1 != kind2);
if (kind2 == lp::lower_t) {
if (kind2 == lra_lp::lower_t) {
if (k2 < k1) {
if (lo_inf == end || k2 > lo_inf->get_value()) {
lo_inf = &other;
@ -1541,14 +1541,14 @@ namespace smt {
}
void mk_bound_axiom(lp::bound& b1, lp::bound& b2) {
void mk_bound_axiom(lra_lp::bound& b1, lra_lp::bound& b2) {
theory_var v = b1.get_var();
literal l1(b1.get_bv());
literal l2(b2.get_bv());
rational const& k1 = b1.get_value();
rational const& k2 = b2.get_value();
lp::bound_kind kind1 = b1.get_bound_kind();
lp::bound_kind kind2 = b2.get_bound_kind();
lra_lp::bound_kind kind1 = b1.get_bound_kind();
lra_lp::bound_kind kind2 = b2.get_bound_kind();
bool v_is_int = is_int(v);
SASSERT(v == b2.get_var());
if (k1 == k2 && kind1 == kind2) return;
@ -1556,8 +1556,8 @@ namespace smt {
parameter coeffs[3] = { parameter(symbol("farkas")),
parameter(rational(1)), parameter(rational(1)) };
if (kind1 == lp::lower_t) {
if (kind2 == lp::lower_t) {
if (kind1 == lra_lp::lower_t) {
if (kind2 == lra_lp::lower_t) {
if (k2 <= k1) {
mk_clause(~l1, l2, 3, coeffs);
}
@ -1578,7 +1578,7 @@ namespace smt {
}
}
}
else if (kind2 == lp::lower_t) {
else if (kind2 == lra_lp::lower_t) {
if (k1 >= k2) {
// k1 >= lo_inf, k1 >= x or lo_inf <= x
mk_clause(l1, l2, 3, coeffs);
@ -1636,21 +1636,21 @@ namespace smt {
iterator begin1 = occs.begin();
iterator begin2 = occs.begin();
iterator end = occs.end();
begin1 = first(lp::lower_t, begin1, end);
begin2 = first(lp::upper_t, begin2, end);
begin1 = first(lra_lp::lower_t, begin1, end);
begin2 = first(lra_lp::upper_t, begin2, end);
iterator lo_inf = begin1, lo_sup = begin1;
iterator hi_inf = begin2, hi_sup = begin2;
iterator lo_inf1 = begin1, lo_sup1 = begin1;
iterator hi_inf1 = begin2, hi_sup1 = begin2;
bool flo_inf, fhi_inf, flo_sup, fhi_sup;
ptr_addr_hashtable<lp::bound> visited;
ptr_addr_hashtable<lra_lp::bound> visited;
for (unsigned i = 0; i < atoms.size(); ++i) {
lp::bound* a1 = atoms[i];
lo_inf1 = next_inf(a1, lp::lower_t, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, lp::upper_t, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, lp::lower_t, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, lp::upper_t, hi_sup, end, fhi_sup);
lra_lp::bound* a1 = atoms[i];
lo_inf1 = next_inf(a1, lra_lp::lower_t, lo_inf, end, flo_inf);
hi_inf1 = next_inf(a1, lra_lp::upper_t, hi_inf, end, fhi_inf);
lo_sup1 = next_sup(a1, lra_lp::lower_t, lo_sup, end, flo_sup);
hi_sup1 = next_sup(a1, lra_lp::upper_t, hi_sup, end, fhi_sup);
if (lo_inf1 != end) lo_inf = lo_inf1;
if (lo_sup1 != end) lo_sup = lo_sup1;
if (hi_inf1 != end) hi_inf = hi_inf1;
@ -1669,24 +1669,24 @@ namespace smt {
}
struct compare_bounds {
bool operator()(lp::bound* a1, lp::bound* a2) const { return a1->get_value() < a2->get_value(); }
bool operator()(lra_lp::bound* a1, lra_lp::bound* a2) const { return a1->get_value() < a2->get_value(); }
};
lp_bounds::iterator first(
lp::bound_kind kind,
lra_lp::bound_kind kind,
iterator it,
iterator end) {
for (; it != end; ++it) {
lp::bound* a = *it;
lra_lp::bound* a = *it;
if (a->get_bound_kind() == kind) return it;
}
return end;
}
lp_bounds::iterator next_inf(
lp::bound* a1,
lp::bound_kind kind,
lra_lp::bound* a1,
lra_lp::bound_kind kind,
iterator it,
iterator end,
bool& found_compatible) {
@ -1694,7 +1694,7 @@ namespace smt {
iterator result = end;
found_compatible = false;
for (; it != end; ++it) {
lp::bound * a2 = *it;
lra_lp::bound * a2 = *it;
if (a1 == a2) continue;
if (a2->get_bound_kind() != kind) continue;
rational const & k2(a2->get_value());
@ -1710,15 +1710,15 @@ namespace smt {
}
lp_bounds::iterator next_sup(
lp::bound* a1,
lp::bound_kind kind,
lra_lp::bound* a1,
lra_lp::bound_kind kind,
iterator it,
iterator end,
bool& found_compatible) {
rational const & k1(a1->get_value());
found_compatible = false;
for (; it != end; ++it) {
lp::bound * a2 = *it;
lra_lp::bound * a2 = *it;
if (a1 == a2) continue;
if (a2->get_bound_kind() != kind) continue;
rational const & k2(a2->get_value());
@ -1732,7 +1732,7 @@ namespace smt {
void propagate_basic_bounds() {
for (auto const& bv : m_to_check) {
lp::bound& b = *m_bool_var2bound.find(bv);
lra_lp::bound& b = *m_bool_var2bound.find(bv);
propagate_bound(bv, ctx().get_assignment(bv) == l_true, b);
if (ctx().inconsistent()) break;
@ -1747,11 +1747,11 @@ namespace smt {
// x <= hi -> x <= hi'
// x <= hi -> ~(x >= hi')
void propagate_bound(bool_var bv, bool is_true, lp::bound& b) {
void propagate_bound(bool_var bv, bool is_true, lra_lp::bound& b) {
if (BP_NONE == propagation_mode()) {
return;
}
lp::bound_kind k = b.get_bound_kind();
lra_lp::bound_kind k = b.get_bound_kind();
theory_var v = b.get_var();
inf_rational val = b.get_value(is_true);
lp_bounds const& bounds = m_bounds[v];
@ -1761,12 +1761,12 @@ namespace smt {
literal lit1(bv, !is_true);
literal lit2 = null_literal;
bool find_glb = (is_true == (k == lp::lower_t));
bool find_glb = (is_true == (k == lra_lp::lower_t));
if (find_glb) {
rational glb;
lp::bound* lb = 0;
lra_lp::bound* lb = 0;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp::bound* b2 = bounds[i];
lra_lp::bound* b2 = bounds[i];
if (b2 == &b) continue;
rational const& val2 = b2->get_value();
if ((is_true ? val2 < val : val2 <= val) && (!lb || glb < val2)) {
@ -1775,14 +1775,14 @@ namespace smt {
}
}
if (!lb) return;
bool sign = lb->get_bound_kind() != lp::lower_t;
bool sign = lb->get_bound_kind() != lra_lp::lower_t;
lit2 = literal(lb->get_bv(), sign);
}
else {
rational lub;
lp::bound* ub = 0;
lra_lp::bound* ub = 0;
for (unsigned i = 0; i < bounds.size(); ++i) {
lp::bound* b2 = bounds[i];
lra_lp::bound* b2 = bounds[i];
if (b2 == &b) continue;
rational const& val2 = b2->get_value();
if ((is_true ? val < val2 : val <= val2) && (!ub || val2 < lub)) {
@ -1791,7 +1791,7 @@ namespace smt {
}
}
if (!ub) return;
bool sign = ub->get_bound_kind() != lp::upper_t;
bool sign = ub->get_bound_kind() != lra_lp::upper_t;
lit2 = literal(ub->get_bv(), sign);
}
TRACE("arith",
@ -1811,27 +1811,27 @@ namespace smt {
++m_stats.m_bounds_propagations;
}
void add_use_lists(lp::bound* b) {
void add_use_lists(lra_lp::bound* b) {
theory_var v = b->get_var();
lean::var_index vi = get_var_index(v);
lp::var_index vi = get_var_index(v);
if (m_solver->is_term(vi)) {
lean::lar_term const& term = m_solver->get_term(vi);
lp::lar_term const& term = m_solver->get_term(vi);
for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) {
lean::var_index wi = i->first;
lp::var_index wi = i->first;
unsigned w = m_var_index2theory_var[wi];
m_use_list.reserve(w + 1, ptr_vector<lp::bound>());
m_use_list.reserve(w + 1, ptr_vector<lra_lp::bound>());
m_use_list[w].push_back(b);
}
}
}
void del_use_lists(lp::bound* b) {
void del_use_lists(lra_lp::bound* b) {
theory_var v = b->get_var();
lean::var_index vi = m_theory_var2var_index[v];
lp::var_index vi = m_theory_var2var_index[v];
if (m_solver->is_term(vi)) {
lean::lar_term const& term = m_solver->get_term(vi);
lp::lar_term const& term = m_solver->get_term(vi);
for (auto i = term.m_coeffs.begin(); i != term.m_coeffs.end(); ++i) {
lean::var_index wi = i->first;
lp::var_index wi = i->first;
unsigned w = m_var_index2theory_var[wi];
SASSERT(m_use_list[w].back() == b);
m_use_list[w].pop_back();
@ -1845,7 +1845,7 @@ namespace smt {
// have been assigned we may know the truth value of the inequality by using simple
// bounds propagation.
//
void propagate_bound_compound(bool_var bv, bool is_true, lp::bound& b) {
void propagate_bound_compound(bool_var bv, bool is_true, lra_lp::bound& b) {
theory_var v = b.get_var();
TRACE("arith", tout << mk_pp(get_owner(v), m) << "\n";);
if (static_cast<unsigned>(v) >= m_use_list.size()) {
@ -1861,7 +1861,7 @@ namespace smt {
// x >= 0, y >= 1 -> x + y >= 1
// x <= 0, y <= 2 -> x + y <= 2
literal lit = null_literal;
if (lp::lower_t == vb->get_bound_kind()) {
if (lra_lp::lower_t == vb->get_bound_kind()) {
if (get_glb(*vb, r) && r >= vb->get_value()) { // vb is assigned true
lit = literal(vb->get_bv(), false);
}
@ -1895,30 +1895,30 @@ namespace smt {
}
}
bool get_lub(lp::bound const& b, inf_rational& lub) {
bool get_lub(lra_lp::bound const& b, inf_rational& lub) {
return get_bound(b, lub, true);
}
bool get_glb(lp::bound const& b, inf_rational& glb) {
bool get_glb(lra_lp::bound const& b, inf_rational& glb) {
return get_bound(b, glb, false);
}
std::ostream& display_bound(std::ostream& out, lp::bound const& b) {
std::ostream& display_bound(std::ostream& out, lra_lp::bound const& b) {
return out << mk_pp(ctx().bool_var2expr(b.get_bv()), m);
}
bool get_bound(lp::bound const& b, inf_rational& r, bool is_lub) {
bool get_bound(lra_lp::bound const& b, inf_rational& r, bool is_lub) {
m_core.reset();
m_eqs.reset();
m_params.reset();
r.reset();
theory_var v = b.get_var();
lean::var_index vi = m_theory_var2var_index[v];
lp::var_index vi = m_theory_var2var_index[v];
SASSERT(m_solver->is_term(vi));
lean::lar_term const& term = m_solver->get_term(vi);
lp::lar_term const& term = m_solver->get_term(vi);
for (auto const coeff : term.m_coeffs) {
lean::var_index wi = coeff.first;
lean::constraint_index ci;
lp::var_index wi = coeff.first;
lp::constraint_index ci;
rational value;
bool is_strict;
if (coeff.second.is_neg() == is_lub) {
@ -1945,24 +1945,24 @@ namespace smt {
return true;
}
void assert_bound(bool_var bv, bool is_true, lp::bound& b) {
if (m_solver->get_status() == lean::lp_status::INFEASIBLE) {
void assert_bound(bool_var bv, bool is_true, lra_lp::bound& b) {
if (m_solver->get_status() == lp::lp_status::INFEASIBLE) {
return;
}
scoped_internalize_state st(*this);
st.vars().push_back(b.get_var());
st.coeffs().push_back(rational::one());
init_left_side(st);
lean::lconstraint_kind k = lean::EQ;
lp::lconstraint_kind k = lp::EQ;
switch (b.get_bound_kind()) {
case lp::lower_t:
k = is_true ? lean::GE : lean::LT;
case lra_lp::lower_t:
k = is_true ? lp::GE : lp::LT;
break;
case lp::upper_t:
k = is_true ? lean::LE : lean::GT;
case lra_lp::upper_t:
k = is_true ? lp::LE : lp::GT;
break;
}
if (k == lean::LT || k == lean::LE) {
if (k == lp::LT || k == lp::LE) {
++m_stats.m_assert_lower;
}
else {
@ -1983,7 +1983,7 @@ namespace smt {
// Then the equality v1 == v2 is propagated to the core.
//
typedef std::pair<lean::constraint_index, rational> constraint_bound;
typedef std::pair<lp::constraint_index, rational> constraint_bound;
vector<constraint_bound> m_lower_terms;
vector<constraint_bound> m_upper_terms;
typedef std::pair<rational, bool> value_sort_pair;
@ -1991,16 +1991,16 @@ namespace smt {
typedef map<value_sort_pair, theory_var, value_sort_pair_hash, default_eq<value_sort_pair> > value2var;
value2var m_fixed_var_table;
void propagate_eqs(lean::var_index vi, lean::constraint_index ci, lean::lconstraint_kind k, lp::bound& b) {
void propagate_eqs(lp::var_index vi, lp::constraint_index ci, lp::lconstraint_kind k, lra_lp::bound& b) {
if (propagate_eqs()) {
rational const& value = b.get_value();
if (k == lean::GE) {
if (k == lp::GE) {
set_lower_bound(vi, ci, value);
if (has_upper_bound(vi, ci, value)) {
fixed_var_eh(b.get_var(), value);
}
}
else if (k == lean::LE) {
else if (k == lp::LE) {
set_upper_bound(vi, ci, value);
if (has_lower_bound(vi, ci, value)) {
fixed_var_eh(b.get_var(), value);
@ -2021,16 +2021,16 @@ namespace smt {
bool use_tableau() const { return lp_params(ctx().get_params()).simplex_strategy() < 2; }
void set_upper_bound(lean::var_index vi, lean::constraint_index ci, rational const& v) { set_bound(vi, ci, v, false); }
void set_upper_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { set_bound(vi, ci, v, false); }
void set_lower_bound(lean::var_index vi, lean::constraint_index ci, rational const& v) { set_bound(vi, ci, v, true); }
void set_lower_bound(lp::var_index vi, lp::constraint_index ci, rational const& v) { set_bound(vi, ci, v, true); }
void set_bound(lean::var_index vi, lean::constraint_index ci, rational const& v, bool is_lower) {
void set_bound(lp::var_index vi, lp::constraint_index ci, rational const& v, bool is_lower) {
if (!m_solver->is_term(vi)) {
// m_solver already tracks bounds on proper variables, but not on terms.
return;
}
lean::var_index ti = m_solver->adjust_term_index(vi);
lp::var_index ti = m_solver->adjust_term_index(vi);
auto& vec = is_lower ? m_lower_terms : m_upper_terms;
if (vec.size() <= ti) {
vec.resize(ti + 1, constraint_bound(UINT_MAX, rational()));
@ -2043,15 +2043,15 @@ namespace smt {
}
}
bool has_upper_bound(lean::var_index vi, lean::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
bool has_upper_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, false); }
bool has_lower_bound(lean::var_index vi, lean::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
bool has_lower_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound) { return has_bound(vi, ci, bound, true); }
bool has_bound(lean::var_index vi, lean::constraint_index& ci, rational const& bound, bool is_lower) {
bool has_bound(lp::var_index vi, lp::constraint_index& ci, rational const& bound, bool is_lower) {
if (m_solver->is_term(vi)) {
lean::var_index ti = m_solver->adjust_term_index(vi);
lp::var_index ti = m_solver->adjust_term_index(vi);
theory_var v = m_term_index2theory_var.get(ti, null_theory_var);
rational val;
TRACE("arith", tout << vi << " " << v << "\n";);
@ -2094,7 +2094,7 @@ namespace smt {
if (static_cast<unsigned>(v2) < th.get_num_vars() && !is_equal(v1, v2)) {
auto vi1 = get_var_index(v1);
auto vi2 = get_var_index(v2);
lean::constraint_index ci1, ci2, ci3, ci4;
lp::constraint_index ci1, ci2, ci3, ci4;
TRACE("arith", tout << "fixed: " << mk_pp(get_owner(v1), m) << " " << mk_pp(get_owner(v2), m) << " " << bound << " " << has_lower_bound(vi2, ci3, bound) << "\n";);
if (has_lower_bound(vi2, ci3, bound) && has_upper_bound(vi2, ci4, bound)) {
VERIFY (has_lower_bound(vi1, ci1, bound));
@ -2148,19 +2148,19 @@ namespace smt {
if (m_solver->A_r().row_count() > m_stats.m_max_rows)
m_stats.m_max_rows = m_solver->A_r().row_count();
TRACE("arith_verbose", display(tout););
lean::lp_status status = m_solver->find_feasible_solution();
lp::lp_status status = m_solver->find_feasible_solution();
m_stats.m_num_iterations = m_solver->settings().st().m_total_iterations;
m_stats.m_num_factorizations = m_solver->settings().st().m_num_factorizations;
m_stats.m_need_to_solve_inf = m_solver->settings().st().m_need_to_solve_inf;
switch (status) {
case lean::lp_status::INFEASIBLE:
case lp::lp_status::INFEASIBLE:
return l_false;
case lean::lp_status::FEASIBLE:
case lean::lp_status::OPTIMAL:
case lp::lp_status::FEASIBLE:
case lp::lp_status::OPTIMAL:
// SASSERT(m_solver->all_constraints_hold());
return l_true;
case lean::lp_status::TIME_EXHAUSTED:
case lp::lp_status::TIME_EXHAUSTED:
default:
TRACE("arith", tout << "status treated as inconclusive: " << status << "\n";);
@ -2170,14 +2170,14 @@ namespace smt {
}
}
vector<std::pair<rational, lean::constraint_index>> m_explanation;
vector<std::pair<rational, lp::constraint_index>> m_explanation;
literal_vector m_core;
svector<enode_pair> m_eqs;
vector<parameter> m_params;
// lean::constraint_index const null_constraint_index = UINT_MAX; // not sure what a correct fix is
// lp::constraint_index const null_constraint_index = UINT_MAX; // not sure what a correct fix is
void set_evidence(lean::constraint_index idx) {
void set_evidence(lp::constraint_index idx) {
if (idx == UINT_MAX) {
return;
}
@ -2327,16 +2327,16 @@ namespace smt {
}
theory_lra::inf_eps value(theory_var v) {
lean::impq ival = get_ivalue(v);
lp::impq ival = get_ivalue(v);
return inf_eps(0, inf_rational(ival.x, ival.y));
}
theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) {
lean::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
vector<std::pair<rational, lean::var_index> > coeffs;
lp::var_index vi = m_theory_var2var_index.get(v, UINT_MAX);
vector<std::pair<rational, lp::var_index> > coeffs;
rational coeff;
if (m_solver->is_term(vi)) {
const lean::lar_term& term = m_solver->get_term(vi);
const lp::lar_term& term = m_solver->get_term(vi);
for (auto & ti : term.m_coeffs) {
coeffs.push_back(std::make_pair(ti.second, ti.first));
}
@ -2346,7 +2346,7 @@ namespace smt {
coeffs.push_back(std::make_pair(rational::one(), vi));
coeff = rational::zero();
}
lean::impq term_max;
lp::impq term_max;
if (m_solver->maximize_term(coeffs, term_max)) {
blocker = mk_gt(v);
inf_rational val(term_max.x + coeff, term_max.y);
@ -2361,7 +2361,7 @@ namespace smt {
}
expr_ref mk_gt(theory_var v) {
lean::impq val = get_ivalue(v);
lp::impq val = get_ivalue(v);
expr* obj = get_enode(v)->get_owner();
rational r = val.x;
expr_ref e(m);
@ -2393,11 +2393,11 @@ namespace smt {
}
app_ref mk_obj(theory_var v) {
lean::var_index vi = m_theory_var2var_index[v];
lp::var_index vi = m_theory_var2var_index[v];
bool is_int = a.is_int(get_enode(v)->get_owner());
if (m_solver->is_term(vi)) {
expr_ref_vector args(m);
const lean::lar_term& term = m_solver->get_term(vi);
const lp::lar_term& term = m_solver->get_term(vi);
for (auto & ti : term.m_coeffs) {
theory_var w = m_var_index2theory_var[ti.first];
expr* o = get_enode(w)->get_owner();
@ -2428,9 +2428,9 @@ namespace smt {
bool_var bv = ctx().mk_bool_var(b);
ctx().set_var_theory(bv, get_id());
// ctx().set_enode_flag(bv, true);
lp::bound_kind bkind = lp::bound_kind::lower_t;
if (is_strict) bkind = lp::bound_kind::upper_t;
lp::bound* a = alloc(lp::bound, bv, v, r, bkind);
lra_lp::bound_kind bkind = lra_lp::bound_kind::lower_t;
if (is_strict) bkind = lra_lp::bound_kind::upper_t;
lra_lp::bound* a = alloc(lra_lp::bound, bv, v, r, bkind);
mk_bound_axioms(*a);
updt_unassigned_bounds(v, +1);
m_bounds[v].push_back(a);
@ -2462,7 +2462,7 @@ namespace smt {
}
}
void display_evidence(std::ostream& out, vector<std::pair<rational, lean::constraint_index>> const& evidence) {
void display_evidence(std::ostream& out, vector<std::pair<rational, lp::constraint_index>> const& evidence) {
for (auto const& ev : evidence) {
expr_ref e(m);
SASSERT(!ev.first.is_zero());