test/unit/expr/expr_manager_public.h

   1 /*********************                                                        */
   2 /*! \file expr_manager_public.h
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Public black-box testing of CVC4::ExprManager.
  15  **
  16  ** Public black-box testing of CVC4::ExprManager.
  17  **/
  18
  19 #include <cxxtest/TestSuite.h>
  20
  21 #include <sstream>
  22 #include <string>
  23
  24 #include "expr/expr_manager.h"
  25 #include "expr/expr.h"
  26 #include "util/Assert.h"
  27 #include "util/exception.h"
  28
  29 using namespace CVC4;
  30 using namespace CVC4::kind;
  31 using namespace std;
  32
  33 class ExprManagerPublic : public CxxTest::TestSuite {
  34 private:
  35
  36   ExprManager* d_exprManager;
  37
  38   void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) {
  39     std::vector<Expr> worklist;
  40     worklist.push_back(expr);
  41
  42     unsigned int childrenFound = 0;
  43
  44     while( !worklist.empty() ) {
  45       Expr current = worklist.back();
  46       worklist.pop_back();
  47       if( current.getKind() == kind ) {
  48         for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
  49           worklist.push_back( current.getChild(i) );
  50         }
  51       } else {
  52         childrenFound++;
  53       }
  54     }
  55
  56     TS_ASSERT_EQUALS( childrenFound, numChildren );
  57   }
  58
  59   std::vector<Expr> mkVars(Type type, unsigned int n) {
  60     std::vector<Expr> vars;
  61     for( unsigned int i = 0; i < n; ++i ) {
  62       vars.push_back( d_exprManager->mkVar(type) );
  63     }
  64     return vars;
  65   }
  66
  67
  68 public:
  69   void setUp() {
  70     d_exprManager = new ExprManager;
  71   }
  72
  73
  74   void tearDown() {
  75     try {
  76       delete d_exprManager;
  77     } catch(Exception e) {
  78       cerr << "Exception during tearDown():" << endl << e;
  79       throw ;
  80     }
  81   }
  82
  83   void testMkAssociative() {
  84     try {
  85       std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 294821);
  86       Expr n = d_exprManager->mkAssociative(AND,vars);
  87       checkAssociative(n,AND,vars.size());
  88
  89       vars = mkVars(d_exprManager->booleanType(), 2);
  90       n = d_exprManager->mkAssociative(OR,vars);
  91       checkAssociative(n,OR,2);
  92     } catch( Exception& e ) {
  93       cerr << "Exception in testMkAssociative(): " << endl << e;
  94       throw;
  95     }
  96   }
  97
  98   void testMkAssociative2() {
  99     try {
 100       std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 2);
 101       Expr n = d_exprManager->mkAssociative(OR,vars);
 102       checkAssociative(n,OR,2);
 103     } catch( Exception& e ) {
 104       cerr << "Exception in testMkAssociative2(): " << endl << e;
 105       throw;
 106     }
 107   }
 108
 109   void testMkAssociative3() {
 110     try {
 111       unsigned int numVars = d_exprManager->maxArity(AND) + 1;
 112       std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), numVars);
 113       Expr n = d_exprManager->mkAssociative(AND,vars);
 114       checkAssociative(n,AND,numVars);
 115     } catch( Exception& e ) {
 116       cerr << "Exception in testMkAssociative3(): " << endl << e;
 117       throw;
 118     }
 119   }
 120
 121   void testMkAssociativeTooFew() {
 122     std::vector<Expr> vars = mkVars(d_exprManager->booleanType(), 1);
 123     TS_ASSERT_THROWS( d_exprManager->mkAssociative(AND,vars), AssertionException);
 124   }
 125
 126   void testMkAssociativeBadKind() {
 127     std::vector<Expr> vars = mkVars(d_exprManager->integerType(), 10);
 128     TS_ASSERT_THROWS( d_exprManager->mkAssociative(TUPLE,vars), AssertionException);
 129   }
 130
 131 };