declaration_scope.h \
declaration_scope.cpp \
expr_manager_scope.h \
- sort.h
+ node_self_iterator.h
nodist_libexpr_la_SOURCES = \
kind.h \
metakind.h \
--- /dev/null
+/********************* */
+/*! \file node_self_iterator.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Iterator supporting Node "self-iteration"
+ **
+ ** Iterator supporting Node "self-iteration."
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__EXPR__NODE_SELF_ITERATOR_H
+#define __CVC4__EXPR__NODE_SELF_ITERATOR_H
+
+#include <iterator>
+
+#include "util/Assert.h"
+#include "expr/node.h"
+
+namespace CVC4 {
+namespace expr {
+
+class NodeSelfIterator : std::iterator<std::input_iterator_tag, Node> {
+ Node d_node;
+ Node::const_iterator d_child;
+
+public:
+ static NodeSelfIterator self(TNode n);
+ static NodeSelfIterator selfEnd(TNode n);
+
+ NodeSelfIterator();
+ NodeSelfIterator(Node n);
+ NodeSelfIterator(TNode n);
+ NodeSelfIterator(const NodeSelfIterator& i);
+
+ NodeSelfIterator(Node::const_iterator i);
+ NodeSelfIterator(TNode::const_iterator i);
+
+ Node operator*() const;
+ NodeSelfIterator& operator++();
+ NodeSelfIterator operator++(int);
+
+ bool operator==(NodeSelfIterator i) const;
+ bool operator!=(NodeSelfIterator i) const;
+
+};/* class NodeSelfIterator */
+
+inline NodeSelfIterator NodeSelfIterator::self(TNode n) {
+ Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
+ return NodeSelfIterator(n);
+}
+
+inline NodeSelfIterator NodeSelfIterator::selfEnd(TNode n) {
+ Assert(!n.isNull(), "Self-iteration over null nodes not permitted.");
+ return NodeSelfIterator(n.end());
+}
+
+inline NodeSelfIterator::NodeSelfIterator() :
+ d_node(),
+ d_child() {
+}
+
+inline NodeSelfIterator::NodeSelfIterator(Node node) :
+ d_node(node),
+ d_child() {
+ Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
+}
+
+inline NodeSelfIterator::NodeSelfIterator(TNode node) :
+ d_node(node),
+ d_child() {
+ Assert(!node.isNull(), "Self-iteration over null nodes not permitted.");
+}
+
+inline NodeSelfIterator::NodeSelfIterator(const NodeSelfIterator& i) :
+ d_node(i.d_node),
+ d_child(i.d_child) {
+}
+
+inline NodeSelfIterator::NodeSelfIterator(Node::const_iterator i) :
+ d_node(),
+ d_child(i) {
+}
+
+inline NodeSelfIterator::NodeSelfIterator(TNode::const_iterator i) :
+ d_node(),
+ d_child(i) {
+}
+
+inline Node NodeSelfIterator::operator*() const {
+ return d_node.isNull() ? *d_child : d_node;
+}
+
+inline NodeSelfIterator& NodeSelfIterator::operator++() {
+ if(d_node.isNull()) {
+ ++d_child;
+ } else {
+ d_child = d_node.end();
+ d_node = Node::null();
+ }
+ return *this;
+}
+
+inline NodeSelfIterator NodeSelfIterator::operator++(int) {
+ NodeSelfIterator i = *this;
+ ++*this;
+ return i;
+}
+
+inline bool NodeSelfIterator::operator==(NodeSelfIterator i) const {
+ return d_node == i.d_node && d_child == i.d_child;
+}
+
+inline bool NodeSelfIterator::operator!=(NodeSelfIterator i) const {
+ return !(*this == i);
+}
+
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__EXPR__NODE_SELF_ITERATOR_H */
static size_t next_id;
-public:
/**
- * Uninitializing constructor for NodeBuilder's use. This is
- * somewhat dangerous, but must also be public for the
- * makeStackNodeBuilder() macro to work.
+ * Uninitializing constructor for NodeBuilder's use.
*/
NodeValue() { /* do not initialize! */ }
const_nv_iterator nv_begin() const;
const_nv_iterator nv_end() const;
- template <typename T>
+ template <class T>
class iterator {
const_nv_iterator d_i;
public:
+ typedef std::random_access_iterator_tag iterator_category;
typedef T value_type;
typedef ptrdiff_t difference_type;
typedef T* pointer;
iterator() : d_i(NULL) {}
explicit iterator(const_nv_iterator i) : d_i(i) {}
- inline T operator*();
+ // conversion of a TNode iterator to a Node iterator
+ inline operator NodeValue::iterator<NodeTemplate<true> >() {
+ return iterator<NodeTemplate<true> >(d_i);
+ }
+
+ inline T operator*() const;
- bool operator==(const iterator& i) {
+ bool operator==(const iterator& i) const {
return d_i == i.d_i;
}
- bool operator!=(const iterator& i) {
+ bool operator!=(const iterator& i) const {
return d_i != i.d_i;
}
difference_type operator-(iterator i) {
return d_i - i.d_i;
}
-
- typedef std::random_access_iterator_tag iterator_category;
};/* class NodeValue::iterator<T> */
// operator+ (as a function) cannot be a template, so we have to
namespace expr {
template <typename T>
-inline T NodeValue::iterator<T>::operator*() {
+inline T NodeValue::iterator<T>::operator*() const {
return T(*d_i);
}
expr/attribute_white \
expr/attribute_black \
expr/declaration_scope_black \
+ expr/node_self_iterator_black \
parser/parser_black \
parser/parser_builder_black \
prop/cnf_stream_black \
Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
- TypeNode *d_booleanType;
- TypeNode *d_realType;
+ TypeNode* d_booleanType;
+ TypeNode* d_realType;
public:
--- /dev/null
+/********************* */
+/*! \file node_self_iterator_black.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Black box testing of CVC4::expr::NodeSelfIterator
+ **
+ ** Black box testing of CVC4::expr::NodeSelfIterator
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "context/context.h"
+#include "expr/node.h"
+#include "expr/node_self_iterator.h"
+#include "expr/node_builder.h"
+#include "expr/convenience_node_builders.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::kind;
+using namespace CVC4::expr;
+using namespace std;
+
+class NodeSelfIteratorBlack : public CxxTest::TestSuite {
+private:
+
+ Context* d_ctxt;
+ NodeManager* d_nodeManager;
+ NodeManagerScope* d_scope;
+ TypeNode* d_booleanType;
+ TypeNode* d_realType;
+
+public:
+
+ void setUp() {
+ d_ctxt = new Context;
+ d_nodeManager = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nodeManager);
+ d_booleanType = new TypeNode(d_nodeManager->booleanType());
+ d_realType = new TypeNode(d_nodeManager->realType());
+ }
+
+ void tearDown() {
+ delete d_booleanType;
+ delete d_scope;
+ delete d_nodeManager;
+ delete d_ctxt;
+ }
+
+ void testSelfIteration() {
+ Node x = d_nodeManager->mkVar("x", *d_booleanType);
+ Node y = d_nodeManager->mkVar("y", *d_booleanType);
+ Node x_and_y = x && y;
+ NodeSelfIterator i = x_and_y, j = NodeSelfIterator::self(x_and_y);
+ TS_ASSERT(i != x_and_y.end());
+ TS_ASSERT(j != x_and_y.end());
+ TS_ASSERT(*i == x_and_y);
+ TS_ASSERT(*j == x_and_y);
+ TS_ASSERT(*i++ == x_and_y);
+ TS_ASSERT(*j++ == x_and_y);
+ TS_ASSERT(i == NodeSelfIterator::selfEnd(x_and_y));
+ TS_ASSERT(j == NodeSelfIterator::selfEnd(x_and_y));
+ TS_ASSERT(i == x_and_y.end());
+ TS_ASSERT(j == x_and_y.end());
+ i = x_and_y.begin();
+ TS_ASSERT(i != x_and_y.end());
+ TS_ASSERT(*i == x);
+ TS_ASSERT(*++i == y);
+ TS_ASSERT(++i == x_and_y.end());
+ }
+
+};
}
ParserBlack(InputLanguage lang) :
- d_lang(lang),
- d_exprManager(new ExprManager()) {
+ d_lang(lang) {
}
-public:
- virtual ~ParserBlack() {
+ void setUp() {
+cout << "SET UP\n";
+ d_exprManager = new ExprManager;
+ }
+
+ void tearDown() {
delete d_exprManager;
}
};
class Cvc4ParserTest : public CxxTest::TestSuite, public ParserBlack {
+ typedef ParserBlack super;
public:
Cvc4ParserTest() : ParserBlack(LANG_CVC4) { }
+ void setUp() {
+ super::setUp();
+ }
+
+ void tearDown() {
+ super::tearDown();
+ }
+
void testGoodCvc4Inputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("ASSERT TRUE;");
};
class SmtParserTest : public CxxTest::TestSuite, public ParserBlack {
+ typedef ParserBlack super;
+
public:
SmtParserTest() : ParserBlack(LANG_SMTLIB) { }
+ void setUp() {
+ super::setUp();
+ }
+
+ void tearDown() {
+ super::tearDown();
+ }
+
void testGoodSmtInputs() {
tryGoodInput(""); // empty string is OK
tryGoodInput("(benchmark foo :assumption true)");
public:
Smt2ParserTest() : ParserBlack(LANG_SMTLIB_V2) { }
+ void setUp() {
+ super::setUp();
+ }
+
+ void tearDown() {
+ super::tearDown();
+ }
+
void setupContext(Smt2& parser) {
parser.addTheory(Smt2::THEORY_CORE);
super::setupContext(parser);
projects / cvc5.git / commitdiff