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::theory. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <sstream> |
17 |
|
#include <vector> |
18 |
|
|
19 |
|
#include "expr/node.h" |
20 |
|
#include "expr/node_builder.h" |
21 |
|
#include "expr/node_value.h" |
22 |
|
#include "test_smt.h" |
23 |
|
#include "theory/rewriter.h" |
24 |
|
|
25 |
|
namespace cvc5 { |
26 |
|
|
27 |
|
using namespace kind; |
28 |
|
using namespace context; |
29 |
|
using namespace theory; |
30 |
|
|
31 |
|
namespace test { |
32 |
|
|
33 |
4 |
class TestTheoryBlack : public TestSmt |
34 |
|
{ |
35 |
|
}; |
36 |
|
|
37 |
10 |
TEST_F(TestTheoryBlack, array_const) |
38 |
|
{ |
39 |
4 |
TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(), |
40 |
8 |
d_nodeManager->integerType()); |
41 |
4 |
Node zero = d_nodeManager->mkConst(Rational(0)); |
42 |
4 |
Node one = d_nodeManager->mkConst(Rational(1)); |
43 |
4 |
Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); |
44 |
2 |
ASSERT_TRUE(storeAll.isConst()); |
45 |
|
|
46 |
4 |
Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); |
47 |
2 |
ASSERT_FALSE(arr.isConst()); |
48 |
2 |
arr = Rewriter::rewrite(arr); |
49 |
2 |
ASSERT_TRUE(arr.isConst()); |
50 |
2 |
arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); |
51 |
2 |
ASSERT_TRUE(arr.isConst()); |
52 |
4 |
Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); |
53 |
2 |
ASSERT_FALSE(arr2.isConst()); |
54 |
2 |
arr2 = Rewriter::rewrite(arr2); |
55 |
2 |
ASSERT_TRUE(arr2.isConst()); |
56 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, one, one); |
57 |
2 |
ASSERT_TRUE(arr2.isConst()); |
58 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); |
59 |
2 |
ASSERT_FALSE(arr2.isConst()); |
60 |
2 |
arr2 = Rewriter::rewrite(arr2); |
61 |
2 |
ASSERT_TRUE(arr2.isConst()); |
62 |
|
|
63 |
4 |
arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1), |
64 |
4 |
d_nodeManager->mkBitVectorType(1)); |
65 |
2 |
zero = d_nodeManager->mkConst(BitVector(1, 0u)); |
66 |
2 |
one = d_nodeManager->mkConst(BitVector(1, 1u)); |
67 |
2 |
storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero)); |
68 |
2 |
ASSERT_TRUE(storeAll.isConst()); |
69 |
|
|
70 |
2 |
arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); |
71 |
2 |
ASSERT_FALSE(arr.isConst()); |
72 |
2 |
arr = Rewriter::rewrite(arr); |
73 |
2 |
ASSERT_TRUE(arr.isConst()); |
74 |
2 |
arr = d_nodeManager->mkNode(STORE, storeAll, zero, one); |
75 |
2 |
arr = Rewriter::rewrite(arr); |
76 |
2 |
ASSERT_TRUE(arr.isConst()); |
77 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); |
78 |
2 |
ASSERT_FALSE(arr2.isConst()); |
79 |
2 |
arr2 = Rewriter::rewrite(arr2); |
80 |
2 |
ASSERT_TRUE(arr2.isConst()); |
81 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, one, one); |
82 |
2 |
ASSERT_FALSE(arr2.isConst()); |
83 |
2 |
arr2 = Rewriter::rewrite(arr2); |
84 |
2 |
ASSERT_TRUE(arr2.isConst()); |
85 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, zero, one); |
86 |
2 |
ASSERT_FALSE(arr2.isConst()); |
87 |
2 |
arr2 = Rewriter::rewrite(arr2); |
88 |
2 |
ASSERT_TRUE(arr2.isConst()); |
89 |
|
|
90 |
4 |
arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2), |
91 |
4 |
d_nodeManager->mkBitVectorType(2)); |
92 |
2 |
zero = d_nodeManager->mkConst(BitVector(2, 0u)); |
93 |
2 |
one = d_nodeManager->mkConst(BitVector(2, 1u)); |
94 |
4 |
Node two = d_nodeManager->mkConst(BitVector(2, 2u)); |
95 |
4 |
Node three = d_nodeManager->mkConst(BitVector(2, 3u)); |
96 |
2 |
storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, one)); |
97 |
2 |
ASSERT_TRUE(storeAll.isConst()); |
98 |
|
|
99 |
2 |
arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero); |
100 |
2 |
ASSERT_TRUE(arr.isConst()); |
101 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, one, zero); |
102 |
2 |
ASSERT_FALSE(arr2.isConst()); |
103 |
2 |
arr2 = Rewriter::rewrite(arr2); |
104 |
2 |
ASSERT_TRUE(arr2.isConst()); |
105 |
|
|
106 |
2 |
arr = d_nodeManager->mkNode(STORE, storeAll, one, three); |
107 |
2 |
ASSERT_TRUE(arr.isConst()); |
108 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, one, one); |
109 |
2 |
ASSERT_FALSE(arr2.isConst()); |
110 |
2 |
arr2 = Rewriter::rewrite(arr2); |
111 |
2 |
ASSERT_TRUE(arr2 == storeAll); |
112 |
|
|
113 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr, zero, zero); |
114 |
2 |
ASSERT_FALSE(arr2.isConst()); |
115 |
2 |
ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); |
116 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr2, two, two); |
117 |
2 |
ASSERT_FALSE(arr2.isConst()); |
118 |
2 |
ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); |
119 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr2, three, one); |
120 |
2 |
ASSERT_FALSE(arr2.isConst()); |
121 |
2 |
ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); |
122 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr2, three, three); |
123 |
2 |
ASSERT_FALSE(arr2.isConst()); |
124 |
2 |
ASSERT_TRUE(Rewriter::rewrite(arr2).isConst()); |
125 |
2 |
arr2 = d_nodeManager->mkNode(STORE, arr2, two, zero); |
126 |
2 |
ASSERT_FALSE(arr2.isConst()); |
127 |
2 |
arr2 = Rewriter::rewrite(arr2); |
128 |
2 |
ASSERT_TRUE(arr2.isConst()); |
129 |
|
} |
130 |
|
} // namespace test |
131 |
31788 |
} // namespace cvc5 |