Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	test/unit/theory/theory_sets_type_enumerator_white.cpp	Lines:	80	80	100.0 %
Date:	2021-05-22	Branches:	259	752	34.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Andrew Reynolds, Mudathir Mohamed
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * White box testing of cvc5::theory::sets::SetsTypeEnumerator
 *
 * These tests depend on the ordering that the SetsTypeEnumerator use, so
 * it's a white-box test.
 */

#include "expr/dtype.h"
#include "test_smt.h"
#include "theory/sets/theory_sets_type_enumerator.h"

namespace cvc5 {

using namespace theory;
using namespace kind;
using namespace theory::sets;

namespace test {

class TestTheoryWhiteSetsTypeEnumerator : public TestSmt
{
 protected:
  void addAndCheckUnique(Node n, std::vector<Node>& elems)
  {
    ASSERT_TRUE(n.isConst());
    ASSERT_TRUE(std::find(elems.begin(), elems.end(), n) == elems.end());
    elems.push_back(n);
  }
};

TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans)
{
  TypeNode boolType = d_nodeManager->booleanType();
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(boolType));
  ASSERT_FALSE(setEnumerator.isFinished());

  std::vector<Node> elems;

  Node actual0 = *setEnumerator;
  addAndCheckUnique(actual0, elems);
  ASSERT_FALSE(setEnumerator.isFinished());

  Node actual1 = *++setEnumerator;
  addAndCheckUnique(actual1, elems);
  ASSERT_FALSE(setEnumerator.isFinished());

  Node actual2 = *++setEnumerator;
  addAndCheckUnique(actual2, elems);
  ASSERT_FALSE(setEnumerator.isFinished());

  Node actual3 = Rewriter::rewrite(*++setEnumerator);
  addAndCheckUnique(actual3, elems);
  ASSERT_FALSE(setEnumerator.isFinished());

  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
}

TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_UF)
{
  TypeNode sort = d_nodeManager->mkSort("Atom");
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(sort));

  Node actual0 = *setEnumerator;
  Node expected0 =
      d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(sort)));
  ASSERT_EQ(expected0, actual0);
  ASSERT_FALSE(setEnumerator.isFinished());

  std::vector<Node> elems;
  for (unsigned i = 0; i < 7; i++)
  {
    Node actual = *setEnumerator;
    addAndCheckUnique(actual, elems);
    ASSERT_FALSE(setEnumerator.isFinished());
    ++setEnumerator;
  }
}

TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_finite_dataype)
{
  DType dt("Colors");
  dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
  dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
  dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
  TypeNode datatype = d_nodeManager->mkDatatypeType(dt);
  const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
      datatype.getDType().getConstructors();
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(datatype));

  Node red =
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor());

  Node green =
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor());

  Node blue =
      d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());

  std::vector<Node> elems;
  for (unsigned i = 0; i < 8; i++)
  {
    Node actual = *setEnumerator;
    addAndCheckUnique(actual, elems);
    ASSERT_FALSE(setEnumerator.isFinished());
    ++setEnumerator;
  }

  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
}

TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv)
{
  TypeNode bitVector2 = d_nodeManager->mkBitVectorType(2);
  SetEnumerator setEnumerator(d_nodeManager->mkSetType(bitVector2));

  std::vector<Node> elems;
  for (unsigned i = 0; i < 16; i++)
  {
    Node actual = *setEnumerator;
    addAndCheckUnique(actual, elems);
    ASSERT_FALSE(setEnumerator.isFinished());
    ++setEnumerator;
  }

  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
  ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
  ASSERT_TRUE(setEnumerator.isFinished());
}
}  // namespace test
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Andrew Reynolds, Mudathir Mohamed
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* White box testing of cvc5::theory::sets::SetsTypeEnumerator
14		*
15		* These tests depend on the ordering that the SetsTypeEnumerator use, so
16		* it's a white-box test.
17		*/
18
19		#include "expr/dtype.h"
20		#include "test_smt.h"
21		#include "theory/sets/theory_sets_type_enumerator.h"
22
23		namespace cvc5 {
24
25		using namespace theory;
26		using namespace kind;
27		using namespace theory::sets;
28
29		namespace test {
30
31	16	class TestTheoryWhiteSetsTypeEnumerator : public TestSmt
32		{
33		protected:
34	70	void addAndCheckUnique(Node n, std::vector<Node>& elems)
35		{
36	70	ASSERT_TRUE(n.isConst());
37	70	ASSERT_TRUE(std::find(elems.begin(), elems.end(), n) == elems.end());
38	70	elems.push_back(n);
39		}
40		};
41
42	13	TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_booleans)
43		{
44	4	TypeNode boolType = d_nodeManager->booleanType();
45	4	SetEnumerator setEnumerator(d_nodeManager->mkSetType(boolType));
46	2	ASSERT_FALSE(setEnumerator.isFinished());
47
48	4	std::vector<Node> elems;
49
50	4	Node actual0 = *setEnumerator;
51	2	addAndCheckUnique(actual0, elems);
52	2	ASSERT_FALSE(setEnumerator.isFinished());
53
54	4	Node actual1 = *++setEnumerator;
55	2	addAndCheckUnique(actual1, elems);
56	2	ASSERT_FALSE(setEnumerator.isFinished());
57
58	4	Node actual2 = *++setEnumerator;
59	2	addAndCheckUnique(actual2, elems);
60	2	ASSERT_FALSE(setEnumerator.isFinished());
61
62	4	Node actual3 = Rewriter::rewrite(*++setEnumerator);
63	2	addAndCheckUnique(actual3, elems);
64	2	ASSERT_FALSE(setEnumerator.isFinished());
65
66	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
67	2	ASSERT_TRUE(setEnumerator.isFinished());
68	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
69	2	ASSERT_TRUE(setEnumerator.isFinished());
70	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
71	2	ASSERT_TRUE(setEnumerator.isFinished());
72		}
73
74	13	TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_UF)
75		{
76	4	TypeNode sort = d_nodeManager->mkSort("Atom");
77	4	SetEnumerator setEnumerator(d_nodeManager->mkSetType(sort));
78
79	4	Node actual0 = *setEnumerator;
80		Node expected0 =
81	4	d_nodeManager->mkConst(EmptySet(d_nodeManager->mkSetType(sort)));
82	2	ASSERT_EQ(expected0, actual0);
83	2	ASSERT_FALSE(setEnumerator.isFinished());
84
85	4	std::vector<Node> elems;
86	16	for (unsigned i = 0; i < 7; i++)
87		{
88	28	Node actual = *setEnumerator;
89	14	addAndCheckUnique(actual, elems);
90	14	ASSERT_FALSE(setEnumerator.isFinished());
91	14	++setEnumerator;
92		}
93		}
94
95	13	TEST_F(TestTheoryWhiteSetsTypeEnumerator, set_of_finite_dataype)
96		{
97	4	DType dt("Colors");
98	2	dt.addConstructor(std::make_shared<DTypeConstructor>("red"));
99	2	dt.addConstructor(std::make_shared<DTypeConstructor>("green"));
100	2	dt.addConstructor(std::make_shared<DTypeConstructor>("blue"));
101	4	TypeNode datatype = d_nodeManager->mkDatatypeType(dt);
102		const std::vector<std::shared_ptr<DTypeConstructor> >& dtcons =
103	2	datatype.getDType().getConstructors();
104	4	SetEnumerator setEnumerator(d_nodeManager->mkSetType(datatype));
105
106		Node red =
107	4	d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[0]->getConstructor());
108
109		Node green =
110	4	d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[1]->getConstructor());
111
112		Node blue =
113	4	d_nodeManager->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
114
115	4	std::vector<Node> elems;
116	18	for (unsigned i = 0; i < 8; i++)
117		{
118	32	Node actual = *setEnumerator;
119	16	addAndCheckUnique(actual, elems);
120	16	ASSERT_FALSE(setEnumerator.isFinished());
121	16	++setEnumerator;
122		}
123
124	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
125	2	ASSERT_TRUE(setEnumerator.isFinished());
126	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
127	2	ASSERT_TRUE(setEnumerator.isFinished());
128	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
129	2	ASSERT_TRUE(setEnumerator.isFinished());
130		}
131
132	13	TEST_F(TestTheoryWhiteSetsTypeEnumerator, bv)
133		{
134	4	TypeNode bitVector2 = d_nodeManager->mkBitVectorType(2);
135	4	SetEnumerator setEnumerator(d_nodeManager->mkSetType(bitVector2));
136
137	4	std::vector<Node> elems;
138	34	for (unsigned i = 0; i < 16; i++)
139		{
140	64	Node actual = *setEnumerator;
141	32	addAndCheckUnique(actual, elems);
142	32	ASSERT_FALSE(setEnumerator.isFinished());
143	32	++setEnumerator;
144		}
145
146	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
147	2	ASSERT_TRUE(setEnumerator.isFinished());
148	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
149	2	ASSERT_TRUE(setEnumerator.isFinished());
150	4	ASSERT_THROW(*++setEnumerator, NoMoreValuesException);
151	2	ASSERT_TRUE(setEnumerator.isFinished());
152		}
153		} // namespace test
154	74671	} // namespace cvc5