test/unit/util/array_store_all_white.h

   1 /*********************                                                        */
   2 /*! \file array_store_all_white.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli, Morgan Deters, Clark Barrett
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing 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 "api/cvc4cpp.h"
  20 #include "expr/array_store_all.h"
  21 #include "expr/expr.h"
  22 #include "expr/expr_manager.h"
  23 #include "expr/type.h"
  24 #include "smt/smt_engine.h"
  25 #include "smt/smt_engine_scope.h"
  26 #include "test_utils.h"
  27
  28 using namespace CVC4;
  29 using namespace std;
  30
  31 class ArrayStoreAllWhite : public CxxTest::TestSuite
  32 {
  33  public:
  34   void setUp() override
  35   {
  36     d_slv = new api::Solver();
  37     d_scope = new smt::SmtScope(d_slv->getSmtEngine());
  38     d_nm = d_slv->getSmtEngine()->d_nodeManager;
  39   }
  40
  41   void tearDown() override
  42   {
  43     delete d_scope;
  44     delete d_slv;
  45   }
  46
  47   void testStoreAll()
  48   {
  49     TypeNode usort = d_nm->mkSort("U");
  50     ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->realType()),
  51                   d_nm->mkConst(Rational(9, 2)));
  52     ArrayStoreAll(d_nm->mkArrayType(d_nm->mkSort("U"), usort),
  53                   d_nm->mkConst(UninterpretedConstant(usort, 0)));
  54     ArrayStoreAll(d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->realType()),
  55                   d_nm->mkConst(Rational(0)));
  56     ArrayStoreAll(
  57         d_nm->mkArrayType(d_nm->mkBitVectorType(8), d_nm->integerType()),
  58         d_nm->mkConst(Rational(0)));
  59   }
  60
  61   void testTypeErrors()
  62   {
  63     TS_ASSERT_THROWS(ArrayStoreAll(d_nm->integerType(),
  64                                    d_nm->mkConst(UninterpretedConstant(
  65                                        d_nm->mkSort("U"), 0))),
  66                      IllegalArgumentException&);
  67     TS_ASSERT_THROWS(
  68         ArrayStoreAll(d_nm->integerType(), d_nm->mkConst(Rational(9, 2))),
  69         IllegalArgumentException&);
  70     TS_ASSERT_THROWS(
  71         ArrayStoreAll(d_nm->mkArrayType(d_nm->integerType(), d_nm->mkSort("U")),
  72                       d_nm->mkConst(Rational(9, 2))),
  73         IllegalArgumentException&);
  74   }
  75
  76   void testConstError()
  77   {
  78     TypeNode usort = d_nm->mkSort("U");
  79     TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
  80         d_nm->mkArrayType(d_nm->mkSort("U"), usort), d_nm->mkVar(usort)));
  81     TS_ASSERT_THROWS_ANYTHING(ArrayStoreAll(
  82         d_nm->integerType(), d_nm->mkVar("x", d_nm->integerType())));
  83     TS_ASSERT_THROWS_ANYTHING(
  84         ArrayStoreAll(d_nm->integerType(),
  85                       d_nm->mkNode(kind::PLUS,
  86                                    d_nm->mkConst(Rational(1)),
  87                                    d_nm->mkConst(Rational(0)))));
  88   }
  89
  90  private:
  91   api::Solver* d_slv;
  92   smt::SmtScope* d_scope;
  93   NodeManager* d_nm;
  94 }; /* class ArrayStoreAllBlack */