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