mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

use portable ptr-initializer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-07-15 11:00:33 -07:00
parent f00f92c3b2
commit 5a9161ed7b
5 changed files with 18 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/sls/sat_ddfw.h
View file

@ -270,11 +270,12 @@ namespace sat {
inline unsigned num_vars() const { return m_vars.size(); }
std::initializer_list<unsigned> use_list(literal lit) {
ptr_iterator<unsigned> use_list(literal lit) {
unsigned i = lit.index();
auto const* b = m_flat_use_list.data() + m_use_list_index[i];
auto const* e = m_flat_use_list.data() + m_use_list_index[i + 1];
return std::initializer_list(b, e);
return { b, e };
}
};

6
src/ast/sls/sls_context.h
View file

@ -52,13 +52,13 @@ namespace sls {
virtual void set_value(expr* e, expr* v) = 0;
};
using clause = std::initializer_list <sat::literal>;
using clause = ptr_iterator<sat::literal>;
class sat_solver_context {
public:
virtual vector<sat::clause_info> const& clauses() const = 0;
virtual sat::clause_info const& get_clause(unsigned idx) const = 0;
virtual std::initializer_list<unsigned> get_use_list(sat::literal lit) = 0;
virtual ptr_iterator<unsigned> get_use_list(sat::literal lit) = 0;
virtual void flip(sat::bool_var v) = 0;
virtual double reward(sat::bool_var v) = 0;
virtual double get_weigth(unsigned clause_idx) = 0;
@ -126,7 +126,7 @@ namespace sls {
// expose sat_solver to plugins
vector<sat::clause_info> const& clauses() const { return s.clauses(); }
sat::clause_info const& get_clause(unsigned idx) const { return s.get_clause(idx); }
std::initializer_list<unsigned> get_use_list(sat::literal lit) { return s.get_use_list(lit); }
ptr_iterator<unsigned> get_use_list(sat::literal lit) { return s.get_use_list(lit); }
double get_weight(unsigned clause_idx) { return s.get_weigth(clause_idx); }
unsigned num_bool_vars() const { return s.num_vars(); }
bool is_true(sat::literal lit) { return s.is_true(lit); }

2
src/ast/sls/sls_smt_solver.cpp
View file

@ -74,7 +74,7 @@ namespace sls {
vector<sat::clause_info> const& clauses() const override { return m_ddfw.clauses(); }
sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw.get_clause_info(idx); }
std::initializer_list<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw.use_list(lit); }
void flip(sat::bool_var v) override { m_ddfw.flip(v); }
double reward(sat::bool_var v) override { return m_ddfw.get_reward(v); }
double get_weigth(unsigned clause_idx) override { return m_ddfw.get_clause_info(clause_idx).m_weight; }

2
src/sat/smt/sls_solver.cpp
View file

@ -125,7 +125,7 @@ namespace sls {
vector<sat::clause_info> const& clauses() const override { return m_ddfw->clauses(); }
sat::clause_info const& get_clause(unsigned idx) const override { return m_ddfw->get_clause_info(idx); }
std::initializer_list<unsigned> get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); }
ptr_iterator<unsigned> get_use_list(sat::literal lit) override { return m_ddfw->use_list(lit); }
void flip(sat::bool_var v) override { m_ddfw->flip(v); }
double reward(sat::bool_var v) override { return m_ddfw->get_reward(v); }
double get_weigth(unsigned clause_idx) override { return m_ddfw->get_clause_info(clause_idx).m_weight; }

10
src/util/util.h
View file

@ -326,6 +326,16 @@ void force_ptr_array_size(T & v, unsigned sz) {
}
}
template<typename T>
class ptr_iterator {
T const* b;
T const* e;
public:
ptr_iterator(T const* b, T const* e): b(b), e(e) {}
T const* begin() const { return b; }
T const* end() const { return e; }
};
class random_gen {
unsigned m_data;
public: