From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 5 Mar 2021 07:21:08 +0000 (-0800)
Subject: google test: Remove dependency on ExprManager in type_cardinality_black. (#6061)
X-Git-Tag: cvc5-1.0.0~2149
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d09ca870bcaef2efbf4f0d5a25b16f301ef5a0df;p=cvc5.git

google test: Remove dependency on ExprManager in type_cardinality_black. (#6061)
---

diff --git a/test/unit/expr/type_cardinality_black.cpp b/test/unit/expr/type_cardinality_black.cpp
index 8473ab5da..b867a4168 100644
--- a/test/unit/expr/type_cardinality_black.cpp
+++ b/test/unit/expr/type_cardinality_black.cpp
@@ -16,11 +16,10 @@
 
 #include <string>
 
-#include "expr/expr_manager.h"
 #include "expr/kind.h"
 #include "expr/node_manager.h"
 #include "expr/type.h"
-#include "test_api.h"
+#include "test_node.h"
 #include "util/cardinality.h"
 
 namespace CVC4 {
@@ -29,40 +28,42 @@ using namespace kind;
 
 namespace test {
 
-class TestTypeCardinalityBlack : public TestApi
+class TestTypeCardinalityBlack : public TestNode
 {
- protected:
-  void SetUp() override
-  {
-    TestApi::SetUp();
-    d_em = d_solver.getExprManager();
-    d_nm = d_solver.getNodeManager();
-  }
-  ExprManager* d_em;
-  NodeManager* d_nm;
 };
 
 TEST_F(TestTypeCardinalityBlack, basics)
 {
-  ASSERT_EQ(d_em->booleanType().getCardinality().compare(2),
-            Cardinality::EQUAL);
-  ASSERT_EQ(d_em->integerType().getCardinality().compare(Cardinality::INTEGERS),
+  ASSERT_EQ(d_nodeManager->booleanType().getCardinality().compare(2),
             Cardinality::EQUAL);
-  ASSERT_EQ(d_em->realType().getCardinality().compare(Cardinality::REALS),
+  ASSERT_EQ(d_nodeManager->integerType().getCardinality().compare(
+                Cardinality::INTEGERS),
             Cardinality::EQUAL);
+  ASSERT_EQ(
+      d_nodeManager->realType().getCardinality().compare(Cardinality::REALS),
+      Cardinality::EQUAL);
 }
 
 TEST_F(TestTypeCardinalityBlack, arrays)
 {
-  Type intToInt = d_em->mkArrayType(d_em->integerType(), d_em->integerType());
-  Type realToReal = d_em->mkArrayType(d_em->realType(), d_em->realType());
-  Type realToInt = d_em->mkArrayType(d_em->realType(), d_em->integerType());
-  Type intToReal = d_em->mkArrayType(d_em->integerType(), d_em->realType());
-  Type intToBool = d_em->mkArrayType(d_em->integerType(), d_em->booleanType());
-  Type realToBool = d_em->mkArrayType(d_em->realType(), d_em->booleanType());
-  Type boolToReal = d_em->mkArrayType(d_em->booleanType(), d_em->realType());
-  Type boolToInt = d_em->mkArrayType(d_em->booleanType(), d_em->integerType());
-  Type boolToBool = d_em->mkArrayType(d_em->booleanType(), d_em->booleanType());
+  TypeNode intToInt = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                 d_nodeManager->integerType());
+  TypeNode realToReal = d_nodeManager->mkArrayType(d_nodeManager->realType(),
+                                                   d_nodeManager->realType());
+  TypeNode realToInt = d_nodeManager->mkArrayType(d_nodeManager->realType(),
+                                                  d_nodeManager->integerType());
+  TypeNode intToReal = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                  d_nodeManager->realType());
+  TypeNode intToBool = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
+                                                  d_nodeManager->booleanType());
+  TypeNode realToBool = d_nodeManager->mkArrayType(
+      d_nodeManager->realType(), d_nodeManager->booleanType());
+  TypeNode boolToReal = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
+                                                   d_nodeManager->realType());
+  TypeNode boolToInt = d_nodeManager->mkArrayType(d_nodeManager->booleanType(),
+                                                  d_nodeManager->integerType());
+  TypeNode boolToBool = d_nodeManager->mkArrayType(
+      d_nodeManager->booleanType(), d_nodeManager->booleanType());
 
   ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
             Cardinality::EQUAL);
@@ -85,19 +86,24 @@ TEST_F(TestTypeCardinalityBlack, arrays)
 
 TEST_F(TestTypeCardinalityBlack, unary_functions)
 {
-  Type intToInt =
-      d_em->mkFunctionType(d_em->integerType(), d_em->integerType());
-  Type realToReal = d_em->mkFunctionType(d_em->realType(), d_em->realType());
-  Type realToInt = d_em->mkFunctionType(d_em->realType(), d_em->integerType());
-  Type intToReal = d_em->mkFunctionType(d_em->integerType(), d_em->realType());
-  Type intToBool =
-      d_em->mkFunctionType(d_em->integerType(), d_em->booleanType());
-  Type realToBool = d_em->mkFunctionType(d_em->realType(), d_em->booleanType());
-  Type boolToReal = d_em->mkFunctionType(d_em->booleanType(), d_em->realType());
-  Type boolToInt =
-      d_em->mkFunctionType(d_em->booleanType(), d_em->integerType());
-  Type boolToBool =
-      d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType());
+  TypeNode intToInt = d_nodeManager->mkFunctionType(
+      d_nodeManager->integerType(), d_nodeManager->integerType());
+  TypeNode realToReal = d_nodeManager->mkFunctionType(
+      d_nodeManager->realType(), d_nodeManager->realType());
+  TypeNode realToInt = d_nodeManager->mkFunctionType(
+      d_nodeManager->realType(), d_nodeManager->integerType());
+  TypeNode intToReal = d_nodeManager->mkFunctionType(
+      d_nodeManager->integerType(), d_nodeManager->realType());
+  TypeNode intToBool = d_nodeManager->mkFunctionType(
+      d_nodeManager->integerType(), d_nodeManager->booleanType());
+  TypeNode realToBool = d_nodeManager->mkFunctionType(
+      d_nodeManager->realType(), d_nodeManager->booleanType());
+  TypeNode boolToReal = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), d_nodeManager->realType());
+  TypeNode boolToInt = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), d_nodeManager->integerType());
+  TypeNode boolToBool = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), d_nodeManager->booleanType());
 
   ASSERT_EQ(intToInt.getCardinality().compare(Cardinality::REALS),
             Cardinality::EQUAL);
@@ -120,69 +126,96 @@ TEST_F(TestTypeCardinalityBlack, unary_functions)
 
 TEST_F(TestTypeCardinalityBlack, binary_functions)
 {
-  std::vector<Type> boolbool;
-  boolbool.push_back(d_em->booleanType());
-  boolbool.push_back(d_em->booleanType());
-  std::vector<Type> boolint;
-  boolint.push_back(d_em->booleanType());
-  boolint.push_back(d_em->integerType());
-  std::vector<Type> intbool;
-  intbool.push_back(d_em->integerType());
-  intbool.push_back(d_em->booleanType());
-  std::vector<Type> intint;
-  intint.push_back(d_em->integerType());
-  intint.push_back(d_em->integerType());
-  std::vector<Type> intreal;
-  intreal.push_back(d_em->integerType());
-  intreal.push_back(d_em->realType());
-  std::vector<Type> realint;
-  realint.push_back(d_em->realType());
-  realint.push_back(d_em->integerType());
-  std::vector<Type> realreal;
-  realreal.push_back(d_em->realType());
-  realreal.push_back(d_em->realType());
-  std::vector<Type> realbool;
-  realbool.push_back(d_em->realType());
-  realbool.push_back(d_em->booleanType());
-  std::vector<Type> boolreal;
-  boolreal.push_back(d_em->booleanType());
-  boolreal.push_back(d_em->realType());
-
-  Type boolboolToBool = d_em->mkFunctionType(boolbool, d_em->booleanType());
-  Type boolboolToInt = d_em->mkFunctionType(boolbool, d_em->integerType());
-  Type boolboolToReal = d_em->mkFunctionType(boolbool, d_em->realType());
-
-  Type boolintToBool = d_em->mkFunctionType(boolint, d_em->booleanType());
-  Type boolintToInt = d_em->mkFunctionType(boolint, d_em->integerType());
-  Type boolintToReal = d_em->mkFunctionType(boolint, d_em->realType());
-
-  Type intboolToBool = d_em->mkFunctionType(intbool, d_em->booleanType());
-  Type intboolToInt = d_em->mkFunctionType(intbool, d_em->integerType());
-  Type intboolToReal = d_em->mkFunctionType(intbool, d_em->realType());
-
-  Type intintToBool = d_em->mkFunctionType(intint, d_em->booleanType());
-  Type intintToInt = d_em->mkFunctionType(intint, d_em->integerType());
-  Type intintToReal = d_em->mkFunctionType(intint, d_em->realType());
-
-  Type intrealToBool = d_em->mkFunctionType(intreal, d_em->booleanType());
-  Type intrealToInt = d_em->mkFunctionType(intreal, d_em->integerType());
-  Type intrealToReal = d_em->mkFunctionType(intreal, d_em->realType());
-
-  Type realintToBool = d_em->mkFunctionType(realint, d_em->booleanType());
-  Type realintToInt = d_em->mkFunctionType(realint, d_em->integerType());
-  Type realintToReal = d_em->mkFunctionType(realint, d_em->realType());
-
-  Type realrealToBool = d_em->mkFunctionType(realreal, d_em->booleanType());
-  Type realrealToInt = d_em->mkFunctionType(realreal, d_em->integerType());
-  Type realrealToReal = d_em->mkFunctionType(realreal, d_em->realType());
-
-  Type realboolToBool = d_em->mkFunctionType(realbool, d_em->booleanType());
-  Type realboolToInt = d_em->mkFunctionType(realbool, d_em->integerType());
-  Type realboolToReal = d_em->mkFunctionType(realbool, d_em->realType());
-
-  Type boolrealToBool = d_em->mkFunctionType(boolreal, d_em->booleanType());
-  Type boolrealToInt = d_em->mkFunctionType(boolreal, d_em->integerType());
-  Type boolrealToReal = d_em->mkFunctionType(boolreal, d_em->realType());
+  std::vector<TypeNode> boolbool;
+  boolbool.push_back(d_nodeManager->booleanType());
+  boolbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> boolint;
+  boolint.push_back(d_nodeManager->booleanType());
+  boolint.push_back(d_nodeManager->integerType());
+  std::vector<TypeNode> intbool;
+  intbool.push_back(d_nodeManager->integerType());
+  intbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> intint;
+  intint.push_back(d_nodeManager->integerType());
+  intint.push_back(d_nodeManager->integerType());
+  std::vector<TypeNode> intreal;
+  intreal.push_back(d_nodeManager->integerType());
+  intreal.push_back(d_nodeManager->realType());
+  std::vector<TypeNode> realint;
+  realint.push_back(d_nodeManager->realType());
+  realint.push_back(d_nodeManager->integerType());
+  std::vector<TypeNode> realreal;
+  realreal.push_back(d_nodeManager->realType());
+  realreal.push_back(d_nodeManager->realType());
+  std::vector<TypeNode> realbool;
+  realbool.push_back(d_nodeManager->realType());
+  realbool.push_back(d_nodeManager->booleanType());
+  std::vector<TypeNode> boolreal;
+  boolreal.push_back(d_nodeManager->booleanType());
+  boolreal.push_back(d_nodeManager->realType());
+
+  TypeNode boolboolToBool =
+      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->booleanType());
+  TypeNode boolboolToInt =
+      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->integerType());
+  TypeNode boolboolToReal =
+      d_nodeManager->mkFunctionType(boolbool, d_nodeManager->realType());
+
+  TypeNode boolintToBool =
+      d_nodeManager->mkFunctionType(boolint, d_nodeManager->booleanType());
+  TypeNode boolintToInt =
+      d_nodeManager->mkFunctionType(boolint, d_nodeManager->integerType());
+  TypeNode boolintToReal =
+      d_nodeManager->mkFunctionType(boolint, d_nodeManager->realType());
+
+  TypeNode intboolToBool =
+      d_nodeManager->mkFunctionType(intbool, d_nodeManager->booleanType());
+  TypeNode intboolToInt =
+      d_nodeManager->mkFunctionType(intbool, d_nodeManager->integerType());
+  TypeNode intboolToReal =
+      d_nodeManager->mkFunctionType(intbool, d_nodeManager->realType());
+
+  TypeNode intintToBool =
+      d_nodeManager->mkFunctionType(intint, d_nodeManager->booleanType());
+  TypeNode intintToInt =
+      d_nodeManager->mkFunctionType(intint, d_nodeManager->integerType());
+  TypeNode intintToReal =
+      d_nodeManager->mkFunctionType(intint, d_nodeManager->realType());
+
+  TypeNode intrealToBool =
+      d_nodeManager->mkFunctionType(intreal, d_nodeManager->booleanType());
+  TypeNode intrealToInt =
+      d_nodeManager->mkFunctionType(intreal, d_nodeManager->integerType());
+  TypeNode intrealToReal =
+      d_nodeManager->mkFunctionType(intreal, d_nodeManager->realType());
+
+  TypeNode realintToBool =
+      d_nodeManager->mkFunctionType(realint, d_nodeManager->booleanType());
+  TypeNode realintToInt =
+      d_nodeManager->mkFunctionType(realint, d_nodeManager->integerType());
+  TypeNode realintToReal =
+      d_nodeManager->mkFunctionType(realint, d_nodeManager->realType());
+
+  TypeNode realrealToBool =
+      d_nodeManager->mkFunctionType(realreal, d_nodeManager->booleanType());
+  TypeNode realrealToInt =
+      d_nodeManager->mkFunctionType(realreal, d_nodeManager->integerType());
+  TypeNode realrealToReal =
+      d_nodeManager->mkFunctionType(realreal, d_nodeManager->realType());
+
+  TypeNode realboolToBool =
+      d_nodeManager->mkFunctionType(realbool, d_nodeManager->booleanType());
+  TypeNode realboolToInt =
+      d_nodeManager->mkFunctionType(realbool, d_nodeManager->integerType());
+  TypeNode realboolToReal =
+      d_nodeManager->mkFunctionType(realbool, d_nodeManager->realType());
+
+  TypeNode boolrealToBool =
+      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->booleanType());
+  TypeNode boolrealToInt =
+      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->integerType());
+  TypeNode boolrealToReal =
+      d_nodeManager->mkFunctionType(boolreal, d_nodeManager->realType());
 
   ASSERT_EQ(boolboolToBool.getCardinality().compare(16), Cardinality::EQUAL);
   ASSERT_EQ(boolboolToInt.getCardinality().compare(Cardinality::INTEGERS),
@@ -250,19 +283,20 @@ TEST_F(TestTypeCardinalityBlack, binary_functions)
 TEST_F(TestTypeCardinalityBlack, ternary_functions)
 {
   std::vector<TypeNode> boolbool;
-  boolbool.push_back(d_nm->booleanType());
-  boolbool.push_back(d_nm->booleanType());
+  boolbool.push_back(d_nodeManager->booleanType());
+  boolbool.push_back(d_nodeManager->booleanType());
   std::vector<TypeNode> boolboolbool = boolbool;
-  boolboolbool.push_back(d_nm->booleanType());
+  boolboolbool.push_back(d_nodeManager->booleanType());
 
-  TypeNode boolboolTuple = d_nm->mkTupleType(boolbool);
-  TypeNode boolboolboolTuple = d_nm->mkTupleType(boolboolbool);
+  TypeNode boolboolTuple = d_nodeManager->mkTupleType(boolbool);
+  TypeNode boolboolboolTuple = d_nodeManager->mkTupleType(boolboolbool);
 
   TypeNode boolboolboolToBool =
-      d_nm->mkFunctionType(boolboolbool, d_nm->booleanType());
-  TypeNode boolboolToBoolbool = d_nm->mkFunctionType(boolbool, boolboolTuple);
-  TypeNode boolToBoolboolbool =
-      d_nm->mkFunctionType(d_nm->booleanType(), boolboolboolTuple);
+      d_nodeManager->mkFunctionType(boolboolbool, d_nodeManager->booleanType());
+  TypeNode boolboolToBoolbool =
+      d_nodeManager->mkFunctionType(boolbool, boolboolTuple);
+  TypeNode boolToBoolboolbool = d_nodeManager->mkFunctionType(
+      d_nodeManager->booleanType(), boolboolboolTuple);
 
   ASSERT_EQ(boolboolboolToBool.getCardinality().compare(/* 2 ^ 8 */ 1 << 8),
             Cardinality::EQUAL);
@@ -275,7 +309,7 @@ TEST_F(TestTypeCardinalityBlack, ternary_functions)
 
 TEST_F(TestTypeCardinalityBlack, undefined_sorts)
 {
-  Type foo = d_em->mkSort("foo", NodeManager::SORT_FLAG_NONE);
+  TypeNode foo = d_nodeManager->mkSort("foo", NodeManager::SORT_FLAG_NONE);
   // We've currently assigned them a specific Beth number, which
   // isn't really correct, but...
   ASSERT_FALSE(foo.getCardinality().isFinite());
@@ -283,13 +317,13 @@ TEST_F(TestTypeCardinalityBlack, undefined_sorts)
 
 TEST_F(TestTypeCardinalityBlack, bitvectors)
 {
-  ASSERT_EQ(d_em->mkBitVectorType(0).getCardinality().compare(0),
+  ASSERT_EQ(d_nodeManager->mkBitVectorType(0).getCardinality().compare(0),
             Cardinality::EQUAL);
   Cardinality lastCard = 0;
   for (unsigned i = 1; i <= 65; ++i)
   {
     Cardinality card = Cardinality(2) ^ i;
-    Cardinality typeCard = d_em->mkBitVectorType(i).getCardinality();
+    Cardinality typeCard = d_nodeManager->mkBitVectorType(i).getCardinality();
     ASSERT_TRUE(typeCard.compare(lastCard) == Cardinality::GREATER
                 || (typeCard.isLargeFinite() && lastCard.isLargeFinite()));
     ASSERT_TRUE(typeCard.compare(card) == Cardinality::EQUAL