mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

move the indices housekeeping from theory_lra to lar_solver

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-17 11:38:22 -08:00
parent 63e62ec1bb
commit 76e1aeb2bb
7 changed files with 285 additions and 314 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

504
src/smt/theory_lra.cpp
View file

File diff suppressed because it is too large Load diff

7
src/test/lp/lp.cpp
View file

@ -2691,7 +2691,7 @@ void test_term() {
term_ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
term_ls.push_back(std::pair<mpq, var_index>(mpq(1), y));
term_ls.push_back(std::make_pair(mpq(3), one));
var_index z = solver.add_term(term_ls);
var_index z = solver.add_term(term_ls, -1);
vector<std::pair<mpq, var_index>> ls;
ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
@ -2761,7 +2761,6 @@ void test_bound_propagation_one_small_sample1() {
vector<std::pair<mpq, var_index>> coeffs;
coeffs.push_back(std::pair<mpq, var_index>(mpq(1), a));
coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), c));
ls.add_term(coeffs);
coeffs.pop_back();
coeffs.push_back(std::pair<mpq, var_index>(mpq(-1), b));
@ -3507,12 +3506,12 @@ void test_maximize_term() {
vector<std::pair<mpq, var_index>> term_ls;
term_ls.push_back(std::pair<mpq, var_index>(mpq(1), x));
term_ls.push_back(std::pair<mpq, var_index>(mpq(-1), y));
unsigned term_x_min_y = solver.add_term(term_ls);
unsigned term_x_min_y = solver.add_term(term_ls, -1);
term_ls.clear();
term_ls.push_back(std::pair<mpq, var_index>(mpq(2), x));
term_ls.push_back(std::pair<mpq, var_index>(mpq(2), y));
unsigned term_2x_pl_2y = solver.add_term(term_ls);
unsigned term_2x_pl_2y = solver.add_term(term_ls, -1);
solver.add_var_bound(term_x_min_y, LE, zero_of_type<mpq>());
solver.add_var_bound(term_2x_pl_2y, LE, mpq(5));
solver.find_feasible_solution();

5
src/util/lp/hnf_cutter.h
View file

@ -26,7 +26,6 @@ Revision History:
namespace lp {
class hnf_cutter {
var_register m_var_register;
general_matrix m_A;
vector<const lar_term*> m_terms;
vector<bool> m_terms_upper;
@ -35,12 +34,14 @@ class hnf_cutter {
lp_settings & m_settings;
mpq m_abs_max;
bool m_overflow;
var_register m_var_register;
public:
const mpq & abs_max() const { return m_abs_max; }
hnf_cutter(lp_settings & settings) : m_settings(settings),
m_abs_max(zero_of_type<mpq>()) {}
m_abs_max(zero_of_type<mpq>()),
m_var_register(0) {}
unsigned terms_count() const {
return m_terms.size();

16
src/util/lp/lar_solver.cpp
View file

@ -29,9 +29,11 @@ void clear() {lp_assert(false); // not implemented
lar_solver::lar_solver() : m_status(lp_status::UNKNOWN),
m_infeasible_column(-1),
m_terms_start_index(1000000),
m_mpq_lar_core_solver(m_settings, *this),
m_int_solver(nullptr)
m_int_solver(nullptr),
m_terms_start_index(1000000),
m_var_register(0),
m_term_register(m_terms_start_index)
{}
void lar_solver::set_track_pivoted_rows(bool v) {
@ -390,6 +392,7 @@ void lar_solver::pop(unsigned k) {
#endif
delete m_terms[i];
}
m_term_register.shrink(m_term_count);
m_terms.resize(m_term_count);
m_simplex_strategy.pop(k);
m_settings.simplex_strategy() = m_simplex_strategy;
@ -1640,7 +1643,7 @@ void lar_solver::register_new_ext_var_index(unsigned ext_v, bool is_int) {
}
bool lar_solver::external_is_used(unsigned v) const {
return m_var_register.external_is_used(v);
return m_var_register.external_is_used(v) || m_term_register.external_is_used(v);
}
void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) {
@ -1749,12 +1752,14 @@ bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>>
return true;
}
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs) {
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i) {
m_term_register.add_var(ext_i);
lp_assert(all_vars_are_registered(coeffs));
if (strategy_is_undecided())
return add_term_undecided(coeffs);
push_and_register_term(new lar_term(coeffs));
SASSERT(m_term_register.size() == m_terms.size());
unsigned adjusted_term_index = m_terms.size() - 1;
var_index ret = m_terms_start_index + adjusted_term_index;
if (use_tableau() && !coeffs.empty()) {
@ -1766,6 +1771,7 @@ var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>> & coeffs)
return ret;
}
void lar_solver::add_row_from_term_no_constraint(const lar_term * term, unsigned term_ext_index) {
TRACE("dump_terms", print_term(*term, tout) << std::endl;);
register_new_ext_var_index(term_ext_index, term_is_int(term));
@ -1866,7 +1872,7 @@ void lar_solver::add_var_bound_on_constraint_for_term(var_index j, lconstraint_k
constraint_index lar_solver::add_constraint(const vector<std::pair<mpq, var_index>>& left_side_with_terms, lconstraint_kind kind_par, const mpq& right_side_parm) {
vector<std::pair<mpq, var_index>> left_side;
substitute_terms_in_linear_expression(left_side_with_terms, left_side);
unsigned term_index = add_term(left_side);
unsigned term_index = add_term(left_side, -1);
constraint_index ci = m_constraints.size();
add_var_bound_on_constraint_for_term(term_index, kind_par, right_side_parm, ci);
return ci;

35
src/util/lp/lar_solver.h
View file

@ -91,7 +91,15 @@ class lar_solver : public column_namer {
lp_settings m_settings;
lp_status m_status;
stacked_value<simplex_strategy_enum> m_simplex_strategy;
stacked_value<int> m_infeasible_column; // such can be found at the initialization step
public:
lar_core_solver m_mpq_lar_core_solver;
private:
int_solver * m_int_solver;
public:
const var_index m_terms_start_index;
var_register m_var_register;
var_register m_term_register;
stacked_vector<ul_pair> m_columns_to_ul_pairs;
vector<lar_base_constraint*> m_constraints;
stacked_value<unsigned> m_constraint_count;
@ -105,14 +113,8 @@ class lar_solver : public column_namer {
stacked_value<int> m_infeasible_column_index; // such can be found at the initialization step
stacked_value<unsigned> m_term_count;
vector<lar_term*> m_terms;
const var_index m_terms_start_index;
indexed_vector<mpq> m_column_buffer;
public:
lar_core_solver m_mpq_lar_core_solver;
private:
int_solver * m_int_solver;
public :
unsigned terms_start_index() const { return m_terms_start_index; }
const vector<lar_term*> & terms() const { return m_terms; }
lar_term const& term(unsigned i) const { return *m_terms[i]; }
@ -182,7 +184,7 @@ public:
// terms
bool all_vars_are_registered(const vector<std::pair<mpq, var_index>> & coeffs);
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs);
var_index add_term(const vector<std::pair<mpq, var_index>> & coeffs, unsigned ext_i);
var_index add_term_undecided(const vector<std::pair<mpq, var_index>> & coeffs);
@ -273,15 +275,21 @@ public:
unsigned map_term_index_to_column_index(unsigned j) const;
var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); }
var_index local_to_external(var_index idx) const { return is_term(idx)?
m_term_register.local_to_external(idx) : m_var_register.local_to_external(idx); }
unsigned number_of_vars() const { return m_var_register.size(); }
var_index external2local(unsigned j) const {
var_index external_to_local(unsigned j) const {
var_index local_j;
lp_assert(m_var_register.external_is_used(j, local_j));
m_var_register.external_is_used(j, local_j);
return local_j;
if (
m_var_register.external_is_used(j, local_j) ||
m_term_register.external_is_used(j, local_j))
{
return local_j;
}
else
return -1;
}
bool column_has_upper_bound(unsigned j) const {
@ -603,6 +611,7 @@ public:
}
bool has_int_var() const;
bool has_inf_int() const {
for (unsigned j = 0; j < column_count(); j++) {
if (column_is_int(j) && ! column_value_is_int(j))

7
src/util/lp/nla_solver.cpp
View file

@ -260,6 +260,7 @@ struct solver::imp {
// return true iff the monomial value is equal to the product of the values of the factors
bool check_monomial(const monomial& m) const {
SASSERT(m_lar_solver.get_column_value(m.var()).is_int());
TRACE("nla_solver", tout << "m = "; print_monomial_with_vars(m, tout););
return product_value(m) == m_lar_solver.get_column_value_rational(m.var());
}
@ -1664,7 +1665,7 @@ struct solver::imp {
unsigned ti = i + s.terms_start_index();
if (!s.term_is_used_as_row(ti))
continue;
lpvar j = s.external2local(ti);
lpvar j = s.external_to_local(ti);
if (var_is_fixed_to_zero(j)) {
TRACE("nla_solver", tout << "term = "; s.print_term(*s.terms()[i], tout););
add_equivalence_maybe(s.terms()[i], s.get_column_upper_bound_witness(j), s.get_column_lower_bound_witness(j));
@ -3347,7 +3348,7 @@ void solver::test_order_lemma_params(bool var_equiv, int sign) {
lp::lar_term t;
t.add_var(lp_k);
t.add_coeff_var(-rational(1), lp_j);
lpvar kj = s.add_term(t.coeffs_as_vector());
lpvar kj = s.add_term(t.coeffs_as_vector(), -1);
s.add_var_bound(kj, llc::LE, rational(0));
s.add_var_bound(kj, llc::GE, rational(0));
}
@ -3548,7 +3549,7 @@ void solver::test_tangent_lemma_equiv() {
lp::lar_term t;
t.add_var(lp_k);
t.add_var(lp_a);
lpvar kj = s.add_term(t.coeffs_as_vector());
lpvar kj = s.add_term(t.coeffs_as_vector(), -1);
s.add_var_bound(kj, llc::LE, rational(0));
s.add_var_bound(kj, llc::GE, rational(0));
s.set_column_value(lp_a, - s.get_column_value(lp_k));

25
src/util/lp/var_register.h
View file

@ -19,7 +19,7 @@ Revision History:
#pragma once
namespace lp {
class ext_var_info {
unsigned m_external_j; // the internal index
unsigned m_external_j;
bool m_is_integer;
std::string m_name;
public:
@ -37,9 +37,9 @@ public:
class var_register {
svector<ext_var_info> m_local_to_external;
std::unordered_map<unsigned, unsigned> m_external_to_local;
unsigned m_local_offset;
public:
var_register(unsigned offset) : m_local_offset(offset) {}
unsigned add_var(unsigned user_var) {
return add_var(user_var, true);
@ -60,7 +60,7 @@ public:
}
m_local_to_external.push_back(ext_var_info(user_var, is_int));
return m_external_to_local[user_var] = size() - 1;
return m_external_to_local[user_var] = size() - 1 + m_local_offset;
}
svector<unsigned> vars() const {
@ -72,7 +72,8 @@ public:
}
unsigned local_to_external(unsigned local_var) const {
return m_local_to_external[local_var].external_j();
SASSERT(local_var >= m_local_offset);
return m_local_to_external[local_var - m_local_offset].external_j();
}
unsigned size() const {
return m_local_to_external.size();
@ -95,24 +96,30 @@ public:
bool external_is_used(unsigned ext_j, unsigned & local_j ) const {
auto it = m_external_to_local.find(ext_j);
if ( it == m_external_to_local.end())
if ( it == m_external_to_local.end()) {
local_j = -1;
return false;
}
local_j = it->second;
return true;
}
bool external_is_used(unsigned ext_j, unsigned & local_j, bool & is_int ) const {
auto it = m_external_to_local.find(ext_j);
if ( it == m_external_to_local.end())
if ( it == m_external_to_local.end()){
local_j = -1;
return false;
}
local_j = it->second;
is_int = m_local_to_external[local_j].is_integer();
SASSERT(local_j >= m_local_offset);
is_int = m_local_to_external[local_j - m_local_offset].is_integer();
return true;
}
bool local_is_int(unsigned j) const {
return m_local_to_external[j].is_integer();
SASSERT(j >= m_local_offset);
return m_local_to_external[j - m_local_offset].is_integer();
}
void shrink(unsigned shrunk_size) {