1 /******************************************************************************
2 * Top contributors (to current version):
3 * Morgan Deters, Tim King, Andrew Reynolds
5 * This file is part of the cvc5 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.
11 * ****************************************************************************
13 * A class giving information about a logic (group a theory modules
14 * and configuration information)
16 #include "theory/logic_info.h"
23 #include "base/check.h"
24 #include "base/configuration.h"
25 #include "expr/kind.h"
28 using namespace cvc5::theory
;
32 LogicInfo::LogicInfo()
34 d_theories(THEORY_LAST
, false),
38 d_transcendentals(true),
40 d_differenceLogic(false),
41 d_cardinalityConstraints(false),
45 for (TheoryId id
= THEORY_FIRST
; id
< THEORY_LAST
; ++id
)
51 LogicInfo::LogicInfo(std::string logicString
)
53 d_theories(THEORY_LAST
, false),
57 d_transcendentals(false),
59 d_differenceLogic(false),
60 d_cardinalityConstraints(false),
64 setLogicString(logicString
);
68 LogicInfo::LogicInfo(const char* logicString
)
70 d_theories(THEORY_LAST
, false),
74 d_transcendentals(false),
76 d_differenceLogic(false),
77 d_cardinalityConstraints(false),
81 setLogicString(logicString
);
85 /** Is sharing enabled for this logic? */
86 bool LogicInfo::isSharingEnabled() const {
87 PrettyCheckArgument(d_locked
, *this,
88 "This LogicInfo isn't locked yet, and cannot be queried");
89 return d_sharingTheories
> 1;
93 /** Is the given theory module active in this logic? */
94 bool LogicInfo::isTheoryEnabled(theory::TheoryId theory
) const {
95 PrettyCheckArgument(d_locked
, *this,
96 "This LogicInfo isn't locked yet, and cannot be queried");
97 return d_theories
[theory
];
100 /** Is this a quantified logic? */
101 bool LogicInfo::isQuantified() const {
102 PrettyCheckArgument(d_locked
, *this,
103 "This LogicInfo isn't locked yet, and cannot be queried");
104 return isTheoryEnabled(theory::THEORY_QUANTIFIERS
);
107 /** Is this a higher-order logic? */
108 bool LogicInfo::isHigherOrder() const
110 PrettyCheckArgument(d_locked
,
112 "This LogicInfo isn't locked yet, and cannot be queried");
113 return d_higherOrder
;
116 bool LogicInfo::hasEverything() const
118 PrettyCheckArgument(d_locked
,
120 "This LogicInfo isn't locked yet, and cannot be queried");
121 LogicInfo everything
;
122 everything
.enableEverything(isHigherOrder());
124 return (*this == everything
);
127 /** Is this the all-exclusive logic? (Here, that means propositional logic) */
128 bool LogicInfo::hasNothing() const {
129 PrettyCheckArgument(d_locked
, *this,
130 "This LogicInfo isn't locked yet, and cannot be queried");
131 LogicInfo
nothing("");
133 return *this == nothing
;
136 bool LogicInfo::isPure(theory::TheoryId theory
) const {
137 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 return isTheoryEnabled(theory
) && !isSharingEnabled() &&
142 ( !isTrueTheory(theory
) || d_sharingTheories
== 1 ) &&
143 ( isTrueTheory(theory
) || d_sharingTheories
== 0 );
146 bool LogicInfo::areIntegersUsed() const {
147 PrettyCheckArgument(d_locked
, *this,
148 "This LogicInfo isn't locked yet, and cannot be queried");
150 isTheoryEnabled(theory::THEORY_ARITH
), *this,
151 "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
155 bool LogicInfo::areRealsUsed() const {
156 PrettyCheckArgument(d_locked
, *this,
157 "This LogicInfo isn't locked yet, and cannot be queried");
159 isTheoryEnabled(theory::THEORY_ARITH
), *this,
160 "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
164 bool LogicInfo::areTranscendentalsUsed() const
166 PrettyCheckArgument(d_locked
,
168 "This LogicInfo isn't locked yet, and cannot be queried");
169 PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH
),
171 "Arithmetic not used in this LogicInfo; cannot ask "
172 "whether transcendentals are used");
173 return d_transcendentals
;
176 bool LogicInfo::isLinear() const {
177 PrettyCheckArgument(d_locked
, *this,
178 "This LogicInfo isn't locked yet, and cannot be queried");
180 isTheoryEnabled(theory::THEORY_ARITH
), *this,
181 "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
182 return d_linear
|| d_differenceLogic
;
185 bool LogicInfo::isDifferenceLogic() const {
186 PrettyCheckArgument(d_locked
, *this,
187 "This LogicInfo isn't locked yet, and cannot be queried");
189 isTheoryEnabled(theory::THEORY_ARITH
), *this,
190 "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
191 return d_differenceLogic
;
194 bool LogicInfo::hasCardinalityConstraints() const {
195 PrettyCheckArgument(d_locked
, *this,
196 "This LogicInfo isn't locked yet, and cannot be queried");
197 return d_cardinalityConstraints
;
201 bool LogicInfo::operator==(const LogicInfo
& other
) const {
202 PrettyCheckArgument(isLocked() && other
.isLocked(), *this,
203 "This LogicInfo isn't locked yet, and cannot be queried");
204 for(theory::TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
205 if(d_theories
[id
] != other
.d_theories
[id
]) {
210 PrettyCheckArgument(d_sharingTheories
== other
.d_sharingTheories
, *this,
211 "LogicInfo internal inconsistency");
212 if (d_cardinalityConstraints
!= other
.d_cardinalityConstraints
||
213 d_higherOrder
!= other
.d_higherOrder
)
217 if(isTheoryEnabled(theory::THEORY_ARITH
)) {
218 return d_integers
== other
.d_integers
&& d_reals
== other
.d_reals
219 && d_transcendentals
== other
.d_transcendentals
220 && d_linear
== other
.d_linear
221 && d_differenceLogic
== other
.d_differenceLogic
;
226 bool LogicInfo::operator<=(const LogicInfo
& other
) const {
227 PrettyCheckArgument(isLocked() && other
.isLocked(), *this,
228 "This LogicInfo isn't locked yet, and cannot be queried");
229 for(theory::TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
230 if(d_theories
[id
] && !other
.d_theories
[id
]) {
234 PrettyCheckArgument(d_sharingTheories
<= other
.d_sharingTheories
, *this,
235 "LogicInfo internal inconsistency");
236 bool res
= (!d_cardinalityConstraints
|| other
.d_cardinalityConstraints
)
237 && (!d_higherOrder
|| other
.d_higherOrder
);
238 if(isTheoryEnabled(theory::THEORY_ARITH
) && other
.isTheoryEnabled(theory::THEORY_ARITH
)) {
239 return (!d_integers
|| other
.d_integers
) && (!d_reals
|| other
.d_reals
)
240 && (!d_transcendentals
|| other
.d_transcendentals
)
241 && (d_linear
|| !other
.d_linear
)
242 && (d_differenceLogic
|| !other
.d_differenceLogic
) && res
;
248 bool LogicInfo::operator>=(const LogicInfo
& other
) const {
249 PrettyCheckArgument(isLocked() && other
.isLocked(), *this,
250 "This LogicInfo isn't locked yet, and cannot be queried");
251 for(theory::TheoryId id
= theory::THEORY_FIRST
; id
< theory::THEORY_LAST
; ++id
) {
252 if(!d_theories
[id
] && other
.d_theories
[id
]) {
256 PrettyCheckArgument(d_sharingTheories
>= other
.d_sharingTheories
, *this,
257 "LogicInfo internal inconsistency");
258 bool res
= (d_cardinalityConstraints
|| !other
.d_cardinalityConstraints
)
259 && (d_higherOrder
|| !other
.d_higherOrder
);
260 if(isTheoryEnabled(theory::THEORY_ARITH
) && other
.isTheoryEnabled(theory::THEORY_ARITH
)) {
261 return (d_integers
|| !other
.d_integers
) && (d_reals
|| !other
.d_reals
)
262 && (d_transcendentals
|| !other
.d_transcendentals
)
263 && (!d_linear
|| other
.d_linear
)
264 && (!d_differenceLogic
|| other
.d_differenceLogic
) && res
;
270 std::string
LogicInfo::getLogicString() const {
273 "This LogicInfo isn't locked yet, and cannot be queried");
274 if(d_logicString
== "") {
275 LogicInfo qf_all_supported
;
276 qf_all_supported
.disableQuantifiers();
277 qf_all_supported
.lock();
287 if (*this == qf_all_supported
|| hasEverything())
293 size_t seen
= 0; // make sure we support all the active theories
294 if (d_theories
[THEORY_SEP
])
299 if(d_theories
[THEORY_ARRAYS
]) {
300 ss
<< (d_sharingTheories
== 1 ? "AX" : "A");
303 if(d_theories
[THEORY_UF
]) {
307 if( d_cardinalityConstraints
){
310 if(d_theories
[THEORY_BV
]) {
314 if(d_theories
[THEORY_FP
]) {
318 if(d_theories
[THEORY_DATATYPES
]) {
322 if(d_theories
[THEORY_STRINGS
]) {
326 if(d_theories
[THEORY_ARITH
]) {
327 if(isDifferenceLogic()) {
328 ss
<< (areIntegersUsed() ? "I" : "");
329 ss
<< (areRealsUsed() ? "R" : "");
332 ss
<< (isLinear() ? "L" : "N");
333 ss
<< (areIntegersUsed() ? "I" : "");
334 ss
<< (areRealsUsed() ? "R" : "");
336 ss
<< (areTranscendentalsUsed() ? "T" : "");
340 if(d_theories
[THEORY_SETS
]) {
344 if (d_theories
[THEORY_BAGS
])
349 if(seen
!= d_sharingTheories
) {
351 << "can't extract a logic string from LogicInfo; at least one "
352 "active theory is unknown to LogicInfo::getLogicString() !";
359 d_logicString
= ss
.str();
361 return d_logicString
;
364 void LogicInfo::setLogicString(std::string logicString
)
366 PrettyCheckArgument(!d_locked
, *this,
367 "This LogicInfo is locked, and cannot be modified");
368 for(TheoryId id
= THEORY_FIRST
; id
< THEORY_LAST
; ++id
) {
369 d_theories
[id
] = false;// ensure it's cleared
371 d_sharingTheories
= 0;
373 // Below, ONLY use enableTheory()/disableTheory() rather than
374 // accessing d_theories[] directly. This makes sure to set up
377 enableTheory(THEORY_BUILTIN
);
378 enableTheory(THEORY_BOOL
);
380 const char* p
= logicString
.c_str();
381 if (!strncmp(p
, "HO_", 3))
387 // propositional logic only; we're done.
388 } else if(!strcmp(p
, "QF_SAT")) {
389 // propositional logic only; we're done.
391 } else if(!strcmp(p
, "SAT")) {
392 // quantified Boolean formulas only; we're done.
395 } else if(!strcmp(p
, "QF_ALL")) {
396 // the "all theories included" logic, no quantifiers.
397 enableEverything(d_higherOrder
);
398 disableQuantifiers();
401 } else if(!strcmp(p
, "ALL")) {
402 // the "all theories included" logic, with quantifiers.
403 enableEverything(d_higherOrder
);
408 else if (!strcmp(p
, "HORN"))
411 enableEverything(d_higherOrder
);
416 if(!strncmp(p
, "QF_", 3)) {
417 disableQuantifiers();
422 if (!strncmp(p
, "SEP_", 4))
424 enableSeparationLogic();
427 if(!strncmp(p
, "AX", 2)) {
428 enableTheory(THEORY_ARRAYS
);
432 enableTheory(THEORY_ARRAYS
);
435 if(!strncmp(p
, "UF", 2)) {
436 enableTheory(THEORY_UF
);
439 if(!strncmp(p
, "C", 1 )) {
440 d_cardinalityConstraints
= true;
443 // allow BV or DT in either order
444 if(!strncmp(p
, "BV", 2)) {
445 enableTheory(THEORY_BV
);
448 if(!strncmp(p
, "FP", 2)) {
449 enableTheory(THEORY_FP
);
452 if(!strncmp(p
, "DT", 2)) {
453 enableTheory(THEORY_DATATYPES
);
456 if(!d_theories
[THEORY_BV
] && !strncmp(p
, "BV", 2)) {
457 enableTheory(THEORY_BV
);
461 enableTheory(THEORY_STRINGS
);
464 if(!strncmp(p
, "IDL", 3)) {
467 arithOnlyDifference();
469 } else if(!strncmp(p
, "RDL", 3)) {
472 arithOnlyDifference();
474 } else if(!strncmp(p
, "IRDL", 4)) {
475 // "IRDL" ?! --not very useful, but getLogicString() can produce
476 // that string, so we really had better be able to read it back in.
479 arithOnlyDifference();
481 } else if(!strncmp(p
, "LIA", 3)) {
486 } else if(!strncmp(p
, "LRA", 3)) {
491 } else if(!strncmp(p
, "LIRA", 4)) {
496 } else if(!strncmp(p
, "NIA", 3)) {
501 } else if(!strncmp(p
, "NRA", 3)) {
508 arithTranscendentals();
511 } else if(!strncmp(p
, "NIRA", 4)) {
518 arithTranscendentals();
522 if(!strncmp(p
, "FS", 2)) {
523 enableTheory(THEORY_SETS
);
529 if (d_theories
[THEORY_FP
])
531 // THEORY_BV is needed for bit-blasting.
532 // We have to set this here rather than in expandDefinition as it
533 // is possible to create variables without any theory specific
534 // operations, so expandDefinition won't be called.
535 enableTheory(THEORY_BV
);
540 err
<< "LogicInfo::setLogicString(): ";
541 if(p
== logicString
) {
542 err
<< "cannot parse logic string: " << logicString
;
544 err
<< "junk (\"" << p
<< "\") at end of logic string: " << logicString
;
546 IllegalArgument(logicString
, err
.str().c_str());
549 // ensure a getLogic() returns the same thing as was set
550 d_logicString
= logicString
;
553 void LogicInfo::enableEverything(bool enableHigherOrder
)
555 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
557 this->d_higherOrder
= enableHigherOrder
;
560 void LogicInfo::disableEverything() {
561 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
562 *this = LogicInfo("");
565 void LogicInfo::enableTheory(theory::TheoryId theory
) {
566 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
567 if(!d_theories
[theory
]) {
568 if(isTrueTheory(theory
)) {
572 d_theories
[theory
] = true;
576 void LogicInfo::disableTheory(theory::TheoryId theory
) {
577 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
578 if(d_theories
[theory
]) {
579 if(isTrueTheory(theory
)) {
580 Assert(d_sharingTheories
> 0);
583 if(theory
== THEORY_BUILTIN
||
584 theory
== THEORY_BOOL
) {
588 d_theories
[theory
] = false;
592 void LogicInfo::enableSygus()
595 enableTheory(THEORY_UF
);
596 enableTheory(THEORY_DATATYPES
);
600 void LogicInfo::enableSeparationLogic()
602 enableTheory(THEORY_SEP
);
603 enableTheory(THEORY_UF
);
604 enableTheory(THEORY_SETS
);
607 void LogicInfo::enableIntegers() {
608 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
610 enableTheory(THEORY_ARITH
);
614 void LogicInfo::disableIntegers() {
615 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
619 disableTheory(THEORY_ARITH
);
623 void LogicInfo::enableReals() {
624 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
626 enableTheory(THEORY_ARITH
);
630 void LogicInfo::disableReals() {
631 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
635 disableTheory(THEORY_ARITH
);
639 void LogicInfo::arithTranscendentals()
642 !d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
644 d_transcendentals
= true;
655 void LogicInfo::arithOnlyDifference() {
656 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
659 d_differenceLogic
= true;
660 d_transcendentals
= false;
663 void LogicInfo::arithOnlyLinear() {
664 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
667 d_differenceLogic
= false;
668 d_transcendentals
= false;
671 void LogicInfo::arithNonLinear() {
672 PrettyCheckArgument(!d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
675 d_differenceLogic
= false;
678 void LogicInfo::enableCardinalityConstraints()
681 !d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
683 d_cardinalityConstraints
= true;
686 void LogicInfo::disableCardinalityConstraints()
689 !d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
691 d_cardinalityConstraints
= false;
694 void LogicInfo::enableHigherOrder()
697 !d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
699 d_higherOrder
= true;
702 void LogicInfo::disableHigherOrder()
705 !d_locked
, *this, "This LogicInfo is locked, and cannot be modified");
707 d_higherOrder
= false;
710 LogicInfo
LogicInfo::getUnlockedCopy() const {
712 LogicInfo info
= *this;
713 info
.d_locked
= false;
720 std::ostream
& operator<<(std::ostream
& out
, const LogicInfo
& logic
) {
721 return out
<< logic
.getLogicString();