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 expr/algorithms/
11 : : */
12 : :
13 : : #include "base/output.h"
14 : : #include "expr/algorithm/flatten.h"
15 : : #include "expr/node_manager.h"
16 : : #include "test_node.h"
17 : :
18 : : namespace cvc5::internal {
19 : :
20 : : using namespace expr;
21 : : using namespace kind;
22 : :
23 : : namespace test {
24 : :
25 : : class TestNodeBlackNodeAlgorithms : public TestNode
26 : : {
27 : : };
28 : :
29 : 4 : TEST_F(TestNodeBlackNodeAlgorithms, flatten)
30 : : {
31 : : {
32 : 1 : Node x = d_nodeManager->mkBoundVar(*d_realTypeNode);
33 : 2 : Node n = d_nodeManager->mkNode(Kind::ADD, x, x);
34 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n));
35 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD));
36 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT));
37 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT));
38 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n), n);
39 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n, Kind::ADD), n);
40 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n, Kind::MULT), n);
41 [ - + ]: 2 : EXPECT_EQ(
42 : : expr::algorithm::flatten(d_nodeManager.get(), n, Kind::ADD, Kind::MULT),
43 : 1 : n);
44 : :
45 : : {
46 : 1 : std::vector<TNode> children;
47 : 1 : expr::algorithm::flatten(n, children);
48 [ - + ]: 1 : EXPECT_EQ(children.size(), 2);
49 [ - + ]: 1 : EXPECT_EQ(children[0], x);
50 [ - + ]: 1 : EXPECT_EQ(children[1], x);
51 : 1 : }
52 : : {
53 : 1 : std::vector<TNode> children;
54 : 1 : expr::algorithm::flatten(n, children, Kind::ADD);
55 [ - + ]: 1 : EXPECT_EQ(children.size(), 2);
56 [ - + ]: 1 : EXPECT_EQ(children[0], x);
57 [ - + ]: 1 : EXPECT_EQ(children[1], x);
58 : 1 : }
59 : : {
60 : 1 : std::vector<TNode> children;
61 : 1 : expr::algorithm::flatten(n, children, Kind::MULT);
62 [ - + ]: 1 : EXPECT_EQ(children.size(), 1);
63 [ - + ]: 1 : EXPECT_EQ(children[0], n);
64 : 1 : }
65 : : {
66 : 1 : std::vector<TNode> children;
67 : 1 : expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT);
68 [ - + ]: 1 : EXPECT_EQ(children.size(), 2);
69 [ - + ]: 1 : EXPECT_EQ(children[0], x);
70 [ - + ]: 1 : EXPECT_EQ(children[1], x);
71 : 1 : }
72 : 1 : }
73 : : {
74 : 1 : Node x = d_nodeManager->mkBoundVar(*d_realTypeNode);
75 : 1 : Node n = d_nodeManager->mkNode(
76 : 2 : Kind::ADD, x, d_nodeManager->mkNode(Kind::ADD, x, x));
77 [ - + ]: 1 : EXPECT_TRUE(expr::algorithm::canFlatten(n));
78 [ - + ]: 1 : EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD));
79 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT));
80 [ - + ]: 1 : EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT));
81 [ - + ]: 2 : EXPECT_NE(expr::algorithm::flatten(d_nodeManager.get(), n), n);
82 [ - + ]: 2 : EXPECT_NE(expr::algorithm::flatten(d_nodeManager.get(), n, Kind::ADD), n);
83 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n, Kind::MULT), n);
84 [ - + ]: 2 : EXPECT_NE(
85 : : expr::algorithm::flatten(d_nodeManager.get(), n, Kind::ADD, Kind::MULT),
86 : 1 : n);
87 : :
88 : : {
89 : 1 : std::vector<TNode> children;
90 : 1 : expr::algorithm::flatten(n, children);
91 [ - + ]: 1 : EXPECT_EQ(children.size(), 3);
92 [ - + ]: 1 : EXPECT_EQ(children[0], x);
93 [ - + ]: 1 : EXPECT_EQ(children[1], x);
94 [ - + ]: 1 : EXPECT_EQ(children[2], x);
95 : 1 : }
96 : : {
97 : 1 : std::vector<TNode> children;
98 : 1 : expr::algorithm::flatten(n, children, Kind::ADD);
99 [ - + ]: 1 : EXPECT_EQ(children.size(), 3);
100 [ - + ]: 1 : EXPECT_EQ(children[0], x);
101 [ - + ]: 1 : EXPECT_EQ(children[1], x);
102 [ - + ]: 1 : EXPECT_EQ(children[2], x);
103 : 1 : }
104 : : {
105 : 1 : std::vector<TNode> children;
106 : 1 : expr::algorithm::flatten(n, children, Kind::MULT);
107 [ - + ]: 1 : EXPECT_EQ(children.size(), 1);
108 [ - + ]: 1 : EXPECT_EQ(children[0], n);
109 : 1 : }
110 : : {
111 : 1 : std::vector<TNode> children;
112 : 1 : expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT);
113 [ - + ]: 1 : EXPECT_EQ(children.size(), 3);
114 [ - + ]: 1 : EXPECT_EQ(children[0], x);
115 [ - + ]: 1 : EXPECT_EQ(children[1], x);
116 [ - + ]: 1 : EXPECT_EQ(children[2], x);
117 : 1 : }
118 : 1 : }
119 : : {
120 : 1 : Node x = d_nodeManager->mkBoundVar(*d_realTypeNode);
121 : 1 : Node n = d_nodeManager->mkNode(
122 : 2 : Kind::ADD, x, d_nodeManager->mkNode(Kind::MULT, x, x));
123 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n));
124 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::ADD));
125 [ - + ]: 1 : EXPECT_FALSE(expr::algorithm::canFlatten(n, Kind::MULT));
126 [ - + ]: 1 : EXPECT_TRUE(expr::algorithm::canFlatten(n, Kind::ADD, Kind::MULT));
127 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n), n);
128 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n, Kind::ADD), n);
129 [ - + ]: 2 : EXPECT_EQ(expr::algorithm::flatten(d_nodeManager.get(), n, Kind::MULT), n);
130 [ - + ]: 2 : EXPECT_NE(
131 : : expr::algorithm::flatten(d_nodeManager.get(), n, Kind::ADD, Kind::MULT),
132 : 1 : n);
133 : :
134 : : {
135 : 1 : std::vector<TNode> children;
136 : 1 : expr::algorithm::flatten(n, children);
137 [ - + ]: 1 : EXPECT_EQ(children.size(), 2);
138 [ - + ]: 1 : EXPECT_EQ(children[0], x);
139 [ - + ]: 2 : EXPECT_EQ(children[1], n[1]);
140 : 1 : }
141 : : {
142 : 1 : std::vector<TNode> children;
143 : 1 : expr::algorithm::flatten(n, children, Kind::ADD);
144 [ - + ]: 1 : EXPECT_EQ(children.size(), 2);
145 [ - + ]: 1 : EXPECT_EQ(children[0], x);
146 [ - + ]: 2 : EXPECT_EQ(children[1], n[1]);
147 : 1 : }
148 : : {
149 : 1 : std::vector<TNode> children;
150 : 1 : expr::algorithm::flatten(n, children, Kind::MULT);
151 [ - + ]: 1 : EXPECT_EQ(children.size(), 1);
152 [ - + ]: 1 : EXPECT_EQ(children[0], n);
153 : 1 : }
154 : : {
155 : 1 : std::vector<TNode> children;
156 : 1 : expr::algorithm::flatten(n, children, Kind::ADD, Kind::MULT);
157 [ - + ]: 1 : EXPECT_EQ(children.size(), 3);
158 [ - + ]: 1 : EXPECT_EQ(children[0], x);
159 [ - + ]: 1 : EXPECT_EQ(children[1], x);
160 [ - + ]: 1 : EXPECT_EQ(children[2], x);
161 : 1 : }
162 : 1 : }
163 : 1 : }
164 : :
165 : : } // namespace test
166 : : } // namespace cvc5::internal
|
