Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Morgan Deters, Andrew Reynolds, Tim King
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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::internal::theory;
29 : :
30 : : namespace cvc5::internal {
31 : :
32 : 371430 : LogicInfo::LogicInfo()
33 : : : d_logicString(""),
34 : 0 : 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(false),
43 : 371430 : d_locked(false)
44 : : {
45 [ + + ]: 5571450 : for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
46 : : {
47 : 5200020 : enableTheory(id);
48 : : }
49 : 371430 : }
50 : :
51 : 49454 : LogicInfo::LogicInfo(std::string logicString)
52 : : : d_logicString(""),
53 : 0 : d_theories(THEORY_LAST, false),
54 : : d_sharingTheories(0),
55 : : d_integers(false),
56 : : d_reals(false),
57 : : d_transcendentals(false),
58 : : d_linear(false),
59 : : d_differenceLogic(false),
60 : : d_cardinalityConstraints(false),
61 : : d_higherOrder(false),
62 : 49454 : d_locked(false)
63 : : {
64 : 49454 : setLogicString(logicString);
65 : 49454 : lock();
66 : 49454 : }
67 : :
68 : 35966 : LogicInfo::LogicInfo(const char* logicString)
69 : : : d_logicString(""),
70 : 0 : d_theories(THEORY_LAST, false),
71 : : d_sharingTheories(0),
72 : : d_integers(false),
73 : : d_reals(false),
74 : : d_transcendentals(false),
75 : : d_linear(false),
76 : : d_differenceLogic(false),
77 : : d_cardinalityConstraints(false),
78 : : d_higherOrder(false),
79 : 35966 : d_locked(false)
80 : : {
81 : 35966 : setLogicString(logicString);
82 : 35966 : lock();
83 : 35966 : }
84 : :
85 : : /** Is sharing enabled for this logic? */
86 : 156838000 : bool LogicInfo::isSharingEnabled() const {
87 [ - + ]: 156838000 : PrettyCheckArgument(d_locked, *this,
88 : : "This LogicInfo isn't locked yet, and cannot be queried");
89 : 156838000 : return d_sharingTheories > 1;
90 : : }
91 : :
92 : :
93 : : /** Is the given theory module active in this logic? */
94 : 237423000 : bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const {
95 [ + + ]: 237423000 : PrettyCheckArgument(d_locked, *this,
96 : : "This LogicInfo isn't locked yet, and cannot be queried");
97 : 237423000 : return d_theories[theory];
98 : : }
99 : :
100 : : /** Is this a quantified logic? */
101 : 1089200 : bool LogicInfo::isQuantified() const {
102 [ + + ]: 1089200 : PrettyCheckArgument(d_locked, *this,
103 : : "This LogicInfo isn't locked yet, and cannot be queried");
104 : 1089200 : return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
105 : : }
106 : :
107 : : /** Is this a higher-order logic? */
108 : 15852800 : bool LogicInfo::isHigherOrder() const
109 : : {
110 [ - + ]: 15852800 : PrettyCheckArgument(d_locked,
111 : : *this,
112 : : "This LogicInfo isn't locked yet, and cannot be queried");
113 : 15852800 : return d_higherOrder;
114 : : }
115 : :
116 : 92493 : bool LogicInfo::hasEverything() const
117 : : {
118 [ - + ]: 92493 : PrettyCheckArgument(d_locked,
119 : : *this,
120 : : "This LogicInfo isn't locked yet, and cannot be queried");
121 : 184986 : LogicInfo everything;
122 : 92493 : everything.enableEverything(isHigherOrder());
123 : 92493 : everything.lock();
124 : 184986 : return (*this == everything);
125 : : }
126 : :
127 : : /** Is this the all-exclusive logic? (Here, that means propositional logic) */
128 : 26 : bool LogicInfo::hasNothing() const {
129 [ - + ]: 26 : PrettyCheckArgument(d_locked, *this,
130 : : "This LogicInfo isn't locked yet, and cannot be queried");
131 : 52 : LogicInfo nothing("");
132 : 26 : nothing.lock();
133 : 52 : return *this == nothing;
134 : : }
135 : :
136 : 528405 : bool LogicInfo::isPure(theory::TheoryId theory) const {
137 [ + + ]: 528405 : PrettyCheckArgument(d_locked, *this,
138 : : "This LogicInfo isn't locked yet, and cannot be queried");
139 : : // the third and fourth conjucts are really just to rule out the misleading
140 : : // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
141 [ + + ]: 988566 : return isTheoryEnabled(theory) && !isSharingEnabled() &&
142 [ + + ][ + + ]: 1004880 : ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
[ + - ][ + + ]
143 [ + + ]: 544714 : ( isTrueTheory(theory) || d_sharingTheories == 0 );
144 : : }
145 : :
146 : 1036150 : bool LogicInfo::areIntegersUsed() const {
147 [ + + ]: 1036150 : PrettyCheckArgument(d_locked, *this,
148 : : "This LogicInfo isn't locked yet, and cannot be queried");
149 [ + + ]: 1036150 : PrettyCheckArgument(
150 : : isTheoryEnabled(theory::THEORY_ARITH), *this,
151 : : "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
152 : 1036140 : return d_integers;
153 : : }
154 : :
155 : 61286 : bool LogicInfo::areRealsUsed() const {
156 [ + + ]: 61286 : PrettyCheckArgument(d_locked, *this,
157 : : "This LogicInfo isn't locked yet, and cannot be queried");
158 [ + + ]: 61285 : PrettyCheckArgument(
159 : : isTheoryEnabled(theory::THEORY_ARITH), *this,
160 : : "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
161 : 61283 : return d_reals;
162 : : }
163 : :
164 : 108014 : bool LogicInfo::areTranscendentalsUsed() const
165 : : {
166 [ - + ]: 108014 : PrettyCheckArgument(d_locked,
167 : : *this,
168 : : "This LogicInfo isn't locked yet, and cannot be queried");
169 [ + + ]: 108014 : PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH),
170 : : *this,
171 : : "Arithmetic not used in this LogicInfo; cannot ask "
172 : : "whether transcendentals are used");
173 : 108012 : return d_transcendentals;
174 : : }
175 : :
176 : 474901 : bool LogicInfo::isLinear() const {
177 [ + + ]: 474901 : PrettyCheckArgument(d_locked, *this,
178 : : "This LogicInfo isn't locked yet, and cannot be queried");
179 [ + + ]: 474900 : PrettyCheckArgument(
180 : : isTheoryEnabled(theory::THEORY_ARITH), *this,
181 : : "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
182 [ + + ][ - + ]: 474898 : return d_linear || d_differenceLogic;
183 : : }
184 : :
185 : 35767 : bool LogicInfo::isDifferenceLogic() const {
186 [ - + ]: 35767 : PrettyCheckArgument(d_locked, *this,
187 : : "This LogicInfo isn't locked yet, and cannot be queried");
188 [ + + ]: 35767 : PrettyCheckArgument(
189 : : isTheoryEnabled(theory::THEORY_ARITH), *this,
190 : : "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
191 : 35765 : return d_differenceLogic;
192 : : }
193 : :
194 : 100088 : bool LogicInfo::hasCardinalityConstraints() const {
195 [ - + ]: 100088 : PrettyCheckArgument(d_locked, *this,
196 : : "This LogicInfo isn't locked yet, and cannot be queried");
197 : 100088 : return d_cardinalityConstraints;
198 : : }
199 : :
200 : :
201 : 130106 : bool LogicInfo::operator==(const LogicInfo& other) const {
202 [ + - ][ - + ]: 130106 : PrettyCheckArgument(isLocked() && other.isLocked(), *this,
[ - + ]
203 : : "This LogicInfo isn't locked yet, and cannot be queried");
204 [ + + ]: 1216920 : for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
205 [ + + ]: 1159280 : if(d_theories[id] != other.d_theories[id]) {
206 : 72461 : return false;
207 : : }
208 : : }
209 : :
210 [ - + ]: 57645 : PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
211 : : "LogicInfo internal inconsistency");
212 [ + + ]: 57645 : if (d_cardinalityConstraints != other.d_cardinalityConstraints ||
213 [ + + ]: 57623 : d_higherOrder != other.d_higherOrder )
214 : : {
215 : 38 : return false;
216 : : }
217 [ + + ]: 57607 : if(isTheoryEnabled(theory::THEORY_ARITH)) {
218 [ + + ]: 56942 : return d_integers == other.d_integers && d_reals == other.d_reals
219 [ + + ]: 56894 : && d_transcendentals == other.d_transcendentals
220 [ + + ]: 56627 : && d_linear == other.d_linear
221 [ + + ][ + + ]: 114516 : && d_differenceLogic == other.d_differenceLogic;
222 : : }
223 : 33 : return true;
224 : : }
225 : :
226 : 3522 : bool LogicInfo::operator<=(const LogicInfo& other) const {
227 [ + - ][ - + ]: 3522 : PrettyCheckArgument(isLocked() && other.isLocked(), *this,
[ - + ]
228 : : "This LogicInfo isn't locked yet, and cannot be queried");
229 [ + + ]: 33786 : for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
230 [ + + ][ + + ]: 32325 : if(d_theories[id] && !other.d_theories[id]) {
[ + + ]
231 : 2061 : return false;
232 : : }
233 : : }
234 [ - + ]: 1461 : PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
235 : : "LogicInfo internal inconsistency");
236 [ - + ]: 12 : bool res = (!d_cardinalityConstraints || other.d_cardinalityConstraints)
237 [ + + ][ + + ]: 1473 : && (!d_higherOrder || other.d_higherOrder);
[ - + ]
238 [ + + ][ + - ]: 1461 : if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
[ + + ]
239 [ + + ][ + + ]: 1317 : return (!d_integers || other.d_integers) && (!d_reals || other.d_reals)
[ + + ]
240 [ + + ][ - + ]: 861 : && (!d_transcendentals || other.d_transcendentals)
241 [ + + ][ + + ]: 852 : && (d_linear || !other.d_linear)
242 [ + + ][ + + ]: 2634 : && (d_differenceLogic || !other.d_differenceLogic) && res;
[ + + ][ + + ]
243 : : } else {
244 : 144 : return res;
245 : : }
246 : : }
247 : :
248 : 3255 : bool LogicInfo::operator>=(const LogicInfo& other) const {
249 [ + - ][ - + ]: 3255 : PrettyCheckArgument(isLocked() && other.isLocked(), *this,
[ - + ]
250 : : "This LogicInfo isn't locked yet, and cannot be queried");
251 [ + + ]: 31377 : for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
252 [ + + ][ + + ]: 30000 : if(!d_theories[id] && other.d_theories[id]) {
[ + + ]
253 : 1878 : return false;
254 : : }
255 : : }
256 [ - + ]: 1377 : PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
257 : : "LogicInfo internal inconsistency");
258 [ + + ]: 1362 : bool res = (d_cardinalityConstraints || !other.d_cardinalityConstraints)
259 [ + + ][ + + ]: 2739 : && (d_higherOrder || !other.d_higherOrder);
[ + + ]
260 [ + + ][ + + ]: 1377 : if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
[ + + ]
261 [ + + ][ + + ]: 1245 : return (d_integers || !other.d_integers) && (d_reals || !other.d_reals)
[ + + ]
262 [ + + ][ + + ]: 797 : && (d_transcendentals || !other.d_transcendentals)
263 [ + + ][ + + ]: 791 : && (!d_linear || other.d_linear)
264 [ + + ][ + + ]: 2490 : && (!d_differenceLogic || other.d_differenceLogic) && res;
[ + + ][ + + ]
265 : : } else {
266 : 132 : return res;
267 : : }
268 : : }
269 : :
270 : 2978 : std::string LogicInfo::getLogicString() const {
271 [ + + ]: 2978 : PrettyCheckArgument(
272 : : d_locked, *this,
273 : : "This LogicInfo isn't locked yet, and cannot be queried");
274 [ + + ]: 2977 : if(d_logicString == "") {
275 : 636 : LogicInfo qf_all_supported;
276 : 318 : qf_all_supported.disableQuantifiers();
277 : 318 : qf_all_supported.lock();
278 : 318 : stringstream ss;
279 [ + + ]: 318 : if (isHigherOrder())
280 : : {
281 : 1 : ss << "HO_";
282 : : }
283 [ + + ]: 318 : if (!isQuantified())
284 : : {
285 : 263 : ss << "QF_";
286 : : }
287 [ + - ][ + + ]: 318 : if (*this == qf_all_supported || hasEverything())
[ + + ]
288 : : {
289 : 3 : ss << "ALL";
290 : : }
291 : : else
292 : : {
293 : 315 : size_t seen = 0; // make sure we support all the active theories
294 [ + + ]: 315 : if (d_theories[THEORY_SEP])
295 : : {
296 : 3 : ss << "SEP_";
297 : 3 : ++seen;
298 : : }
299 [ + + ]: 315 : if(d_theories[THEORY_ARRAYS]) {
300 [ + + ]: 10 : ss << (d_sharingTheories == 1 ? "AX" : "A");
301 : 10 : ++seen;
302 : : }
303 [ + + ]: 315 : if(d_theories[THEORY_UF]) {
304 : 5 : ss << "UF";
305 : 5 : ++seen;
306 : : }
307 [ - + ]: 315 : if( d_cardinalityConstraints ){
308 : 0 : ss << "C";
309 : : }
310 [ + + ]: 315 : if(d_theories[THEORY_BV]) {
311 : 300 : ss << "BV";
312 : 300 : ++seen;
313 : : }
314 [ + + ]: 315 : if (d_theories[THEORY_FF])
315 : : {
316 : 2 : ss << "FF";
317 : 2 : ++seen;
318 : : }
319 [ + + ]: 315 : if(d_theories[THEORY_FP]) {
320 : 5 : ss << "FP";
321 : 5 : ++seen;
322 : : }
323 [ + + ]: 315 : if(d_theories[THEORY_DATATYPES]) {
324 : 2 : ss << "DT";
325 : 2 : ++seen;
326 : : }
327 [ - + ]: 315 : if(d_theories[THEORY_STRINGS]) {
328 : 0 : ss << "S";
329 : 0 : ++seen;
330 : : }
331 [ + + ]: 315 : if(d_theories[THEORY_ARITH]) {
332 [ - + ]: 310 : if(isDifferenceLogic()) {
333 [ - - ]: 0 : ss << (areIntegersUsed() ? "I" : "");
334 [ - - ]: 0 : ss << (areRealsUsed() ? "R" : "");
335 : 0 : ss << "DL";
336 : : } else {
337 [ + + ]: 310 : ss << (isLinear() ? "L" : "N");
338 [ + + ]: 310 : ss << (areIntegersUsed() ? "I" : "");
339 [ + + ]: 310 : ss << (areRealsUsed() ? "R" : "");
340 : 310 : ss << "A";
341 [ + + ]: 310 : ss << (areTranscendentalsUsed() ? "T" : "");
342 : : }
343 : 310 : ++seen;
344 : : }
345 [ - + ]: 315 : if(d_theories[THEORY_SETS]) {
346 : 0 : ss << "FS";
347 : 0 : ++seen;
348 : : }
349 [ - + ]: 315 : if (d_theories[THEORY_BAGS])
350 : : {
351 : 0 : ss << "FB";
352 : 0 : ++seen;
353 : : }
354 [ - + ]: 315 : if(seen != d_sharingTheories) {
355 : 0 : Unhandled()
356 : : << "can't extract a logic string from LogicInfo; at least one "
357 : 0 : "active theory is unknown to LogicInfo::getLogicString() !";
358 : : }
359 : :
360 [ - + ]: 315 : if(seen == 0) {
361 : 0 : ss << "SAT";
362 : : }
363 : : }
364 : 318 : d_logicString = ss.str();
365 : : }
366 : 2977 : return d_logicString;
367 : : }
368 : :
369 : 0 : void throwTwoArithmeticTheoriesError(const char* th1, const char* th2)
370 : : {
371 : 0 : stringstream err;
372 : : err << "a logic name can only contain one arithmetic theory but found two: "
373 : 0 : << th1 << " and " << th2;
374 : 0 : throw cvc5::internal::Exception(err.str().c_str());
375 : : }
376 : :
377 : 49621 : void checkMultipleArithmeticTheories(const char* prevTheory,
378 : : const char* currentTheory)
379 : : {
380 [ - + ]: 49621 : if (*prevTheory != '\0')
381 : : {
382 : 0 : throwTwoArithmeticTheoriesError(prevTheory, currentTheory);
383 : : }
384 : 49621 : }
385 : :
386 : 63282 : void LogicInfo::checkDuplicateTheory(TheoryId theory, const char* id)
387 : : {
388 [ - + ]: 63282 : if (d_theories[theory])
389 : : {
390 : 0 : stringstream err;
391 : 0 : err << "duplicate theory: " << id;
392 : 0 : throw cvc5::internal::Exception(err.str().c_str());
393 : : }
394 : 63282 : }
395 : :
396 : 85420 : void LogicInfo::setLogicString(std::string logicString)
397 : : {
398 [ - + ]: 85420 : PrettyCheckArgument(!d_locked, *this,
399 : : "This LogicInfo is locked, and cannot be modified");
400 [ + + ]: 1281300 : for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
401 : 1195880 : d_theories[id] = false;// ensure it's cleared
402 : : }
403 : 85420 : d_sharingTheories = 0;
404 : :
405 : : // Below, ONLY use enableTheory()/disableTheory() rather than
406 : : // accessing d_theories[] directly. This makes sure to set up
407 : : // sharing properly.
408 : :
409 : 85420 : enableTheory(THEORY_BUILTIN);
410 : 85420 : enableTheory(THEORY_BOOL);
411 : :
412 : 85420 : const char* p = logicString.c_str();
413 [ + + ]: 85420 : if (!strncmp(p, "HO_", 3))
414 : : {
415 : 2047 : enableHigherOrder();
416 : 2047 : p += 3;
417 : : }
418 [ + + ]: 85420 : if(*p == '\0') {
419 : : // propositional logic only; we're done.
420 [ + + ]: 85393 : } else if(!strcmp(p, "QF_SAT")) {
421 : : // propositional logic only; we're done.
422 : 41 : p += 6;
423 [ + + ]: 85352 : } else if(!strcmp(p, "SAT")) {
424 : : // quantified Boolean formulas only; we're done.
425 : 60 : enableQuantifiers();
426 : 60 : p += 3;
427 [ + + ]: 85292 : } else if(!strcmp(p, "QF_ALL")) {
428 : : // the "all theories included" logic, no quantifiers.
429 : 1038 : enableEverything(d_higherOrder);
430 : 1038 : disableQuantifiers();
431 : 1038 : arithNonLinear();
432 : 1038 : p += 6;
433 [ + + ]: 84254 : } else if(!strcmp(p, "ALL")) {
434 : : // the "all theories included" logic, with quantifiers.
435 : 20808 : enableEverything(d_higherOrder);
436 : 20808 : enableQuantifiers();
437 : 20808 : arithNonLinear();
438 : 20808 : p += 3;
439 : : }
440 [ - + ]: 63446 : else if (!strcmp(p, "HORN"))
441 : : {
442 : : // the HORN logic
443 : 0 : enableEverything(d_higherOrder);
444 : 0 : enableQuantifiers();
445 : 0 : arithNonLinear();
446 : 0 : p += 4;
447 : : } else {
448 [ + + ]: 63446 : if(!strncmp(p, "QF_", 3)) {
449 : 56620 : disableQuantifiers();
450 : 56620 : p += 3;
451 : : } else {
452 : 6826 : enableQuantifiers();
453 : : }
454 [ + + ]: 63446 : if (!strncmp(p, "SEP_", 4))
455 : : {
456 : 24 : enableSeparationLogic();
457 : 24 : p += 4;
458 : : }
459 [ + + ]: 63446 : if(!strncmp(p, "AX", 2)) {
460 : 147 : enableTheory(THEORY_ARRAYS);
461 : 147 : p += 2;
462 : : } else {
463 : : // arithmeticTheory points to "\0" if no arithmetic theory has been read
464 : : // yet; otherwise it points to the arithmetic theory that has already been
465 : : // read.
466 : 63299 : const char* arithmeticTheory = "\0";
467 : : // whether an unrecognized theory has been read
468 : 63299 : bool unrecognizedTheory = false;
469 [ + - ][ + + ]: 176327 : while (!unrecognizedTheory && (*p != '\0'))
470 : : {
471 [ + + ]: 113028 : if (*p == 'A')
472 : : {
473 : 4303 : checkDuplicateTheory(THEORY_ARRAYS, "A");
474 : 4303 : enableTheory(THEORY_ARRAYS);
475 : 4303 : ++p;
476 : : }
477 [ + + ]: 108725 : else if (!strncmp(p, "UF", 2))
478 : : {
479 : 43280 : checkDuplicateTheory(THEORY_UF, "UF");
480 : 43280 : enableTheory(THEORY_UF);
481 : 43280 : p += 2;
482 : : }
483 [ + + ]: 65445 : else if (!strncmp(p, "C", 1))
484 : : {
485 [ - + ]: 125 : if (d_cardinalityConstraints)
486 : : {
487 : 0 : throw cvc5::internal::Exception("duplicate theory: C");
488 : : }
489 : 125 : enableCardinalityConstraints();
490 : 125 : p += 1;
491 : : }
492 [ + + ]: 65320 : else if (!strncmp(p, "BV", 2))
493 : : {
494 : 10598 : checkDuplicateTheory(THEORY_BV, "BV");
495 : 10598 : enableTheory(THEORY_BV);
496 : 10598 : p += 2;
497 : : }
498 [ + + ]: 54722 : else if (!strncmp(p, "FF", 2))
499 : : {
500 : 682 : checkDuplicateTheory(THEORY_FF, "FF");
501 : 682 : enableTheory(THEORY_FF);
502 : 682 : p += 2;
503 : : }
504 [ + + ]: 54040 : else if (!strncmp(p, "FP", 2))
505 : : {
506 : 377 : checkDuplicateTheory(THEORY_FP, "FP");
507 : 377 : enableTheory(THEORY_FP);
508 : 377 : p += 2;
509 : : }
510 [ + + ]: 53663 : else if (!strncmp(p, "DT", 2))
511 : : {
512 : 444 : checkDuplicateTheory(THEORY_DATATYPES, "DT");
513 : 444 : enableTheory(THEORY_DATATYPES);
514 : 444 : p += 2;
515 : : }
516 [ + + ]: 53219 : else if (*p == 'S')
517 : : {
518 : 3202 : checkDuplicateTheory(THEORY_STRINGS, "S");
519 : 3202 : enableTheory(THEORY_STRINGS);
520 : 3202 : ++p;
521 : : }
522 [ + + ]: 50017 : else if (!strncmp(p, "IDL", 3))
523 : : {
524 : 170 : checkMultipleArithmeticTheories(arithmeticTheory, "IDL");
525 : 170 : enableIntegers();
526 : 170 : disableReals();
527 : 170 : arithOnlyDifference();
528 : 170 : p += 3;
529 : 170 : arithmeticTheory = "IDL";
530 : : }
531 [ + + ]: 49847 : else if (!strncmp(p, "RDL", 3))
532 : : {
533 : 109 : checkMultipleArithmeticTheories(arithmeticTheory, "RDL");
534 : 109 : disableIntegers();
535 : 109 : enableReals();
536 : 109 : arithOnlyDifference();
537 : 109 : arithmeticTheory = "RDL";
538 : 109 : p += 3;
539 : : }
540 [ - + ]: 49738 : else if (!strncmp(p, "IRDL", 4))
541 : : {
542 : : // "IRDL" ?! --not very useful, but getLogicString() can produce
543 : : // that string, so we really had better be able to read it back in.
544 : 0 : checkMultipleArithmeticTheories(arithmeticTheory, "IRDL");
545 : 0 : enableIntegers();
546 : 0 : enableReals();
547 : 0 : arithOnlyDifference();
548 : 0 : arithmeticTheory = "IRDL";
549 : 0 : p += 4;
550 : : }
551 [ + + ]: 49738 : else if (!strncmp(p, "LIA", 3))
552 : : {
553 : 8430 : checkMultipleArithmeticTheories(arithmeticTheory, "LIA");
554 : 8430 : enableIntegers();
555 : 8430 : disableReals();
556 : 8430 : arithOnlyLinear();
557 : 8430 : arithmeticTheory = "LIA";
558 : 8430 : p += 3;
559 : : }
560 [ + + ]: 41308 : else if (!strncmp(p, "LRA", 3))
561 : : {
562 : 1778 : checkMultipleArithmeticTheories(arithmeticTheory, "LRA");
563 : 1778 : disableIntegers();
564 : 1778 : enableReals();
565 : 1778 : arithOnlyLinear();
566 : 1778 : arithmeticTheory = "LRA";
567 : 1778 : p += 3;
568 : : }
569 [ + + ]: 39530 : else if (!strncmp(p, "LIRA", 4))
570 : : {
571 : 947 : checkMultipleArithmeticTheories(arithmeticTheory, "LIRA");
572 : 947 : enableIntegers();
573 : 947 : enableReals();
574 : 947 : arithOnlyLinear();
575 : 947 : arithmeticTheory = "LIRA";
576 : 947 : p += 4;
577 : : }
578 [ + + ]: 38583 : else if (!strncmp(p, "NIA", 3))
579 : : {
580 : 1587 : checkMultipleArithmeticTheories(arithmeticTheory, "NIA");
581 : 1587 : enableIntegers();
582 : 1587 : disableReals();
583 : 1587 : arithNonLinear();
584 : 1587 : arithmeticTheory = "NIA";
585 : 1587 : p += 3;
586 : : }
587 [ + + ]: 36996 : else if (!strncmp(p, "NRA", 3))
588 : : {
589 : 36124 : checkMultipleArithmeticTheories(arithmeticTheory, "NRA");
590 : 36124 : disableIntegers();
591 : 36124 : enableReals();
592 : 36124 : arithNonLinear();
593 : 36124 : arithmeticTheory = "NRA";
594 : 36124 : p += 3;
595 [ + + ]: 36124 : if (*p == 'T')
596 : : {
597 : 662 : arithTranscendentals();
598 : 662 : p += 1;
599 : : }
600 : : }
601 [ + + ]: 872 : else if (!strncmp(p, "NIRA", 4))
602 : : {
603 : 476 : checkMultipleArithmeticTheories(arithmeticTheory, "NIRA");
604 : 476 : enableIntegers();
605 : 476 : enableReals();
606 : 476 : arithNonLinear();
607 : 476 : arithmeticTheory = "NIRA";
608 : 476 : p += 4;
609 [ + + ]: 476 : if (*p == 'T')
610 : : {
611 : 12 : arithTranscendentals();
612 : 12 : p += 1;
613 : : }
614 : : }
615 [ + - ]: 396 : else if (!strncmp(p, "FS", 2))
616 : : {
617 : 396 : checkDuplicateTheory(THEORY_SETS, "FS");
618 : 396 : enableTheory(THEORY_SETS);
619 : 396 : p += 2;
620 : : }
621 : : else
622 : : {
623 : 0 : unrecognizedTheory = true;
624 : : }
625 : : }
626 : : }
627 : : }
628 : :
629 [ + + ]: 85420 : if (d_theories[THEORY_FP])
630 : : {
631 : : // THEORY_BV is needed for bit-blasting.
632 : : // We have to set this here rather than in expandDefinition as it
633 : : // is possible to create variables without any theory specific
634 : : // operations, so expandDefinition won't be called.
635 : 22223 : enableTheory(THEORY_BV);
636 : : }
637 : :
638 [ - + ]: 85420 : if(*p != '\0') {
639 : 0 : stringstream err;
640 : 0 : err << "LogicInfo::setLogicString(): ";
641 [ - - ]: 0 : if(p == logicString) {
642 : 0 : err << "cannot parse logic string: " << logicString;
643 : : } else {
644 : 0 : err << "junk (\"" << p << "\") at end of logic string: " << logicString;
645 : : }
646 : : // The strings logicString and p are user-provided and
647 : : // may include format specifiers (e.g. "QF_LIA%s").
648 : : // Do not use unsafe macros/functions such as IllegalArgument.
649 : 0 : throw cvc5::internal::Exception(err.str().c_str());
650 : : }
651 : :
652 : : // ensure a getLogic() returns the same thing as was set
653 : 85420 : d_logicString = logicString;
654 : 85420 : }
655 : :
656 : 114340 : void LogicInfo::enableEverything(bool enableHigherOrder)
657 : : {
658 [ - + ]: 114340 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
659 : 114340 : *this = LogicInfo();
660 : 114340 : this->d_higherOrder = enableHigherOrder;
661 : 114340 : }
662 : :
663 : 1 : void LogicInfo::disableEverything() {
664 [ - + ]: 1 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
665 : 1 : *this = LogicInfo("");
666 : 1 : }
667 : :
668 : 5572090 : void LogicInfo::enableTheory(theory::TheoryId theory) {
669 [ - + ]: 5572090 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
670 [ + + ]: 5572090 : if(!d_theories[theory]) {
671 [ + + ]: 5498320 : if(isTrueTheory(theory)) {
672 : 4204620 : ++d_sharingTheories;
673 : : }
674 : 5498320 : d_logicString = "";
675 : 5498320 : d_theories[theory] = true;
676 : : }
677 : 5572090 : }
678 : :
679 : 96096 : void LogicInfo::disableTheory(theory::TheoryId theory) {
680 [ + + ]: 96096 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
681 [ + + ]: 96091 : if(d_theories[theory]) {
682 [ + + ]: 1457 : if(isTrueTheory(theory)) {
683 [ - + ][ - + ]: 100 : Assert(d_sharingTheories > 0);
[ - - ]
684 : 100 : --d_sharingTheories;
685 : : }
686 [ + - ][ - + ]: 1457 : if(theory == THEORY_BUILTIN ||
687 : : theory == THEORY_BOOL) {
688 : 0 : return;
689 : : }
690 : 1457 : d_logicString = "";
691 : 1457 : d_theories[theory] = false;
692 : : }
693 : : }
694 : :
695 : 8008 : void LogicInfo::enableSygus()
696 : : {
697 : 8008 : enableQuantifiers();
698 : 8008 : enableTheory(THEORY_UF);
699 : 8008 : enableTheory(THEORY_DATATYPES);
700 : 8008 : enableIntegers();
701 : 8008 : }
702 : :
703 : 24 : void LogicInfo::enableSeparationLogic()
704 : : {
705 : 24 : enableTheory(THEORY_SEP);
706 : 24 : enableTheory(THEORY_UF);
707 : 24 : enableTheory(THEORY_SETS);
708 : 24 : }
709 : :
710 : 20379 : void LogicInfo::enableIntegers() {
711 [ + + ]: 20379 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
712 : 20378 : d_logicString = "";
713 : 20378 : enableTheory(THEORY_ARITH);
714 : 20378 : d_integers = true;
715 : 20378 : }
716 : :
717 : 38013 : void LogicInfo::disableIntegers() {
718 [ + + ]: 38013 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
719 : 38012 : d_logicString = "";
720 : 38012 : d_integers = false;
721 [ + + ]: 38012 : if(!d_reals) {
722 : 38011 : disableTheory(THEORY_ARITH);
723 : : }
724 : 38012 : }
725 : :
726 : 39434 : void LogicInfo::enableReals() {
727 [ - + ]: 39434 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
728 : 39434 : d_logicString = "";
729 : 39434 : enableTheory(THEORY_ARITH);
730 : 39434 : d_reals = true;
731 : 39434 : }
732 : :
733 : 10189 : void LogicInfo::disableReals() {
734 [ + + ]: 10189 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
735 : 10188 : d_logicString = "";
736 : 10188 : d_reals = false;
737 [ - + ]: 10188 : if(!d_integers) {
738 : 0 : disableTheory(THEORY_ARITH);
739 : : }
740 : 10188 : }
741 : :
742 : 674 : void LogicInfo::arithTranscendentals()
743 : : {
744 [ - + ]: 674 : PrettyCheckArgument(
745 : : !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
746 : 674 : d_logicString = "";
747 : 674 : d_transcendentals = true;
748 [ - + ]: 674 : if (!d_reals)
749 : : {
750 : 0 : enableReals();
751 : : }
752 [ - + ]: 674 : if (d_linear)
753 : : {
754 : 0 : arithNonLinear();
755 : : }
756 : 674 : }
757 : :
758 : 279 : void LogicInfo::arithOnlyDifference() {
759 [ - + ]: 279 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
760 : 279 : d_logicString = "";
761 : 279 : d_linear = true;
762 : 279 : d_differenceLogic = true;
763 : 279 : d_transcendentals = false;
764 : 279 : }
765 : :
766 : 11414 : void LogicInfo::arithOnlyLinear() {
767 [ + + ]: 11414 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
768 : 11413 : d_logicString = "";
769 : 11413 : d_linear = true;
770 : 11413 : d_differenceLogic = false;
771 : 11413 : d_transcendentals = false;
772 : 11413 : }
773 : :
774 : 60535 : void LogicInfo::arithNonLinear() {
775 [ - + ]: 60535 : PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
776 : 60535 : d_logicString = "";
777 : 60535 : d_linear = false;
778 : 60535 : d_differenceLogic = false;
779 : 60535 : }
780 : :
781 : 125 : void LogicInfo::enableCardinalityConstraints()
782 : : {
783 [ - + ]: 125 : PrettyCheckArgument(
784 : : !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
785 : 125 : d_logicString = "";
786 : 125 : d_cardinalityConstraints = true;
787 : 125 : }
788 : :
789 : 0 : void LogicInfo::disableCardinalityConstraints()
790 : : {
791 [ - - ]: 0 : PrettyCheckArgument(
792 : : !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
793 : 0 : d_logicString = "";
794 : 0 : d_cardinalityConstraints = false;
795 : 0 : }
796 : :
797 : 2048 : void LogicInfo::enableHigherOrder()
798 : : {
799 [ - + ]: 2048 : PrettyCheckArgument(
800 : : !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
801 : 2048 : d_logicString = "";
802 : 2048 : d_higherOrder = true;
803 : 2048 : }
804 : :
805 : 0 : void LogicInfo::disableHigherOrder()
806 : : {
807 [ - - ]: 0 : PrettyCheckArgument(
808 : : !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
809 : 0 : d_logicString = "";
810 : 0 : d_higherOrder = false;
811 : 0 : }
812 : :
813 : 43652 : LogicInfo LogicInfo::getUnlockedCopy() const {
814 [ + - ]: 43652 : if(d_locked) {
815 : 87304 : LogicInfo info = *this;
816 : 43652 : info.d_locked = false;
817 : 43652 : return info;
818 : : } else {
819 : 0 : return *this;
820 : : }
821 : : }
822 : :
823 : 2600 : std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) {
824 : 2600 : return out << logic.getLogicString();
825 : : }
826 : :
827 : : } // namespace cvc5::internal
|
