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-2016 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 <string>
  21 #include <cstring>
  22 #include <sstream>
  23
  24 #include "base/cvc4_assert.h"
  25 #include "expr/kind.h"
  26
  27
  28 using namespace std;
  29 using namespace CVC4::theory;
  30
  31 namespace CVC4 {
  32
  33 LogicInfo::LogicInfo() :
  34   d_logicString(""),
  35   d_theories(THEORY_LAST, false),
  36   d_sharingTheories(0),
  37   d_integers(true),
  38   d_reals(true),
  39   d_linear(true),// for now, "everything enabled" doesn't include non-linear arith
  40   d_differenceLogic(false),
  41   d_cardinalityConstraints(false),
  42   d_locked(false) {
  43
  44   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
  45     enableTheory(id);
  46   }
  47 }
  48
  49 LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
  50   d_logicString(""),
  51   d_theories(THEORY_LAST, false),
  52   d_sharingTheories(0),
  53   d_integers(false),
  54   d_reals(false),
  55   d_linear(false),
  56   d_differenceLogic(false),
  57   d_cardinalityConstraints(false),
  58   d_locked(false) {
  59
  60   setLogicString(logicString);
  61   lock();
  62 }
  63
  64 LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) :
  65   d_logicString(""),
  66   d_theories(THEORY_LAST, false),
  67   d_sharingTheories(0),
  68   d_integers(false),
  69   d_reals(false),
  70   d_linear(false),
  71   d_differenceLogic(false),
  72   d_cardinalityConstraints(false),
  73   d_locked(false) {
  74
  75   setLogicString(logicString);
  76   lock();
  77 }
  78
  79 /** Is sharing enabled for this logic? */
  80 bool LogicInfo::isSharingEnabled() const {
  81   PrettyCheckArgument(d_locked, *this,
  82                       "This LogicInfo isn't locked yet, and cannot be queried");
  83   return d_sharingTheories > 1;
  84 }
  85
  86
  87 /** Is the given theory module active in this logic? */
  88 bool LogicInfo::isTheoryEnabled(theory::TheoryId theory) const {
  89   PrettyCheckArgument(d_locked, *this,
  90                       "This LogicInfo isn't locked yet, and cannot be queried");
  91   return d_theories[theory];
  92 }
  93
  94 /** Is this a quantified logic? */
  95 bool LogicInfo::isQuantified() const {
  96   PrettyCheckArgument(d_locked, *this,
  97                       "This LogicInfo isn't locked yet, and cannot be queried");
  98   return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
  99 }
 100
 101 /** Is this the all-inclusive logic? */
 102 bool LogicInfo::hasEverything() const {
 103   PrettyCheckArgument(d_locked, *this,
 104                       "This LogicInfo isn't locked yet, and cannot be queried");
 105   LogicInfo everything;
 106   everything.lock();
 107   return *this == everything;
 108 }
 109
 110 /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
 111 bool LogicInfo::hasNothing() const {
 112   PrettyCheckArgument(d_locked, *this,
 113                       "This LogicInfo isn't locked yet, and cannot be queried");
 114   LogicInfo nothing("");
 115   nothing.lock();
 116   return *this == nothing;
 117 }
 118
 119 bool LogicInfo::isPure(theory::TheoryId theory) const {
 120   PrettyCheckArgument(d_locked, *this,
 121                       "This LogicInfo isn't locked yet, and cannot be queried");
 122   // the third and fourth conjucts are really just to rule out the misleading
 123   // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
 124   return isTheoryEnabled(theory) && !isSharingEnabled() &&
 125       ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
 126       ( isTrueTheory(theory) || d_sharingTheories == 0 );
 127 }
 128
 129 bool LogicInfo::areIntegersUsed() const {
 130   PrettyCheckArgument(d_locked, *this,
 131                       "This LogicInfo isn't locked yet, and cannot be queried");
 132   PrettyCheckArgument(
 133       isTheoryEnabled(theory::THEORY_ARITH), *this,
 134       "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
 135   return d_integers;
 136 }
 137
 138 bool LogicInfo::areRealsUsed() const {
 139   PrettyCheckArgument(d_locked, *this,
 140                       "This LogicInfo isn't locked yet, and cannot be queried");
 141   PrettyCheckArgument(
 142       isTheoryEnabled(theory::THEORY_ARITH), *this,
 143       "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
 144   return d_reals;
 145 }
 146
 147 bool LogicInfo::isLinear() const {
 148   PrettyCheckArgument(d_locked, *this,
 149                       "This LogicInfo isn't locked yet, and cannot be queried");
 150   PrettyCheckArgument(
 151       isTheoryEnabled(theory::THEORY_ARITH), *this,
 152       "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
 153   return d_linear || d_differenceLogic;
 154 }
 155
 156 bool LogicInfo::isDifferenceLogic() const {
 157   PrettyCheckArgument(d_locked, *this,
 158                       "This LogicInfo isn't locked yet, and cannot be queried");
 159   PrettyCheckArgument(
 160       isTheoryEnabled(theory::THEORY_ARITH), *this,
 161       "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
 162   return d_differenceLogic;
 163 }
 164
 165 bool LogicInfo::hasCardinalityConstraints() const {
 166   PrettyCheckArgument(d_locked, *this,
 167                       "This LogicInfo isn't locked yet, and cannot be queried");
 168   return d_cardinalityConstraints;
 169 }
 170
 171
 172 bool LogicInfo::operator==(const LogicInfo& other) const {
 173   PrettyCheckArgument(isLocked() && other.isLocked(), *this,
 174                       "This LogicInfo isn't locked yet, and cannot be queried");
 175   for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 176     if(d_theories[id] != other.d_theories[id]) {
 177       return false;
 178     }
 179   }
 180
 181   PrettyCheckArgument(d_sharingTheories == other.d_sharingTheories, *this,
 182                       "LogicInfo internal inconsistency");
 183   if(isTheoryEnabled(theory::THEORY_ARITH)) {
 184     return
 185         d_integers == other.d_integers &&
 186         d_reals == other.d_reals &&
 187         d_linear == other.d_linear &&
 188         d_differenceLogic == other.d_differenceLogic;
 189   } else {
 190     return true;
 191   }
 192 }
 193
 194 bool LogicInfo::operator<=(const LogicInfo& other) const {
 195   PrettyCheckArgument(isLocked() && other.isLocked(), *this,
 196                       "This LogicInfo isn't locked yet, and cannot be queried");
 197   for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 198     if(d_theories[id] && !other.d_theories[id]) {
 199       return false;
 200     }
 201   }
 202   PrettyCheckArgument(d_sharingTheories <= other.d_sharingTheories, *this,
 203                       "LogicInfo internal inconsistency");
 204   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
 205     return
 206         (!d_integers || other.d_integers) &&
 207         (!d_reals || other.d_reals) &&
 208         (d_linear || !other.d_linear) &&
 209         (d_differenceLogic || !other.d_differenceLogic);
 210   } else {
 211     return true;
 212   }
 213 }
 214
 215 bool LogicInfo::operator>=(const LogicInfo& other) const {
 216   PrettyCheckArgument(isLocked() && other.isLocked(), *this,
 217                       "This LogicInfo isn't locked yet, and cannot be queried");
 218   for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 219     if(!d_theories[id] && other.d_theories[id]) {
 220       return false;
 221     }
 222   }
 223   PrettyCheckArgument(d_sharingTheories >= other.d_sharingTheories, *this,
 224                       "LogicInfo internal inconsistency");
 225   if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
 226     return
 227         (d_integers || !other.d_integers) &&
 228         (d_reals || !other.d_reals) &&
 229         (!d_linear || other.d_linear) &&
 230         (!d_differenceLogic || other.d_differenceLogic);
 231     } else {
 232     return true;
 233   }
 234 }
 235
 236 std::string LogicInfo::getLogicString() const {
 237   PrettyCheckArgument(
 238       d_locked, *this,
 239       "This LogicInfo isn't locked yet, and cannot be queried");
 240   if(d_logicString == "") {
 241     LogicInfo qf_all_supported;
 242     qf_all_supported.disableQuantifiers();
 243     qf_all_supported.lock();
 244     if(hasEverything()) {
 245       d_logicString = "ALL";
 246     } else if(*this == qf_all_supported) {
 247       d_logicString = "QF_ALL";
 248     } else {
 249       size_t seen = 0; // make sure we support all the active theories
 250
 251       stringstream ss;
 252       if(!isQuantified()) {
 253         ss << "QF_";
 254       }
 255       if(d_theories[THEORY_ARRAY]) {
 256         ss << (d_sharingTheories == 1 ? "AX" : "A");
 257         ++seen;
 258       }
 259       if(d_theories[THEORY_UF]) {
 260         ss << "UF";
 261         ++seen;
 262       }
 263       if( d_cardinalityConstraints ){
 264         ss << "C";
 265       }
 266       if(d_theories[THEORY_BV]) {
 267         ss << "BV";
 268         ++seen;
 269       }
 270       if(d_theories[THEORY_FP]) {
 271         ss << "FP";
 272         ++seen;
 273       }
 274       if(d_theories[THEORY_DATATYPES]) {
 275         ss << "DT";
 276         ++seen;
 277       }
 278       if(d_theories[THEORY_STRINGS]) {
 279         ss << "S";
 280         ++seen;
 281       }
 282       if(d_theories[THEORY_ARITH]) {
 283         if(isDifferenceLogic()) {
 284           ss << (areIntegersUsed() ? "I" : "");
 285           ss << (areRealsUsed() ? "R" : "");
 286           ss << "DL";
 287         } else {
 288           ss << (isLinear() ? "L" : "N");
 289           ss << (areIntegersUsed() ? "I" : "");
 290           ss << (areRealsUsed() ? "R" : "");
 291           ss << "A";
 292         }
 293         ++seen;
 294       }
 295       if(d_theories[THEORY_SETS]) {
 296         ss << "FS";
 297         ++seen;
 298       }
 299       if(d_theories[THEORY_SEP]) {
 300         ss << "SEP";
 301         ++seen;
 302       }
 303       if(seen != d_sharingTheories) {
 304         Unhandled("can't extract a logic string from LogicInfo; at least one "
 305                   "active theory is unknown to LogicInfo::getLogicString() !");
 306       }
 307
 308       if(seen == 0) {
 309         ss << "SAT";
 310       }
 311
 312       d_logicString = ss.str();
 313     }
 314   }
 315   return d_logicString;
 316 }
 317
 318 void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
 319   PrettyCheckArgument(!d_locked, *this,
 320                       "This LogicInfo is locked, and cannot be modified");
 321   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
 322     d_theories[id] = false;// ensure it's cleared
 323   }
 324   d_sharingTheories = 0;
 325
 326   // Below, ONLY use enableTheory()/disableTheory() rather than
 327   // accessing d_theories[] directly.  This makes sure to set up
 328   // sharing properly.
 329
 330   enableTheory(THEORY_BUILTIN);
 331   enableTheory(THEORY_BOOL);
 332
 333   const char* p = logicString.c_str();
 334   if(*p == '\0') {
 335     // propositional logic only; we're done.
 336   } else if(!strcmp(p, "QF_SAT")) {
 337     // propositional logic only; we're done.
 338     p += 6;
 339   } else if(!strcmp(p, "QF_ALL_SUPPORTED")) {
 340     // the "all theories included" logic, no quantifiers
 341     enableEverything();
 342     disableQuantifiers();
 343     p += 16;
 344   } else if(!strcmp(p, "QF_ALL")) {
 345     // the "all theories included" logic, no quantifiers
 346     enableEverything();
 347     disableQuantifiers();
 348     p += 6;
 349   } else if(!strcmp(p, "ALL_SUPPORTED")) {
 350     // the "all theories included" logic, with quantifiers
 351     enableEverything();
 352     enableQuantifiers();
 353     p += 13;
 354   } else if(!strcmp(p, "ALL")) {
 355     // the "all theories included" logic, with quantifiers
 356     enableEverything();
 357     enableQuantifiers();
 358     p += 3;
 359   } else {
 360     if(!strncmp(p, "QF_", 3)) {
 361       disableQuantifiers();
 362       p += 3;
 363     } else {
 364       enableQuantifiers();
 365     }
 366     if(!strncmp(p, "AX", 2)) {
 367       enableTheory(THEORY_ARRAY);
 368       p += 2;
 369     } else {
 370       if(*p == 'A') {
 371         enableTheory(THEORY_ARRAY);
 372         ++p;
 373       }
 374       if(!strncmp(p, "UF", 2)) {
 375         enableTheory(THEORY_UF);
 376         p += 2;
 377       }
 378       if(!strncmp(p, "C", 1 )) {
 379         d_cardinalityConstraints = true;
 380         p += 1;
 381       }
 382       // allow BV or DT in either order
 383       if(!strncmp(p, "BV", 2)) {
 384         enableTheory(THEORY_BV);
 385         p += 2;
 386       }
 387       if(!strncmp(p, "FP", 2)) {
 388         enableTheory(THEORY_FP);
 389         p += 2;
 390       }
 391       if(!strncmp(p, "DT", 2)) {
 392         enableTheory(THEORY_DATATYPES);
 393         p += 2;
 394       }
 395       if(!d_theories[THEORY_BV] && !strncmp(p, "BV", 2)) {
 396         enableTheory(THEORY_BV);
 397         p += 2;
 398       }
 399       if(*p == 'S') {
 400         enableTheory(THEORY_STRINGS);
 401         ++p;
 402       }
 403       if(!strncmp(p, "IDL", 3)) {
 404         enableIntegers();
 405         disableReals();
 406         arithOnlyDifference();
 407         p += 3;
 408       } else if(!strncmp(p, "RDL", 3)) {
 409         disableIntegers();
 410         enableReals();
 411         arithOnlyDifference();
 412         p += 3;
 413       } else if(!strncmp(p, "IRDL", 4)) {
 414         // "IRDL" ?! --not very useful, but getLogicString() can produce
 415         // that string, so we really had better be able to read it back in.
 416         enableIntegers();
 417         enableReals();
 418         arithOnlyDifference();
 419         p += 4;
 420       } else if(!strncmp(p, "LIA", 3)) {
 421         enableIntegers();
 422         disableReals();
 423         arithOnlyLinear();
 424         p += 3;
 425       } else if(!strncmp(p, "LRA", 3)) {
 426         disableIntegers();
 427         enableReals();
 428         arithOnlyLinear();
 429         p += 3;
 430       } else if(!strncmp(p, "LIRA", 4)) {
 431         enableIntegers();
 432         enableReals();
 433         arithOnlyLinear();
 434         p += 4;
 435       } else if(!strncmp(p, "NIA", 3)) {
 436         enableIntegers();
 437         disableReals();
 438         arithNonLinear();
 439         p += 3;
 440       } else if(!strncmp(p, "NRA", 3)) {
 441         disableIntegers();
 442         enableReals();
 443         arithNonLinear();
 444         p += 3;
 445       } else if(!strncmp(p, "NIRA", 4)) {
 446         enableIntegers();
 447         enableReals();
 448         arithNonLinear();
 449         p += 4;
 450       }
 451       if(!strncmp(p, "FS", 2)) {
 452         enableTheory(THEORY_SETS);
 453         p += 2;
 454       }
 455       if(!strncmp(p, "SEP", 3)) {
 456         enableTheory(THEORY_SEP);
 457         p += 3;
 458       }
 459     }
 460   }
 461   if(*p != '\0') {
 462     stringstream err;
 463     err << "LogicInfo::setLogicString(): ";
 464     if(p == logicString) {
 465       err << "cannot parse logic string: " << logicString;
 466     } else {
 467       err << "junk (\"" << p << "\") at end of logic string: " << logicString;
 468     }
 469     IllegalArgument(logicString, err.str().c_str());
 470   }
 471
 472   // ensure a getLogic() returns the same thing as was set
 473   d_logicString = logicString;
 474 }
 475
 476 void LogicInfo::enableEverything() {
 477   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 478   *this = LogicInfo();
 479 }
 480
 481 void LogicInfo::disableEverything() {
 482   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 483   *this = LogicInfo("");
 484 }
 485
 486 void LogicInfo::enableTheory(theory::TheoryId theory) {
 487   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 488   if(!d_theories[theory]) {
 489     if(isTrueTheory(theory)) {
 490       ++d_sharingTheories;
 491     }
 492     d_logicString = "";
 493     d_theories[theory] = true;
 494   }
 495 }
 496
 497 void LogicInfo::disableTheory(theory::TheoryId theory) {
 498   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 499   if(d_theories[theory]) {
 500     if(isTrueTheory(theory)) {
 501       Assert(d_sharingTheories > 0);
 502       --d_sharingTheories;
 503     }
 504     if(theory == THEORY_BUILTIN ||
 505        theory == THEORY_BOOL) {
 506       return;
 507     }
 508     d_logicString = "";
 509     d_theories[theory] = false;
 510   }
 511 }
 512
 513 void LogicInfo::enableIntegers() {
 514   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 515   d_logicString = "";
 516   enableTheory(THEORY_ARITH);
 517   d_integers = true;
 518 }
 519
 520 void LogicInfo::disableIntegers() {
 521   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 522   d_logicString = "";
 523   d_integers = false;
 524   if(!d_reals) {
 525     disableTheory(THEORY_ARITH);
 526   }
 527 }
 528
 529 void LogicInfo::enableReals() {
 530   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 531   d_logicString = "";
 532   enableTheory(THEORY_ARITH);
 533   d_reals = true;
 534 }
 535
 536 void LogicInfo::disableReals() {
 537   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 538   d_logicString = "";
 539   d_reals = false;
 540   if(!d_integers) {
 541     disableTheory(THEORY_ARITH);
 542   }
 543 }
 544
 545 void LogicInfo::arithOnlyDifference() {
 546   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 547   d_logicString = "";
 548   d_linear = true;
 549   d_differenceLogic = true;
 550 }
 551
 552 void LogicInfo::arithOnlyLinear() {
 553   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 554   d_logicString = "";
 555   d_linear = true;
 556   d_differenceLogic = false;
 557 }
 558
 559 void LogicInfo::arithNonLinear() {
 560   PrettyCheckArgument(!d_locked, *this, "This LogicInfo is locked, and cannot be modified");
 561   d_logicString = "";
 562   d_linear = false;
 563   d_differenceLogic = false;
 564 }
 565
 566 LogicInfo LogicInfo::getUnlockedCopy() const {
 567   if(d_locked) {
 568     LogicInfo info = *this;
 569     info.d_locked = false;
 570     return info;
 571   } else {
 572     return *this;
 573   }
 574 }
 575
 576 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) {
 577   return out << logic.getLogicString();
 578 }
 579
 580 }/* CVC4 namespace */