mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
introdure lar_term.ext_coeffs(), dio passes some tests
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson
Lev Nachmanson
parent
083926c658
commit
9a9ccf19c5
2 changed files with 117 additions and 33 deletions
|
|
@ -174,8 +174,6 @@ namespace lp {
|
|||
else if (val != numeric_traits<mpq>::one())
|
||||
out << T_to_string(val);
|
||||
out << "x";
|
||||
if (is_fresh_var(j))
|
||||
out << "~";
|
||||
out << j;
|
||||
}
|
||||
|
||||
|
|
@ -374,7 +372,7 @@ namespace lp {
|
|||
|
||||
void register_columns_to_term(const lar_term& t) {
|
||||
TRACE("dioph_eq", tout << "register term:"; lra.print_term(t, tout););
|
||||
for (const auto &p: t) {
|
||||
for (const auto &p: t.ext_coeffs()) {
|
||||
auto it = m_columns_to_terms.find(p.var());
|
||||
if (it != m_columns_to_terms.end()) {
|
||||
it->second.insert(t.j());
|
||||
|
|
@ -405,7 +403,7 @@ namespace lp {
|
|||
m_e_matrix.add_row();
|
||||
SASSERT(m_e_matrix.row_count() == m_entries.size());
|
||||
|
||||
for (const auto& p : t) {
|
||||
for (const auto& p : t.ext_coeffs()) {
|
||||
SASSERT(p.coeff().is_int());
|
||||
if (is_fixed(p.var()))
|
||||
e.m_c += p.coeff() * lia.lower_bound(p.var()).x;
|
||||
|
|
@ -415,13 +413,6 @@ namespace lp {
|
|||
m_e_matrix.add_new_element(entry_index, lj, p.coeff());
|
||||
}
|
||||
}
|
||||
if (is_fixed(t.j())) {
|
||||
e.m_c -= lia.lower_bound(t.j()).x;
|
||||
} else {
|
||||
unsigned lj = add_var(t.j());
|
||||
m_e_matrix.add_columns_up_to(lj);
|
||||
m_e_matrix.add_new_element(entry_index, lj, -mpq(1));
|
||||
}
|
||||
SASSERT(entry_invariant(entry_index));
|
||||
}
|
||||
|
||||
|
|
@ -866,7 +857,7 @@ namespace lp {
|
|||
print_lar_term_L(term_to_tighten, tout) << std::endl;
|
||||
tout << "m_tmp_l:"; print_lar_term_L(m_tmp_l, tout) << std::endl;
|
||||
tout << "open_ml:";
|
||||
print_term_o(open_ml(m_tmp_l), tout) << std::endl;
|
||||
print_lar_term_L(open_ml(m_tmp_l), tout) << std::endl;
|
||||
tout << "term_to_tighten + open_ml:";
|
||||
print_term_o(term_to_tighten + open_ml(m_tmp_l), tout)
|
||||
<< std::endl;
|
||||
|
|
@ -1307,7 +1298,7 @@ namespace lp {
|
|||
for (unsigned k = 0; k < lra.terms().size(); k ++ ) {
|
||||
const lar_term* t = lra.terms()[k];
|
||||
if (!all_vars_are_int(*t)) continue;
|
||||
for (const auto& p: *t) {
|
||||
for (const auto& p: (*t).ext_coeffs()) {
|
||||
unsigned j = p.var();
|
||||
auto it = c2t.find(j);
|
||||
if (it == c2t.end()) {
|
||||
|
|
@ -1317,7 +1308,8 @@ namespace lp {
|
|||
} else {
|
||||
it->second.insert(t->j());
|
||||
}
|
||||
|
||||
|
||||
|
||||
}
|
||||
}
|
||||
for (const auto & p : c2t) {
|
||||
|
|
@ -1502,14 +1494,14 @@ namespace lp {
|
|||
{
|
||||
tout << "get_term_from_entry(" << ei << "):";
|
||||
print_term_o(get_term_from_entry(ei), tout) << std::endl;
|
||||
tout << "remove_fresh_vars:";
|
||||
tout << "ls:";
|
||||
print_term_o(remove_fresh_vars(get_term_from_entry(ei)), tout)
|
||||
<< std::endl;
|
||||
tout << "e.m_l:"; print_lar_term_L(l_term_from_row(ei), tout) << std::endl;
|
||||
tout << "open_ml(e.m_l):";
|
||||
print_term_o(open_ml(l_term_from_row(ei)), tout) << std::endl;
|
||||
tout << "fix_vars(open_ml(e.m_l)):";
|
||||
print_term_o(fix_vars(open_ml(l_term_from_row(ei))), tout) << std::endl;
|
||||
print_lar_term_L(open_ml(l_term_from_row(ei)), tout) << std::endl;
|
||||
tout << "rs:";
|
||||
print_term_o(fix_vars(open_ml(m_l_matrix.m_rows[ei])), tout) << std::endl;
|
||||
}
|
||||
);
|
||||
return ret;
|
||||
|
|
@ -1544,7 +1536,7 @@ namespace lp {
|
|||
|
||||
std::ostream& print_ml(const lar_term& ml, std::ostream& out) {
|
||||
term_o opened_ml = open_ml(ml);
|
||||
return print_term_o(opened_ml, out);
|
||||
return print_lar_term_L(opened_ml, out);
|
||||
}
|
||||
|
||||
template <typename T> term_o open_ml(const T& ml) const {
|
||||
|
|
@ -1564,7 +1556,7 @@ namespace lp {
|
|||
m_indexed_work_vector.clear();
|
||||
for (const auto & p: m_l_matrix.m_rows[ei]) {
|
||||
const lar_term& t = lra.get_term(p.var());
|
||||
for (const auto & q: t) {
|
||||
for (const auto & q: t.ext_coeffs()) {
|
||||
if (is_fixed(q.var())) {
|
||||
c += p.coeff()*q.coeff()*lia.lower_bound(q.var()).x;
|
||||
} else {
|
||||
|
|
@ -1572,13 +1564,6 @@ namespace lp {
|
|||
m_indexed_work_vector.add_value_at_index(q.var(), p.coeff() * q.coeff());
|
||||
}
|
||||
}
|
||||
if (is_fixed(t.j())) {
|
||||
c -= lia.lower_bound(t.j()).x;
|
||||
}
|
||||
else {
|
||||
make_space_in_work_vector(t.j());
|
||||
m_indexed_work_vector.add_value_at_index(t.j(), -p.coeff());
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -30,6 +30,8 @@ protected:
|
|||
// the column index related to the term
|
||||
lpvar m_j = -1;
|
||||
public:
|
||||
|
||||
|
||||
// the column index related to the term
|
||||
lpvar j() const { return m_j; }
|
||||
void set_j(unsigned j) {
|
||||
|
|
@ -92,8 +94,6 @@ public:
|
|||
}
|
||||
// constructors
|
||||
lar_term() = default;
|
||||
<<<<<<< HEAD
|
||||
=======
|
||||
lar_term(lar_term&& other) noexcept = default;
|
||||
// copy assignment operator
|
||||
lar_term& operator=(const lar_term& other) = default;
|
||||
|
|
@ -106,7 +106,6 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
>>>>>>> 956229fb6 (test that pivoting is correct in dioph_eq.cpp)
|
||||
lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
|
||||
for (auto const& p : coeffs) {
|
||||
add_monomial(p.first, p.second);
|
||||
|
|
@ -257,10 +256,9 @@ public:
|
|||
m_coeffs.reset();
|
||||
}
|
||||
|
||||
class ival {
|
||||
struct ival {
|
||||
lpvar m_var;
|
||||
const mpq & m_coeff;
|
||||
public:
|
||||
ival(lpvar var, const mpq & val) : m_var(var), m_coeff(val) { }
|
||||
lpvar j() const { return m_var; }
|
||||
lpvar var() const { return m_var; }
|
||||
|
|
@ -274,7 +272,12 @@ public:
|
|||
const_iterator operator++() { const_iterator i = *this; m_it++; return i; }
|
||||
const_iterator operator++(int) { m_it++; return *this; }
|
||||
const_iterator(u_map<mpq>::iterator it) : m_it(it) {}
|
||||
bool operator!=(const const_iterator &other) const { return m_it != other.m_it; }
|
||||
bool operator==(const const_iterator &other) const { return m_it == other.m_it; }
|
||||
bool operator!=(const const_iterator &other) const { return !(*this == other); }
|
||||
// Return a pointer to the same object returned by operator*.
|
||||
const ival* operator->() const {
|
||||
return &(**this);
|
||||
}
|
||||
};
|
||||
|
||||
bool is_normalized() const {
|
||||
|
|
@ -316,5 +319,101 @@ public:
|
|||
}
|
||||
const_iterator begin() const { return m_coeffs.begin();}
|
||||
const_iterator end() const { return m_coeffs.end(); }
|
||||
// This iterator yields all (coefficient, variable) pairs
|
||||
// plus one final pair: (mpq(-1), j()).
|
||||
class ext_const_iterator {
|
||||
// We'll store a reference to the lar_term, and an
|
||||
// iterator into m_coeffs. Once we reach end of m_coeffs,
|
||||
// we'll yield exactly one extra pair, then we are done.
|
||||
const lar_term& m_term;
|
||||
lar_term::const_iterator m_it;
|
||||
bool m_done; // Have we gone past m_coeffs?
|
||||
|
||||
public:
|
||||
// Construct either a "begin" iterator (end=false) or "end" iterator (end=true).
|
||||
ext_const_iterator(const lar_term& t, bool is_end)
|
||||
: m_term(t)
|
||||
, m_it(is_end ? t.end() : t.begin())
|
||||
, m_done(false)
|
||||
{
|
||||
// If it is_end == true, we represent a genuine end-iterator.
|
||||
if (is_end) {
|
||||
m_done = true;
|
||||
}
|
||||
}
|
||||
|
||||
// Compare iterators. Two iterators are equal if both are "done" or hold the same internal iterator.
|
||||
bool operator==(ext_const_iterator const &other) const {
|
||||
// They are equal if they are both at the special extra pair or both at the same spot in m_coeffs.
|
||||
if (m_done && other.m_done) {
|
||||
return true;
|
||||
}
|
||||
return (!m_done && !other.m_done && m_it == other.m_it);
|
||||
}
|
||||
|
||||
bool operator!=(ext_const_iterator const &other) const {
|
||||
return !(*this == other);
|
||||
}
|
||||
|
||||
// Return the element we point to:
|
||||
// 1) If we haven't finished m_coeffs, yield (coefficient, var).
|
||||
// 2) If we've iterated past m_coeffs exactly once, return (mpq(-1), j()).
|
||||
auto operator*() const {
|
||||
if (!m_done && m_it != m_term.end()) {
|
||||
// Normal monomial from m_coeffs
|
||||
// Each entry is of type { m_value, m_key } in this context
|
||||
return *m_it;
|
||||
}
|
||||
else {
|
||||
// We've gone past normal entries, so return the extra pair
|
||||
// (mpq(-1), j()).
|
||||
return ival(m_term.j(), rational::minus_one());
|
||||
}
|
||||
}
|
||||
|
||||
// Pre-increment
|
||||
ext_const_iterator& operator++() {
|
||||
if (!m_done && m_it != m_term.end()) {
|
||||
++m_it;
|
||||
}
|
||||
else {
|
||||
// We were about to return that extra pair:
|
||||
// after we move once more, we are done.
|
||||
m_done = true;
|
||||
}
|
||||
return *this;
|
||||
}
|
||||
|
||||
// Post-increment
|
||||
ext_const_iterator operator++(int) {
|
||||
ext_const_iterator temp(*this);
|
||||
++(*this);
|
||||
return temp;
|
||||
}
|
||||
};
|
||||
|
||||
// Return the begin/end of our extended iteration.
|
||||
// begin: starts at first real monomial
|
||||
// end: marks a finalized end of iteration
|
||||
ext_const_iterator ext_coeffs_begin() const {
|
||||
return ext_const_iterator(*this, /*is_end=*/false);
|
||||
}
|
||||
ext_const_iterator ext_coeffs_end() const {
|
||||
return ext_const_iterator(*this, /*is_end=*/true);
|
||||
}
|
||||
|
||||
// Provide a small helper for "range-based for":
|
||||
// for (auto & [coef, var] : myTerm.ext_coeffs()) { ... }
|
||||
struct ext_range {
|
||||
ext_const_iterator b, e;
|
||||
ext_const_iterator begin() const { return b; }
|
||||
ext_const_iterator end() const { return e; }
|
||||
};
|
||||
|
||||
// return an object that can be used in range-based for loops
|
||||
ext_range ext_coeffs() const {
|
||||
return { ext_coeffs_begin(), ext_coeffs_end() };
|
||||
}
|
||||
|
||||
};
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue