mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
9804ba9fd2
commit
6366f8f6b2
|
@ -109,9 +109,9 @@ bool has_skolem_functions(expr * n) {
|
|||
|
||||
subterms::subterms(expr_ref_vector const& es, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp): m_include_bound(include_bound), m_es(es), m_esp(esp), m_vp(vp) {}
|
||||
subterms::subterms(expr_ref const& e, bool include_bound, ptr_vector<expr>* esp, expr_mark* vp) : m_include_bound(include_bound), m_es(e.m()), m_esp(esp), m_vp(vp) { if (e) m_es.push_back(e); }
|
||||
subterms::iterator subterms::begin() { return iterator(* this, m_esp, m_vp, true); }
|
||||
subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); }
|
||||
subterms::iterator::iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
|
||||
subterms::iterator subterms::begin() const { return iterator(* this, m_esp, m_vp, true); }
|
||||
subterms::iterator subterms::end() const { return iterator(*this, nullptr, nullptr, false); }
|
||||
subterms::iterator::iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start): m_include_bound(f.m_include_bound), m_esp(esp), m_visitedp(vp) {
|
||||
if (!esp)
|
||||
m_esp = &m_es;
|
||||
else
|
||||
|
|
|
@ -186,7 +186,7 @@ public:
|
|||
expr_mark m_visited;
|
||||
expr_mark* m_visitedp = nullptr;
|
||||
public:
|
||||
iterator(subterms& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
|
||||
iterator(subterms const& f, ptr_vector<expr>* esp, expr_mark* vp, bool start);
|
||||
expr* operator*();
|
||||
iterator operator++(int);
|
||||
iterator& operator++();
|
||||
|
@ -198,8 +198,8 @@ public:
|
|||
static subterms ground(expr_ref const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
|
||||
static subterms all(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, true, esp, vp); }
|
||||
static subterms ground(expr_ref_vector const& e, ptr_vector<expr>* esp = nullptr, expr_mark* vp = nullptr) { return subterms(e, false, esp, vp); }
|
||||
iterator begin();
|
||||
iterator end();
|
||||
iterator begin() const;
|
||||
iterator end() const;
|
||||
};
|
||||
|
||||
class subterms_postorder {
|
||||
|
|
|
@ -258,7 +258,7 @@ namespace lp {
|
|||
m_crossed_bounds_column.pop(k);
|
||||
unsigned n = m_columns_to_ul_pairs.peek_size(k);
|
||||
m_var_register.shrink(n);
|
||||
pop_tableau();
|
||||
pop_tableau(n);
|
||||
lp_assert(A_r().column_count() == n);
|
||||
TRACE("lar_solver_details",
|
||||
for (unsigned j = 0; j < n; j++) {
|
||||
|
@ -1326,15 +1326,15 @@ namespace lp {
|
|||
lp_assert(A_r().column_count() == m_mpq_lar_core_solver.m_r_solver.m_costs.size());
|
||||
}
|
||||
|
||||
void lar_solver::pop_tableau() {
|
||||
void lar_solver::pop_tableau(unsigned old_size) {
|
||||
lp_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count());
|
||||
|
||||
lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count());
|
||||
lp_assert(m_mpq_lar_core_solver.m_r_solver.basis_heading_is_correct());
|
||||
// We remove last variables starting from m_column_names.size() to m_vec_of_canonic_left_sides.size().
|
||||
// At this moment m_column_names is already popped
|
||||
unsigned size = m_var_register.size();
|
||||
while (A_r().column_count() > size)
|
||||
|
||||
while (A_r().column_count() > old_size)
|
||||
remove_last_column_from_tableau();
|
||||
lp_assert(m_mpq_lar_core_solver.m_r_solver.m_costs.size() == A_r().column_count());
|
||||
lp_assert(m_mpq_lar_core_solver.m_r_solver.m_basis.size() == A_r().row_count());
|
||||
|
@ -1544,12 +1544,7 @@ namespace lp {
|
|||
|
||||
// terms
|
||||
bool lar_solver::all_vars_are_registered(const vector<std::pair<mpq, var_index>>& coeffs) {
|
||||
for (const auto& p : coeffs) {
|
||||
if (p.second >= m_var_register.size()) {
|
||||
return false;
|
||||
}
|
||||
}
|
||||
return true;
|
||||
return all_of(coeffs, [&](const auto& p) { return p.second < m_var_register.size(); });
|
||||
}
|
||||
|
||||
void lar_solver::subst_known_terms(lar_term* t) {
|
||||
|
|
|
@ -225,7 +225,7 @@ class lar_solver : public column_namer {
|
|||
|
||||
void remove_last_column_from_basis_tableau(unsigned j);
|
||||
void remove_last_column_from_tableau();
|
||||
void pop_tableau();
|
||||
void pop_tableau(unsigned old_size);
|
||||
void clean_inf_heap_of_r_solver_after_pop();
|
||||
inline bool column_value_is_integer(unsigned j) const { return get_column_value(j).is_int(); }
|
||||
bool model_is_int_feasible() const;
|
||||
|
|
|
@ -72,9 +72,8 @@ public:
|
|||
|
||||
svector<unsigned> vars() const {
|
||||
svector<unsigned> ret;
|
||||
for (const auto& p : m_local_to_external) {
|
||||
for (const auto& p : m_local_to_external)
|
||||
ret.push_back(p.external_j());
|
||||
}
|
||||
return ret;
|
||||
}
|
||||
|
||||
|
@ -126,11 +125,7 @@ public:
|
|||
}
|
||||
|
||||
bool has_int_var() const {
|
||||
for (const auto & vi : m_local_to_external) {
|
||||
if (vi.is_integer())
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
return any_of(m_local_to_external, [&](const auto& vi) { return vi.is_integer(); });
|
||||
}
|
||||
|
||||
bool local_is_int(unsigned j) const {
|
||||
|
@ -138,9 +133,8 @@ public:
|
|||
}
|
||||
|
||||
void shrink(unsigned shrunk_size) {
|
||||
for (unsigned j = size(); j-- > shrunk_size;) {
|
||||
for (unsigned j = size(); j-- > shrunk_size;)
|
||||
m_external_to_local.erase(m_local_to_external[j].external_j());
|
||||
}
|
||||
m_local_to_external.resize(shrunk_size);
|
||||
}
|
||||
|
||||
|
|
|
@ -363,7 +363,7 @@ void set_fatal_error_handler(void (*pfn)(int error_code));
|
|||
|
||||
|
||||
template<typename S, typename T>
|
||||
bool any_of(S& set, T const& p) {
|
||||
bool any_of(S const& set, T const& p) {
|
||||
for (auto const& s : set)
|
||||
if (p(s))
|
||||
return true;
|
||||
|
@ -371,7 +371,7 @@ bool any_of(S& set, T const& p) {
|
|||
}
|
||||
|
||||
template<typename S, typename T>
|
||||
bool all_of(S& set, T const& p) {
|
||||
bool all_of(S const& set, T const& p) {
|
||||
for (auto const& s : set)
|
||||
if (!p(s))
|
||||
return false;
|
||||
|
|
Loading…
Reference in a new issue