mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 09:34:08 +00:00
Code Activity

shorthands in enode to access args and partents

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-06 14:01:09 -07:00
parent be4edddd2b
commit 3b78bdc8e5
2 changed files with 23 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
examples/c++/example.cpp
View file

@ -927,7 +927,10 @@ void tuple_example() {
sort sorts[2] = { ctx.int_sort(), ctx.bool_sort() };
func_decl_vector projs(ctx);
func_decl pair = ctx.tuple_sort("pair", 2, names, sorts, projs);
std::cout << pair << "\n";
sorts[1] = pair.range();
func_decl pair2 = ctx.tuple_sort("pair2", 2, names, sorts, projs);
std::cout << pair2 << "\n";
}
void expr_vector_example() {

19
src/smt/smt_enode.h
View file

@ -216,6 +216,15 @@ namespace smt {
return m_args;
}
class args {
enode const& n;
public:
args(enode const& n):n(n) {}
args(enode const* n):n(*n) {}
enode_vector::const_iterator begin() const { return n.get_args(); }
enode_vector::const_iterator end() const { return n.get_args() + n.get_num_args(); }
};
// unsigned get_id() const {
// return m_id;
// }
@ -285,6 +294,16 @@ namespace smt {
return m_commutative;
}
class parents {
enode const& n;
public:
parents(enode const& _n):n(_n) {}
parents(enode const* _n):n(*_n) {}
enode_vector::const_iterator begin() const { return n.begin_parents(); }
enode_vector::const_iterator end() const { return n.end_parents(); }
};
unsigned get_num_parents() const {
return m_parents.size();
}