GCC Code Coverage Report
Directory: . Exec Total Coverage
File: test/unit/theory/theory_black.cpp Lines: 86 86 100.0 %
Date: 2021-03-23 Branches: 328 944 34.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_black.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Aina Niemetz
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Black box testing of CVC4::theory
13
 **
14
 ** Black box testing of CVC4::theory
15
 **/
16
17
#include <sstream>
18
#include <vector>
19
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
26
namespace CVC4 {
27
28
using namespace kind;
29
using namespace context;
30
using namespace theory;
31
32
namespace test {
33
34
4
class TestTheoryBlack : public TestSmt
35
{
36
};
37
38
10
TEST_F(TestTheoryBlack, array_const)
39
{
40
4
  TypeNode arrType = d_nodeManager->mkArrayType(d_nodeManager->integerType(),
41
8
                                                d_nodeManager->integerType());
42
4
  Node zero = d_nodeManager->mkConst(Rational(0));
43
4
  Node one = d_nodeManager->mkConst(Rational(1));
44
4
  Node storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
45
2
  ASSERT_TRUE(storeAll.isConst());
46
47
4
  Node arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
48
2
  ASSERT_FALSE(arr.isConst());
49
2
  arr = Rewriter::rewrite(arr);
50
2
  ASSERT_TRUE(arr.isConst());
51
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
52
2
  ASSERT_TRUE(arr.isConst());
53
4
  Node arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
54
2
  ASSERT_FALSE(arr2.isConst());
55
2
  arr2 = Rewriter::rewrite(arr2);
56
2
  ASSERT_TRUE(arr2.isConst());
57
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
58
2
  ASSERT_TRUE(arr2.isConst());
59
2
  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
60
2
  ASSERT_FALSE(arr2.isConst());
61
2
  arr2 = Rewriter::rewrite(arr2);
62
2
  ASSERT_TRUE(arr2.isConst());
63
64
4
  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(1),
65
4
                                       d_nodeManager->mkBitVectorType(1));
66
2
  zero = d_nodeManager->mkConst(BitVector(1, 0u));
67
2
  one = d_nodeManager->mkConst(BitVector(1, 1u));
68
2
  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, zero));
69
2
  ASSERT_TRUE(storeAll.isConst());
70
71
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
72
2
  ASSERT_FALSE(arr.isConst());
73
2
  arr = Rewriter::rewrite(arr);
74
2
  ASSERT_TRUE(arr.isConst());
75
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, one);
76
2
  arr = Rewriter::rewrite(arr);
77
2
  ASSERT_TRUE(arr.isConst());
78
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
79
2
  ASSERT_FALSE(arr2.isConst());
80
2
  arr2 = Rewriter::rewrite(arr2);
81
2
  ASSERT_TRUE(arr2.isConst());
82
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
83
2
  ASSERT_FALSE(arr2.isConst());
84
2
  arr2 = Rewriter::rewrite(arr2);
85
2
  ASSERT_TRUE(arr2.isConst());
86
2
  arr2 = d_nodeManager->mkNode(STORE, arr, zero, one);
87
2
  ASSERT_FALSE(arr2.isConst());
88
2
  arr2 = Rewriter::rewrite(arr2);
89
2
  ASSERT_TRUE(arr2.isConst());
90
91
4
  arrType = d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(2),
92
4
                                       d_nodeManager->mkBitVectorType(2));
93
2
  zero = d_nodeManager->mkConst(BitVector(2, 0u));
94
2
  one = d_nodeManager->mkConst(BitVector(2, 1u));
95
4
  Node two = d_nodeManager->mkConst(BitVector(2, 2u));
96
4
  Node three = d_nodeManager->mkConst(BitVector(2, 3u));
97
2
  storeAll = d_nodeManager->mkConst(ArrayStoreAll(arrType, one));
98
2
  ASSERT_TRUE(storeAll.isConst());
99
100
2
  arr = d_nodeManager->mkNode(STORE, storeAll, zero, zero);
101
2
  ASSERT_TRUE(arr.isConst());
102
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, zero);
103
2
  ASSERT_FALSE(arr2.isConst());
104
2
  arr2 = Rewriter::rewrite(arr2);
105
2
  ASSERT_TRUE(arr2.isConst());
106
107
2
  arr = d_nodeManager->mkNode(STORE, storeAll, one, three);
108
2
  ASSERT_TRUE(arr.isConst());
109
2
  arr2 = d_nodeManager->mkNode(STORE, arr, one, one);
110
2
  ASSERT_FALSE(arr2.isConst());
111
2
  arr2 = Rewriter::rewrite(arr2);
112
2
  ASSERT_TRUE(arr2 == storeAll);
113
114
2
  arr2 = d_nodeManager->mkNode(STORE, arr, zero, zero);
115
2
  ASSERT_FALSE(arr2.isConst());
116
2
  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
117
2
  arr2 = d_nodeManager->mkNode(STORE, arr2, two, two);
118
2
  ASSERT_FALSE(arr2.isConst());
119
2
  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
120
2
  arr2 = d_nodeManager->mkNode(STORE, arr2, three, one);
121
2
  ASSERT_FALSE(arr2.isConst());
122
2
  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
123
2
  arr2 = d_nodeManager->mkNode(STORE, arr2, three, three);
124
2
  ASSERT_FALSE(arr2.isConst());
125
2
  ASSERT_TRUE(Rewriter::rewrite(arr2).isConst());
126
2
  arr2 = d_nodeManager->mkNode(STORE, arr2, two, zero);
127
2
  ASSERT_FALSE(arr2.isConst());
128
2
  arr2 = Rewriter::rewrite(arr2);
129
2
  ASSERT_TRUE(arr2.isConst());
130
}
131
}  // namespace test
132
32150
}  // namespace CVC4