1
2
3
4 #include "Test/UnitTesting.hpp"
5 #include "Test/SyntaxSugar.hpp"
6 #include "Kernel/Rebalancing.hpp"
7 #include "Kernel/Rebalancing/Inverters.hpp"
8 #include "Indexing/TermSharing.hpp"
9 #include "Kernel/InterpretedLiteralEvaluator.hpp"
10
11 #define UNIT_ID Rebalancing
12 UT_CREATE;
13 using namespace std;
14 using namespace Kernel;
15 using namespace Rebalancing;
16 using namespace Inverters;
17
18
19 #define __expand__frac(...) { __VA_ARGS__ }
20 #define __expand__int(...) { __VA_ARGS__ }
21 #define __expand__list(...) { __VA_ARGS__ }
22 #define bal(l,r) expected_t(l, TermWrapper(r))
23
24 template<class Range, class Pred>
any(Range range,Pred p)25 bool any(Range range, Pred p) {
26 for (auto x : range) {
27 if (p(x)) return true;
28 }
29 return false;
30 }
31
32 using expected_t = tuple<TermList, TermList>;
33
34 template<class ConstantType>
35 void test_rebalance(Literal& lit, initializer_list<expected_t> expected);
36
37 #define __TO_CONSTANT_TYPE_INT IntegerConstantType
38 #define __TO_CONSTANT_TYPE_RAT RationalConstantType
39 #define __TO_CONSTANT_TYPE_REAL RealConstantType
40 #define ToConstantType(type) __TO_CONSTANT_TYPE_ ## type
41
42 #define TEST_REBALANCE(name, type, equality, __list) \
43 TEST_FUN(name ## _ ## type) { \
44 THEORY_SYNTAX_SUGAR(type) \
45 _Pragma("GCC diagnostic push") \
46 _Pragma("GCC diagnostic ignored \"-Wunused\"") \
47 THEORY_SYNTAX_SUGAR_FUN(f, 1) \
48 _Pragma("GCC diagnostic pop") \
49 test_rebalance<ToConstantType(type)>((equality), __expand ## __list); \
50 } \
51
52
53 #define TEST_REBALANCE_SPLIT(name, equality, __frac, __int) \
54 TEST_REBALANCE(name, REAL, equality, __frac) \
55 TEST_REBALANCE(name, RAT , equality, __frac) \
56 TEST_REBALANCE(name, INT , equality, __int) \
57
58
59 #define TEST_REBALANCE_ALL(name, equality, __list) \
60 TEST_REBALANCE(name, REAL, equality, __list) \
61 TEST_REBALANCE(name, RAT , equality, __list) \
62 TEST_REBALANCE(name, INT , equality, __list) \
63
64
65
66 TEST_REBALANCE_SPLIT(constants_1
67 , eq(mul(2, x), 5)
68 , __frac(
69 bal(x, frac(5,2))
70 )
71 , __int( ))
72
73 TEST_REBALANCE_SPLIT(constants_2,
74 eq(mul(2, x), 4),
75 __frac(
76 bal(x, 2)
77 ),
78 __int())
79
80 TEST_REBALANCE_ALL(uninterpreted_1
81 , eq(add(2, x), a)
82 , __list(
83 bal(x, add(-2, a))
84 ))
85
86 TEST_REBALANCE_SPLIT(uninterpreted_2
87 , eq(mul(x, 2), a)
88 , __frac(
89 bal(x, mul(frac(1, 2), a))
90 )
91 , __int( ))
92
93 TEST_REBALANCE_SPLIT(multi_var_1
94 , eq(mul(x, 2), mul(y, 2))
95 , __frac(
96 bal(x, y)
97 , bal(y, x)
98 )
99 , __int( )
100 )
101
102 TEST_REBALANCE_SPLIT(multi_var_2
103 , eq(mul(x, 4), mul(y, 2))
104 , __frac(
105 bal(y, mul(2, x))
106 , bal(x, mul(frac(1,2), y))
107 )
108 , __int(
109 // bal(y, mul(2, x))
110 )
111 )
112
113
114 TEST_REBALANCE_SPLIT(multi_var_3
115 , eq(mul(x, 6), mul(y, 2))
116 , __frac(
117 bal(y, mul(3, x))
118 , bal(x, mul(frac(1,3), y))
119 )
120 , __frac(
121 // bal(y, mul(3, x))
122 )
123 )
124
125
126 TEST_REBALANCE_SPLIT(multi_var_4
127 , eq(mul(x, 2), y)
128 , __frac(
129 bal(x, mul(frac(1, 2), y))
130 , bal(y, mul(2, x))
131 )
132 , __int(
133 bal(y, mul(2, x))
134 ))
135
136 TEST_REBALANCE_SPLIT(multi_var_5
137 , eq(mul(x, 2), mul(y, 3))
138 , __frac(
139 bal(x, mul(frac(3, 2), y))
140 , bal(y, mul(frac(2, 3), x))
141 )
142 , __int( ))
143
144
145 TEST_REBALANCE_ALL(rebalance_multiple_vars
146 , eq(add(x, minus(y)), f(y))
147 , __list(
148 bal(x, add(f(y), y))
149 , bal(y, minus(add(f(y), minus(x))))
150 ))
151
152 TEST_REBALANCE_SPLIT(div_zero_1
153 , eq(mul(x, 0), 7)
154 , __int()
155 , __frac()
156 )
157
158 TEST_REBALANCE_SPLIT(div_zero_2
159 , eq(mul(x, a), 7)
160 , __int()
161 , __frac()
162 )
163
164 TEST_REBALANCE_SPLIT(div_zero_3
165 , eq(mul(x, y), 7)
166 , __int()
167 , __frac()
168 )
169
170 TEST_REBALANCE_SPLIT(div_zero_4
171 , eq(mul(x, f(y)), 7)
172 , __int()
173 , __frac()
174 )
175
176 TEST_REBALANCE_SPLIT(div_zero_5
177 , eq(mul(0, x), 0)
178 , __int()
179 , __frac()
180 )
181
182 TEST_REBALANCE_SPLIT(div_zero_6
183 , eq(mul(2, x), 0)
184 , __frac(
185 bal(x, 0)
186 )
187 , __int()
188 )
189
190 TEST_REBALANCE_ALL(bug_1
191 , neq(f(mul(16, z)), y)
192 , __list(
193 bal(y, f(mul(16, z)))
194 ))
195
196
197 TEST_REBALANCE_ALL(bug_2
198 , neq(add(x,mul(-1,x)), y)
199 , __list(
200 bal(y, add(x,mul(-1,x)))
201 , bal(x, add(y, minus(mul(-1,x))))
202 , bal(x, mul(-1, add(y, minus(x))))
203 ))
204
205 std::ostream& operator<<(std::ostream& out, initializer_list<expected_t> expected) {
206 for (auto x : expected ) {
207 out << "\t" << get<0>(x) << "\t->\t" << get<1>(x) << "\n";
208 }
209 return out;
210 }
211 template<class A>
operator <<(std::ostream & out,const BalanceIter<A> & x)212 std::ostream& operator<<(std::ostream& out, const BalanceIter<A>& x) {
213 return out << "\t" << x.lhs() << "\t->\t" << x.buildRhs() << endl;
214 }
215 template<class A>
operator <<(std::ostream & out,const Balancer<A> & b)216 std::ostream& operator<<(std::ostream& out, const Balancer<A>& b) {
217 for (auto x : b) {
218 out << x;
219 }
220 return out;
221 }
222
223
224 template<class A>
test_rebalance(Literal & lit,initializer_list<expected_t> expected)225 void test_rebalance(Literal& lit, initializer_list<expected_t> expected) {
226 ASS(lit.isEquality());
227 using balancer_t = Balancer<NumberTheoryInverter>;
228 auto simplified = [](TermList t) -> TermList {
229 // DBG("simplifying ", t)
230 static InterpretedLiteralEvaluator e = InterpretedLiteralEvaluator();
231 if (t.isTerm()) {
232 t = e.evaluate(t);
233 }
234 // DBG("end simplifying ", t)
235 return t;
236 };
237
238 Stack<expected_t> results;
239 unsigned cnt = 0;
240 for (auto bal : balancer_t(lit)) {
241
242 auto lhs = bal.lhs();
243 // auto rhs = bal.buildRhs();
244 auto rhs = simplified(bal.buildRhs());
245
246 results.push(expected_t(lhs, rhs));
247
248 if (!any(expected, [&](const expected_t& ex) -> bool
249 { return get<0>(ex) == lhs && get<1>(ex) == rhs; }
250 )) {
251
252 cout << "case: " << lit << endl;
253 cout << "unexpected entry in balancer:" << endl;
254 cout << "\t" << lhs << "\t->\t" << rhs << endl;
255 cout << "expected: \n" << expected << endl;
256 exit(-1);
257
258 }
259 cnt++;
260 }
261 if (cnt != expected.size()) {
262 cout << "case: " << lit << endl;
263 cout << "unexpected results in balancer:" << endl;
264 if (results.isEmpty()) {
265 cout << "\t< nothing >" << endl;
266 } else {
267 for (auto r : results) {
268 cout << "\t" << get<0>(r) << "\t->\t" << get<1>(r) << endl;
269 }
270 }
271 cout << "expected: \n" << expected << endl;
272 exit(-1);
273 }
274 }
275
276
277