test/unit/util/array_store_all_black.h

   1 /*********************                                                        */
   2 /*! \file array_store_all_black.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Black box testing of CVC4::ArrayStoreAll
  13  **
  14  ** Black box testing of CVC4::ArrayStoreAll.
  15  **/
  16
  17 #include <cxxtest/TestSuite.h>
  18
  19 #include "util/array_store_all.h"
  20 #include "expr/expr_manager.h"
  21 #include "expr/expr_manager_scope.h"
  22 #include "expr/type.h"
  23 #include "expr/expr.h"
  24
  25 using namespace CVC4;
  26 using namespace std;
  27
  28 class ArrayStoreAllBlack : public CxxTest::TestSuite {
  29
  30   ExprManager* d_em;
  31   ExprManagerScope* d_scope;
  32
  33 public:
  34
  35   void setUp() {
  36     d_em = new ExprManager();
  37     d_scope = new ExprManagerScope(*d_em);
  38   }
  39
  40   void tearDown() {
  41     delete d_scope;
  42     delete d_em;
  43   }
  44
  45   void testStoreAll() {
  46     Type usort = d_em->mkSort("U");
  47     ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->realType()), d_em->mkConst(Rational(9, 2)));
  48     ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkConst(UninterpretedConstant(usort, 0)));
  49     ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->realType()), d_em->mkConst(Rational(0)));
  50     ArrayStoreAll(d_em->mkArrayType(d_em->mkBitVectorType(8), d_em->integerType()), d_em->mkConst(Rational(0)));
  51   }
  52
  53   void testTypeErrors() {
  54     // these two throw an AssertionException in assertions-enabled builds, and an IllegalArgumentException in production builds
  55     TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(UninterpretedConstant(d_em->mkSort("U"), 0))) );
  56     TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkConst(Rational(9, 2))) );
  57
  58     TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
  59     TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->integerType(), d_em->mkSort("U")), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
  60     TS_ASSERT_THROWS( ArrayStoreAll(d_em->mkArrayType(d_em->realType(), d_em->integerType()), d_em->mkConst(Rational(9, 2))), IllegalArgumentException );
  61   }
  62
  63   void testConstError() {
  64     Type usort = d_em->mkSort("U");
  65     TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->mkArrayType(d_em->mkSort("U"), usort), d_em->mkVar(usort)) );
  66     TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkVar("x", d_em->integerType())) );
  67     TS_ASSERT_THROWS_ANYTHING( ArrayStoreAll(d_em->integerType(), d_em->mkExpr(kind::PLUS, d_em->mkConst(Rational(1)), d_em->mkConst(Rational(0)))) );
  68   }
  69
  70 };/* class ArrayStoreAllBlack */