mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-22 05:43:39 +00:00
Code Activity

support recursive terms (#5246)

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2021-05-05 12:53:20 -07:00 • committed by GitHub
parent 466269ee13
commit 179988e161
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 37 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -162,7 +162,7 @@ namespace lp {
continue; continue;
if (!m_terms[k]->contains(basis_j)) if (!m_terms[k]->contains(basis_j))
continue; continue;
m_terms[k]->subst(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row); m_terms[k]->subst_in_row(basis_j, m_mpq_lar_core_solver.m_r_solver.m_pivot_row);
} }
} }
@ -1717,6 +1717,27 @@ namespace lp {
return true; return true;
} }
void lar_solver::subst_known_terms(lar_term* t) {
std::set<unsigned> seen_terms;
for (const auto&p : *t) {
auto j = p.column();
if (this->column_corresponds_to_term(j)) {
seen_terms.insert(j);
}
}
while (!seen_terms.empty()) {
unsigned j = *seen_terms.begin();
seen_terms.erase(j);
auto tj = this->m_var_register.local_to_external(j);
auto& ot = this->get_term(tj);
for(const auto& p : ot){
if (this->column_corresponds_to_term(p.column())) {
seen_terms.insert(p.column());
}
}
t->subst_by_term(ot, j);
}
}
// do not register in m_var_register this term if ext_i == UINT_MAX // do not register in m_var_register this term if ext_i == UINT_MAX
var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>>& coeffs, unsigned ext_i) { var_index lar_solver::add_term(const vector<std::pair<mpq, var_index>>& coeffs, unsigned ext_i) {
TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";); TRACE("lar_solver_terms", print_linear_combination_of_column_indices_only(coeffs, tout) << ", ext_i =" << ext_i << "\n";);
@ -1726,6 +1747,7 @@ namespace lp {
if (strategy_is_undecided()) if (strategy_is_undecided())
return add_term_undecided(coeffs); return add_term_undecided(coeffs);
lar_term* t = new lar_term(coeffs); lar_term* t = new lar_term(coeffs);
subst_known_terms(t);
push_term(t); push_term(t);
SASSERT(m_terms.size() == m_term_register.size()); SASSERT(m_terms.size() == m_term_register.size());
unsigned adjusted_term_index = m_terms.size() - 1; unsigned adjusted_term_index = m_terms.size() - 1;

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

@ -585,6 +585,8 @@ public:
return out; return out;
} }
void subst_known_terms(lar_term*);
inline std::ostream& print_column_bound_info(unsigned j, std::ostream& out) const { inline std::ostream& print_column_bound_info(unsigned j, std::ostream& out) const {
return m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, out); return m_mpq_lar_core_solver.m_r_solver.print_column_bound_info(j, out);
} }

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

@ -57,6 +57,16 @@ public:
return m_coeffs; return m_coeffs;
} }
void subst_by_term(const lar_term& t, unsigned term_column) {
auto it = this->m_coeffs.find_core(term_column);
if (it == nullptr) return;
mpq a = it->get_data().m_value;
this->m_coeffs.erase(term_column);
for (const auto & p : t) {
this->add_monomial(a * p.coeff(), p.column());
}
}
lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) { lar_term(const vector<std::pair<mpq, unsigned>>& coeffs) {
for (const auto & p : coeffs) { for (const auto & p : coeffs) {
add_monomial(p.first, p.second); add_monomial(p.first, p.second);
@ -94,7 +104,7 @@ public:
} }
// j is the basic variable to substitute // j is the basic variable to substitute
void subst(unsigned j, indexed_vector<mpq> & li) { void subst_in_row(unsigned j, indexed_vector<mpq> & li) {
auto* it = m_coeffs.find_core(j); auto* it = m_coeffs.find_core(j);
if (it == nullptr) return; if (it == nullptr) return;
const mpq & b = it->get_data().m_value; const mpq & b = it->get_data().m_value;