summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/expr_manager_template.cpp57
-rw-r--r--src/expr/expr_manager_template.h13
-rw-r--r--src/expr/expr_template.cpp7
-rw-r--r--src/expr/expr_template.h7
-rw-r--r--src/expr/metakind_template.h17
-rw-r--r--src/expr/node_manager.h1
-rw-r--r--src/parser/smt/Smt.g2
-rw-r--r--test/unit/Makefile.am1
-rw-r--r--test/unit/expr/expr_manager_public.h128
-rw-r--r--test/unit/expr/node_manager_black.h17
10 files changed, 250 insertions, 0 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 6fd33113b..59dbf77e5 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -250,6 +250,63 @@ Expr ExprManager::mkVar(const Type& type) {
return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
}
+Expr ExprManager::mkAssociative(Kind kind,
+ const std::vector<Expr>& children) {
+ NodeManagerScope nms(d_nodeManager);
+ const unsigned int max = maxArity(kind);
+ const unsigned int min = minArity(kind);
+ unsigned int numChildren = children.size();
+
+ if( numChildren <= max ) {
+ return mkExpr(kind,children);
+ } else {
+ std::vector<Expr>::const_iterator it = children.begin() ;
+ std::vector<Expr>::const_iterator end = children.end() ;
+
+ /* The new top-level children and the children of each sub node */
+ std::vector<Node> newChildren;
+ std::vector<Node> subChildren;
+
+ while( it != end && numChildren > max ) {
+ /* Grab the next max children and make a node for them. */
+ for( std::vector<Expr>::const_iterator next = it + max;
+ it != next;
+ ++it, --numChildren ) {
+ subChildren.push_back(it->getNode());
+ }
+ Node subNode = d_nodeManager->mkNode(kind,subChildren);
+ newChildren.push_back(subNode);
+
+ subChildren.clear();
+ }
+
+ /* If there's children left, "top off" the Expr. */
+ if(numChildren > 0) {
+ /* If the leftovers are too few, just copy them into newChildren;
+ * otherwise make a new sub-node */
+ if(numChildren < min) {
+ for(; it != end; ++it) {
+ newChildren.push_back(it->getNode());
+ }
+ } else {
+ for(; it != end; ++it) {
+ subChildren.push_back(it->getNode());
+ }
+ Node subNode = d_nodeManager->mkNode(kind, subChildren);
+ newChildren.push_back(subNode);
+ }
+ }
+
+ /* It would be really weird if this happened, but let's make sure. */
+ Assert( newChildren.size() >= min, "Too few new children in mkAssociative" );
+ /* We could call mkAssociative recursively with newChildren in this case, but it
+ * would take an astonishing number of children to make this fail. */
+ Assert( newChildren.size() <= max, "Too many new children in mkAssociative" );
+
+ return Expr(this, d_nodeManager->mkNodePtr(kind,newChildren) );
+ }
+}
+
unsigned ExprManager::minArity(Kind kind) {
return metakind::getLowerBoundForKind(kind);
}
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 323f21469..4cde091ac 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -180,6 +180,19 @@ public:
template <class T>
Expr mkConst(const T&);
+ /** Create an Expr by applying an associative operator to the children.
+ * If <code>children.size()</code> is greater than the max arity for
+ * <code>kind</code>, then the expression will be broken up into
+ * suitably-sized chunks, taking advantage of the associativity of
+ * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
+ * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
+ * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>.
+ * The order of the arguments will be preserved in a left-to-right
+ * traversal of the resulting tree.
+ */
+ Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
+
+
/** Make a function type from domain to range. */
FunctionType mkFunctionType(const Type& domain, const Type& range);
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 5c4e30a0c..edd49f032 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -140,6 +140,13 @@ size_t Expr::getNumChildren() const {
return d_node->getNumChildren();
}
+Expr Expr::getChild(unsigned int i) const {
+ ExprManagerScope ems(*this);
+ Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+ Assert(i >= 0 && i < d_node->getNumChildren(), "Child index out of bounds");
+ return Expr(d_exprManager,new Node((*d_node)[i]));
+}
+
bool Expr::hasOperator() const {
ExprManagerScope ems(*this);
Assert(d_node != NULL, "Unexpected NULL expression pointer!");
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 08dd1d25f..6597d5f14 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -164,6 +164,13 @@ public:
size_t getNumChildren() const;
/**
+ * Returns the i'th child of this expression.
+ * @param i the index of the child to retrieve
+ * @return the child
+ */
+ Expr getChild(unsigned int i) const;
+
+ /**
* Check if this is an expression that has an operator.
* @return true if this expression has an operator
*/
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 3c17507cf..b2e45533a 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -292,6 +292,23 @@ ${metakind_ubchildren}
return ubs[k];
}
+/** Returns true if the given kind is associative. This is used by ExprManager to
+ * decide whether it's safe to modify big expressions by changing the grouping of
+ * the arguments. */
+/* TODO: This could be generated. */
+inline bool isAssociative(::CVC4::Kind k) {
+ switch(k) {
+ case kind::AND:
+ case kind::OR:
+ case kind::MULT:
+ case kind::PLUS:
+ return true;
+
+ default:
+ return false;
+ }
+}
+
}/* CVC4::kind::metakind namespace */
}/* CVC4::kind namespace */
}/* CVC4 namespace */
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index a5f82b489..5642a8372 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -519,6 +519,7 @@ public:
* Get the type for the given node.
*/
TypeNode getType(TNode n) throw (TypeCheckingExceptionPrivate);
+
};
/**
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index 07dd3de5b..cfe41316c 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -187,6 +187,8 @@ annotatedFormula[CVC4::Expr& expr]
/* Unary AND/OR can be replaced with the argument.
It just so happens expr should already by the only argument. */
Assert( expr == args[0] );
+ } else if( (kind == CVC4::kind::AND || kind == CVC4::kind::OR) ) {
+ expr = EXPR_MANAGER->mkAssociative(kind,args);
} else {
PARSER_STATE->checkArity(kind, args.size());
expr = MK_EXPR(kind, args);
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index ef60febf8..c48afc10d 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -1,6 +1,7 @@
# All unit tests
UNIT_TESTS = \
expr/expr_public \
+ expr/expr_manager_public \
expr/node_white \
expr/node_black \
expr/kind_black \
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
new file mode 100644
index 000000000..ecb71081d
--- /dev/null
+++ b/test/unit/expr/expr_manager_public.h
@@ -0,0 +1,128 @@
+/********************* */
+/** expr_manager_public.h
+ ** Original author: cconway
+ ** 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.
+ **
+ ** Public black-box testing of CVC4::Expr.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <sstream>
+#include <string>
+
+#include "expr/expr_manager.h"
+#include "expr/expr.h"
+#include "util/Assert.h"
+#include "util/exception.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace std;
+
+class ExprManagerPublic : public CxxTest::TestSuite {
+private:
+
+ ExprManager* d_exprManager;
+
+ void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) {
+ std::vector<Expr> worklist;
+ worklist.push_back(expr);
+
+ unsigned int childrenFound = 0;
+
+ while( !worklist.empty() ) {
+ Expr current = worklist.back();
+ worklist.pop_back();
+ if( current.getKind() == kind ) {
+ for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
+ worklist.push_back( current.getChild(i) );
+ }
+ } else {
+ childrenFound++;
+ }
+ }
+
+ TS_ASSERT_EQUALS( childrenFound, numChildren );
+ }
+
+ std::vector<Expr> mkVars(Type type, unsigned int n) {
+ std::vector<Expr> vars;
+ for( unsigned int i = 0; i < n; ++i ) {
+ vars.push_back( d_exprManager->mkVar(type) );
+ }
+ return vars;
+ }
+
+
+public:
+ void setUp() {
+ d_exprManager = new ExprManager;
+ }
+
+
+ void tearDown() {
+ try {
+ delete d_exprManager;
+ } catch(Exception e) {
+ cerr << "Exception during tearDown():" << endl << e;
+ throw ;
+ }
+ }
+
+ void testMkAssociative() {
+ try {
+ std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 294821);
+ Expr n = d_exprManager->mkAssociative(AND,vars);
+ checkAssociative(n,AND,vars.size());
+
+ vars = mkVars(d_exprManager->booleanType(), 2);
+ n = d_exprManager->mkAssociative(OR,vars);
+ checkAssociative(n,OR,2);
+ } catch( Exception& e ) {
+ cerr << "Exception in testMkAssociative(): " << endl << e;
+ throw;
+ }
+ }
+
+ void testMkAssociative2() {
+ try {
+ std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 2);
+ Expr n = d_exprManager->mkAssociative(OR,vars);
+ checkAssociative(n,OR,2);
+ } catch( Exception& e ) {
+ cerr << "Exception in testMkAssociative2(): " << endl << e;
+ throw;
+ }
+ }
+
+ void testMkAssociative3() {
+ try {
+ unsigned int numVars = d_exprManager->maxArity(AND) + 1;
+ std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), numVars);
+ Expr n = d_exprManager->mkAssociative(AND,vars);
+ checkAssociative(n,AND,numVars);
+ } catch( Exception& e ) {
+ cerr << "Exception in testMkAssociative3(): " << endl << e;
+ throw;
+ }
+ }
+
+ void testMkAssociativeTooFew() {
+ std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1);
+ TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException);
+ }
+
+ void testMkAssociativeBadKind() {
+ std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
+ TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), AssertionException);
+ }
+
+};
diff --git a/test/unit/expr/node_manager_black.h b/test/unit/expr/node_manager_black.h
index 6ff2b64e0..e3be1bedd 100644
--- a/test/unit/expr/node_manager_black.h
+++ b/test/unit/expr/node_manager_black.h
@@ -337,4 +337,21 @@ public:
TS_ASSERT_EQUALS(ft.getRangeType(), booleanType);
}
+
+ void testMkNodeTooFew() {
+ TS_ASSERT_THROWS( d_nodeManager->mkNode(AND), AssertionException );
+ Node x = d_nodeManager->mkVar( d_nodeManager->booleanType() );
+ TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, x), AssertionException );
+ }
+
+ void testMkNodeTooMany() {
+ std::vector<Node> vars;
+ const unsigned int max = metakind::getUpperBoundForKind(AND);
+ TypeNode boolType = d_nodeManager->booleanType();
+ for( unsigned int i = 0; i <= max; ++i ) {
+ vars.push_back( d_nodeManager->mkVar(boolType) );
+ }
+ TS_ASSERT_THROWS( d_nodeManager->mkNode(AND, vars), AssertionException );
+ }
+
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback