From cfb3b789e26fdab73e733825950b24492c6c5e4c Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Mon, 31 May 2010 21:55:40 +0000 Subject: [PATCH] First draft implementation of mkAssociative --- src/expr/expr_manager_template.cpp | 57 ++++++++++++ src/expr/expr_manager_template.h | 13 +++ src/expr/expr_template.cpp | 7 ++ src/expr/expr_template.h | 7 ++ src/expr/metakind_template.h | 17 ++++ src/expr/node_manager.h | 1 + src/parser/smt/Smt.g | 2 + test/unit/Makefile.am | 1 + test/unit/expr/expr_manager_public.h | 128 +++++++++++++++++++++++++++ test/unit/expr/node_manager_black.h | 17 ++++ 10 files changed, 250 insertions(+) create mode 100644 test/unit/expr/expr_manager_public.h 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& 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::const_iterator it = children.begin() ; + std::vector::const_iterator end = children.end() ; + + /* The new top-level children and the children of each sub node */ + std::vector newChildren; + std::vector subChildren; + + while( it != end && numChildren > max ) { + /* Grab the next max children and make a node for them. */ + for( std::vector::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 Expr mkConst(const T&); + /** Create an Expr by applying an associative operator to the children. + * If children.size() is greater than the max arity for + * kind, then the expression will be broken up into + * suitably-sized chunks, taking advantage of the associativity of + * kind. For example, if kind FOO has max arity + * 2, then calling mkAssociative(FOO,a,b,c) will return + * (FOO (FOO a b) c) or code>(FOO a (FOO b c)). + * 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& 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 @@ -163,6 +163,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 + +#include +#include + +#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 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 mkVars(Type type, unsigned int n) { + std::vector 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 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 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 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 vars = mkVars(d_exprManager->booleanType(), 1); + TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException); + } + + void testMkAssociativeBadKind() { + std::vector 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 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 ); + } + }; -- 2.30.2