src/theory/logic_info.cpp

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