test/unit/theory/theory_sets_type_rules_white.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets_type_rules_white.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Mudathir Mohamed
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2021 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 White box testing of sets typing rules
  13  **/
  14
  15 #include "expr/dtype.h"
  16 #include "test_api.h"
  17 #include "test_node.h"
  18
  19 namespace CVC5 {
  20
  21 using namespace CVC5::api;
  22
  23 namespace test {
  24
  25 class TestTheoryWhiteSetsTypeRuleApi : public TestApi
  26 {
  27 };
  28 class TestTheoryWhiteSetsTypeRuleInternal : public TestNode
  29 {
  30 };
  31
  32 TEST_F(TestTheoryWhiteSetsTypeRuleInternal, is_comparable_to)
  33 {
  34   TypeNode setRealType = d_nodeManager->mkSetType(d_nodeManager->realType());
  35   TypeNode setIntType = d_nodeManager->mkSetType(d_nodeManager->integerType());
  36   ASSERT_FALSE(setIntType.isComparableTo(setRealType));
  37   ASSERT_FALSE(setIntType.isSubtypeOf(setRealType));
  38   ASSERT_FALSE(setRealType.isComparableTo(setIntType));
  39   ASSERT_FALSE(setRealType.isComparableTo(setIntType));
  40 }
  41
  42 TEST_F(TestTheoryWhiteSetsTypeRuleApi, singleton_term)
  43 {
  44   Sort realSort = d_solver.getRealSort();
  45   Sort intSort = d_solver.getIntegerSort();
  46   Term emptyReal = d_solver.mkEmptySet(d_solver.mkSetSort(realSort));
  47   Term integerOne = d_solver.mkInteger(1);
  48   Term realOne = d_solver.mkReal(1);
  49   Term singletonInt = d_solver.mkTerm(api::SINGLETON, integerOne);
  50   Term singletonReal = d_solver.mkTerm(api::SINGLETON, realOne);
  51   // (union
  52   //    (singleton (singleton_op Int) 1)
  53   //    (as emptyset (Set Real)))
  54   ASSERT_THROW(d_solver.mkTerm(UNION, singletonInt, emptyReal),
  55                CVC4ApiException);
  56   // (union
  57   //    (singleton (singleton_op Real) 1)
  58   //    (as emptyset (Set Real)))
  59   ASSERT_NO_THROW(d_solver.mkTerm(UNION, singletonReal, emptyReal));
  60 }
  61
  62 TEST_F(TestTheoryWhiteSetsTypeRuleInternal, singleton_node)
  63 {
  64   Node singletonInt =
  65       d_nodeManager->mkConst(SingletonOp(d_nodeManager->integerType()));
  66   Node singletonReal =
  67       d_nodeManager->mkConst(SingletonOp(d_nodeManager->realType()));
  68   Node intConstant = d_nodeManager->mkConst(Rational(1));
  69   Node realConstant = d_nodeManager->mkConst(Rational(1, 5));
  70   // (singleton (singleton_op Real) 1)
  71   ASSERT_NO_THROW(
  72       d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant));
  73   // (singleton (singleton_op Int) (/ 1 5))
  74   ASSERT_DEATH(
  75       d_nodeManager->mkSingleton(d_nodeManager->integerType(), realConstant),
  76       "Invalid operands for mkSingleton");
  77
  78   Node n = d_nodeManager->mkSingleton(d_nodeManager->realType(), intConstant);
  79   // the type of (singleton (singleton_op Real) 1) is (Set Real)
  80   ASSERT_TRUE(n.getType()
  81               == d_nodeManager->mkSetType(d_nodeManager->realType()));
  82   // (singleton (singleton_op Real) 1) is a constant in normal form
  83   ASSERT_TRUE(n.isConst());
  84 }
  85 }  // namespace test
  86 }  // namespace CVC5