Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Aina Niemetz, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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::internal {
29 : :
30 : : using namespace context;
31 : : using namespace theory;
32 : :
33 : : namespace test {
34 : :
35 : : class TestTheoryBlack : public TestSmt
36 : : {
37 : : };
38 : :
39 : 2 : TEST_F(TestTheoryBlack, array_const)
40 : : {
41 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
42 : 3 : TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
43 : 3 : d_nodeManager->integerType());
44 : 1 : Node zero = d_nodeManager->mkConstInt(Rational(0));
45 : 1 : Node one = d_nodeManager->mkConstInt(Rational(1));
46 : 1 : Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
47 [ - + ]: 1 : ASSERT_TRUE(storeAll.isConst());
48 : :
49 : 2 : Node arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
50 [ - + ]: 1 : ASSERT_FALSE(arr.isConst());
51 : 1 : arr = rr->rewrite(arr);
52 [ - + ]: 1 : ASSERT_TRUE(arr.isConst());
53 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, one);
54 [ - + ]: 1 : ASSERT_TRUE(arr.isConst());
55 : 2 : Node arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
56 : 1 : arr2 = rr->rewrite(arr2);
57 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
58 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
59 : 1 : arr2 = rr->rewrite(arr2);
60 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
61 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, one);
62 : 1 : arr2 = rr->rewrite(arr2);
63 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
64 : :
65 : 2 : arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
66 : 2 : d_nodeManager->mkBitVectorType(1));
67 : 1 : zero = d_nodeManager->mkConst(BitVector(1, 0u));
68 : 1 : one = d_nodeManager->mkConst(BitVector(1, 1u));
69 : 1 : storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
70 [ - + ]: 1 : ASSERT_TRUE(storeAll.isConst());
71 : :
72 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
73 [ - + ]: 1 : ASSERT_FALSE(arr.isConst());
74 : 1 : arr = rr->rewrite(arr);
75 [ - + ]: 1 : ASSERT_TRUE(arr.isConst());
76 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, one);
77 : 1 : arr = rr->rewrite(arr);
78 [ - + ]: 1 : ASSERT_TRUE(arr.isConst());
79 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
80 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
81 : 1 : arr2 = rr->rewrite(arr2);
82 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
83 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
84 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
85 : 1 : arr2 = rr->rewrite(arr2);
86 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
87 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, one);
88 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
89 : 1 : arr2 = rr->rewrite(arr2);
90 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
91 : :
92 : 2 : arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2),
93 : 2 : d_nodeManager->mkBitVectorType(2));
94 : 1 : zero = d_nodeManager->mkConst(BitVector(2, 0u));
95 : 1 : one = d_nodeManager->mkConst(BitVector(2, 1u));
96 : 1 : Node two = d_nodeManager->mkConst(BitVector(2, 2u));
97 : 1 : Node three = d_nodeManager->mkConst(BitVector(2, 3u));
98 : 1 : storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, one));
99 [ - + ]: 1 : ASSERT_TRUE(storeAll.isConst());
100 : :
101 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
102 [ - + ]: 1 : ASSERT_TRUE(arr.isConst());
103 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
104 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
105 : 1 : arr2 = rr->rewrite(arr2);
106 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
107 : :
108 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, one, three);
109 [ - + ]: 1 : ASSERT_TRUE(arr.isConst());
110 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
111 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
112 : 1 : arr2 = rr->rewrite(arr2);
113 [ - + ]: 1 : ASSERT_TRUE(arr2 == storeAll);
114 : :
115 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, zero);
116 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
117 [ - + ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
118 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, two, two);
119 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
120 [ - + ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
121 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, three, one);
122 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
123 [ - + ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
124 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, three, three);
125 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
126 [ - + ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
127 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, two, zero);
128 [ - + ]: 1 : ASSERT_FALSE(arr2.isConst());
129 : 1 : arr2 = rr->rewrite(arr2);
130 [ - + ]: 1 : ASSERT_TRUE(arr2.isConst());
131 : : }
132 : : } // namespace test
133 : : } // namespace cvc5::internal
|
