Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Black box testing of cvc5::theory.
11 : : */
12 : :
13 : : #include <sstream>
14 : : #include <vector>
15 : :
16 : : #include "expr/array_store_all.h"
17 : : #include "expr/node.h"
18 : : #include "expr/node_builder.h"
19 : : #include "expr/node_value.h"
20 : : #include "test_smt.h"
21 : : #include "theory/rewriter.h"
22 : : #include "util/bitvector.h"
23 : : #include "util/rational.h"
24 : :
25 : : namespace cvc5::internal {
26 : :
27 : : using namespace context;
28 : : using namespace theory;
29 : :
30 : : namespace test {
31 : :
32 : : class TestTheoryBlack : public TestSmt
33 : : {
34 : : };
35 : :
36 : 4 : TEST_F(TestTheoryBlack, array_const)
37 : : {
38 : 1 : Rewriter* rr = d_slvEngine->getEnv().getRewriter();
39 : 3 : TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
40 : 2 : d_nodeManager->integerType());
41 : 1 : Node zero = d_nodeManager->mkConstInt(Rational(0));
42 : 1 : Node one = d_nodeManager->mkConstInt(Rational(1));
43 : 1 : Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
44 [ - + ][ + - ]: 1 : ASSERT_TRUE(storeAll.isConst());
45 : :
46 : 2 : Node arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
47 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr.isConst());
48 : 1 : arr = rr->rewrite(arr);
49 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
50 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, one);
51 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
52 : 2 : Node arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
53 : 1 : arr2 = rr->rewrite(arr2);
54 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
55 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
56 : 1 : arr2 = rr->rewrite(arr2);
57 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
58 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, one);
59 : 1 : arr2 = rr->rewrite(arr2);
60 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
61 : :
62 : 2 : arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
63 : 2 : d_nodeManager->mkBitVectorType(1));
64 : 1 : zero = d_nodeManager->mkConst(BitVector(1, 0u));
65 : 1 : one = d_nodeManager->mkConst(BitVector(1, 1u));
66 : 1 : storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
67 [ - + ][ + - ]: 1 : ASSERT_TRUE(storeAll.isConst());
68 : :
69 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
70 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr.isConst());
71 : 1 : arr = rr->rewrite(arr);
72 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
73 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, one);
74 : 1 : arr = rr->rewrite(arr);
75 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
76 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
77 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
78 : 1 : arr2 = rr->rewrite(arr2);
79 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
80 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
81 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
82 : 1 : arr2 = rr->rewrite(arr2);
83 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
84 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, one);
85 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
86 : 1 : arr2 = rr->rewrite(arr2);
87 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
88 : :
89 : 2 : arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2),
90 : 2 : d_nodeManager->mkBitVectorType(2));
91 : 1 : zero = d_nodeManager->mkConst(BitVector(2, 0u));
92 : 1 : one = d_nodeManager->mkConst(BitVector(2, 1u));
93 : 1 : Node two = d_nodeManager->mkConst(BitVector(2, 2u));
94 : 1 : Node three = d_nodeManager->mkConst(BitVector(2, 3u));
95 : 1 : storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, one));
96 [ - + ][ + - ]: 1 : ASSERT_TRUE(storeAll.isConst());
97 : :
98 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, zero, zero);
99 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
100 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, zero);
101 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
102 : 1 : arr2 = rr->rewrite(arr2);
103 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
104 : :
105 : 1 : arr = d_nodeManager->mkNode(Kind::STORE, storeAll, one, three);
106 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr.isConst());
107 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, one, one);
108 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
109 : 1 : arr2 = rr->rewrite(arr2);
110 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2 == storeAll);
111 : :
112 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr, zero, zero);
113 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
114 [ - + ][ + - ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
115 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, two, two);
116 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
117 [ - + ][ + - ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
118 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, three, one);
119 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
120 [ - + ][ + - ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
121 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, three, three);
122 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
123 [ - + ][ + - ]: 1 : ASSERT_TRUE(rr->rewrite(arr2).isConst());
124 : 1 : arr2 = d_nodeManager->mkNode(Kind::STORE, arr2, two, zero);
125 [ - + ][ + - ]: 1 : ASSERT_FALSE(arr2.isConst());
126 : 1 : arr2 = rr->rewrite(arr2);
127 [ - + ][ + - ]: 1 : ASSERT_TRUE(arr2.isConst());
128 [ + - ][ + - ]: 1 : }
[ + - ][ + - ]
129 : : } // namespace test
130 : : } // namespace cvc5::internal
|
