mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

use u_map in lar_term

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-12-30 17:58:56 -08:00 • committed by Nikolaj Bjorner
parent f5c7b9fb2f
commit 1fff7bb51d
5 changed files with 70 additions and 60 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -128,18 +128,18 @@ bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be,
}
rs_of_evidence /= ratio;
} else {
const lar_term * t = m_terms[adjust_term_index(be.m_j)];
const auto first_coeff = *t->m_coeffs.begin();
unsigned j = first_coeff.first;
lar_term & t = *m_terms[adjust_term_index(be.m_j)];
auto first_coeff = t.begin();
unsigned j = (*first_coeff).var();
auto it = coeff_map.find(j);
if (it == coeff_map.end())
return false;
mpq ratio = it->second / first_coeff.second;
for (auto & p : t->m_coeffs) {
it = coeff_map.find(p.first);
mpq ratio = it->second / (*first_coeff).coeff();
for (auto p : t) {
it = coeff_map.find(p.var());
if (it == coeff_map.end())
return false;
if (p.second * ratio != it->second)
if (p.coeff() * ratio != it->second)
return false;
}
if (ratio < zero_of_type<mpq>()) {
@ -686,8 +686,8 @@ void lar_solver::substitute_terms_in_linear_expression(const vector<std::pair<mp
register_monoid_in_map(coeffs, t.first, j);
} else {
const lar_term & term = * m_terms[adjust_term_index(t.second)];
for (auto & p : term.coeffs()){
register_monoid_in_map(coeffs, t.first * p.second , p.first);
for (auto p : term){
register_monoid_in_map(coeffs, t.first * p.coeff() , p.var());
}
}
}
@ -943,10 +943,10 @@ void lar_solver::fill_last_row_of_A_r(static_matrix<mpq, numeric_pair<mpq>> & A,
lp_assert(A.column_count() > 0);
unsigned last_row = A.row_count() - 1;
lp_assert(A.m_rows[last_row].size() == 0);
for (auto & t : ls->m_coeffs) {
lp_assert(!is_zero(t.second));
var_index j = t.first;
A.set(last_row, j, - t.second);
for (auto t : *ls) {
lp_assert(!is_zero(t.coeff()));
var_index j = t.var();
A.set(last_row, j, - t.coeff());
}
unsigned basis_j = A.column_count() - 1;
A.set(last_row, basis_j, mpq(1));
@ -1364,8 +1364,8 @@ void lar_solver::fill_var_set_for_random_update(unsigned sz, var_index const * v
for (unsigned i = 0; i < sz; i++) {
var_index var = vars[i];
if (var >= m_terms_start_index) { // handle the term
for (auto & it : m_terms[var - m_terms_start_index]->m_coeffs) {
column_list.push_back(it.first);
for (auto it : *m_terms[var - m_terms_start_index]) {
column_list.push_back(it.var());
}
} else {
column_list.push_back(var);
@ -1560,8 +1560,8 @@ bool lar_solver::model_is_int_feasible() const {
}
bool lar_solver::term_is_int(const lar_term * t) const {
for (auto const & p : t->m_coeffs)
if (! (column_is_int(p.first) && p.second.is_int()))
for (auto const p : *t)
if (! (column_is_int(p.var()) && p.coeff().is_int()))
return false;
return true;
}
@ -1920,10 +1920,10 @@ void lar_solver::fill_last_row_of_A_d(static_matrix<double, double> & A, const l
unsigned last_row = A.row_count() - 1;
lp_assert(A.m_rows[last_row].empty());
for (auto & t : ls->m_coeffs) {
lp_assert(!is_zero(t.second));
var_index j = t.first;
A.set(last_row, j, -t.second.get_double());
for (auto t : *ls) {
lp_assert(!is_zero(t.coeff()));
var_index j = t.var();
A.set(last_row, j, -t.coeff().get_double());
}
unsigned basis_j = A.column_count() - 1;

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

@ -545,17 +545,13 @@ public:
void subs_term_columns(lar_term& t) {
vector<std::pair<unsigned,unsigned>> columns_to_subs;
for (const auto & m : t.m_coeffs) {
unsigned tj = adjust_column_index_to_term_index(m.first);
if (tj == m.first) continue;
columns_to_subs.push_back(std::make_pair(m.first, tj));
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));
}
for (const auto & p : columns_to_subs) {
auto it = t.m_coeffs.find(p.first);
lp_assert(it != t.m_coeffs.end());
mpq v = it->second;
t.m_coeffs.erase(it);
t.m_coeffs[p.second] = v;
t.subst_index(p.first, p.second);
}
}

58
src/util/lp/lar_term.h
View file

@ -19,20 +19,23 @@
--*/
#pragma once
#include "util/lp/indexed_vector.h"
#include "util/map.h"
namespace lp {
struct lar_term {
class lar_term {
// the term evaluates to sum of m_coeffs
std::unordered_map<unsigned, mpq> m_coeffs;
u_map<mpq> m_coeffs;
// mpq m_v;
public:
lar_term() {}
void add_monomial(const mpq& c, unsigned j) {
auto it = m_coeffs.find(j);
if (it == m_coeffs.end()) {
m_coeffs.emplace(j, c);
auto *e = m_coeffs.find_core(j);
if (e == nullptr) {
m_coeffs.insert(j, c);
} else {
it->second += c;
if (is_zero(it->second))
m_coeffs.erase(it);
e->get_data().m_value += c;
if (e->get_data().m_value.is_zero())
m_coeffs.erase(j);
}
}
@ -41,8 +44,9 @@ struct lar_term {
}
unsigned size() const { return static_cast<unsigned>(m_coeffs.size()); }
const std::unordered_map<unsigned, mpq> & coeffs() const {
template <typename T>
const T & coeffs() const {
return m_coeffs;
}
@ -59,42 +63,51 @@ struct lar_term {
vector<std::pair<mpq, unsigned>> coeffs_as_vector() const {
vector<std::pair<mpq, unsigned>> ret;
for (const auto & p : m_coeffs) {
ret.push_back(std::make_pair(p.second, p.first));
ret.push_back(std::make_pair(p.m_value, p.m_key));
}
return ret;
}
// j is the basic variable to substitute
void subst(unsigned j, indexed_vector<mpq> & li) {
auto it = m_coeffs.find(j);
if (it == m_coeffs.end()) return;
const mpq & b = it->second;
auto* it = m_coeffs.find_core(j);
if (it == nullptr) return;
const mpq & b = it->get_data().m_value;
for (unsigned it_j :li.m_index) {
add_monomial(- b * li.m_data[it_j], it_j);
}
m_coeffs.erase(it);
m_coeffs.erase(j);
}
// the monomial ax[j] is substituted by ax[k]
void subst_index(unsigned j, unsigned k) {
auto* it = m_coeffs.find_core(j);
if (it == nullptr) return;
mpq b = it->get_data().m_value;
m_coeffs.erase(j);
m_coeffs.insert(k, b);
}
bool contains(unsigned j) const {
return m_coeffs.find(j) != m_coeffs.end();
return m_coeffs.contains(j);
}
void negate() {
for (auto & t : m_coeffs)
t.second.neg();
t.m_value.neg();
}
template <typename T>
T apply(const vector<T>& x) const {
T ret(0);
for (const auto & t : m_coeffs) {
ret += t.second * x[t.first];
ret += t.m_value * x[t.m_key];
}
return ret;
}
void clear() {
m_coeffs.clear();
m_coeffs.reset();
}
struct ival {
@ -108,7 +121,7 @@ struct lar_term {
struct const_iterator {
//fields
std::unordered_map<unsigned, mpq>::const_iterator m_it;
u_map< mpq>::iterator m_it;
typedef const_iterator self_type;
typedef ival value_type;
@ -118,19 +131,20 @@ struct lar_term {
typedef std::forward_iterator_tag iterator_category;
reference operator*() const {
return ival(m_it->first, m_it->second);
return ival(m_it->m_key, m_it->m_value);
}
self_type operator++() { self_type i = *this; m_it++; return i; }
self_type operator++(int) { m_it++; return *this; }
const_iterator(std::unordered_map<unsigned, mpq>::const_iterator it) : m_it(it) {}
const_iterator(u_map<mpq>::iterator it) : m_it(it) {}
bool operator==(const self_type &other) const {
return m_it == other.m_it;
}
bool operator!=(const self_type &other) const { return !(*this == other); }
};
const_iterator begin() const { return m_coeffs.begin();}
const_iterator end() const { return m_coeffs.end(); }
};