mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

init m_e_matrix on terms instead of the tableau

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-10-21 14:11:07 -07:00 committed by Lev Nachmanson
parent 392c24a145
commit 5f5f1d4fd1
4 changed files with 36 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

43
src/math/lp/dioph_eq.cpp
View file

@ -176,29 +176,37 @@ namespace lp {
} }
private: private:
// the row comes from lar_solver // the row comes from lar_solver
void fill_eprime_entry(const row_strip<mpq>& row, unsigned row_index) { void fill_eprime_entry(const lar_term& t, unsigned term_index) {
m_f.push_back(row_index); m_f.push_back(term_index);
eprime_entry& e = m_eprime[row_index]; eprime_entry& e = m_eprime[term_index];
e.m_row_index = row_index; e.m_row_index = term_index;
const auto lcm = get_denominators_lcm(row); const auto lcm = get_denominators_lcm(t);
mpq & c = e.m_c; mpq & c = e.m_c;
SASSERT(c.is_zero()); SASSERT(c.is_zero());
for (const auto & p: row) { for (const auto & p: t) {
if (lia.is_fixed(p.var())) { if (lia.is_fixed(p.var())) {
c += p.coeff()*lia.lower_bound(p.var()).x; c += p.coeff()*lia.lower_bound(p.var()).x;
e.m_l = lra.mk_join(e.m_l, lra.get_bound_constraint_witnesses_for_column(p.var())); e.m_l = lra.mk_join(e.m_l, lra.get_bound_constraint_witnesses_for_column(p.var()));
} }
else { else {
m_e_matrix.add_new_element(row_index, p.var(), lcm * p.coeff()); m_e_matrix.add_new_element(term_index, p.var(), lcm * p.coeff());
} }
} }
unsigned j = t.j();
if (lia.is_fixed(j)) {
c -= lia.lower_bound(j).x;
e.m_l = lra.mk_join(e.m_l, lra.get_bound_constraint_witnesses_for_column(j));
}
else {
m_e_matrix.add_new_element(term_index, j, - lcm);
}
c *= lcm; c *= lcm;
e.m_entry_status = entry_status::F; e.m_entry_status = entry_status::F;
} }
bool all_vars_are_int_and_small(const row_strip<mpq>& row) const { bool all_vars_are_int_and_small(const lar_term& term) const {
for (const auto& p : row) { for (const auto& p : term) {
if (!lia.column_is_int(p.var())) if (!lia.column_is_int(p.var()))
return false; return false;
if (p.coeff().is_big()) if (p.coeff().is_big())
@ -218,19 +226,20 @@ namespace lp {
m_infeas_explanation.clear(); m_infeas_explanation.clear();
lia.get_term().clear(); lia.get_term().clear();
m_eprime.clear(); m_eprime.clear();
m_eprime.resize(n_of_rows); m_eprime.resize(lra.terms().size());
for (unsigned i = 0; i < n_of_rows; i++) { for (unsigned i = 0; i < lra.terms().size(); i++) {
auto & row = lra.get_row(i); const lar_term* t = lra.terms()[i];
TRACE("dioph_eq", tout << "row "<< i <<":"; lra.print_row(row, tout) << "\n"; TRACE("dioph_eq", tout << "term "<< i <<":"; lra.print_term(*t, tout) << "\n";
for(auto & p: row) { for(auto & p: *t) {
lra.print_column_info(p.var(), tout); lra.print_column_info(p.var(), tout);
}); }
if (!all_vars_are_int_and_small(row)) { );
if (t->j() == UINT_MAX || !all_vars_are_int_and_small(*t)) {
TRACE("dioph_eq", tout << "not all vars are int and small\n";); TRACE("dioph_eq", tout << "not all vars are int and small\n";);
m_eprime[i].m_entry_status = entry_status::NO_S_NO_F; m_eprime[i].m_entry_status = entry_status::NO_S_NO_F;
continue; continue;
} }
fill_eprime_entry(row, i); fill_eprime_entry(*t, i);
TRACE("dioph_eq", print_eprime_entry(static_cast<unsigned>(i), tout);); TRACE("dioph_eq", print_eprime_entry(static_cast<unsigned>(i), tout););
} }

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

@ -237,6 +237,7 @@ public:
public: public:
ival(lpvar var, const mpq & val) : m_var(var), m_coeff(val) { } ival(lpvar var, const mpq & val) : m_var(var), m_coeff(val) { }
lpvar j() const { return m_var; } lpvar j() const { return m_var; }
lpvar var() const { return m_var; }
const mpq & coeff() const { return m_coeff; } const mpq & coeff() const { return m_coeff; }
}; };

6
src/math/lp/static_matrix.cpp
View file

@ -26,12 +26,6 @@ Revision History:
#include "math/lp/lp_primal_core_solver.h" #include "math/lp/lp_primal_core_solver.h"
#include "math/lp/lar_solver.h" #include "math/lp/lar_solver.h"
namespace lp { namespace lp {
mpq get_denominators_lcm(const row_strip<mpq> & row) {
mpq r(1);
for (auto & c : row)
r = lcm(r, denominator(c.coeff()));
return r;
}
template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain(); template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::mpq>::get_domain();
template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain(); template std::set<std::pair<unsigned, unsigned>> lp::static_matrix<lp::mpq, lp::numeric_pair<lp::mpq> >::get_domain();

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

@ -45,7 +45,14 @@ typedef vector<column_cell> column_strip;
template <typename T> template <typename T>
using row_strip = vector<row_cell<T>>; using row_strip = vector<row_cell<T>>;
mpq get_denominators_lcm(const row_strip<mpq> & row); template <typename K> mpq get_denominators_lcm(const K & row) {
mpq r = mpq(1);
for (auto & c : row)
r = lcm(r, denominator(c.coeff()));
return r;
}
template <typename T> template <typename T>
std::ostream& operator<<(std::ostream& out, const row_strip<T>& r) { std::ostream& operator<<(std::ostream& out, const row_strip<T>& r) {