1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Tim King, Andrew Reynolds |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* A class giving information about a logic (group a theory modules |
14 |
|
* and configuration information) |
15 |
|
*/ |
16 |
|
#include "theory/logic_info.h" |
17 |
|
|
18 |
|
#include <cstring> |
19 |
|
#include <iostream> |
20 |
|
#include <sstream> |
21 |
|
#include <string> |
22 |
|
|
23 |
|
#include "base/check.h" |
24 |
|
#include "base/configuration.h" |
25 |
|
#include "expr/kind.h" |
26 |
|
|
27 |
|
using namespace std; |
28 |
|
using namespace cvc5::theory; |
29 |
|
|
30 |
|
namespace cvc5 { |
31 |
|
|
32 |
61596 |
LogicInfo::LogicInfo() |
33 |
|
: d_logicString(""), |
34 |
|
d_theories(THEORY_LAST, false), |
35 |
|
d_sharingTheories(0), |
36 |
|
d_integers(true), |
37 |
|
d_reals(true), |
38 |
|
d_transcendentals(true), |
39 |
|
d_linear(false), |
40 |
|
d_differenceLogic(false), |
41 |
|
d_cardinalityConstraints(false), |
42 |
|
d_higherOrder(true), |
43 |
61596 |
d_locked(false) |
44 |
|
{ |
45 |
862344 |
for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) |
46 |
|
{ |
47 |
800748 |
if (id == THEORY_FP && !Configuration::isBuiltWithSymFPU()) |
48 |
|
{ |
49 |
|
continue; |
50 |
|
} |
51 |
800748 |
enableTheory(id); |
52 |
|
} |
53 |
61596 |
} |
54 |
|
|
55 |
10493 |
LogicInfo::LogicInfo(std::string logicString) |
56 |
|
: d_logicString(""), |
57 |
|
d_theories(THEORY_LAST, false), |
58 |
|
d_sharingTheories(0), |
59 |
|
d_integers(false), |
60 |
|
d_reals(false), |
61 |
|
d_transcendentals(false), |
62 |
|
d_linear(false), |
63 |
|
d_differenceLogic(false), |
64 |
|
d_cardinalityConstraints(false), |
65 |
|
d_higherOrder(false), |
66 |
10495 |
d_locked(false) |
67 |
|
{ |
68 |
10495 |
setLogicString(logicString); |
69 |
10491 |
lock(); |
70 |
10491 |
} |
71 |
|
|
72 |
11909 |
LogicInfo::LogicInfo(const char* logicString) |
73 |
|
: d_logicString(""), |
74 |
|
d_theories(THEORY_LAST, false), |
75 |
|
d_sharingTheories(0), |
76 |
|
d_integers(false), |
77 |
|
d_reals(false), |
78 |
|
d_transcendentals(false), |
79 |
|
d_linear(false), |
80 |
|
d_differenceLogic(false), |
81 |
|
d_cardinalityConstraints(false), |
82 |
|
d_higherOrder(false), |
83 |
11909 |
d_locked(false) |
84 |
|
{ |
85 |
11909 |
setLogicString(logicString); |
86 |
11909 |
lock(); |
87 |
11909 |
} |
88 |
|
|
89 |
|
/** Is sharing enabled for this logic? */ |
90 |
55972153 |
bool LogicInfo::isSharingEnabled() const { |
91 |
55972153 |
PrettyCheckArgument(d_locked, *this, |
92 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
93 |
55972153 |
return d_sharingTheories > 1; |
94 |
|
} |
95 |
|
|
96 |
|
|
97 |
|
/** Is the given theory module active in this logic? */ |
98 |
61373264 |
bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const { |
99 |
61373264 |
PrettyCheckArgument(d_locked, *this, |
100 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
101 |
61373248 |
return d_theories[theory]; |
102 |
|
} |
103 |
|
|
104 |
|
/** Is this a quantified logic? */ |
105 |
198358 |
bool LogicInfo::isQuantified() const { |
106 |
198358 |
PrettyCheckArgument(d_locked, *this, |
107 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
108 |
198356 |
return isTheoryEnabled(theory::THEORY_QUANTIFIERS); |
109 |
|
} |
110 |
|
|
111 |
|
/** Is this a higher-order logic? */ |
112 |
2521 |
bool LogicInfo::isHigherOrder() const |
113 |
|
{ |
114 |
2521 |
PrettyCheckArgument(d_locked, |
115 |
|
*this, |
116 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
117 |
2521 |
return d_higherOrder; |
118 |
|
} |
119 |
|
|
120 |
|
/** Is this the all-inclusive logic? */ |
121 |
30281 |
bool LogicInfo::hasEverything() const { |
122 |
30281 |
PrettyCheckArgument(d_locked, *this, |
123 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
124 |
60562 |
LogicInfo everything; |
125 |
30281 |
everything.lock(); |
126 |
60562 |
return *this == everything; |
127 |
|
} |
128 |
|
|
129 |
|
/** Is this the all-exclusive logic? (Here, that means propositional logic) */ |
130 |
52 |
bool LogicInfo::hasNothing() const { |
131 |
52 |
PrettyCheckArgument(d_locked, *this, |
132 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
133 |
104 |
LogicInfo nothing(""); |
134 |
52 |
nothing.lock(); |
135 |
104 |
return *this == nothing; |
136 |
|
} |
137 |
|
|
138 |
90420 |
bool LogicInfo::isPure(theory::TheoryId theory) const { |
139 |
90420 |
PrettyCheckArgument(d_locked, *this, |
140 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
141 |
|
// the third and fourth conjucts are really just to rule out the misleading |
142 |
|
// case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA |
143 |
172151 |
return isTheoryEnabled(theory) && !isSharingEnabled() && |
144 |
122721 |
( !isTrueTheory(theory) || d_sharingTheories == 1 ) && |
145 |
100936 |
( isTrueTheory(theory) || d_sharingTheories == 0 ); |
146 |
|
} |
147 |
|
|
148 |
15900 |
bool LogicInfo::areIntegersUsed() const { |
149 |
15900 |
PrettyCheckArgument(d_locked, *this, |
150 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
151 |
15898 |
PrettyCheckArgument( |
152 |
|
isTheoryEnabled(theory::THEORY_ARITH), *this, |
153 |
|
"Arithmetic not used in this LogicInfo; cannot ask whether integers are used"); |
154 |
15894 |
return d_integers; |
155 |
|
} |
156 |
|
|
157 |
8305 |
bool LogicInfo::areRealsUsed() const { |
158 |
8305 |
PrettyCheckArgument(d_locked, *this, |
159 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
160 |
8303 |
PrettyCheckArgument( |
161 |
|
isTheoryEnabled(theory::THEORY_ARITH), *this, |
162 |
|
"Arithmetic not used in this LogicInfo; cannot ask whether reals are used"); |
163 |
8299 |
return d_reals; |
164 |
|
} |
165 |
|
|
166 |
12280 |
bool LogicInfo::areTranscendentalsUsed() const |
167 |
|
{ |
168 |
12280 |
PrettyCheckArgument(d_locked, |
169 |
|
*this, |
170 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
171 |
12280 |
PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH), |
172 |
|
*this, |
173 |
|
"Arithmetic not used in this LogicInfo; cannot ask " |
174 |
|
"whether transcendentals are used"); |
175 |
12276 |
return d_transcendentals; |
176 |
|
} |
177 |
|
|
178 |
175411 |
bool LogicInfo::isLinear() const { |
179 |
175411 |
PrettyCheckArgument(d_locked, *this, |
180 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
181 |
175409 |
PrettyCheckArgument( |
182 |
|
isTheoryEnabled(theory::THEORY_ARITH), *this, |
183 |
|
"Arithmetic not used in this LogicInfo; cannot ask whether it's linear"); |
184 |
175405 |
return d_linear || d_differenceLogic; |
185 |
|
} |
186 |
|
|
187 |
8147 |
bool LogicInfo::isDifferenceLogic() const { |
188 |
8147 |
PrettyCheckArgument(d_locked, *this, |
189 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
190 |
8147 |
PrettyCheckArgument( |
191 |
|
isTheoryEnabled(theory::THEORY_ARITH), *this, |
192 |
|
"Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic"); |
193 |
8143 |
return d_differenceLogic; |
194 |
|
} |
195 |
|
|
196 |
12246 |
bool LogicInfo::hasCardinalityConstraints() const { |
197 |
12246 |
PrettyCheckArgument(d_locked, *this, |
198 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
199 |
12246 |
return d_cardinalityConstraints; |
200 |
|
} |
201 |
|
|
202 |
|
|
203 |
46640 |
bool LogicInfo::operator==(const LogicInfo& other) const { |
204 |
46640 |
PrettyCheckArgument(isLocked() && other.isLocked(), *this, |
205 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
206 |
357156 |
for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { |
207 |
342479 |
if(d_theories[id] != other.d_theories[id]) { |
208 |
31963 |
return false; |
209 |
|
} |
210 |
|
} |
211 |
|
|
212 |
14677 |
PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this, |
213 |
|
"LogicInfo internal inconsistency"); |
214 |
29354 |
bool res = d_cardinalityConstraints == other.d_cardinalityConstraints |
215 |
14677 |
&& d_higherOrder == other.d_higherOrder; |
216 |
14677 |
if(isTheoryEnabled(theory::THEORY_ARITH)) { |
217 |
28568 |
return d_integers == other.d_integers && d_reals == other.d_reals |
218 |
13917 |
&& d_transcendentals == other.d_transcendentals |
219 |
13755 |
&& d_linear == other.d_linear |
220 |
28088 |
&& d_differenceLogic == other.d_differenceLogic && res; |
221 |
|
} else { |
222 |
122 |
return res; |
223 |
|
} |
224 |
|
} |
225 |
|
|
226 |
7044 |
bool LogicInfo::operator<=(const LogicInfo& other) const { |
227 |
7044 |
PrettyCheckArgument(isLocked() && other.isLocked(), *this, |
228 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
229 |
63594 |
for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { |
230 |
60672 |
if(d_theories[id] && !other.d_theories[id]) { |
231 |
4122 |
return false; |
232 |
|
} |
233 |
|
} |
234 |
2922 |
PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, |
235 |
|
"LogicInfo internal inconsistency"); |
236 |
5868 |
bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints) |
237 |
5820 |
&& (!d_higherOrder || other.d_higherOrder); |
238 |
2922 |
if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { |
239 |
4128 |
return (!d_integers || other.d_integers) && (!d_reals || other.d_reals) |
240 |
1722 |
&& (!d_transcendentals || other.d_transcendentals) |
241 |
1704 |
&& (d_linear || !other.d_linear) |
242 |
4038 |
&& (d_differenceLogic || !other.d_differenceLogic) && res; |
243 |
|
} else { |
244 |
288 |
return res; |
245 |
|
} |
246 |
|
} |
247 |
|
|
248 |
6510 |
bool LogicInfo::operator>=(const LogicInfo& other) const { |
249 |
6510 |
PrettyCheckArgument(isLocked() && other.isLocked(), *this, |
250 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
251 |
59092 |
for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { |
252 |
56338 |
if(!d_theories[id] && other.d_theories[id]) { |
253 |
3756 |
return false; |
254 |
|
} |
255 |
|
} |
256 |
2754 |
PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, |
257 |
|
"LogicInfo internal inconsistency"); |
258 |
8232 |
bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints) |
259 |
5490 |
&& (d_higherOrder || !other.d_higherOrder); |
260 |
2754 |
if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) { |
261 |
3186 |
return (d_integers || !other.d_integers) && (d_reals || !other.d_reals) |
262 |
1594 |
&& (d_transcendentals || !other.d_transcendentals) |
263 |
1582 |
&& (!d_linear || other.d_linear) |
264 |
3800 |
&& (!d_differenceLogic || other.d_differenceLogic) && res; |
265 |
|
} else { |
266 |
264 |
return res; |
267 |
|
} |
268 |
|
} |
269 |
|
|
270 |
9587 |
std::string LogicInfo::getLogicString() const { |
271 |
9587 |
PrettyCheckArgument( |
272 |
|
d_locked, *this, |
273 |
|
"This LogicInfo isn't locked yet, and cannot be queried"); |
274 |
9585 |
if(d_logicString == "") { |
275 |
5708 |
LogicInfo qf_all_supported; |
276 |
2854 |
qf_all_supported.disableQuantifiers(); |
277 |
2854 |
qf_all_supported.lock(); |
278 |
2854 |
if(hasEverything()) { |
279 |
1770 |
d_logicString = "ALL"; |
280 |
1084 |
} else if(*this == qf_all_supported) { |
281 |
|
d_logicString = "QF_ALL"; |
282 |
|
} else { |
283 |
1084 |
size_t seen = 0; // make sure we support all the active theories |
284 |
|
|
285 |
2168 |
stringstream ss; |
286 |
1084 |
if(!isQuantified()) { |
287 |
98 |
ss << "QF_"; |
288 |
|
} |
289 |
1084 |
if (d_theories[THEORY_SEP]) |
290 |
|
{ |
291 |
8 |
ss << "SEP_"; |
292 |
8 |
++seen; |
293 |
|
} |
294 |
1084 |
if(d_theories[THEORY_ARRAYS]) { |
295 |
37 |
ss << (d_sharingTheories == 1 ? "AX" : "A"); |
296 |
37 |
++seen; |
297 |
|
} |
298 |
1084 |
if(d_theories[THEORY_UF]) { |
299 |
737 |
ss << "UF"; |
300 |
737 |
++seen; |
301 |
|
} |
302 |
1084 |
if( d_cardinalityConstraints ){ |
303 |
|
ss << "C"; |
304 |
|
} |
305 |
1084 |
if(d_theories[THEORY_BV]) { |
306 |
251 |
ss << "BV"; |
307 |
251 |
++seen; |
308 |
|
} |
309 |
1084 |
if(d_theories[THEORY_FP]) { |
310 |
10 |
ss << "FP"; |
311 |
10 |
++seen; |
312 |
|
} |
313 |
1084 |
if(d_theories[THEORY_DATATYPES]) { |
314 |
703 |
ss << "DT"; |
315 |
703 |
++seen; |
316 |
|
} |
317 |
1084 |
if(d_theories[THEORY_STRINGS]) { |
318 |
322 |
ss << "S"; |
319 |
322 |
++seen; |
320 |
|
} |
321 |
1084 |
if(d_theories[THEORY_ARITH]) { |
322 |
942 |
if(isDifferenceLogic()) { |
323 |
|
ss << (areIntegersUsed() ? "I" : ""); |
324 |
|
ss << (areRealsUsed() ? "R" : ""); |
325 |
|
ss << "DL"; |
326 |
|
} else { |
327 |
942 |
ss << (isLinear() ? "L" : "N"); |
328 |
942 |
ss << (areIntegersUsed() ? "I" : ""); |
329 |
942 |
ss << (areRealsUsed() ? "R" : ""); |
330 |
942 |
ss << "A"; |
331 |
942 |
ss << (areTranscendentalsUsed() ? "T" : ""); |
332 |
|
} |
333 |
942 |
++seen; |
334 |
|
} |
335 |
1084 |
if(d_theories[THEORY_SETS]) { |
336 |
2 |
ss << "FS"; |
337 |
2 |
++seen; |
338 |
|
} |
339 |
1084 |
if (d_theories[THEORY_BAGS]) |
340 |
|
{ |
341 |
2 |
ss << "FB"; |
342 |
2 |
++seen; |
343 |
|
} |
344 |
1084 |
if(seen != d_sharingTheories) { |
345 |
|
Unhandled() |
346 |
|
<< "can't extract a logic string from LogicInfo; at least one " |
347 |
|
"active theory is unknown to LogicInfo::getLogicString() !"; |
348 |
|
} |
349 |
|
|
350 |
1084 |
if(seen == 0) { |
351 |
|
ss << "SAT"; |
352 |
|
} |
353 |
|
|
354 |
1084 |
d_logicString = ss.str(); |
355 |
|
} |
356 |
|
} |
357 |
9585 |
return d_logicString; |
358 |
|
} |
359 |
|
|
360 |
22402 |
void LogicInfo::setLogicString(std::string logicString) |
361 |
|
{ |
362 |
22402 |
PrettyCheckArgument(!d_locked, *this, |
363 |
|
"This LogicInfo is locked, and cannot be modified"); |
364 |
313628 |
for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) { |
365 |
291226 |
d_theories[id] = false;// ensure it's cleared |
366 |
|
} |
367 |
22402 |
d_sharingTheories = 0; |
368 |
|
|
369 |
|
// Below, ONLY use enableTheory()/disableTheory() rather than |
370 |
|
// accessing d_theories[] directly. This makes sure to set up |
371 |
|
// sharing properly. |
372 |
|
|
373 |
22402 |
enableTheory(THEORY_BUILTIN); |
374 |
22402 |
enableTheory(THEORY_BOOL); |
375 |
|
|
376 |
22402 |
const char* p = logicString.c_str(); |
377 |
22402 |
if(*p == '\0') { |
378 |
|
// propositional logic only; we're done. |
379 |
22348 |
} else if(!strcmp(p, "QF_SAT")) { |
380 |
|
// propositional logic only; we're done. |
381 |
20 |
p += 6; |
382 |
22328 |
} else if(!strcmp(p, "SAT")) { |
383 |
|
// quantified Boolean formulas only; we're done. |
384 |
10 |
enableQuantifiers(); |
385 |
10 |
p += 3; |
386 |
22318 |
} else if(!strcmp(p, "QF_ALL_SUPPORTED")) { |
387 |
|
// the "all theories included" logic, no quantifiers |
388 |
287 |
enableEverything(); |
389 |
287 |
disableQuantifiers(); |
390 |
287 |
arithNonLinear(); |
391 |
287 |
p += 16; |
392 |
22031 |
} else if(!strcmp(p, "QF_ALL")) { |
393 |
|
// the "all theories included" logic, no quantifiers |
394 |
68 |
enableEverything(); |
395 |
68 |
disableQuantifiers(); |
396 |
68 |
arithNonLinear(); |
397 |
68 |
p += 6; |
398 |
21963 |
} else if(!strcmp(p, "ALL_SUPPORTED")) { |
399 |
|
// the "all theories included" logic, with quantifiers |
400 |
926 |
enableEverything(); |
401 |
926 |
enableQuantifiers(); |
402 |
926 |
arithNonLinear(); |
403 |
926 |
p += 13; |
404 |
21037 |
} else if(!strcmp(p, "ALL")) { |
405 |
|
// the "all theories included" logic, with quantifiers |
406 |
1780 |
enableEverything(); |
407 |
1780 |
enableQuantifiers(); |
408 |
1780 |
arithNonLinear(); |
409 |
1780 |
p += 3; |
410 |
|
} |
411 |
19257 |
else if (!strcmp(p, "HORN")) |
412 |
|
{ |
413 |
|
// the HORN logic |
414 |
|
enableEverything(); |
415 |
|
enableQuantifiers(); |
416 |
|
arithNonLinear(); |
417 |
|
p += 4; |
418 |
|
} else { |
419 |
19257 |
if(!strncmp(p, "QF_", 3)) { |
420 |
16615 |
disableQuantifiers(); |
421 |
16615 |
p += 3; |
422 |
|
} else { |
423 |
2642 |
enableQuantifiers(); |
424 |
|
} |
425 |
19257 |
if (!strncmp(p, "SEP_", 4)) |
426 |
|
{ |
427 |
8 |
enableSeparationLogic(); |
428 |
8 |
p += 4; |
429 |
|
} |
430 |
19257 |
if(!strncmp(p, "AX", 2)) { |
431 |
50 |
enableTheory(THEORY_ARRAYS); |
432 |
50 |
p += 2; |
433 |
|
} else { |
434 |
19207 |
if(*p == 'A') { |
435 |
1974 |
enableTheory(THEORY_ARRAYS); |
436 |
1974 |
++p; |
437 |
|
} |
438 |
19207 |
if(!strncmp(p, "UF", 2)) { |
439 |
13515 |
enableTheory(THEORY_UF); |
440 |
13515 |
p += 2; |
441 |
|
} |
442 |
19207 |
if(!strncmp(p, "C", 1 )) { |
443 |
54 |
d_cardinalityConstraints = true; |
444 |
54 |
p += 1; |
445 |
|
} |
446 |
|
// allow BV or DT in either order |
447 |
19207 |
if(!strncmp(p, "BV", 2)) { |
448 |
2675 |
enableTheory(THEORY_BV); |
449 |
2675 |
p += 2; |
450 |
|
} |
451 |
19207 |
if(!strncmp(p, "FP", 2)) { |
452 |
108 |
enableTheory(THEORY_FP); |
453 |
108 |
p += 2; |
454 |
|
} |
455 |
19207 |
if(!strncmp(p, "DT", 2)) { |
456 |
126 |
enableTheory(THEORY_DATATYPES); |
457 |
126 |
p += 2; |
458 |
|
} |
459 |
19207 |
if(!d_theories[THEORY_BV] && !strncmp(p, "BV", 2)) { |
460 |
|
enableTheory(THEORY_BV); |
461 |
|
p += 2; |
462 |
|
} |
463 |
19207 |
if(*p == 'S') { |
464 |
762 |
enableTheory(THEORY_STRINGS); |
465 |
762 |
++p; |
466 |
|
} |
467 |
19207 |
if(!strncmp(p, "IDL", 3)) { |
468 |
227 |
enableIntegers(); |
469 |
227 |
disableReals(); |
470 |
227 |
arithOnlyDifference(); |
471 |
227 |
p += 3; |
472 |
18980 |
} else if(!strncmp(p, "RDL", 3)) { |
473 |
118 |
disableIntegers(); |
474 |
118 |
enableReals(); |
475 |
118 |
arithOnlyDifference(); |
476 |
118 |
p += 3; |
477 |
18862 |
} else if(!strncmp(p, "IRDL", 4)) { |
478 |
|
// "IRDL" ?! --not very useful, but getLogicString() can produce |
479 |
|
// that string, so we really had better be able to read it back in. |
480 |
|
enableIntegers(); |
481 |
|
enableReals(); |
482 |
|
arithOnlyDifference(); |
483 |
|
p += 4; |
484 |
18862 |
} else if(!strncmp(p, "LIA", 3)) { |
485 |
2790 |
enableIntegers(); |
486 |
2790 |
disableReals(); |
487 |
2790 |
arithOnlyLinear(); |
488 |
2790 |
p += 3; |
489 |
16072 |
} else if(!strncmp(p, "LRA", 3)) { |
490 |
972 |
disableIntegers(); |
491 |
972 |
enableReals(); |
492 |
972 |
arithOnlyLinear(); |
493 |
972 |
p += 3; |
494 |
15100 |
} else if(!strncmp(p, "LIRA", 4)) { |
495 |
416 |
enableIntegers(); |
496 |
416 |
enableReals(); |
497 |
416 |
arithOnlyLinear(); |
498 |
416 |
p += 4; |
499 |
14684 |
} else if(!strncmp(p, "NIA", 3)) { |
500 |
680 |
enableIntegers(); |
501 |
680 |
disableReals(); |
502 |
680 |
arithNonLinear(); |
503 |
680 |
p += 3; |
504 |
14004 |
} else if(!strncmp(p, "NRA", 3)) { |
505 |
10119 |
disableIntegers(); |
506 |
10119 |
enableReals(); |
507 |
10119 |
arithNonLinear(); |
508 |
10119 |
p += 3; |
509 |
10119 |
if (*p == 'T') |
510 |
|
{ |
511 |
196 |
arithTranscendentals(); |
512 |
196 |
p += 1; |
513 |
|
} |
514 |
3885 |
} else if(!strncmp(p, "NIRA", 4)) { |
515 |
294 |
enableIntegers(); |
516 |
294 |
enableReals(); |
517 |
294 |
arithNonLinear(); |
518 |
294 |
p += 4; |
519 |
294 |
if (*p == 'T') |
520 |
|
{ |
521 |
6 |
arithTranscendentals(); |
522 |
6 |
p += 1; |
523 |
|
} |
524 |
|
} |
525 |
19207 |
if(!strncmp(p, "FS", 2)) { |
526 |
160 |
enableTheory(THEORY_SETS); |
527 |
160 |
p += 2; |
528 |
|
} |
529 |
|
} |
530 |
|
} |
531 |
|
|
532 |
22402 |
if (d_theories[THEORY_FP]) |
533 |
|
{ |
534 |
|
// THEORY_BV is needed for bit-blasting. |
535 |
|
// We have to set this here rather than in expandDefinition as it |
536 |
|
// is possible to create variables without any theory specific |
537 |
|
// operations, so expandDefinition won't be called. |
538 |
3169 |
enableTheory(THEORY_BV); |
539 |
|
} |
540 |
|
|
541 |
22402 |
if(*p != '\0') { |
542 |
4 |
stringstream err; |
543 |
2 |
err << "LogicInfo::setLogicString(): "; |
544 |
2 |
if(p == logicString) { |
545 |
|
err << "cannot parse logic string: " << logicString; |
546 |
|
} else { |
547 |
2 |
err << "junk (\"" << p << "\") at end of logic string: " << logicString; |
548 |
|
} |
549 |
2 |
IllegalArgument(logicString, err.str().c_str()); |
550 |
|
} |
551 |
|
|
552 |
|
// ensure a getLogic() returns the same thing as was set |
553 |
22400 |
d_logicString = logicString; |
554 |
22400 |
} |
555 |
|
|
556 |
3063 |
void LogicInfo::enableEverything() { |
557 |
3063 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
558 |
3063 |
*this = LogicInfo(); |
559 |
3063 |
} |
560 |
|
|
561 |
2 |
void LogicInfo::disableEverything() { |
562 |
2 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
563 |
2 |
*this = LogicInfo(""); |
564 |
2 |
} |
565 |
|
|
566 |
894920 |
void LogicInfo::enableTheory(theory::TheoryId theory) { |
567 |
894920 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
568 |
894920 |
if(!d_theories[theory]) { |
569 |
885310 |
if(isTrueTheory(theory)) { |
570 |
652557 |
++d_sharingTheories; |
571 |
|
} |
572 |
885310 |
d_logicString = ""; |
573 |
885310 |
d_theories[theory] = true; |
574 |
|
} |
575 |
894920 |
} |
576 |
|
|
577 |
31117 |
void LogicInfo::disableTheory(theory::TheoryId theory) { |
578 |
31117 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
579 |
31107 |
if(d_theories[theory]) { |
580 |
3277 |
if(isTrueTheory(theory)) { |
581 |
66 |
Assert(d_sharingTheories > 0); |
582 |
66 |
--d_sharingTheories; |
583 |
|
} |
584 |
3277 |
if(theory == THEORY_BUILTIN || |
585 |
|
theory == THEORY_BOOL) { |
586 |
|
return; |
587 |
|
} |
588 |
3277 |
d_logicString = ""; |
589 |
3277 |
d_theories[theory] = false; |
590 |
|
} |
591 |
|
} |
592 |
|
|
593 |
838 |
void LogicInfo::enableSygus() |
594 |
|
{ |
595 |
838 |
enableQuantifiers(); |
596 |
838 |
enableTheory(THEORY_UF); |
597 |
838 |
enableTheory(THEORY_DATATYPES); |
598 |
838 |
enableIntegers(); |
599 |
838 |
enableHigherOrder(); |
600 |
838 |
} |
601 |
|
|
602 |
8 |
void LogicInfo::enableSeparationLogic() |
603 |
|
{ |
604 |
8 |
enableTheory(THEORY_SEP); |
605 |
8 |
enableTheory(THEORY_UF); |
606 |
8 |
enableTheory(THEORY_SETS); |
607 |
8 |
} |
608 |
|
|
609 |
5376 |
void LogicInfo::enableIntegers() { |
610 |
5376 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
611 |
5374 |
d_logicString = ""; |
612 |
5374 |
enableTheory(THEORY_ARITH); |
613 |
5374 |
d_integers = true; |
614 |
5374 |
} |
615 |
|
|
616 |
11213 |
void LogicInfo::disableIntegers() { |
617 |
11213 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
618 |
11211 |
d_logicString = ""; |
619 |
11211 |
d_integers = false; |
620 |
11211 |
if(!d_reals) { |
621 |
11209 |
disableTheory(THEORY_ARITH); |
622 |
|
} |
623 |
11211 |
} |
624 |
|
|
625 |
11919 |
void LogicInfo::enableReals() { |
626 |
11919 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
627 |
11919 |
d_logicString = ""; |
628 |
11919 |
enableTheory(THEORY_ARITH); |
629 |
11919 |
d_reals = true; |
630 |
11919 |
} |
631 |
|
|
632 |
3701 |
void LogicInfo::disableReals() { |
633 |
3701 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
634 |
3699 |
d_logicString = ""; |
635 |
3699 |
d_reals = false; |
636 |
3699 |
if(!d_integers) { |
637 |
|
disableTheory(THEORY_ARITH); |
638 |
|
} |
639 |
3699 |
} |
640 |
|
|
641 |
202 |
void LogicInfo::arithTranscendentals() |
642 |
|
{ |
643 |
202 |
PrettyCheckArgument( |
644 |
|
!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
645 |
202 |
d_logicString = ""; |
646 |
202 |
d_transcendentals = true; |
647 |
202 |
if (!d_reals) |
648 |
|
{ |
649 |
|
enableReals(); |
650 |
|
} |
651 |
202 |
if (d_linear) |
652 |
|
{ |
653 |
|
arithNonLinear(); |
654 |
|
} |
655 |
202 |
} |
656 |
|
|
657 |
345 |
void LogicInfo::arithOnlyDifference() { |
658 |
345 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
659 |
345 |
d_logicString = ""; |
660 |
345 |
d_linear = true; |
661 |
345 |
d_differenceLogic = true; |
662 |
345 |
d_transcendentals = false; |
663 |
345 |
} |
664 |
|
|
665 |
4309 |
void LogicInfo::arithOnlyLinear() { |
666 |
4309 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
667 |
4307 |
d_logicString = ""; |
668 |
4307 |
d_linear = true; |
669 |
4307 |
d_differenceLogic = false; |
670 |
4307 |
d_transcendentals = false; |
671 |
4307 |
} |
672 |
|
|
673 |
14309 |
void LogicInfo::arithNonLinear() { |
674 |
14309 |
PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
675 |
14309 |
d_logicString = ""; |
676 |
14309 |
d_linear = false; |
677 |
14309 |
d_differenceLogic = false; |
678 |
14309 |
} |
679 |
|
|
680 |
|
void LogicInfo::enableCardinalityConstraints() |
681 |
|
{ |
682 |
|
PrettyCheckArgument( |
683 |
|
!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
684 |
|
d_logicString = ""; |
685 |
|
d_cardinalityConstraints = true; |
686 |
|
} |
687 |
|
|
688 |
|
void LogicInfo::disableCardinalityConstraints() |
689 |
|
{ |
690 |
|
PrettyCheckArgument( |
691 |
|
!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
692 |
|
d_logicString = ""; |
693 |
|
d_cardinalityConstraints = false; |
694 |
|
} |
695 |
|
|
696 |
840 |
void LogicInfo::enableHigherOrder() |
697 |
|
{ |
698 |
840 |
PrettyCheckArgument( |
699 |
|
!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
700 |
840 |
d_logicString = ""; |
701 |
840 |
d_higherOrder = true; |
702 |
840 |
} |
703 |
|
|
704 |
|
void LogicInfo::disableHigherOrder() |
705 |
|
{ |
706 |
|
PrettyCheckArgument( |
707 |
|
!d_locked, *this, "This LogicInfo is locked, and cannot be modified"); |
708 |
|
d_logicString = ""; |
709 |
|
d_higherOrder = false; |
710 |
|
} |
711 |
|
|
712 |
6767 |
LogicInfo LogicInfo::getUnlockedCopy() const { |
713 |
6767 |
if(d_locked) { |
714 |
13534 |
LogicInfo info = *this; |
715 |
6767 |
info.d_locked = false; |
716 |
6767 |
return info; |
717 |
|
} else { |
718 |
|
return *this; |
719 |
|
} |
720 |
|
} |
721 |
|
|
722 |
2352 |
std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) { |
723 |
2352 |
return out << logic.getLogicString(); |
724 |
|
} |
725 |
|
|
726 |
28191 |
} // namespace cvc5 |