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

make it easier to iterate over arguments of an application

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-02 09:51:59 -07:00
parent e9a4a9a390
commit 55285b2193
2 changed files with 35 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/api/c++/z3++.h
View file

@ -1495,6 +1495,26 @@ namespace z3 {
*/
expr substitute(expr_vector const& dst);
class iterator {
expr& e;
unsigned i;
public:
iterator(expr& e, unsigned i): e(e), i(i) {}
bool operator==(iterator const& other) noexcept {
return i == other.i;
}
bool operator!=(iterator const& other) noexcept {
return i != other.i;
}
expr operator*() const { return e.arg(i); }
iterator& operator++() { ++i; return *this; }
iterator operator++(int) { assert(false); return *this; }
};
iterator begin() { return iterator(*this, 0); }
iterator end() { return iterator(*this, is_app() ? num_args() : 0); }
};
#define _Z3_MK_BIN_(a, b, binop) \