mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-31 16:33:18 +00:00
Code Activity

nits, add local functions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-08 18:53:04 -07:00
parent 3df12a641f
commit f4a6c0df3e
4 changed files with 17 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/ast/for_each_expr.cpp
View file

@ -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_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::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::begin() const { return iterator(* this, m_esp, m_vp, true); }
subterms::iterator subterms::end() { return iterator(*this, nullptr, nullptr, false); } subterms::iterator subterms::end() const { 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::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) if (!esp)
m_esp = &m_es; m_esp = &m_es;
else else

6
src/ast/for_each_expr.h
View file

@ -186,7 +186,7 @@ public:
expr_mark m_visited; expr_mark m_visited;
expr_mark* m_visitedp = nullptr; expr_mark* m_visitedp = nullptr;
public: 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*(); expr* operator*();
iterator operator++(int); iterator operator++(int);
iterator& operator++(); 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 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 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); } 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 begin() const;
iterator end(); iterator end() const;
}; };
class subterms_postorder { class subterms_postorder {

15
src/sat/smt/synth_solver.cpp
View file

@ -37,15 +37,18 @@ namespace synth {
auto * n = expr2enode(e->get_arg(0)); auto * n = expr2enode(e->get_arg(0));
expr_ref_vector repr(m); expr_ref_vector repr(m);
euf::enode_vector todo;
auto has_rep = [&](euf::enode* n) { return !!repr.get(n->get_root_id(), nullptr); };
auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); }; auto get_rep = [&](euf::enode* n) { return repr.get(n->get_root_id(), nullptr); };
auto has_rep = [&](euf::enode* n) { return !!get_rep(n); };
auto set_rep = [&](euf::enode* n, expr* e) { repr.setx(n->get_root_id(), e); };
euf::enode_vector todo;
for (unsigned i = 1; i < e->get_num_args(); ++i) { for (unsigned i = 1; i < e->get_num_args(); ++i) {
expr * arg = e->get_arg(i); expr * arg = e->get_arg(i);
auto * narg = expr2enode(arg); auto * narg = expr2enode(arg);
todo.push_back(narg); todo.push_back(narg);
repr.setx(narg->get_root_id(), arg); set_rep(narg, arg);
} }
for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) { for (unsigned i = 0; i < todo.size() && !has_rep(n); ++i) {
auto * nn = todo[i]; auto * nn = todo[i];
for (auto * p : euf::enode_parents(nn)) { for (auto * p : euf::enode_parents(nn)) {
@ -56,8 +59,8 @@ namespace synth {
for (auto * ch : euf::enode_args(p)) for (auto * ch : euf::enode_args(p))
args.push_back(get_rep(ch)); args.push_back(get_rep(ch));
app * papp = m.mk_app(p->get_decl(), args); app * papp = m.mk_app(p->get_decl(), args);
repr.setx(p->get_root_id(), papp); set_rep(p, papp);
todo.push_back(p); todo.push_back(p);
} }
} }
} }

4
src/util/util.h
View file

@ -363,7 +363,7 @@ void set_fatal_error_handler(void (*pfn)(int error_code));
template<typename S, typename T> 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) for (auto const& s : set)
if (p(s)) if (p(s))
return true; return true;
@ -371,7 +371,7 @@ bool any_of(S& set, T const& p) {
} }
template<typename S, typename T> 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) for (auto const& s : set)
if (!p(s)) if (!p(s))
return false; return false;