mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add ad-hoc any-of for cross compatibility and simplifying interface

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-04 12:48:30 -07:00
parent de9368bab0
commit 49d1490454
2 changed files with 17 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/ast/simplifiers/model_reconstruction_trail.h
View file

@ -44,7 +44,10 @@ class model_reconstruction_trail {
bool is_loose() const { return !m_removed.empty(); } bool is_loose() const { return !m_removed.empty(); }
bool intersects(ast_mark const& free_vars) const { bool intersects(ast_mark const& free_vars) const {
return std::any_of(m_subst->sub().begin(), m_subst->sub().end(), [&](auto const& kv) { return free_vars.is_marked(kv.m_key); }); for (auto const& [k, v] : m_subst->sub())
if (free_vars.is_marked(k))
return true;
return false;
} }
@ -61,8 +64,7 @@ class model_reconstruction_trail {
bool intersects(ast_mark const& free_vars, dependent_expr const& d) { bool intersects(ast_mark const& free_vars, dependent_expr const& d) {
expr_ref term(d.fml(), d.get_manager()); expr_ref term(d.fml(), d.get_manager());
auto iter = subterms::all(term); return any_of(subterms::all(term), [&](expr* t) { return free_vars.is_marked(t); });
return std::any_of(iter.begin(), iter.end(), [&](expr* t) { return free_vars.is_marked(t); });
} }
bool intersects(ast_mark const& free_vars, vector<dependent_expr> const& added) { bool intersects(ast_mark const& free_vars, vector<dependent_expr> const& added) {

13
src/util/util.h
View file

@ -25,6 +25,7 @@ Revision History:
#include<limits> #include<limits>
#include<stdint.h> #include<stdint.h>
#include <string> #include <string>
#include <functional>
#ifndef SIZE_MAX #ifndef SIZE_MAX
#define SIZE_MAX std::numeric_limits<std::size_t>::max() #define SIZE_MAX std::numeric_limits<std::size_t>::max()
@ -179,10 +180,9 @@ void display(std::ostream & out, const IT & begin, const IT & end, const char *
template<typename T> template<typename T>
struct delete_proc { struct delete_proc {
void operator()(T * ptr) { void operator()(T * ptr) {
if (ptr) { if (ptr)
dealloc(ptr); dealloc(ptr);
} }
}
}; };
void set_verbosity_level(unsigned lvl); void set_verbosity_level(unsigned lvl);
@ -360,6 +360,15 @@ void fatal_error(int error_code);
void set_fatal_error_handler(void (*pfn)(int error_code)); void set_fatal_error_handler(void (*pfn)(int error_code));
template<typename S, typename T>
bool any_of(S& set, T& p) {
for (auto const& s : set)
if (p(s))
return true;
return false;
}
// #define any_of(S, p) { for (auto const& s : S) if (p(s)) return true; return false; }
/** /**
\brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]). \brief Iterator for the [0..sz[0]) X [0..sz[1]) X ... X [0..sz[n-1]).
it contains the current value. it contains the current value.