3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

u_set replaced by indexed_uint_set (#6841)

* replace u_set by indexed_uint_set

* replace u_set by indexed_uint_set

* create insert-fresh and insert for indexed_uint_set to make use cases with non-fresh inserts easier

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* update nightly to pull arm

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* update nightly to pull arm

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* fixing the build of lp_tst

* update nightly to pull arm

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

* replace u_set by indexed_uint_set

* replace u_set by indexed_uint_set

* fixing the build of lp_tst

* remove unnecessery call to contains() before
insert to indexed_uint_set

* formatting, no check for contains()
 in indexed_uint_set, always init m_touched_rows to nullptr

---------

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Lev Nachmanson 2023-08-03 13:01:27 -10:00 committed by GitHub
parent 4637339091
commit f58b703ac5
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
21 changed files with 69 additions and 192 deletions

View file

@ -76,7 +76,7 @@ bool horner::lemmas_on_expr(cross_nested& cn, nex_sum* e) {
template <typename T>
bool horner::lemmas_on_row(const T& row) {
SASSERT (row_is_interesting(row));
c().clear_and_resize_active_var_set();
c().clear_active_var_set();
u_dependency* dep = nullptr;
create_sum_from_row(row, m_nex_creator, m_row_sum, dep);
c().set_active_vars_weights(m_nex_creator); // without this call the comparisons will be incorrect
@ -110,7 +110,7 @@ bool horner::horner_lemmas() {
for (auto & s : matrix.m_columns[j])
rows_to_check.insert(s.var());
}
c().clear_and_resize_active_var_set();
c().clear_active_var_set();
svector<unsigned> rows;
for (unsigned i : rows_to_check) {
if (row_is_interesting(matrix.m_rows[i]))

View file

@ -23,7 +23,7 @@
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
namespace nla {
class core;

View file

@ -20,7 +20,7 @@ Revision History:
#pragma once
#include "math/lp/lp_settings.h"
#include "math/lp/static_matrix.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
#include "math/lp/lar_term.h"
#include "math/lp/lar_constraints.h"
#include "math/lp/hnf_cutter.h"

View file

@ -234,13 +234,13 @@ namespace lp {
m_usage_in_terms.push();
}
void lar_solver::clean_popped_elements(unsigned n, u_set& set) {
void lar_solver::clean_popped_elements(unsigned n, indexed_uint_set& set) {
vector<int> to_remove;
for (unsigned j : set)
if (j >= n)
to_remove.push_back(j);
for (unsigned j : to_remove)
set.erase(j);
set.remove(j);
}
void lar_solver::clean_popped_elements_for_heap(unsigned n, lpvar_heap& heap) {
@ -361,7 +361,6 @@ namespace lp {
void lar_solver::prepare_costs_for_r_solver(const lar_term& term) {
TRACE("lar_solver", print_term(term, tout << "prepare: ") << "\n";);
m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
move_non_basic_columns_to_bounds(false);
auto& rslv = m_mpq_lar_core_solver.m_r_solver;
lp_assert(costs_are_zeros_for_r_solver());
@ -619,7 +618,7 @@ namespace lp {
}
void lar_solver::add_touched_row(unsigned rid) {
if (m_settings.bound_propagation())
if (m_settings.bound_propagation())
m_touched_rows.insert(rid);
}
@ -710,9 +709,6 @@ namespace lp {
void lar_solver::solve_with_core_solver() {
m_mpq_lar_core_solver.prefix_r();
if (costs_are_used()) {
m_basic_columns_with_changed_cost.resize(m_mpq_lar_core_solver.m_r_x.size());
}
update_x_and_inf_costs_for_columns_with_changed_bounds_tableau();
m_mpq_lar_core_solver.solve();
set_status(m_mpq_lar_core_solver.m_r_solver.get_status());
@ -1431,7 +1427,6 @@ namespace lp {
void lar_solver::add_non_basic_var_to_core_fields(unsigned ext_j, bool is_int) {
register_new_ext_var_index(ext_j, is_int);
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
increase_by_one_columns_with_changed_bounds();
add_new_var_to_core_fields_for_mpq(false); // false for not adding a row
}
@ -1585,11 +1580,7 @@ namespace lp {
void lar_solver::add_basic_var_to_core_fields() {
m_mpq_lar_core_solver.m_column_types.push_back(column_type::free_column);
increase_by_one_columns_with_changed_bounds();
m_incorrect_columns.increase_size_by_one();
m_touched_rows.increase_size_by_one();
add_new_var_to_core_fields_for_mpq(true);
}
bool lar_solver::bound_is_integer_for_integer_column(unsigned j, const mpq& right_side) const {
@ -1739,8 +1730,8 @@ namespace lp {
TRACE("lar_solver_feas", tout << "j = " << j << " became " << (this->column_is_feasible(j)?"feas":"non-feas") << ", and " << (this->column_is_bounded(j)? "bounded":"non-bounded") << std::endl;);
}
void lar_solver::insert_to_columns_with_changed_bounds(unsigned j) {
m_columns_with_changed_bounds.insert(j);
TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
m_columns_with_changed_bounds.insert(j);
TRACE("lar_solver", tout << "column " << j << (column_is_feasible(j) ? " feas" : " non-feas") << "\n";);
}
void lar_solver::update_column_type_and_bound_check_on_equal(unsigned j,
lconstraint_kind kind,
@ -2063,7 +2054,6 @@ namespace lp {
void lar_solver::round_to_integer_solution() {
m_incorrect_columns.resize(column_count());
for (unsigned j = 0; j < column_count(); j++) {
if (!column_is_int(j)) continue;
if (column_corresponds_to_term(j)) continue;
@ -2085,7 +2075,7 @@ namespace lp {
}
if (!m_incorrect_columns.empty()) {
fix_terms_with_rounded_columns();
m_incorrect_columns.clear();
m_incorrect_columns.reset();
}
}

View file

@ -85,14 +85,14 @@ class lar_solver : public column_namer {
stacked_vector<ul_pair> m_columns_to_ul_pairs;
constraint_set m_constraints;
// the set of column indices j such that bounds have changed for j
u_set m_columns_with_changed_bounds;
u_set m_touched_rows;
indexed_uint_set m_columns_with_changed_bounds;
indexed_uint_set m_touched_rows;
unsigned_vector m_row_bounds_to_replay;
u_set m_basic_columns_with_changed_cost;
indexed_uint_set m_basic_columns_with_changed_cost;
// these are basic columns with the value changed, so the corresponding row in the tableau
// does not sum to zero anymore
u_set m_incorrect_columns;
indexed_uint_set m_incorrect_columns;
// copy of m_r_solver.inf_heap()
unsigned_vector m_inf_index_copy;
stacked_value<unsigned> m_term_count;
@ -132,8 +132,7 @@ class lar_solver : public column_namer {
void add_basic_var_to_core_fields();
bool compare_values(impq const& lhs, lconstraint_kind k, const mpq& rhs);
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.clear(); }
inline void increase_by_one_columns_with_changed_bounds() { m_columns_with_changed_bounds.increase_size_by_one(); }
inline void clear_columns_with_changed_bounds() { m_columns_with_changed_bounds.reset(); }
void insert_to_columns_with_changed_bounds(unsigned j);
void update_column_type_and_bound_check_on_equal(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index, unsigned&);
void update_column_type_and_bound(unsigned j, lconstraint_kind kind, const mpq& right_side, constraint_index constr_index);
@ -175,7 +174,7 @@ class lar_solver : public column_namer {
}
static void clean_popped_elements_for_heap(unsigned n, lpvar_heap& set);
static void clean_popped_elements(unsigned n, u_set& set);
static void clean_popped_elements(unsigned n, indexed_uint_set& set);
bool maximize_term_on_tableau(const lar_term& term,
impq& term_max);
bool costs_are_zeros_for_r_solver() const;
@ -349,7 +348,7 @@ class lar_solver : public column_namer {
m_row_bounds_to_replay.push_back(i);
}
}
m_touched_rows.clear();
m_touched_rows.reset();
}
template <typename T>

View file

@ -27,7 +27,7 @@ Revision History:
#include "math/lp/static_matrix.h"
#include "math/lp/permutation_matrix.h"
#include "math/lp/column_namer.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
#include "util/heap.h"
namespace lp {
@ -92,7 +92,7 @@ public:
vector<unsigned> m_trace_of_basis_change_vector; // the even positions are entering, the odd positions are leaving
bool m_tracing_basis_changes;
// these rows are changed by adding to them a multiple of the pivot row
u_set* m_touched_rows;
indexed_uint_set* m_touched_rows = nullptr;
bool m_look_for_feasible_solution_only;
void start_tracing_basis_changes() {

View file

@ -21,7 +21,7 @@ Revision History:
#include "math/lp/core_solver_pretty_printer.h"
#include "math/lp/lp_core_solver_base.h"
#include "math/lp/static_matrix.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
#include "util/vector.h"
#include <algorithm>
#include <cstdlib>
@ -46,7 +46,7 @@ namespace lp {
vector<T> m_costs_backup;
unsigned m_inf_row_index_for_tableau;
bool m_bland_mode_tableau;
u_set m_left_basis_tableau;
indexed_uint_set m_left_basis_tableau;
unsigned m_bland_mode_threshold;
unsigned m_left_basis_repeated;
vector<unsigned> m_leaving_candidates;
@ -627,8 +627,7 @@ namespace lp {
void init_reduced_costs_tableau();
void init_tableau_rows() {
m_bland_mode_tableau = false;
m_left_basis_tableau.clear();
m_left_basis_tableau.resize(this->m_A.column_count());
m_left_basis_tableau.reset();
m_left_basis_repeated = 0;
}
// stage1 constructor

View file

@ -10,7 +10,7 @@
#include "math/lp/nla_common.h"
#include "math/lp/nla_intervals.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
namespace nla {
class core;

View file

@ -828,14 +828,14 @@ void core::insert_to_refine(lpvar j) {
void core::erase_from_to_refine(lpvar j) {
TRACE("lar_solver", tout << "j=" << j << '\n';);
m_to_refine.erase(j);
if (m_to_refine.contains(j))
m_to_refine.remove(j);
}
void core::init_to_refine() {
TRACE("nla_solver_details", tout << "emons:" << pp_emons(*this, m_emons););
m_to_refine.clear();
m_to_refine.resize(m_lar_solver.number_of_vars());
m_to_refine.reset();
unsigned r = random(), sz = m_emons.number_of_monics();
for (unsigned k = 0; k < sz; k++) {
auto const & m = *(m_emons.begin() + (k + r)% sz);
@ -1407,8 +1407,12 @@ void core::patch_monomial(lpvar j) {
}
void core::patch_monomials_on_to_refine() {
auto to_refine = m_to_refine.index();
// the rest of the function might change m_to_refine, so have to copy
unsigned_vector to_refine;
for (unsigned j :m_to_refine) {
to_refine.push_back(j);
}
unsigned sz = to_refine.size();
unsigned start = random();

View file

@ -84,7 +84,7 @@ class core {
reslimit& m_reslim;
std::function<bool(lpvar)> m_relevant;
vector<lemma> * m_lemma_vec;
lp::u_set m_to_refine;
indexed_uint_set m_to_refine;
tangents m_tangents;
basics m_basics;
order m_order;
@ -99,7 +99,7 @@ class core {
grobner m_grobner;
emonics m_emons;
svector<lpvar> m_add_buffer;
mutable lp::u_set m_active_var_set;
mutable indexed_uint_set m_active_var_set;
reslimit m_nra_lim;
@ -118,18 +118,15 @@ public:
void insert_to_refine(lpvar j);
void erase_from_to_refine(lpvar j);
const lp::u_set& active_var_set () const { return m_active_var_set;}
const indexed_uint_set& active_var_set () const { return m_active_var_set;}
bool active_var_set_contains(unsigned j) const { return m_active_var_set.contains(j); }
void insert_to_active_var_set(unsigned j) const { m_active_var_set.insert(j); }
void insert_to_active_var_set(unsigned j) const {
m_active_var_set.insert(j);
}
void clear_active_var_set() const { m_active_var_set.clear(); }
void clear_active_var_set() const { m_active_var_set.reset(); }
void clear_and_resize_active_var_set() const {
m_active_var_set.clear();
m_active_var_set.resize(m_lar_solver.number_of_vars());
}
unsigned get_var_weight(lpvar) const;
reslimit& reslim() { return m_reslim; }

View file

@ -498,9 +498,8 @@ namespace nla {
}
void grobner::prepare_rows_and_active_vars() {
m_rows.clear();
m_rows.resize(m_lar_solver.row_count());
c().clear_and_resize_active_var_set();
m_rows.reset();
c().clear_active_var_set();
}

View file

@ -12,7 +12,7 @@
#include "math/lp/nla_intervals.h"
#include "math/lp/nex.h"
#include "math/lp/cross_nested.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
#include "math/grobner/pdd_solver.h"
namespace nla {
@ -22,7 +22,7 @@ namespace nla {
dd::pdd_manager m_pdd_manager;
dd::solver m_solver;
lp::lar_solver& m_lar_solver;
lp::u_set m_rows;
indexed_uint_set m_rows;
lp::lp_settings& lp_settings();

View file

@ -9,7 +9,7 @@
#include "math/polynomial/polynomial.h"
#include "math/polynomial/algebraic_numbers.h"
#include "util/map.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
#include "math/lp/nla_core.h"
@ -23,7 +23,7 @@ struct solver::imp {
reslimit& m_limit;
params_ref m_params;
u_map<polynomial::var> m_lp2nl; // map from lar_solver variables to nlsat::solver variables
lp::u_set m_term_set;
indexed_uint_set m_term_set;
scoped_ptr<nlsat::solver> m_nlsat;
scoped_ptr<scoped_anum> m_zero;
mutable variable_map_type m_variable_values; // current model
@ -55,7 +55,7 @@ struct solver::imp {
m_zero = nullptr;
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_zero = alloc(scoped_anum, am());
m_term_set.clear();
m_term_set.reset();
m_lp2nl.reset();
vector<nlsat::assumption, false> core;
@ -182,7 +182,7 @@ struct solver::imp {
m_nlsat = alloc(nlsat::solver, m_limit, m_params, false);
m_zero = alloc(scoped_anum, am());
m_lp2nl.reset();
m_term_set.clear();
m_term_set.reset();
for (auto const& eq : eqs)
add_eq(eq);
for (auto const& [v, w] : m_lp2nl) {
@ -283,8 +283,6 @@ struct solver::imp {
r = m_nlsat->mk_var(is_int(v));
m_lp2nl.insert(v, r);
if (!m_term_set.contains(v) && s.column_corresponds_to_term(v)) {
if (v >= m_term_set.data_size())
m_term_set.resize(v + 1);
m_term_set.insert(v);
}
}

View file

@ -25,14 +25,14 @@ Revision History:
#include <string>
#include <algorithm>
#include "math/lp/lp_settings.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
// see http://research.microsoft.com/projects/z3/smt07.pdf
// The class searches for a feasible solution with as many different values of variables as it can find
namespace lp {
template <typename T> struct numeric_pair; // forward definition
class lar_solver; // forward definition
class random_updater {
u_set m_var_set;
indexed_uint_set m_var_set;
lar_solver & m_lar_solver;
unsigned m_range;
bool shift_var(unsigned j);

View file

@ -32,7 +32,6 @@ random_updater::random_updater(
const vector<unsigned> & column_indices) :
m_lar_solver(lar_solver),
m_range(100000) {
m_var_set.resize(m_lar_solver.number_of_vars());
for (unsigned j : column_indices)
m_var_set.insert(j);
TRACE("lar_solver_rand", tout << "size = " << m_var_set.size() << "\n";);
@ -45,7 +44,9 @@ bool random_updater::shift_var(unsigned j) {
if (ret) {
const auto & A = m_lar_solver.A_r();
for (const auto& c : A.m_columns[j]) {
m_var_set.erase(m_lar_solver.r_basis()[c.var()]);
unsigned k = m_lar_solver.r_basis()[c.var()];
if (m_var_set.contains(k))
m_var_set.remove(k);
}
}
return ret;
@ -54,7 +55,11 @@ bool random_updater::shift_var(unsigned j) {
void random_updater::update() {
// VERIFY(m_lar_solver.check_feasible());
auto columns = m_var_set.index(); // m_var_set is going to change during the loop
unsigned_vector columns;
// m_var_set is going to change during the loop, make a copy
for (unsigned j : m_var_set) {
columns.push_back(j);
}
for (auto j : columns) {
if (!m_var_set.contains(j)) {
TRACE("lar_solver_rand", tout << "skipped " << j << "\n";);

View file

@ -1,114 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
<name>
Abstract:
<abstract>
Author:
Lev Nachmanson (levnach)
Revision History:
TBD use indexed_uint_set from src/util/uint_set.h,
--*/
#pragma once
#include "util/vector.h"
#include <ostream>
namespace lp {
// serves at a set of non-negative integers smaller than the set size
class u_set {
svector<int> m_data;
unsigned_vector m_index;
public:
u_set(unsigned size): m_data(size, -1) {}
u_set() {}
u_set(u_set const& other):
m_data(other.m_data),
m_index(other.m_index) {}
bool contains(unsigned j) const {
if (j >= m_data.size())
return false;
return m_data[j] >= 0;
}
void insert(unsigned j) {
lp_assert(j < m_data.size());
if (contains(j)) return;
m_data[j] = m_index.size();
m_index.push_back(j);
}
void erase(unsigned j) {
if (!contains(j)) return;
unsigned pos_j = m_data[j];
unsigned last_pos = m_index.size() - 1;
int last_j = m_index[last_pos];
if (last_pos != pos_j) {
// move last to j spot
m_data[last_j] = pos_j;
m_index[pos_j] = last_j;
}
m_index.pop_back();
m_data[j] = -1;
}
int operator[](unsigned j) const { return m_index[j]; }
void resize(unsigned size) {
if (size < data_size()) {
bool copy = false;
unsigned i = 0;
for (unsigned j : m_index) {
if (j < size) {
if (copy) {
m_data[j] = i;
m_index[i] = j;
}
i++;
} else {
copy = true;
}
}
m_index.shrink(i);
}
m_data.resize(size, -1);
}
void increase_size_by_one() {
resize(m_data.size() + 1);
}
unsigned data_size() const { return m_data.size(); }
unsigned size() const { return m_index.size();}
bool empty() const { return size() == 0; }
void clear() {
for (unsigned j : m_index)
m_data[j] = -1;
m_index.resize(0);
}
std::ostream& display(std::ostream& out) const {
for (unsigned j : m_index) {
out << j << " ";
}
out << std::endl;
return out;
}
const unsigned * begin() const { return m_index.begin(); }
const unsigned * end() const { return m_index.end(); }
const unsigned_vector& index() { return m_index; }
};
}
inline std::ostream& operator<<(std::ostream& out, lp::u_set const& s) {
return s.display(out);
}

View file

@ -847,8 +847,7 @@ namespace arith {
if (m_nla)
return;
TRACE("arith", tout << s().scope_lvl() << "\n"; tout.flush(););
m_tmp_var_set.clear();
m_tmp_var_set.resize(get_num_vars());
m_tmp_var_set.reset();
m_model_eqs.reset();
svector<lpvar> vars;
theory_var sz = static_cast<theory_var>(get_num_vars());

View file

@ -225,7 +225,7 @@ namespace arith {
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
unsigned m_assume_eq_head = 0;
lp::u_set m_tmp_var_set;
indexed_uint_set m_tmp_var_set;
unsigned m_num_conflicts = 0;
lp_api::stats m_stats;

View file

@ -168,7 +168,7 @@ class theory_lra::imp {
svector<std::pair<theory_var, theory_var> > m_assume_eq_candidates;
unsigned m_assume_eq_head;
lp::u_set m_tmp_var_set;
indexed_uint_set m_tmp_var_set;
unsigned m_num_conflicts;
@ -1493,8 +1493,7 @@ public:
void random_update() {
if (m_nla && m_nla->need_check())
return;
m_tmp_var_set.clear();
m_tmp_var_set.resize(th.get_num_vars());
m_tmp_var_set.reset();
m_model_eqs.reset();
svector<lpvar> vars;
theory_var sz = static_cast<theory_var>(th.get_num_vars());

View file

@ -50,7 +50,7 @@
#include "math/lp/nla_solver.h"
#include "math/lp/numeric_pair.h"
#include "math/lp/static_matrix.h"
#include "math/lp/u_set.h"
#include "util/uint_set.h"
#include "test/lp/argument_parser.h"
#include "test/lp/gomory_test.h"
#include "test/lp/smt_reader.h"
@ -1072,20 +1072,18 @@ void test_bound_propagation() {
}
void test_int_set() {
u_set s(4);
s.insert(2);
indexed_uint_set s;
s.insert(1);
s.insert(2);
lp_assert(s.contains(2));
lp_assert(s.size() == 2);
s.erase(2);
lp_assert(s.size() == 1);
s.erase(2);
s.remove(2);
lp_assert(s.size() == 1);
s.insert(3);
s.insert(2);
s.clear();
s.reset();
lp_assert(s.size() == 0);
std::cout << "done test_int_set\n";
}
void test_rationals_no_numeric_pairs() {

View file

@ -350,6 +350,10 @@ public:
SASSERT(index < m_size);
return m_elems[index];
}
unsigned operator[](unsigned index) const {
SASSERT(index < m_size);
return m_elems[index];
}
bool contains(unsigned x) const { return x < m_index.size() && m_index[x] < m_size && m_elems[m_index[x]] == x; }
void reset() { m_size = 0; }