src/theory/logic_info.cpp

   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 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(false),
  43       d_locked(false)
  44 {
  45   for (TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id)
  46   {
  47     enableTheory(id);
  48   }
  49 }
  50
  51 LogicInfo::LogicInfo(std::string logicString)
  52     : d_logicString(""),
  53       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       d_locked(false)
  63 {
  64   setLogicString(logicString);
  65   lock();
  66 }
  67
  68 LogicInfo::LogicInfo(const char* logicString)
  69     : d_logicString(""),
  70       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       d_locked(false)
  80 {
  81   setLogicString(logicString);
  82   lock();
  83 }
  84
  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;
  90 }
  91
  92
  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];
  98 }
  99
 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);
 105 }
 106
 107 /** Is this a higher-order logic? */
 108 bool LogicInfo::isHigherOrder() const
 109 {
 110   PrettyCheckArgument(d_locked,
 111                       *this,
 112                       "This LogicInfo isn't locked yet, and cannot be queried");
 113   return d_higherOrder;
 114 }
 115
 116 bool LogicInfo::hasEverything() const
 117 {
 118   PrettyCheckArgument(d_locked,
 119                       *this,
 120                       "This LogicInfo isn't locked yet, and cannot be queried");
 121   LogicInfo everything;
 122   everything.enableEverything(isHigherOrder());
 123   everything.lock();
 124   return (*this == everything);
 125 }
 126
 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("");
 132   nothing.lock();
 133   return *this == nothing;
 134 }
 135
 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 );
 144 }
 145
 146 bool LogicInfo::areIntegersUsed() const {
 147   PrettyCheckArgument(d_locked, *this,
 148                       "This LogicInfo isn't locked yet, and cannot be queried");
 149   PrettyCheckArgument(
 150       isTheoryEnabled(theory::THEORY_ARITH), *this,
 151       "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
 152   return d_integers;
 153 }
 154
 155 bool LogicInfo::areRealsUsed() const {
 156   PrettyCheckArgument(d_locked, *this,
 157                       "This LogicInfo isn't locked yet, and cannot be queried");
 158   PrettyCheckArgument(
 159       isTheoryEnabled(theory::THEORY_ARITH), *this,
 160       "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
 161   return d_reals;
 162 }
 163
 164 bool LogicInfo::areTranscendentalsUsed() const
 165 {
 166   PrettyCheckArgument(d_locked,
 167                       *this,
 168                       "This LogicInfo isn't locked yet, and cannot be queried");
 169   PrettyCheckArgument(isTheoryEnabled(theory::THEORY_ARITH),
 170                       *this,
 171                       "Arithmetic not used in this LogicInfo; cannot ask "
 172                       "whether transcendentals are used");
 173   return d_transcendentals;
 174 }
 175
 176 bool LogicInfo::isLinear() const {
 177   PrettyCheckArgument(d_locked, *this,
 178                       "This LogicInfo isn't locked yet, and cannot be queried");
 179   PrettyCheckArgument(
 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;
 183 }
 184
 185 bool LogicInfo::isDifferenceLogic() const {
 186   PrettyCheckArgument(d_locked, *this,
 187                       "This LogicInfo isn't locked yet, and cannot be queried");
 188   PrettyCheckArgument(
 189       isTheoryEnabled(theory::THEORY_ARITH), *this,
 190       "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
 191   return d_differenceLogic;
 192 }
 193
 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;
 198 }
 199
 200
 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]) {
 206       return false;
 207     }
 208   }
 209
 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 )
 214   {
 215     return false;
 216   }
 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;
 222   }
 223   return true;
 224 }
 225
 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]) {
 231       return false;
 232     }
 233   }
 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;
 243   } else {
 244     return res;
 245   }
 246 }
 247
 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]) {
 253       return false;
 254     }
 255   }
 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;
 265     } else {
 266       return res;
 267   }
 268 }
 269
 270 std::string LogicInfo::getLogicString() const {
 271   PrettyCheckArgument(
 272       d_locked, *this,
 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();
 278     stringstream ss;
 279     if (isHigherOrder())
 280     {
 281       ss << "HO_";
 282     }
 283     if (!isQuantified())
 284     {
 285       ss << "QF_";
 286     }
 287     if (*this == qf_all_supported || hasEverything())
 288     {
 289       ss << "ALL";
 290     }
 291     else
 292     {
 293       size_t seen = 0; // make sure we support all the active theories
 294       if (d_theories[THEORY_SEP])
 295       {
 296         ss << "SEP_";
 297         ++seen;
 298       }
 299       if(d_theories[THEORY_ARRAYS]) {
 300         ss << (d_sharingTheories == 1 ? "AX" : "A");
 301         ++seen;
 302       }
 303       if(d_theories[THEORY_UF]) {
 304         ss << "UF";
 305         ++seen;
 306       }
 307       if( d_cardinalityConstraints ){
 308         ss << "C";
 309       }
 310       if(d_theories[THEORY_BV]) {
 311         ss << "BV";
 312         ++seen;
 313       }
 314       if(d_theories[THEORY_FP]) {
 315         ss << "FP";
 316         ++seen;
 317       }
 318       if(d_theories[THEORY_DATATYPES]) {
 319         ss << "DT";
 320         ++seen;
 321       }
 322       if(d_theories[THEORY_STRINGS]) {
 323         ss << "S";
 324         ++seen;
 325       }
 326       if(d_theories[THEORY_ARITH]) {
 327         if(isDifferenceLogic()) {
 328           ss << (areIntegersUsed() ? "I" : "");
 329           ss << (areRealsUsed() ? "R" : "");
 330           ss << "DL";
 331         } else {
 332           ss << (isLinear() ? "L" : "N");
 333           ss << (areIntegersUsed() ? "I" : "");
 334           ss << (areRealsUsed() ? "R" : "");
 335           ss << "A";
 336           ss << (areTranscendentalsUsed() ? "T" : "");
 337         }
 338         ++seen;
 339       }
 340       if(d_theories[THEORY_SETS]) {
 341         ss << "FS";
 342         ++seen;
 343       }
 344       if (d_theories[THEORY_BAGS])
 345       {
 346         ss << "FB";
 347         ++seen;
 348       }
 349       if(seen != d_sharingTheories) {
 350         Unhandled()
 351             << "can't extract a logic string from LogicInfo; at least one "
 352                "active theory is unknown to LogicInfo::getLogicString() !";
 353       }
 354
 355       if(seen == 0) {
 356         ss << "SAT";
 357       }
 358     }
 359     d_logicString = ss.str();
 360   }
 361   return d_logicString;
 362 }
 363
 364 void LogicInfo::setLogicString(std::string logicString)
 365 {
 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
 370   }
 371   d_sharingTheories = 0;
 372
 373   // Below, ONLY use enableTheory()/disableTheory() rather than
 374   // accessing d_theories[] directly.  This makes sure to set up
 375   // sharing properly.
 376
 377   enableTheory(THEORY_BUILTIN);
 378   enableTheory(THEORY_BOOL);
 379
 380   const char* p = logicString.c_str();
 381   if (!strncmp(p, "HO_", 3))
 382   {
 383     enableHigherOrder();
 384     p += 3;
 385   }
 386   if(*p == '\0') {
 387     // propositional logic only; we're done.
 388   } else if(!strcmp(p, "QF_SAT")) {
 389     // propositional logic only; we're done.
 390     p += 6;
 391   } else if(!strcmp(p, "SAT")) {
 392     // quantified Boolean formulas only; we're done.
 393     enableQuantifiers();
 394     p += 3;
 395   } else if(!strcmp(p, "QF_ALL")) {
 396     // the "all theories included" logic, no quantifiers.
 397     enableEverything(d_higherOrder);
 398     disableQuantifiers();
 399     arithNonLinear();
 400     p += 6;
 401   } else if(!strcmp(p, "ALL")) {
 402     // the "all theories included" logic, with quantifiers.
 403     enableEverything(d_higherOrder);
 404     enableQuantifiers();
 405     arithNonLinear();
 406     p += 3;
 407   }
 408   else if (!strcmp(p, "HORN"))
 409   {
 410     // the HORN logic
 411     enableEverything(d_higherOrder);
 412     enableQuantifiers();
 413     arithNonLinear();
 414     p += 4;
 415   } else {
 416     if(!strncmp(p, "QF_", 3)) {
 417       disableQuantifiers();
 418       p += 3;
 419     } else {
 420       enableQuantifiers();
 421     }
 422     if (!strncmp(p, "SEP_", 4))
 423     {
 424       enableSeparationLogic();
 425       p += 4;
 426     }
 427     if(!strncmp(p, "AX", 2)) {
 428       enableTheory(THEORY_ARRAYS);
 429       p += 2;
 430     } else {
 431       if(*p == 'A') {
 432         enableTheory(THEORY_ARRAYS);
 433         ++p;
 434       }
 435       if(!strncmp(p, "UF", 2)) {
 436         enableTheory(THEORY_UF);
 437         p += 2;
 438       }
 439       if(!strncmp(p, "C", 1 )) {
 440         d_cardinalityConstraints = true;
 441         p += 1;
 442       }
 443       // allow BV or DT in either order
 444       if(!strncmp(p, "BV", 2)) {
 445         enableTheory(THEORY_BV);
 446         p += 2;
 447       }
 448       if(!strncmp(p, "FP", 2)) {
 449         enableTheory(THEORY_FP);
 450         p += 2;
 451       }
 452       if(!strncmp(p, "DT", 2)) {
 453         enableTheory(THEORY_DATATYPES);
 454         p += 2;
 455       }
 456       if(!d_theories[THEORY_BV] && !strncmp(p, "BV", 2)) {
 457         enableTheory(THEORY_BV);
 458         p += 2;
 459       }
 460       if(*p == 'S') {
 461         enableTheory(THEORY_STRINGS);
 462         ++p;
 463       }
 464       if(!strncmp(p, "IDL", 3)) {
 465         enableIntegers();
 466         disableReals();
 467         arithOnlyDifference();
 468         p += 3;
 469       } else if(!strncmp(p, "RDL", 3)) {
 470         disableIntegers();
 471         enableReals();
 472         arithOnlyDifference();
 473         p += 3;
 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.
 477         enableIntegers();
 478         enableReals();
 479         arithOnlyDifference();
 480         p += 4;
 481       } else if(!strncmp(p, "LIA", 3)) {
 482         enableIntegers();
 483         disableReals();
 484         arithOnlyLinear();
 485         p += 3;
 486       } else if(!strncmp(p, "LRA", 3)) {
 487         disableIntegers();
 488         enableReals();
 489         arithOnlyLinear();
 490         p += 3;
 491       } else if(!strncmp(p, "LIRA", 4)) {
 492         enableIntegers();
 493         enableReals();
 494         arithOnlyLinear();
 495         p += 4;
 496       } else if(!strncmp(p, "NIA", 3)) {
 497         enableIntegers();
 498         disableReals();
 499         arithNonLinear();
 500         p += 3;
 501       } else if(!strncmp(p, "NRA", 3)) {
 502         disableIntegers();
 503         enableReals();
 504         arithNonLinear();
 505         p += 3;
 506         if (*p == 'T')
 507         {
 508           arithTranscendentals();
 509           p += 1;
 510         }
 511       } else if(!strncmp(p, "NIRA", 4)) {
 512         enableIntegers();
 513         enableReals();
 514         arithNonLinear();
 515         p += 4;
 516         if (*p == 'T')
 517         {
 518           arithTranscendentals();
 519           p += 1;
 520         }
 521       }
 522       if(!strncmp(p, "FS", 2)) {
 523         enableTheory(THEORY_SETS);
 524         p += 2;
 525       }
 526     }
 527   }
 528
 529   if (d_theories[THEORY_FP])
 530   {
 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);
 536   }
 537
 538   if(*p != '\0') {
 539     stringstream err;
 540     err << "LogicInfo::setLogicString(): ";
 541     if(p == logicString) {
 542       err << "cannot parse logic string: " << logicString;
 543     } else {
 544       err << "junk (\"" << p << "\") at end of logic string: " << logicString;
 545     }
 546     IllegalArgument(logicString, err.str().c_str());
 547   }
 548
 549   // ensure a getLogic() returns the same thing as was set
 550   d_logicString = logicString;
 551 }
 552
 553 void LogicInfo::enableEverything(bool enableHigherOrder)
 554 {
 555   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 556   *this = LogicInfo();
 557   this->d_higherOrder = enableHigherOrder;
 558 }
 559
 560 void LogicInfo::disableEverything() {
 561   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 562   *this = LogicInfo("");
 563 }
 564
 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)) {
 569       ++d_sharingTheories;
 570     }
 571     d_logicString = "";
 572     d_theories[theory] = true;
 573   }
 574 }
 575
 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);
 581       --d_sharingTheories;
 582     }
 583     if(theory == THEORY_BUILTIN ||
 584        theory == THEORY_BOOL) {
 585       return;
 586     }
 587     d_logicString = "";
 588     d_theories[theory] = false;
 589   }
 590 }
 591
 592 void LogicInfo::enableSygus()
 593 {
 594   enableQuantifiers();
 595   enableTheory(THEORY_UF);
 596   enableTheory(THEORY_DATATYPES);
 597   enableIntegers();
 598 }
 599
 600 void LogicInfo::enableSeparationLogic()
 601 {
 602   enableTheory(THEORY_SEP);
 603   enableTheory(THEORY_UF);
 604   enableTheory(THEORY_SETS);
 605 }
 606
 607 void LogicInfo::enableIntegers() {
 608   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 609   d_logicString = "";
 610   enableTheory(THEORY_ARITH);
 611   d_integers = true;
 612 }
 613
 614 void LogicInfo::disableIntegers() {
 615   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 616   d_logicString = "";
 617   d_integers = false;
 618   if(!d_reals) {
 619     disableTheory(THEORY_ARITH);
 620   }
 621 }
 622
 623 void LogicInfo::enableReals() {
 624   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 625   d_logicString = "";
 626   enableTheory(THEORY_ARITH);
 627   d_reals = true;
 628 }
 629
 630 void LogicInfo::disableReals() {
 631   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 632   d_logicString = "";
 633   d_reals = false;
 634   if(!d_integers) {
 635     disableTheory(THEORY_ARITH);
 636   }
 637 }
 638
 639 void LogicInfo::arithTranscendentals()
 640 {
 641   PrettyCheckArgument(
 642       !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 643   d_logicString = "";
 644   d_transcendentals = true;
 645   if (!d_reals)
 646   {
 647     enableReals();
 648   }
 649   if (d_linear)
 650   {
 651     arithNonLinear();
 652   }
 653 }
 654
 655 void LogicInfo::arithOnlyDifference() {
 656   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 657   d_logicString = "";
 658   d_linear = true;
 659   d_differenceLogic = true;
 660   d_transcendentals = false;
 661 }
 662
 663 void LogicInfo::arithOnlyLinear() {
 664   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 665   d_logicString = "";
 666   d_linear = true;
 667   d_differenceLogic = false;
 668   d_transcendentals = false;
 669 }
 670
 671 void LogicInfo::arithNonLinear() {
 672   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 673   d_logicString = "";
 674   d_linear = false;
 675   d_differenceLogic = false;
 676 }
 677
 678 void LogicInfo::enableCardinalityConstraints()
 679 {
 680   PrettyCheckArgument(
 681       !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 682   d_logicString = "";
 683   d_cardinalityConstraints = true;
 684 }
 685
 686 void LogicInfo::disableCardinalityConstraints()
 687 {
 688   PrettyCheckArgument(
 689       !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 690   d_logicString = "";
 691   d_cardinalityConstraints = false;
 692 }
 693
 694 void LogicInfo::enableHigherOrder()
 695 {
 696   PrettyCheckArgument(
 697       !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 698   d_logicString = "";
 699   d_higherOrder = true;
 700 }
 701
 702 void LogicInfo::disableHigherOrder()
 703 {
 704   PrettyCheckArgument(
 705       !d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 706   d_logicString = "";
 707   d_higherOrder = false;
 708 }
 709
 710 LogicInfo LogicInfo::getUnlockedCopy() const {
 711   if(d_locked) {
 712     LogicInfo info = *this;
 713     info.d_locked = false;
 714     return info;
 715   } else {
 716     return *this;
 717   }
 718 }
 719
 720 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) {
 721   return out << logic.getLogicString();
 722 }
 723
 724 }  // namespace cvc5