diff options
Diffstat (limited to 'src/expr/expr_template.cpp')
-rw-r--r-- | src/expr/expr_template.cpp | 67 |
1 files changed, 65 insertions, 2 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 7c2d02809..619fd5280 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -21,15 +21,19 @@ #include "expr/expr_manager_scope.h" #include "util/Assert.h" +#include <iterator> +#include <utility> + ${includes} // This is a hack, but an important one: if there's an error, the // compiler directs the user to the template file instead of the // generated one. We don't want the user to modify the generated one, // since it'll get overwritten on a later build. -#line 31 "${template}" +#line 34 "${template}" using namespace CVC4::kind; +using namespace std; namespace CVC4 { @@ -73,7 +77,7 @@ TypeCheckingException::~TypeCheckingException() throw () { } void TypeCheckingException::toStream(std::ostream& os) const { - os << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr; + os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr; } Expr TypeCheckingException::getExpression() const { @@ -208,6 +212,59 @@ Type Expr::getType(bool check) const throw (TypeCheckingException) { return d_exprManager->getType(*this, check); } +Expr Expr::substitute(Expr e, Expr replacement) const { + return Expr(d_exprManager, new Node(d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node)))); +} + +template <class Iterator> +class NodeIteratorAdaptor : public std::iterator<std::input_iterator_tag, Node> { + Iterator d_iterator; +public: + NodeIteratorAdaptor(Iterator i) : d_iterator(i) { + } + NodeIteratorAdaptor& operator++() { ++d_iterator; return *this; } + NodeIteratorAdaptor operator++(int) { NodeIteratorAdaptor i(d_iterator); ++d_iterator; return i; } + bool operator==(NodeIteratorAdaptor i) { return d_iterator == i.d_iterator; } + bool operator!=(NodeIteratorAdaptor i) { return !(*this == i); } + Node operator*() { return Node::fromExpr(*d_iterator); } +};/* class NodeIteratorAdaptor */ + +template <class Iterator> +static inline NodeIteratorAdaptor<Iterator> mkNodeIteratorAdaptor(Iterator i) { + return NodeIteratorAdaptor<Iterator>(i); +} + +Expr Expr::substitute(const std::vector<Expr> exes, + const std::vector<Expr>& replacements) const { + return Expr(d_exprManager, + new Node(d_node->substitute(mkNodeIteratorAdaptor(exes.begin()), + mkNodeIteratorAdaptor(exes.end()), + mkNodeIteratorAdaptor(replacements.begin()), + mkNodeIteratorAdaptor(replacements.end())))); +} + +template <class Iterator> +class NodePairIteratorAdaptor : public std::iterator<std::input_iterator_tag, pair<Node, Node> > { + Iterator d_iterator; +public: + NodePairIteratorAdaptor(Iterator i) : d_iterator(i) { + } + NodePairIteratorAdaptor& operator++() { ++d_iterator; return *this; } + NodePairIteratorAdaptor operator++(int) { NodePairIteratorAdaptor i(d_iterator); ++d_iterator; return i; } + bool operator==(NodePairIteratorAdaptor i) { return d_iterator == i.d_iterator; } + bool operator!=(NodePairIteratorAdaptor i) { return !(*this == i); } + pair<Node, Node> operator*() { return make_pair(Node::fromExpr((*d_iterator).first), Node::fromExpr((*d_iterator).second)); } +};/* class NodePairIteratorAdaptor */ + +template <class Iterator> +static inline NodePairIteratorAdaptor<Iterator> mkNodePairIteratorAdaptor(Iterator i) { + return NodePairIteratorAdaptor<Iterator>(i); +} + +Expr Expr::substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const { + return Expr(d_exprManager, new Node(d_node->substitute(mkNodePairIteratorAdaptor(map.begin()), mkNodePairIteratorAdaptor(map.end())))); +} + Expr::const_iterator::const_iterator() : d_iterator(NULL) { } @@ -280,6 +337,12 @@ Expr::operator bool() const { return !isNull(); } +bool Expr::isVariable() const { + ExprManagerScope ems(*this); + Assert(d_node != NULL, "Unexpected NULL expression pointer!"); + return d_node->getMetaKind() == kind::metakind::VARIABLE; +} + bool Expr::isConst() const { ExprManagerScope ems(*this); Assert(d_node != NULL, "Unexpected NULL expression pointer!"); |