From 3b78bdc8e5250617fe9c527c589845453852c43f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Apr 2018 14:01:09 -0700 Subject: [PATCH] shorthands in enode to access args and partents Signed-off-by: Nikolaj Bjorner --- examples/c++/example.cpp | 5 ++++- src/smt/smt_enode.h | 19 +++++++++++++++++++ 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp index ed5bf7086..b25507885 100644 --- a/examples/c++/example.cpp +++ b/examples/c++/example.cpp @@ -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() { diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h index b216665e5..df6309424 100644 --- a/src/smt/smt_enode.h +++ b/src/smt/smt_enode.h @@ -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(); }