mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
fix vector<> to support non-POD types
adjust code to std::move and avoid unnecessary/illegal
This commit is contained in:
parent
4d1acadabb
commit
9b54b4e784
|
@ -768,7 +768,7 @@ func_decl * basic_decl_plugin::mk_compressed_proof_decl(char const * name, basic
|
|||
|
||||
func_decl * basic_decl_plugin::mk_proof_decl(char const * name, basic_op_kind k, unsigned num_parents, ptr_vector<func_decl> & cache) {
|
||||
if (num_parents >= cache.size()) {
|
||||
cache.resize(num_parents+1, 0);
|
||||
cache.resize(num_parents+1);
|
||||
}
|
||||
if (cache[num_parents] == 0) {
|
||||
cache[num_parents] = mk_proof_decl(name, k, num_parents);
|
||||
|
|
|
@ -121,6 +121,20 @@ public:
|
|||
explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {}
|
||||
parameter(parameter const&);
|
||||
|
||||
parameter(parameter && other) noexcept : m_kind(other.m_kind) {
|
||||
switch (other.m_kind) {
|
||||
case PARAM_INT: m_int = other.get_int(); break;
|
||||
case PARAM_AST: m_ast = other.get_ast(); break;
|
||||
case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
|
||||
case PARAM_RATIONAL: m_rational = 0; std::swap(m_rational, other.m_rational); break;
|
||||
case PARAM_DOUBLE: m_dval = other.m_dval; break;
|
||||
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
}
|
||||
|
||||
~parameter();
|
||||
|
||||
parameter& operator=(parameter const& other);
|
||||
|
|
|
@ -179,11 +179,11 @@ expr_pattern_match::compile(expr* q)
|
|||
}
|
||||
|
||||
if (m_regs.size() <= max_reg) {
|
||||
m_regs.resize(max_reg+1, 0);
|
||||
m_regs.resize(max_reg+1);
|
||||
}
|
||||
if (m_bound_dom.size() <= num_bound) {
|
||||
m_bound_dom.resize(num_bound+1, 0);
|
||||
m_bound_rng.resize(num_bound+1, 0);
|
||||
m_bound_dom.resize(num_bound+1);
|
||||
m_bound_rng.resize(num_bound+1);
|
||||
}
|
||||
|
||||
instr.m_kind = YIELD;
|
||||
|
|
|
@ -272,7 +272,7 @@ void bit_blaster_tpl<Cfg>::mk_multiplier(unsigned sz, expr * const * a_bits, exp
|
|||
zero = m().mk_false();
|
||||
|
||||
vector< expr_ref_vector > pps;
|
||||
pps.resize(sz, m());
|
||||
pps.resize(sz, expr_ref_vector(m()));
|
||||
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
checkpoint();
|
||||
|
|
|
@ -256,7 +256,7 @@ void substitution_tree::insert(expr * new_expr) {
|
|||
sort * s = to_var(new_expr)->get_sort();
|
||||
unsigned id = s->get_decl_id();
|
||||
if (id >= m_vars.size())
|
||||
m_vars.resize(id+1, 0);
|
||||
m_vars.resize(id+1);
|
||||
if (m_vars[id] == 0)
|
||||
m_vars[id] = alloc(var_ref_vector, m_manager);
|
||||
var_ref_vector * v = m_vars[id];
|
||||
|
@ -277,7 +277,7 @@ void substitution_tree::insert(app * new_expr) {
|
|||
unsigned id = d->get_decl_id();
|
||||
|
||||
if (id >= m_roots.size())
|
||||
m_roots.resize(id+1, 0);
|
||||
m_roots.resize(id+1);
|
||||
|
||||
if (!m_roots[id]) {
|
||||
// there is no tree for the function symbol heading new_expr
|
||||
|
|
|
@ -58,7 +58,7 @@ void used_vars::process(expr * n, unsigned delta) {
|
|||
if (idx >= delta) {
|
||||
idx = idx - delta;
|
||||
if (idx >= m_found_vars.size())
|
||||
m_found_vars.resize(idx + 1, 0);
|
||||
m_found_vars.resize(idx + 1);
|
||||
m_found_vars[idx] = to_var(n)->get_sort();
|
||||
}
|
||||
break;
|
||||
|
|
|
@ -2632,10 +2632,14 @@ namespace algebraic_numbers {
|
|||
scoped_mpz neg_n(qm());
|
||||
qm().set(neg_n, v.numerator());
|
||||
qm().neg(neg_n);
|
||||
mpz const coeffs[2] = { neg_n.get(), v.denominator() };
|
||||
unsynch_mpz_manager zmgr;
|
||||
// FIXME: remove these copies
|
||||
mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
|
||||
out << "(";
|
||||
upm().display(out, 2, coeffs, "#");
|
||||
out << ", 1)"; // first root of the polynomial d*# - n
|
||||
zmgr.del(coeffs[0]);
|
||||
zmgr.del(coeffs[1]);
|
||||
}
|
||||
else {
|
||||
algebraic_cell * c = a.to_algebraic();
|
||||
|
@ -2678,10 +2682,14 @@ namespace algebraic_numbers {
|
|||
scoped_mpz neg_n(qm());
|
||||
qm().set(neg_n, v.numerator());
|
||||
qm().neg(neg_n);
|
||||
mpz const coeffs[2] = { neg_n.get(), v.denominator() };
|
||||
unsynch_mpz_manager zmgr;
|
||||
// FIXME: remove these copies
|
||||
mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
|
||||
out << "(root-obj ";
|
||||
upm().display_smt2(out, 2, coeffs, "x");
|
||||
out << " 1)"; // first root of the polynomial d*# - n
|
||||
zmgr.del(coeffs[0]);
|
||||
zmgr.del(coeffs[1]);
|
||||
}
|
||||
else {
|
||||
algebraic_cell * c = a.to_algebraic();
|
||||
|
|
|
@ -4822,10 +4822,9 @@ namespace polynomial {
|
|||
|
||||
polynomial * mk_x_minus_y(var x, var y) {
|
||||
numeral zero(0);
|
||||
numeral one(1);
|
||||
numeral minus_one; // It is not safe to initialize with -1 when numeral_manager is GF_2
|
||||
m_manager.set(minus_one, -1);
|
||||
numeral as[2] = { one, minus_one };
|
||||
numeral as[2] = { numeral(1), std::move(minus_one) };
|
||||
var xs[2] = { x, y };
|
||||
return mk_linear(2, as, xs, zero);
|
||||
}
|
||||
|
@ -4845,8 +4844,7 @@ namespace polynomial {
|
|||
|
||||
polynomial * mk_x_plus_y(var x, var y) {
|
||||
numeral zero(0);
|
||||
numeral one(1);
|
||||
numeral as[2] = { one, one };
|
||||
numeral as[2] = { numeral(1), numeral(1) };
|
||||
var xs[2] = { x, y };
|
||||
return mk_linear(2, as, xs, zero);
|
||||
}
|
||||
|
|
|
@ -45,7 +45,7 @@ namespace upolynomial {
|
|||
for (unsigned i = 0; i < p.size(); ++ i) {
|
||||
numeral p_i; // no need to delete, we keep it pushed in zp_p
|
||||
zp_nm.set(p_i, p[i]);
|
||||
zp_p.push_back(p_i);
|
||||
zp_p.push_back(std::move(p_i));
|
||||
}
|
||||
zp_upm.trim(zp_p);
|
||||
}
|
||||
|
|
|
@ -35,7 +35,7 @@ namespace simplex {
|
|||
struct row_entry {
|
||||
numeral m_coeff;
|
||||
var_t m_var;
|
||||
row_entry(numeral const& c, var_t v): m_coeff(c), m_var(v) {}
|
||||
row_entry(numeral && c, var_t v) noexcept : m_coeff(std::move(c)), m_var(v) {}
|
||||
};
|
||||
|
||||
private:
|
||||
|
@ -61,7 +61,7 @@ namespace simplex {
|
|||
int m_col_idx;
|
||||
int m_next_free_row_entry_idx;
|
||||
};
|
||||
_row_entry(numeral const & c, var_t v): row_entry(c, v), m_col_idx(0) {}
|
||||
_row_entry(numeral && c, var_t v) : row_entry(std::move(c), v), m_col_idx(0) {}
|
||||
_row_entry() : row_entry(numeral(), dead_id), m_col_idx(0) {}
|
||||
bool is_dead() const { return row_entry::m_var == dead_id; }
|
||||
};
|
||||
|
|
|
@ -739,7 +739,7 @@ void context_t<C>::del_sum(polynomial * p) {
|
|||
|
||||
template<typename C>
|
||||
var context_t<C>::mk_sum(numeral const & c, unsigned sz, numeral const * as, var const * xs) {
|
||||
m_num_buffer.reserve(num_vars(), numeral());
|
||||
m_num_buffer.reserve(num_vars());
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
SASSERT(xs[i] < num_vars());
|
||||
nm().set(m_num_buffer[xs[i]], as[i]);
|
||||
|
|
|
@ -117,7 +117,7 @@ bool func_interp::is_fi_entry_expr(expr * e, ptr_vector<expr> & args) {
|
|||
(m_arity > 1 && (!m().is_and(c) || to_app(c)->get_num_args() != m_arity)))
|
||||
return false;
|
||||
|
||||
args.resize(m_arity, 0);
|
||||
args.resize(m_arity);
|
||||
for (unsigned i = 0; i < m_arity; i++) {
|
||||
expr * ci = (m_arity == 1 && i == 0) ? c : to_app(c)->get_arg(i);
|
||||
|
||||
|
|
|
@ -128,7 +128,7 @@ namespace datalog {
|
|||
void set_reg(reg_idx i, reg_type val) {
|
||||
if (i >= m_registers.size()) {
|
||||
check_overflow(i);
|
||||
m_registers.resize(i+1,0);
|
||||
m_registers.resize(i+1);
|
||||
}
|
||||
if (m_registers[i]) {
|
||||
m_registers[i]->deallocate();
|
||||
|
|
|
@ -465,7 +465,7 @@ namespace datalog {
|
|||
|
||||
unsigned sz = r.get_signature().size();
|
||||
ptr_vector<expr> subst_arg;
|
||||
subst_arg.resize(sz, 0);
|
||||
subst_arg.resize(sz);
|
||||
unsigned ofs = sz-1;
|
||||
for (unsigned i=0; i<sz; i++) {
|
||||
SASSERT(!r.is_undefined(i) || !contains_var(m_new_rule, i));
|
||||
|
|
|
@ -1272,7 +1272,7 @@ namespace qe {
|
|||
family_id fid = p->get_family_id();
|
||||
SASSERT(fid != null_family_id);
|
||||
if (static_cast<int>(m_plugins.size()) <= fid) {
|
||||
m_plugins.resize(fid+1,0);
|
||||
m_plugins.resize(fid+1);
|
||||
}
|
||||
SASSERT(!m_plugins[fid]);
|
||||
m_plugins[fid] = p;
|
||||
|
|
|
@ -1999,7 +1999,7 @@ namespace smt {
|
|||
m_ast_manager(ctx.get_manager()),
|
||||
m_mam(m),
|
||||
m_use_filters(use_filters) {
|
||||
m_args.resize(INIT_ARGS_SIZE, 0);
|
||||
m_args.resize(INIT_ARGS_SIZE);
|
||||
}
|
||||
|
||||
~interpreter() {
|
||||
|
|
|
@ -1286,7 +1286,7 @@ namespace smt {
|
|||
else {
|
||||
if (depth >= m_almost_cg_tables.size()) {
|
||||
unsigned old_sz = m_almost_cg_tables.size();
|
||||
m_almost_cg_tables.resize(depth+1, 0);
|
||||
m_almost_cg_tables.resize(depth+1);
|
||||
for (unsigned i = old_sz; i < depth + 1; i++)
|
||||
m_almost_cg_tables[i] = alloc(almost_cg_table);
|
||||
}
|
||||
|
|
|
@ -617,8 +617,8 @@ namespace smt {
|
|||
m_else_values.reset();
|
||||
m_parents.reset();
|
||||
m_parents.resize(num_vars, -1);
|
||||
m_defaults.resize(num_vars, 0);
|
||||
m_else_values.resize(num_vars, 0);
|
||||
m_defaults.resize(num_vars);
|
||||
m_else_values.resize(num_vars);
|
||||
|
||||
if (m_use_unspecified_default)
|
||||
return;
|
||||
|
|
|
@ -620,7 +620,7 @@ namespace smt {
|
|||
sort * s = recognizer->get_decl()->get_domain(0);
|
||||
if (d->m_recognizers.empty()) {
|
||||
SASSERT(m_util.is_datatype(s));
|
||||
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), 0);
|
||||
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
|
||||
}
|
||||
SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
|
||||
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());
|
||||
|
|
|
@ -914,6 +914,8 @@ namespace smt {
|
|||
}
|
||||
verbose_stream() << " + " << m_objective_consts[v] << "\n";);
|
||||
|
||||
unsynch_mpq_manager mgr;
|
||||
unsynch_mpq_inf_manager inf_mgr;
|
||||
unsigned num_nodes = get_num_vars();
|
||||
unsigned num_edges = m_edges.size();
|
||||
S.ensure_var(num_nodes + num_edges + m_objectives.size());
|
||||
|
@ -921,8 +923,9 @@ namespace smt {
|
|||
numeral const& a = m_assignment[i];
|
||||
rational fin = a.get_rational().to_rational();
|
||||
rational inf = a.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(), inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_value(i, q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
for (unsigned i = 0; i < num_nodes; ++i) {
|
||||
enode * n = get_enode(i);
|
||||
|
@ -933,7 +936,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
svector<unsigned> vars;
|
||||
unsynch_mpq_manager mgr;
|
||||
scoped_mpq_vector coeffs(mgr);
|
||||
coeffs.push_back(mpq(1));
|
||||
coeffs.push_back(mpq(-1));
|
||||
|
@ -954,8 +956,9 @@ namespace smt {
|
|||
numeral const& w = e.m_offset;
|
||||
rational fin = w.get_rational().to_rational();
|
||||
rational inf = w.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(),inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_upper(base_var, q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
unsigned w = num_nodes + num_edges + v;
|
||||
|
||||
|
|
|
@ -1107,6 +1107,8 @@ unsigned theory_diff_logic<Ext>::simplex2edge(unsigned e) {
|
|||
|
||||
template<typename Ext>
|
||||
void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
||||
unsynch_mpq_manager mgr;
|
||||
unsynch_mpq_inf_manager inf_mgr;
|
||||
unsigned num_nodes = m_graph.get_num_nodes();
|
||||
vector<dl_edge<GExt> > const& es = m_graph.get_all_edges();
|
||||
S.ensure_var(num_simplex_vars());
|
||||
|
@ -1114,13 +1116,13 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
|||
numeral const& a = m_graph.get_assignment(i);
|
||||
rational fin = a.get_rational().to_rational();
|
||||
rational inf = a.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(), inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_value(node2simplex(i), q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
S.set_lower(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
|
||||
S.set_upper(node2simplex(get_zero()), mpq_inf(mpq(0), mpq(0)));
|
||||
svector<unsigned> vars;
|
||||
unsynch_mpq_manager mgr;
|
||||
scoped_mpq_vector coeffs(mgr);
|
||||
coeffs.push_back(mpq(1));
|
||||
coeffs.push_back(mpq(-1));
|
||||
|
@ -1145,8 +1147,9 @@ void theory_diff_logic<Ext>::update_simplex(Simplex& S) {
|
|||
numeral const& w = e.get_weight();
|
||||
rational fin = w.get_rational().to_rational();
|
||||
rational inf = w.get_infinitesimal().to_rational();
|
||||
mpq_inf q(fin.to_mpq(),inf.to_mpq());
|
||||
mpq_inf q(mgr.dup(fin.to_mpq()), mgr.dup(inf.to_mpq()));
|
||||
S.set_upper(base_var, q);
|
||||
inf_mgr.del(q);
|
||||
}
|
||||
else {
|
||||
S.unset_upper(base_var);
|
||||
|
|
|
@ -806,8 +806,9 @@ namespace smt {
|
|||
if (c != 0) {
|
||||
if (m_enable_simplex) {
|
||||
row_info const& info = m_ineq_row_info.find(v);
|
||||
unsynch_mpq_manager mgr;
|
||||
scoped_eps_numeral coeff(m_mpq_inf_mgr);
|
||||
coeff = std::make_pair(info.m_bound.to_mpq(), mpq(0));
|
||||
coeff = std::make_pair(mgr.dup(info.m_bound.to_mpq()), mpq(0));
|
||||
unsigned slack = info.m_slack;
|
||||
if (is_true) {
|
||||
update_bound(slack, literal(v), true, coeff);
|
||||
|
|
|
@ -279,7 +279,6 @@ namespace smt {
|
|||
//
|
||||
void compile_ineq(ineq& c);
|
||||
void inc_propagations(ineq& c);
|
||||
unsigned get_compilation_threshold(ineq& c);
|
||||
|
||||
//
|
||||
// Conflict resolution, cutting plane derivation.
|
||||
|
|
|
@ -238,7 +238,7 @@ bool bvsls_opt_engine::what_if(
|
|||
|
||||
mpz bvsls_opt_engine::find_best_move(
|
||||
ptr_vector<func_decl> & to_evaluate,
|
||||
mpz score,
|
||||
mpz & score,
|
||||
unsigned & best_const,
|
||||
mpz & best_value,
|
||||
unsigned & new_bit,
|
||||
|
|
|
@ -61,7 +61,7 @@ protected:
|
|||
bool what_if(func_decl * fd, const unsigned & fd_inx, const mpz & temp,
|
||||
mpz & best_score, unsigned & best_const, mpz & best_value);
|
||||
|
||||
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz score,
|
||||
mpz find_best_move(ptr_vector<func_decl> & to_evaluate, mpz & score,
|
||||
unsigned & best_const, mpz & best_value, unsigned & new_bit, move_type & move,
|
||||
mpz const & max_score, expr * objective);
|
||||
|
||||
|
|
|
@ -41,7 +41,20 @@ class sls_tracker {
|
|||
|
||||
struct value_score {
|
||||
value_score() : m(0), value(unsynch_mpz_manager::mk_z(0)), score(0.0), score_prune(0.0), has_pos_occ(0), has_neg_occ(0), distance(0), touched(1) {};
|
||||
value_score(value_score && other) :
|
||||
m(other.m),
|
||||
value(std::move(other.value)),
|
||||
score(other.score),
|
||||
score_prune(other.score_prune),
|
||||
has_pos_occ(other.has_pos_occ),
|
||||
has_neg_occ(other.has_neg_occ),
|
||||
distance(other.distance),
|
||||
touched(other.touched) {}
|
||||
~value_score() { if (m) m->del(value); }
|
||||
void operator=(value_score && other) {
|
||||
this->~value_score();
|
||||
new (this) value_score(std::move(other));
|
||||
}
|
||||
unsynch_mpz_manager * m;
|
||||
mpz value;
|
||||
double score;
|
||||
|
@ -50,15 +63,6 @@ class sls_tracker {
|
|||
unsigned has_neg_occ;
|
||||
unsigned distance; // max distance from any root
|
||||
unsigned touched;
|
||||
value_score & operator=(const value_score & other) {
|
||||
SASSERT(m == 0 || m == other.m);
|
||||
if (m) m->set(value, 0); else m = other.m;
|
||||
m->set(value, other.value);
|
||||
score = other.score;
|
||||
distance = other.distance;
|
||||
touched = other.touched;
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
public:
|
||||
|
@ -294,7 +298,7 @@ public:
|
|||
if (!m_scores.contains(n)) {
|
||||
value_score vs;
|
||||
vs.m = & m_mpz_manager;
|
||||
m_scores.insert(n, vs);
|
||||
m_scores.insert(n, std::move(vs));
|
||||
}
|
||||
|
||||
// Update uplinks
|
||||
|
@ -539,7 +543,7 @@ public:
|
|||
rational r_val;
|
||||
unsigned bv_sz;
|
||||
m_bv_util.is_numeral(val, r_val, bv_sz);
|
||||
mpq q = r_val.to_mpq();
|
||||
const mpq& q = r_val.to_mpq();
|
||||
SASSERT(m_mpz_manager.is_one(q.denominator()));
|
||||
set_value(fd, q.numerator());
|
||||
}
|
||||
|
@ -630,7 +634,7 @@ public:
|
|||
if (m_bv_util.is_bv_sort(s))
|
||||
return get_random_bv(s);
|
||||
else if (m_manager.is_bool(s))
|
||||
return get_random_bool();
|
||||
return m_mpz_manager.dup(get_random_bool());
|
||||
else
|
||||
NOT_IMPLEMENTED_YET(); // This only works for bit-vectors for now.
|
||||
}
|
||||
|
@ -653,9 +657,7 @@ public:
|
|||
TRACE("sls", tout << "Abandoned model:" << std::endl; show_model(tout); );
|
||||
|
||||
for (entry_point_type::iterator it = m_entry_points.begin(); it != m_entry_points.end(); it++) {
|
||||
mpz temp = m_zero;
|
||||
set_value(it->m_value, temp);
|
||||
m_mpz_manager.del(temp);
|
||||
set_value(it->m_value, m_zero);
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -931,7 +933,7 @@ public:
|
|||
rational q;
|
||||
if (!m_bv_util.is_numeral(n, q, bv_sz))
|
||||
NOT_IMPLEMENTED_YET();
|
||||
mpq temp = q.to_mpq();
|
||||
const mpq& temp = q.to_mpq();
|
||||
SASSERT(m_mpz_manager.is_one(temp.denominator()));
|
||||
m_mpz_manager.set(result, temp.numerator());
|
||||
}
|
||||
|
@ -1039,7 +1041,6 @@ public:
|
|||
unsigned pos = -1;
|
||||
if (m_ucb)
|
||||
{
|
||||
value_score vscore;
|
||||
double max = -1.0;
|
||||
// Andreas: Commented things here might be used for track_unsat data structures as done in SLS for SAT. But seems to have no benefit.
|
||||
/* for (unsigned i = 0; i < m_where_false.size(); i++) {
|
||||
|
@ -1048,7 +1049,7 @@ public:
|
|||
expr * e = as[i];
|
||||
if (m_mpz_manager.neq(get_value(e), m_one))
|
||||
{
|
||||
vscore = m_scores.find(e);
|
||||
value_score & vscore = m_scores.find(e);
|
||||
// Andreas: Select the assertion with the greatest ucb score. Potentially add some noise.
|
||||
// double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched);
|
||||
double q = vscore.score + m_ucb_constant * sqrt(log((double)m_touched) / vscore.touched) + m_ucb_noise * get_random_uint(8);
|
||||
|
|
|
@ -149,6 +149,13 @@ public:
|
|||
new (m_buffer + m_pos) T(elem);
|
||||
m_pos++;
|
||||
}
|
||||
|
||||
void push_back(T && elem) {
|
||||
if (m_pos >= m_capacity)
|
||||
expand();
|
||||
new (m_buffer + m_pos) T(std::move(elem));
|
||||
m_pos++;
|
||||
}
|
||||
|
||||
void pop_back() {
|
||||
if (CallDestructors) {
|
||||
|
|
|
@ -54,7 +54,7 @@ public:
|
|||
bool is_used() const { return m_state == HT_USED; }
|
||||
T & get_data() { return m_data; }
|
||||
const T & get_data() const { return m_data; }
|
||||
void set_data(const T & d) { m_data = d; m_state = HT_USED; }
|
||||
void set_data(T && d) { m_data = std::move(d); m_state = HT_USED; }
|
||||
void set_hash(unsigned h) { m_hash = h; }
|
||||
void mark_as_deleted() { m_state = HT_DELETED; }
|
||||
void mark_as_free() { m_state = HT_FREE; }
|
||||
|
@ -187,10 +187,42 @@ protected:
|
|||
}
|
||||
}
|
||||
|
||||
static void move_table(entry * source, unsigned source_capacity, entry * target, unsigned target_capacity) {
|
||||
SASSERT(target_capacity >= source_capacity);
|
||||
unsigned target_mask = target_capacity - 1;
|
||||
entry * source_end = source + source_capacity;
|
||||
entry * target_end = target + target_capacity;
|
||||
for (entry * source_curr = source; source_curr != source_end; ++source_curr) {
|
||||
if (source_curr->is_used()) {
|
||||
unsigned hash = source_curr->get_hash();
|
||||
unsigned idx = hash & target_mask;
|
||||
entry * target_begin = target + idx;
|
||||
entry * target_curr = target_begin;
|
||||
for (; target_curr != target_end; ++target_curr) {
|
||||
SASSERT(!target_curr->is_deleted());
|
||||
if (target_curr->is_free()) {
|
||||
*target_curr = std::move(*source_curr);
|
||||
goto end;
|
||||
}
|
||||
}
|
||||
for (target_curr = target; target_curr != target_begin; ++target_curr) {
|
||||
SASSERT(!target_curr->is_deleted());
|
||||
if (target_curr->is_free()) {
|
||||
*target_curr = std::move(*source_curr);
|
||||
goto end;
|
||||
}
|
||||
}
|
||||
UNREACHABLE();
|
||||
end:
|
||||
;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void expand_table() {
|
||||
unsigned new_capacity = m_capacity << 1;
|
||||
entry * new_table = alloc_table(new_capacity);
|
||||
copy_table(m_table, m_capacity, new_table, new_capacity);
|
||||
move_table(m_table, m_capacity, new_table, new_capacity);
|
||||
delete_table();
|
||||
m_table = new_table;
|
||||
m_capacity = new_capacity;
|
||||
|
@ -202,7 +234,7 @@ protected:
|
|||
if (memory::is_out_of_memory())
|
||||
return;
|
||||
entry * new_table = alloc_table(m_capacity);
|
||||
copy_table(m_table, m_capacity, new_table, m_capacity);
|
||||
move_table(m_table, m_capacity, new_table, m_capacity);
|
||||
delete_table();
|
||||
m_table = new_table;
|
||||
m_num_deleted = 0;
|
||||
|
@ -321,7 +353,7 @@ public:
|
|||
#define INSERT_LOOP_BODY() { \
|
||||
if (curr->is_used()) { \
|
||||
if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \
|
||||
curr->set_data(e); \
|
||||
curr->set_data(std::move(e)); \
|
||||
return; \
|
||||
} \
|
||||
HS_CODE(m_st_collision++;); \
|
||||
|
@ -330,7 +362,7 @@ public:
|
|||
entry * new_entry; \
|
||||
if (del_entry) { new_entry = del_entry; m_num_deleted--; } \
|
||||
else { new_entry = curr; } \
|
||||
new_entry->set_data(e); \
|
||||
new_entry->set_data(std::move(e)); \
|
||||
new_entry->set_hash(hash); \
|
||||
m_size++; \
|
||||
return; \
|
||||
|
@ -342,7 +374,7 @@ public:
|
|||
} \
|
||||
} ((void) 0)
|
||||
|
||||
void insert(data const & e) {
|
||||
void insert(data && e) {
|
||||
if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
|
||||
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
|
||||
expand_table();
|
||||
|
@ -363,6 +395,11 @@ public:
|
|||
UNREACHABLE();
|
||||
}
|
||||
|
||||
void insert(const data & e) {
|
||||
data tmp(e);
|
||||
insert(std::move(tmp));
|
||||
}
|
||||
|
||||
#define INSERT_LOOP_CORE_BODY() { \
|
||||
if (curr->is_used()) { \
|
||||
if (curr->get_hash() == hash && equals(curr->get_data(), e)) { \
|
||||
|
@ -375,7 +412,7 @@ public:
|
|||
entry * new_entry; \
|
||||
if (del_entry) { new_entry = del_entry; m_num_deleted--; } \
|
||||
else { new_entry = curr; } \
|
||||
new_entry->set_data(e); \
|
||||
new_entry->set_data(std::move(e)); \
|
||||
new_entry->set_hash(hash); \
|
||||
m_size++; \
|
||||
et = new_entry; \
|
||||
|
@ -393,7 +430,7 @@ public:
|
|||
Return true if it is a new element, and false otherwise.
|
||||
Store the entry/slot of the table in et.
|
||||
*/
|
||||
bool insert_if_not_there_core(data const & e, entry * & et) {
|
||||
bool insert_if_not_there_core(data && e, entry * & et) {
|
||||
if ((m_size + m_num_deleted) << 2 > (m_capacity * 3)) {
|
||||
// if ((m_size + m_num_deleted) * 2 > (m_capacity)) {
|
||||
expand_table();
|
||||
|
@ -415,6 +452,11 @@ public:
|
|||
return 0;
|
||||
}
|
||||
|
||||
bool insert_if_not_there_core(const data & e, entry * & et) {
|
||||
data temp(e);
|
||||
return insert_if_not_there_core(std::move(temp), et);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Insert the element e if it is not in the table.
|
||||
Return a reference to e or to an object identical to e
|
||||
|
|
|
@ -31,11 +31,10 @@ class mpq {
|
|||
public:
|
||||
mpq(int v):m_num(v), m_den(1) {}
|
||||
mpq():m_den(1) {}
|
||||
mpq(mpq && other) noexcept : m_num(std::move(other.m_num)), m_den(std::move(other.m_den)) {}
|
||||
void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
|
||||
mpz const & numerator() const { return m_num; }
|
||||
mpz const & denominator() const { return m_den; }
|
||||
|
||||
double get_double() const;
|
||||
};
|
||||
|
||||
inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
|
||||
|
@ -745,6 +744,12 @@ public:
|
|||
reset_denominator(a);
|
||||
}
|
||||
|
||||
mpq dup(const mpq & source) {
|
||||
mpq temp;
|
||||
set(temp, source);
|
||||
return temp;
|
||||
}
|
||||
|
||||
void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
|
||||
|
||||
void swap(mpq & a, mpq & b) {
|
||||
|
|
|
@ -94,6 +94,9 @@ class mpz {
|
|||
public:
|
||||
mpz(int v):m_val(v), m_ptr(0) {}
|
||||
mpz():m_val(0), m_ptr(0) {}
|
||||
mpz(mpz && other) noexcept : m_val(other.m_val), m_ptr(0) {
|
||||
std::swap(m_val, other.m_val);
|
||||
}
|
||||
void swap(mpz & other) {
|
||||
std::swap(m_val, other.m_val);
|
||||
std::swap(m_ptr, other.m_ptr);
|
||||
|
@ -668,6 +671,12 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void set(mpz & target, mpz && source) {
|
||||
del(target);
|
||||
target.m_val = source.m_val;
|
||||
std::swap(target.m_ptr, source.m_ptr);
|
||||
}
|
||||
|
||||
void set(mpz & a, int val) {
|
||||
del(a);
|
||||
a.m_val = val;
|
||||
|
@ -700,6 +709,12 @@ public:
|
|||
|
||||
void set(mpz & target, unsigned sz, digit_t const * digits);
|
||||
|
||||
mpz dup(const mpz & source) {
|
||||
mpz temp;
|
||||
set(temp, source);
|
||||
return temp;
|
||||
}
|
||||
|
||||
void reset(mpz & a) {
|
||||
del(a);
|
||||
a.m_val = 0;
|
||||
|
|
|
@ -69,6 +69,10 @@ public:
|
|||
m_key(k),
|
||||
m_value(v) {
|
||||
}
|
||||
key_data(Key * k, Value && v) :
|
||||
m_key(k),
|
||||
m_value(std::move(v)) {
|
||||
}
|
||||
Value const & get_value() const { return m_value; }
|
||||
Key & get_key () const { return *m_key; }
|
||||
unsigned hash() const { return m_key->hash(); }
|
||||
|
@ -86,7 +90,7 @@ public:
|
|||
bool is_used() const { return m_data.m_key != reinterpret_cast<Key *>(0) && m_data.m_key != reinterpret_cast<Key *>(1); }
|
||||
key_data const & get_data() const { return m_data; }
|
||||
key_data & get_data() { return m_data; }
|
||||
void set_data(key_data const & d) { m_data = d; }
|
||||
void set_data(key_data && d) { m_data = std::move(d); }
|
||||
void set_hash(unsigned h) { SASSERT(h == m_data.hash()); }
|
||||
void mark_as_deleted() { m_data.m_key = reinterpret_cast<Key *>(1); }
|
||||
void mark_as_free() { m_data.m_key = 0; }
|
||||
|
@ -137,6 +141,10 @@ public:
|
|||
void insert(Key * const k, Value const & v) {
|
||||
m_table.insert(key_data(k, v));
|
||||
}
|
||||
|
||||
void insert(Key * const k, Value && v) {
|
||||
m_table.insert(key_data(k, std::move(v)));
|
||||
}
|
||||
|
||||
key_data const & insert_if_not_there(Key * k, Value const & v) {
|
||||
return m_table.insert_if_not_there(key_data(k, v));
|
||||
|
|
|
@ -63,7 +63,7 @@ public:
|
|||
void resize(unsigned sz) {
|
||||
if (sz < m_nodes.size())
|
||||
dec_range_ref(m_nodes.begin() + sz, m_nodes.end());
|
||||
m_nodes.resize(sz, 0);
|
||||
m_nodes.resize(sz);
|
||||
}
|
||||
|
||||
void resize(unsigned sz, T * d) {
|
||||
|
@ -80,7 +80,7 @@ public:
|
|||
void reserve(unsigned sz) {
|
||||
if (sz <= m_nodes.size())
|
||||
return;
|
||||
m_nodes.resize(sz, 0);
|
||||
m_nodes.resize(sz);
|
||||
}
|
||||
|
||||
void shrink(unsigned sz) {
|
||||
|
|
|
@ -63,8 +63,7 @@ public:
|
|||
unsigned old_sz = this->size();
|
||||
if (sz <= old_sz)
|
||||
shrink(sz);
|
||||
typename Manager::numeral zero(0);
|
||||
svector<typename Manager::numeral>::resize(sz, zero);
|
||||
svector<typename Manager::numeral>::resize(sz, 0);
|
||||
}
|
||||
};
|
||||
|
||||
|
|
|
@ -322,7 +322,7 @@ bool compare_arrays(const T * array1, const T * array2, unsigned size) {
|
|||
template<typename T>
|
||||
void force_ptr_array_size(T & v, unsigned sz) {
|
||||
if (sz > v.size()) {
|
||||
v.resize(sz, 0);
|
||||
v.resize(sz);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
|
@ -26,6 +26,7 @@ Revision History:
|
|||
|
||||
#include "util/debug.h"
|
||||
#include<algorithm>
|
||||
#include<type_traits>
|
||||
#include<memory.h>
|
||||
#include "util/memory_manager.h"
|
||||
#include "util/hash.h"
|
||||
|
@ -74,9 +75,24 @@ class vector {
|
|||
if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
|
||||
throw default_exception("Overflow encountered when expanding vector");
|
||||
}
|
||||
SZ *mem = (SZ*)memory::reallocate(reinterpret_cast<SZ*>(m_data)-2, new_capacity_T);
|
||||
SZ *mem, *old_mem = reinterpret_cast<SZ*>(m_data) - 2;
|
||||
if (std::is_trivially_copyable<T>::value) {
|
||||
mem = (SZ*)memory::reallocate(old_mem, new_capacity_T);
|
||||
} else {
|
||||
mem = (SZ*)memory::allocate(new_capacity_T);
|
||||
}
|
||||
auto old_data = m_data;
|
||||
auto old_size = size();
|
||||
*mem = new_capacity;
|
||||
m_data = reinterpret_cast<T *>(mem + 2);
|
||||
if (!std::is_trivially_copyable<T>::value) {
|
||||
static_assert(std::is_move_constructible<T>::value, "");
|
||||
int i = 0;
|
||||
for (auto I = old_data; I != old_data + old_size; ++I) {
|
||||
new (&m_data[i++]) T(std::move(*I));
|
||||
}
|
||||
memory::deallocate(old_mem);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -148,6 +164,10 @@ public:
|
|||
SASSERT(size() == source.size());
|
||||
}
|
||||
|
||||
vector(vector&& other) noexcept : m_data(0) {
|
||||
std::swap(m_data, other.m_data);
|
||||
}
|
||||
|
||||
vector(SZ s, T const * data):
|
||||
m_data(0) {
|
||||
for (SZ i = 0; i < s; i++) {
|
||||
|
@ -179,6 +199,16 @@ public:
|
|||
return *this;
|
||||
}
|
||||
|
||||
vector & operator=(vector && source) {
|
||||
if (this == &source) {
|
||||
return *this;
|
||||
}
|
||||
destroy();
|
||||
m_data = 0;
|
||||
std::swap(m_data, source.m_data);
|
||||
return *this;
|
||||
}
|
||||
|
||||
void reset() {
|
||||
if (m_data) {
|
||||
if (CallDestructors) {
|
||||
|
@ -292,6 +322,11 @@ public:
|
|||
m_data[idx] = val;
|
||||
}
|
||||
|
||||
void set(SZ idx, T && val) {
|
||||
SASSERT(idx < size());
|
||||
m_data[idx] = std::move(val);
|
||||
}
|
||||
|
||||
T & back() {
|
||||
SASSERT(!empty());
|
||||
return operator[](size() - 1);
|
||||
|
@ -318,6 +353,14 @@ public:
|
|||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
|
||||
}
|
||||
|
||||
void push_back(T && elem) {
|
||||
if (m_data == 0 || reinterpret_cast<SZ *>(m_data)[SIZE_IDX] == reinterpret_cast<SZ *>(m_data)[CAPACITY_IDX]) {
|
||||
expand_vector();
|
||||
}
|
||||
new (m_data + reinterpret_cast<SZ *>(m_data)[SIZE_IDX]) T(std::move(elem));
|
||||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX]++;
|
||||
}
|
||||
|
||||
void insert(T const & elem) {
|
||||
push_back(elem);
|
||||
}
|
||||
|
@ -357,7 +400,8 @@ public:
|
|||
}
|
||||
}
|
||||
|
||||
void resize(SZ s, T const & elem=T()) {
|
||||
template<typename Args>
|
||||
void resize(SZ s, Args args...) {
|
||||
SZ sz = size();
|
||||
if (s <= sz) { shrink(s); return; }
|
||||
while (s > capacity()) {
|
||||
|
@ -367,8 +411,23 @@ public:
|
|||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
|
||||
iterator it = m_data + sz;
|
||||
iterator end = m_data + s;
|
||||
for(; it != end; ++it) {
|
||||
new (it) T(elem);
|
||||
for (; it != end; ++it) {
|
||||
new (it) T(std::forward<Args>(args));
|
||||
}
|
||||
}
|
||||
|
||||
void resize(SZ s) {
|
||||
SZ sz = size();
|
||||
if (s <= sz) { shrink(s); return; }
|
||||
while (s > capacity()) {
|
||||
expand_vector();
|
||||
}
|
||||
SASSERT(m_data != 0);
|
||||
reinterpret_cast<SZ *>(m_data)[SIZE_IDX] = s;
|
||||
iterator it = m_data + sz;
|
||||
iterator end = m_data + s;
|
||||
for (; it != end; ++it) {
|
||||
new (it) T();
|
||||
}
|
||||
}
|
||||
|
||||
|
@ -439,10 +498,15 @@ public:
|
|||
return m_data[idx];
|
||||
}
|
||||
|
||||
void reserve(SZ s, T const & d = T()) {
|
||||
void reserve(SZ s, T const & d) {
|
||||
if (s > size())
|
||||
resize(s, d);
|
||||
}
|
||||
|
||||
void reserve(SZ s) {
|
||||
if (s > size())
|
||||
resize(s);
|
||||
}
|
||||
};
|
||||
|
||||
template<typename T>
|
||||
|
@ -452,7 +516,12 @@ public:
|
|||
ptr_vector(unsigned s):vector<T *, false>(s) {}
|
||||
ptr_vector(unsigned s, T * elem):vector<T *, false>(s, elem) {}
|
||||
ptr_vector(ptr_vector const & source):vector<T *, false>(source) {}
|
||||
ptr_vector(ptr_vector && other) noexcept : vector<T*, false>(std::move(other)) {}
|
||||
ptr_vector(unsigned s, T * const * data):vector<T *, false>(s, const_cast<T**>(data)) {}
|
||||
ptr_vector & operator=(ptr_vector const & source) {
|
||||
vector<T *, false>::operator=(source);
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
template<typename T, typename SZ = unsigned>
|
||||
|
@ -462,7 +531,12 @@ public:
|
|||
svector(SZ s):vector<T, false, SZ>(s) {}
|
||||
svector(SZ s, T const & elem):vector<T, false, SZ>(s, elem) {}
|
||||
svector(svector const & source):vector<T, false, SZ>(source) {}
|
||||
svector(svector && other) noexcept : vector<T, false, SZ>(std::move(other)) {}
|
||||
svector(SZ s, T const * data):vector<T, false, SZ>(s, data) {}
|
||||
svector & operator=(svector const & source) {
|
||||
vector<T, false, SZ>::operator=(source);
|
||||
return *this;
|
||||
}
|
||||
};
|
||||
|
||||
typedef svector<int> int_vector;
|
||||
|
@ -494,23 +568,4 @@ struct vector_hash : public vector_hash_tpl<Hash, vector<typename Hash::data> >
|
|||
template<typename Hash>
|
||||
struct svector_hash : public vector_hash_tpl<Hash, svector<typename Hash::data> > {};
|
||||
|
||||
#include <vector>
|
||||
// Specialize vector<std::string> to be an instance of std::vector instead.
|
||||
// This will catch any regression of issue #564 and #420.
|
||||
|
||||
template <>
|
||||
class vector<std::string, true, unsigned> : public std::vector<std::string> {
|
||||
public:
|
||||
vector(vector<std::string, true, unsigned> const& other): std::vector<std::string>(other) {}
|
||||
vector(size_t sz, char const* s): std::vector<std::string>(sz, s) {}
|
||||
vector() {}
|
||||
|
||||
void reset() { clear(); }
|
||||
|
||||
|
||||
};
|
||||
|
||||
|
||||
|
||||
#endif /* VECTOR_H_ */
|
||||
|
||||
|
|
Loading…
Reference in a new issue