1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz |
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 |
|
* Black box testing of cvc5::Kind. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <iostream> |
17 |
|
#include <sstream> |
18 |
|
#include <string> |
19 |
|
|
20 |
|
#include "expr/kind.h" |
21 |
|
#include "test.h" |
22 |
|
|
23 |
|
namespace cvc5 { |
24 |
|
|
25 |
|
using namespace kind; |
26 |
|
|
27 |
|
namespace test { |
28 |
|
|
29 |
16 |
class TestNodeBlackKind : public TestInternal |
30 |
|
{ |
31 |
|
protected: |
32 |
8 |
void SetUp() override |
33 |
|
{ |
34 |
8 |
d_undefined = UNDEFINED_KIND; |
35 |
8 |
d_null = NULL_EXPR; |
36 |
8 |
d_last = LAST_KIND; |
37 |
8 |
d_beyond = ((int32_t)LAST_KIND) + 1; |
38 |
8 |
d_unknown = (Kind)d_beyond; |
39 |
8 |
} |
40 |
|
|
41 |
6 |
bool string_is_as_expected(Kind k, const char* s) |
42 |
|
{ |
43 |
12 |
std::stringstream act; |
44 |
12 |
std::stringstream exp; |
45 |
6 |
act << k; |
46 |
6 |
exp << s; |
47 |
12 |
return act.str() == exp.str(); |
48 |
|
} |
49 |
|
|
50 |
|
Kind d_undefined; |
51 |
|
Kind d_unknown; |
52 |
|
Kind d_null; |
53 |
|
Kind d_last; |
54 |
|
int32_t d_beyond; |
55 |
|
}; |
56 |
|
|
57 |
13 |
TEST_F(TestNodeBlackKind, equality) |
58 |
|
{ |
59 |
2 |
ASSERT_EQ(d_undefined, UNDEFINED_KIND); |
60 |
2 |
ASSERT_EQ(d_last, LAST_KIND); |
61 |
|
} |
62 |
|
|
63 |
13 |
TEST_F(TestNodeBlackKind, order) |
64 |
|
{ |
65 |
2 |
ASSERT_LT((int32_t)d_undefined, (int32_t)d_null); |
66 |
2 |
ASSERT_LT((int32_t)d_null, (int32_t)d_last); |
67 |
2 |
ASSERT_LT((int32_t)d_undefined, (int32_t)d_last); |
68 |
2 |
ASSERT_LT((int32_t)d_last, (int32_t)d_unknown); |
69 |
|
} |
70 |
|
|
71 |
13 |
TEST_F(TestNodeBlackKind, output) |
72 |
|
{ |
73 |
2 |
ASSERT_TRUE(string_is_as_expected(d_undefined, "UNDEFINED_KIND")); |
74 |
2 |
ASSERT_TRUE(string_is_as_expected(d_null, "NULL")); |
75 |
2 |
ASSERT_TRUE(string_is_as_expected(d_last, "LAST_KIND")); |
76 |
|
} |
77 |
|
|
78 |
13 |
TEST_F(TestNodeBlackKind, output_concat) |
79 |
|
{ |
80 |
4 |
std::stringstream act, exp; |
81 |
2 |
act << d_undefined << d_null << d_last << d_unknown; |
82 |
|
exp << "UNDEFINED_KIND" |
83 |
|
<< "NULL" |
84 |
|
<< "LAST_KIND" |
85 |
2 |
<< "?"; |
86 |
2 |
ASSERT_EQ(act.str(), exp.str()); |
87 |
|
} |
88 |
|
} // namespace test |
89 |
15 |
} // namespace cvc5 |