mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

change the return type of ival.var() to tv

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-25 16:02:36 -07:00
parent 119a491b17
commit f5b62015fc
10 changed files with 57 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -109,7 +109,7 @@ public:
auto & row = m_data[adjust_row(i)];
lp_assert(row_is_initialized_correctly(row));
for (const auto & p : c) {
unsigned j = adjust_column(column_fix(p.var()));
unsigned j = adjust_column(column_fix(p.var().index()));
row[j] = sign * p.coeff();
}
}

4
src/math/lp/gomory.cpp
View file

@ -191,7 +191,7 @@ class create_cut {
void dump_coeff(std::ostream & out, const T& c) const {
out << "( * ";
dump_coeff_val(out, c.coeff());
out << " " << var_name(c.var()) << ")";
out << " " << var_name(c.var().index()) << ")";
}
std::ostream& dump_row_coefficients(std::ostream & out) const {
@ -221,7 +221,7 @@ class create_cut {
dump_declaration(out, p.var());
}
for (const auto& p : m_t) {
unsigned v = p.var();
unsigned v = p.var().index();
if (lp::tv::is_term(v)) {
dump_declaration(out, v);
}

2
src/math/lp/hnf_cutter.cpp
View file

@ -50,7 +50,7 @@ namespace lp {
m_constraints_for_explanation.push_back(ci);
for (const auto &p : *t) {
m_var_register.add_var(p.var(), true); // hnf only deals with integral variables for now
m_var_register.add_var(p.var().index(), true); // hnf only deals with integral variables for now
mpq t = abs(ceil(p.coeff()));
if (t > m_abs_max)
m_abs_max = t;

4
src/math/lp/int_cube.cpp
View file

@ -86,7 +86,7 @@ namespace lp {
bool seen_minus = false;
bool seen_plus = false;
for(const auto & p : t) {
if (!lia.column_is_int(p.var()))
if (!lia.column_is_int(p.var().index()))
goto usual_delta;
const mpq & c = p.coeff();
if (c == one_of_type<mpq>()) {
@ -104,7 +104,7 @@ namespace lp {
usual_delta:
mpq delta = zero_of_type<mpq>();
for (const auto & p : t)
if (lia.column_is_int(p.var()))
if (lia.column_is_int(p.var().index()))
delta += abs(p.coeff());
delta *= mpq(1, 2);

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

@ -115,13 +115,13 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
} else {
lar_term & t = *m_terms[tv::unmask_term(be.m_j)];
auto first_coeff = t.begin();
unsigned j = (*first_coeff).var();
unsigned j = (*first_coeff).var().index();
auto it = coeff_map.find(j);
if (it == coeff_map.end())
return false;
mpq ratio = it->second / (*first_coeff).coeff();
for (auto p : t) {
it = coeff_map.find(p.var());
it = coeff_map.find(p.var().index());
if (it == coeff_map.end())
return false;
if (p.coeff() * ratio != it->second)
@ -421,7 +421,7 @@ void lar_solver::set_costs_to_zero(const lar_term& term) {
lp_assert(jset.is_empty());
for (const auto & p : term) {
unsigned j = p.var();
unsigned j = p.var().index();
rslv.m_costs[j] = zero_of_type<mpq>();
int i = rslv.m_basis_heading[j];
if (i < 0)
@ -452,7 +452,7 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
lp_assert(reduced_costs_are_zeroes_for_r_solver());
rslv.m_costs.resize(A_r().column_count(), zero_of_type<mpq>());
for (const auto & p : term) {
unsigned j = p.var();
unsigned j = p.var().index();
rslv.m_costs[j] = p.coeff();
if (rslv.m_basis_heading[j] < 0)
rslv.m_d[j] += p.coeff();
@ -679,7 +679,7 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
const lar_term & term = * m_terms[tv::unmask_term(t.second)];
for (auto p : term){
register_monoid_in_map(coeffs, t.first * p.coeff() , p.var());
register_monoid_in_map(coeffs, t.first * p.coeff() , p.var().index());
}
}
}
@ -915,7 +915,7 @@ void lar_solver::fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A,
lp_assert(A.m_rows[last_row].size() == 0);
for (auto t : *ls) {
lp_assert(!is_zero(t.coeff()));
var_index j = t.var();
var_index j = t.var().index();
A.set(last_row, j, - t.coeff());
}
unsigned basis_j = A.column_count() - 1;
@ -1145,7 +1145,7 @@ bool lar_solver::has_value(var_index var, mpq& value) const {
lar_term const& t = get_term(var);
value = 0;
for (auto const& cv : t) {
impq const& r = get_column_value(cv.var());
impq const& r = get_column_value(cv.var().index());
if (!numeric_traits<mpq>::is_zero(r.y)) return false;
value += r.x * cv.coeff();
}
@ -1304,7 +1304,7 @@ std::ostream& lar_solver::print_term(lar_term const& term, std::ostream & out) c
out << " - ";
else if (val != numeric_traits<mpq>::one())
out << T_to_string(val);
out << this->get_variable_name(p.var());
out << this->get_variable_name(p.var().index());
}
return out;
}
@ -1331,7 +1331,7 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v
var_index var = vars[i];
if (tv::is_term(var)) { // handle the term
for (auto it : *m_terms[tv::unmask_term(var)]) {
column_list.push_back(it.var());
column_list.push_back(it.var().index());
}
} else {
column_list.push_back(var);
@ -1527,7 +1527,7 @@ bool lar_solver::model_is_int_feasible() const {
bool lar_solver::term_is_int(const lar_term * t) const {
for (auto const p : *t)
if (! (column_is_int(p.var()) && p.coeff().is_int()))
if (! (column_is_int(p.var().index()) && p.coeff().is_int()))
return false;
return true;
}
@ -1938,7 +1938,7 @@ void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const l
for (auto t : *ls) {
lp_assert(!is_zero(t.coeff()));
var_index j = t.var();
var_index j = t.var().index();
A.set(last_row, j, -t.coeff().get_double());
}
@ -2239,7 +2239,7 @@ void lar_solver::fix_terms_with_rounded_columns() {
bool need_to_fix = false;
const lar_term & t = *m_terms[i];
for (const auto & p : t) {
if (m_incorrect_columns.contains(p.var())) {
if (m_incorrect_columns.contains(p.var().index())) {
need_to_fix = true;
break;
}
@ -2256,7 +2256,7 @@ void lar_solver::fix_terms_with_rounded_columns() {
bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
val = zero_of_type<mpq>();
for (const auto & c : t) {
const auto & x = m_mpq_lar_core_solver.m_r_x[c.var()];
const auto & x = m_mpq_lar_core_solver.m_r_x[c.var().index()];
if (!is_zero(x.y))
return false;
val += x.x * c.coeff();

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

@ -59,7 +59,7 @@ class lar_solver : public column_namer {
size_t seed = 0;
int i = 0;
for (const auto p : t) {
hash_combine(seed, p.var());
hash_combine(seed, p.var().index());
hash_combine(seed, p.coeff());
if (i++ > 10)
break;
@ -578,9 +578,9 @@ public:
void subs_term_columns(lar_term& t) {
vector<std::pair<unsigned,unsigned>> columns_to_subs;
for (const auto & m : t) {
unsigned tj = adjust_column_index_to_term_index(m.var());
if (tj == m.var()) continue;
columns_to_subs.push_back(std::make_pair(m.var(), tj));
unsigned tj = adjust_column_index_to_term_index(m.var().index());
if (tj == m.var().index()) continue;
columns_to_subs.push_back(std::make_pair(m.var().index(), tj));
}
for (const auto & p : columns_to_subs) {
t.subst_index(p.first, p.second);

9
src/math/lp/lar_term.h
View file

@ -123,7 +123,8 @@ public:
const mpq & m_coeff;
public:
ival(unsigned var, const mpq & val) : m_var(var), m_coeff(val) { }
unsigned var() const { return m_var; }
unsigned raw() const { return m_var; }
tv var() const { return tv::raw(m_var); }
const mpq & coeff() const { return m_coeff; }
};
@ -142,13 +143,13 @@ public:
lpvar min_var = -1;
mpq c;
for (const auto & p : *this) {
if (p.var() < min_var) {
min_var = p.var();
if (p.var().index() < min_var) {
min_var = p.var().index();
}
}
lar_term r;
for (const auto & p : *this) {
if (p.var() == min_var) {
if (p.var().index() == min_var) {
return p.coeff().is_one();
}
}

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

@ -50,7 +50,7 @@ bool core::compare_holds(const rational& ls, llc cmp, const rational& rs) const
rational core::value(const lp::lar_term& r) const {
rational ret(0);
for (const auto & t : r) {
ret += t.coeff() * val(t.var());
ret += t.coeff() * val(t.var().index());
}
return ret;
}
@ -58,7 +58,7 @@ rational core::value(const lp::lar_term& r) const {
lp::lar_term core::subs_terms_to_columns(const lp::lar_term& t) const {
lp::lar_term r;
for (const auto& p : t) {
lpvar j = p.var();
lpvar j = p.var().index();
if (lp::tv::is_term(j))
j = m_lar_solver.map_term_index_to_column_index(j);
r.add_monomial(p.coeff(), j);
@ -323,25 +323,25 @@ bool core:: explain_coeff_lower_bound(const lp::lar_term::ival& p, rational& bou
SASSERT(!a.is_zero());
unsigned c; // the index for the lower or the upper bound
if (a.is_pos()) {
unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var());
unsigned c = m_lar_solver.get_column_lower_bound_witness(p.var().index());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_lower_bound(p.var()).x;
bound = a * m_lar_solver.get_lower_bound(p.var().index()).x;
e.add(c);
return true;
}
// a.is_neg()
c = m_lar_solver.get_column_upper_bound_witness(p.var());
c = m_lar_solver.get_column_upper_bound_witness(p.var().index());
if (c + 1 == 0)
return false;
bound = a * m_lar_solver.get_upper_bound(p.var()).x;
bound = a * m_lar_solver.get_upper_bound(p.var().index()).x;
e.add(c);
return true;
}
bool core::explain_coeff_upper_bound(const lp::lar_term::ival& p, rational& bound, lp::explanation& e) const {
const rational& a = p.coeff();
lpvar j = lp::tv::is_term(p.var())? m_lar_solver.map_term_index_to_column_index(p.var()) : p.var();
lpvar j = p.var().is_term()? m_lar_solver.map_term_index_to_column_index(p.var().index()) : p.var().index();
SASSERT(!a.is_zero());
unsigned c; // the index for the lower or the upper bound
if (a.is_neg()) {
@ -681,7 +681,7 @@ std::ostream & core::print_ineqs(const lemma& l, std::ostream & out) const {
print_ineq(in, out);
if (i + 1 < l.ineqs().size()) out << " or ";
for (const auto & p: in.m_term)
vars.insert(p.var());
vars.insert(p.var().index());
}
out << std::endl;
for (lpvar j : vars) {
@ -864,9 +864,9 @@ bool core:: is_octagon_term(const lp::lar_term& t, bool & sign, lpvar& i, lpvar
return false;
}
if (i == static_cast<lpvar>(-1))
i = p.var();
i = p.var().index();
else
j = p.var();
j = p.var().index();
}
SASSERT(j != static_cast<unsigned>(-1));
sign = (seen_minus && seen_plus)? false : true;
@ -986,7 +986,7 @@ std::unordered_set<lpvar> core::collect_vars(const lemma& l) const {
for (const auto& i : current_lemma().ineqs()) {
for (const auto& p : i.term()) {
insert_j(p.var());
insert_j(p.var().index());
}
}
for (const auto& p : current_expl()) {
@ -1628,9 +1628,9 @@ std::unordered_set<lpvar> core::get_vars_of_expr_with_opening_terms(const nex *e
if (ls.column_corresponds_to_term(j)) {
const auto& t = m_lar_solver.get_term(ls.local_to_external(j));
for (auto p : t) {
if (ret.find(p.var()) == ret.end()) {
added.push_back(p.var());
ret.insert(p.var());
if (ret.find(p.var().index()) == ret.end()) {
added.push_back(p.var().index());
ret.insert(p.var().index());
}
}
}

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

@ -357,14 +357,14 @@ public:
// we use the form -it + 1 = 0
m_work_vector.set_value(one_of_type<T>(), bj);
for (auto p : row) {
m_work_vector.set_value(-p.coeff(), p.var());
m_work_vector.set_value(-p.coeff(), p.var().index());
// but take care of the basis 1 later
}
// now iterate with pivoting
fill_last_row_with_pivoting_loop_block(bj, basis_heading);
for (auto p : row) {
fill_last_row_with_pivoting_loop_block(p.var(), basis_heading);
fill_last_row_with_pivoting_loop_block(p.var().index(), basis_heading);
}
lp_assert(m_work_vector.is_OK());
unsigned last_row = row_count() - 1;

26
src/smt/theory_lra.cpp
View file

@ -1503,7 +1503,7 @@ public:
if (lp::tv::is_term(vi)) {
const lp::lar_term& term = lp().get_term(vi);
for (const auto & i: term) {
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
m_todo_terms.push_back(std::make_pair(i.var().index(), coeff * i.coeff()));
}
}
else {
@ -1535,11 +1535,11 @@ public:
if (lp::tv::is_term(wi)) {
const lp::lar_term& term = lp().get_term(wi);
for (const auto & i : term) {
if (m_variable_values.count(i.var()) > 0) {
result += m_variable_values[i.var()] * coeff * i.coeff();
if (m_variable_values.count(i.var().index()) > 0) {
result += m_variable_values[i.var().index()] * coeff * i.coeff();
}
else {
m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff()));
m_todo_terms.push_back(std::make_pair(i.var().index(), coeff * i.coeff()));
}
}
}
@ -1931,7 +1931,7 @@ public:
expr_ref t(m);
expr_ref_vector ts(m);
for (auto const& p : term) {
lpvar wi = p.var();
lpvar wi = p.var().index();
if (lp::tv::is_term(wi)) {
ts.push_back(multerm(p.coeff(), term2expr(lp().get_term(wi))));
}
@ -1973,7 +1973,7 @@ public:
lp().print_term(term, out << "bound: ");
out << (upper?" <= ":" >= ") << k << "\n";
for (auto const& p : term) {
lpvar wi = p.var();
lpvar wi = p.var().index();
out << p.coeff() << " * ";
if (lp::tv::is_term(wi)) {
lp().print_term(lp().get_term(wi), out) << "\n";
@ -2771,7 +2771,7 @@ public:
m_todo_vars.pop_back();
lp::lar_term const& term = lp().get_term(vi);
for (auto const& p : term) {
lpvar wi = p.var();
lpvar wi = p.var().index();
if (lp::tv::is_term(wi)) {
m_todo_vars.push_back(wi);
}
@ -2796,7 +2796,7 @@ public:
m_todo_vars.pop_back();
lp::lar_term const& term = lp().get_term(vi);
for (auto const& coeff : term) {
lpvar wi = coeff.var();
lpvar wi = coeff.var().index();
if (lp::tv::is_term(wi)) {
m_todo_vars.push_back(wi);
}
@ -2886,7 +2886,7 @@ public:
SASSERT(lp::tv::is_term(vi));
lp::lar_term const& term = m_solver->get_term(vi);
for (auto const mono : term) {
lp::var_index wi = mono.var();
lp::var_index wi = mono.var().index();
lp::constraint_index ci;
rational value;
bool is_strict;
@ -3349,7 +3349,7 @@ public:
m_nra->am().set(r1, c1.to_mpq());
m_nra->am().add(r, r1, r);
for (auto const & arg : term) {
lpvar wi = arg.var();
lpvar wi = arg.var().index();
c1 = arg.coeff() * wcoeff;
if (lp::tv::is_term(wi)) {
m_todo_terms.push_back(std::make_pair(wi, c1));
@ -3621,16 +3621,16 @@ public:
void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff) {
for (const auto & ti : term) {
theory_var w;
if (lp::tv::is_term(ti.var())) {
if (ti.var().is_term()) {
//w = m_term_index2theory_var.get(lp::tv::unmask_term(ti.m_key), null_theory_var);
//if (w == null_theory_var) // if extracting expressions directly from nested term
lp::lar_term const& term1 = lp().get_term(ti.var());
lp::lar_term const& term1 = lp().get_term(ti.var().index());
rational coeff2 = coeff * ti.coeff();
term2coeffs(term1, coeffs, coeff2);
continue;
}
else {
w = lp().local_to_external(ti.var());
w = lp().local_to_external(ti.var().index());
}
rational c0(0);
coeffs.find(w, c0);