src/theory/logic_info.cpp

   1 /*********************                                                        */
   2 /*! \file logic_info.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009--2012  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief A class giving information about a logic (group a theory modules
  15  ** and configuration information)
  16  **
  17  ** A class giving information about a logic (group of theory modules and
  18  ** configuration information).
  19  **/
  20
  21 #include <string>
  22 #include <cstring>
  23 #include <sstream>
  24
  25 #include "expr/kind.h"
  26 #include "theory/logic_info.h"
  27 #include "util/Assert.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(),
  37   d_sharingTheories(0),
  38   d_integers(true),
  39   d_reals(true),
  40   d_linear(false) {
  41
  42   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
  43     d_theories[id] = false;// ensure it's cleared
  44     enableTheory(id);
  45   }
  46 }
  47
  48 LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
  49   d_logicString(""),
  50   d_theories(),
  51   d_sharingTheories(0),
  52   d_integers(false),
  53   d_reals(false),
  54   d_linear(false) {
  55   setLogicString(logicString);
  56 }
  57
  58 std::string LogicInfo::getLogicString() const {
  59   if(d_logicString == "") {
  60     size_t seen = 0; // make sure we support all the active theories
  61
  62     stringstream ss;
  63     if(!isQuantified()) {
  64       ss << "QF_";
  65     }
  66     if(d_theories[THEORY_ARRAY]) {
  67       ss << (d_sharingTheories == 1 ? "AX" : "A");
  68       ++seen;
  69     }
  70     if(d_theories[THEORY_UF]) {
  71       ss << "UF";
  72       ++seen;
  73     }
  74     if(d_theories[THEORY_BV]) {
  75       ss << "BV";
  76       ++seen;
  77     }
  78     if(d_theories[THEORY_DATATYPES]) {
  79       ss << "DT";
  80       ++seen;
  81     }
  82     if(d_theories[THEORY_ARITH]) {
  83       if(isDifferenceLogic()) {
  84         ss << (areIntegersUsed() ? "I" : "");
  85         ss << (areRealsUsed() ? "R" : "");
  86         ss << "DL";
  87       } else {
  88         ss << (isLinear() ? "L" : "N");
  89         ss << (areIntegersUsed() ? "I" : "");
  90         ss << (areRealsUsed() ? "R" : "");
  91         ss << "A";
  92       }
  93       ++seen;
  94     }
  95
  96     if(seen != d_sharingTheories) {
  97       Unhandled("can't extract a logic string from LogicInfo; at least one "
  98                 "active theory is unknown to LogicInfo::getLogicString() !");
  99     }
 100
 101     if(seen == 0) {
 102       ss << "SAT";
 103     }
 104
 105     d_logicString = ss.str();
 106   }
 107   return d_logicString;
 108 }
 109
 110 void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentException) {
 111   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
 112     d_theories[id] = false;// ensure it's cleared
 113   }
 114   d_sharingTheories = 0;
 115
 116   // Below, ONLY use enableTheory()/disableTheory() rather than
 117   // accessing d_theories[] directly.  This makes sure to set up
 118   // sharing properly.
 119
 120   enableTheory(THEORY_BUILTIN);
 121   enableTheory(THEORY_BOOL);
 122
 123   const char* p = logicString.c_str();
 124   if(!strcmp(p, "QF_SAT") || *p == '\0') {
 125     // propositional logic only; we're done.
 126     p += 6;
 127   } else {
 128     if(!strncmp(p, "QF_", 3)) {
 129       disableQuantifiers();
 130       p += 3;
 131     } else {
 132       enableQuantifiers();
 133     }
 134     if(!strncmp(p, "AX", 2)) {
 135       enableTheory(THEORY_ARRAY);
 136       p += 2;
 137     } else {
 138       if(*p == 'A') {
 139         enableTheory(THEORY_ARRAY);
 140         ++p;
 141       }
 142       if(!strncmp(p, "UF", 2)) {
 143         enableTheory(THEORY_UF);
 144         p += 2;
 145       }
 146       if(!strncmp(p, "BV", 2)) {
 147         enableTheory(THEORY_BV);
 148         p += 2;
 149       }
 150       if(!strncmp(p, "DT", 2)) {
 151         enableTheory(THEORY_DATATYPES);
 152         p += 2;
 153       }
 154       if(!strncmp(p, "IDL", 3)) {
 155         enableIntegers();
 156         disableReals();
 157         arithOnlyDifference();
 158         p += 3;
 159       } else if(!strncmp(p, "RDL", 3)) {
 160         disableIntegers();
 161         enableReals();
 162         arithOnlyDifference();
 163         p += 3;
 164       } else if(!strncmp(p, "IRDL", 4)) {
 165         // "IRDL" ?! --not very useful, but getLogicString() can produce
 166         // that string, so we really had better be able to read it back in.
 167         enableIntegers();
 168         enableReals();
 169         arithOnlyDifference();
 170         p += 4;
 171       } else if(!strncmp(p, "LIA", 3)) {
 172         enableIntegers();
 173         disableReals();
 174         arithOnlyLinear();
 175         p += 3;
 176       } else if(!strncmp(p, "LRA", 3)) {
 177         disableIntegers();
 178         enableReals();
 179         arithOnlyLinear();
 180         p += 3;
 181       } else if(!strncmp(p, "LIRA", 4)) {
 182         enableIntegers();
 183         enableReals();
 184         arithOnlyLinear();
 185         p += 4;
 186       } else if(!strncmp(p, "NIA", 3)) {
 187         enableIntegers();
 188         disableReals();
 189         arithNonLinear();
 190         p += 3;
 191       } else if(!strncmp(p, "NRA", 3)) {
 192         disableIntegers();
 193         enableReals();
 194         arithNonLinear();
 195         p += 3;
 196       } else if(!strncmp(p, "NIRA", 4)) {
 197         enableIntegers();
 198         enableReals();
 199         arithNonLinear();
 200         p += 4;
 201       }
 202     }
 203   }
 204   if(*p != '\0') {
 205     stringstream err;
 206     err << "LogicInfo::setLogicString(): junk (\"" << p << "\") at end of logic string: " << logicString;
 207     IllegalArgument(logicString, err.str().c_str());
 208   }
 209
 210   // ensure a getLogic() returns the same thing as was set
 211   d_logicString = logicString;
 212 }
 213
 214 void LogicInfo::enableTheory(theory::TheoryId theory) {
 215   if(!d_theories[theory]) {
 216     if(isTrueTheory(theory)) {
 217       ++d_sharingTheories;
 218     }
 219     d_logicString = "";
 220     d_theories[theory] = true;
 221   }
 222 }
 223
 224 void LogicInfo::disableTheory(theory::TheoryId theory) {
 225   if(d_theories[theory]) {
 226     if(isTrueTheory(theory)) {
 227       Assert(d_sharingTheories > 0);
 228       --d_sharingTheories;
 229     }
 230     if(theory == THEORY_BUILTIN ||
 231        theory == THEORY_BOOL) {
 232       return;
 233     }
 234     d_logicString = "";
 235     d_theories[theory] = false;
 236   }
 237 }
 238
 239 void LogicInfo::enableIntegers() {
 240   d_logicString = "";
 241   enableTheory(THEORY_ARITH);
 242   d_integers = true;
 243 }
 244
 245 void LogicInfo::disableIntegers() {
 246   d_logicString = "";
 247   d_integers = false;
 248   if(!d_reals) {
 249     disableTheory(THEORY_ARITH);
 250   }
 251 }
 252
 253 void LogicInfo::enableReals() {
 254   d_logicString = "";
 255   enableTheory(THEORY_ARITH);
 256   d_reals = true;
 257 }
 258
 259 void LogicInfo::disableReals() {
 260   d_logicString = "";
 261   d_reals = false;
 262   if(!d_integers) {
 263     disableTheory(THEORY_ARITH);
 264   }
 265 }
 266
 267 void LogicInfo::arithOnlyDifference() {
 268   d_logicString = "";
 269   d_linear = true;
 270   d_differenceLogic = true;
 271 }
 272
 273 void LogicInfo::arithOnlyLinear() {
 274   d_logicString = "";
 275   d_linear = true;
 276   d_differenceLogic = false;
 277 }
 278
 279 void LogicInfo::arithNonLinear() {
 280   d_logicString = "";
 281   d_linear = false;
 282   d_differenceLogic = false;
 283 }
 284
 285 }/* CVC4 namespace */