src/theory/logic_info.h

   1 /*********************                                                        */
   2 /*! \file logic_info.h
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): Dejan Jovanovic, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** 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
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__LOGIC_INFO_H
  22 #define __CVC4__LOGIC_INFO_H
  23
  24 #include <string>
  25 #include <vector>
  26 #include "expr/kind.h"
  27 #include "options/logic_info_forward.h"
  28
  29 namespace CVC4 {
  30
  31 /**
  32  * A LogicInfo instance describes a collection of theory modules and some
  33  * basic configuration about them.  Conceptually, it provides a background
  34  * context for all operations in CVC4.  Typically, when CVC4's SmtEngine
  35  * is created, it is issued a setLogic() command indicating features of the
  36  * assertions and queries to follow---for example, whether quantifiers are
  37  * used, whether integers or reals (or both) will be used, etc.
  38  *
  39  * Most places in CVC4 will only ever need to access a const reference to an
  40  * instance of this class.  Such an instance is generally set by the SmtEngine
  41  * when setLogic() is called.  However, mutating member functions are also
  42  * provided by this class so that it can be used as a more general mechanism
  43  * (e.g., for communicating to the SmtEngine which theories should be used,
  44  * rather than having to provide an SMT-LIB string).
  45  */
  46 class CVC4_PUBLIC LogicInfo {
  47   mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
  48   std::vector<bool> d_theories; /**< set of active theories */
  49   size_t d_sharingTheories; /**< count of theories that need sharing */
  50
  51   // for arithmetic
  52   bool d_integers; /**< are integers used in this logic? */
  53   bool d_reals; /**< are reals used in this logic? */
  54   bool d_linear; /**< linear-only arithmetic in this logic? */
  55   bool d_differenceLogic; /**< difference-only arithmetic in this logic? */
  56   bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */
  57
  58   bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
  59
  60   /**
  61    * Returns true iff this is a "true" theory (one that must be worried
  62    * about for sharing
  63    */
  64   static inline bool isTrueTheory(theory::TheoryId theory) {
  65     switch(theory) {
  66     case theory::THEORY_BUILTIN:
  67     case theory::THEORY_BOOL:
  68     case theory::THEORY_QUANTIFIERS:
  69       return false;
  70     default:
  71       return true;
  72     }
  73   }
  74
  75 public:
  76
  77   /**
  78    * Constructs a LogicInfo for the most general logic (quantifiers, all
  79    * background theory modules, ...).
  80    */
  81   LogicInfo();
  82
  83   /**
  84    * Construct a LogicInfo from an SMT-LIB-like logic string.
  85    * Throws an IllegalArgumentException if the logic string cannot
  86    * be interpreted.
  87    */
  88   LogicInfo(std::string logicString) throw(IllegalArgumentException);
  89
  90   /**
  91    * Construct a LogicInfo from an SMT-LIB-like logic string.
  92    * Throws an IllegalArgumentException if the logic string cannot
  93    * be interpreted.
  94    */
  95   LogicInfo(const char* logicString) throw(IllegalArgumentException);
  96
  97   // ACCESSORS
  98
  99   /**
 100    * Get an SMT-LIB-like logic string.  These are only guaranteed to
 101    * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
 102    * the constructor and no mutating functions were called.
 103    */
 104   std::string getLogicString() const;
 105
 106   /** Is sharing enabled for this logic? */
 107   bool isSharingEnabled() const {
 108     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 109     return d_sharingTheories > 1;
 110   }
 111
 112   /** Is the given theory module active in this logic? */
 113   bool isTheoryEnabled(theory::TheoryId theory) const {
 114     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 115     return d_theories[theory];
 116   }
 117
 118   /** Is this a quantified logic? */
 119   bool isQuantified() const {
 120     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 121     return isTheoryEnabled(theory::THEORY_QUANTIFIERS);
 122   }
 123
 124   /** Is this the all-inclusive logic? */
 125   bool hasEverything() const {
 126     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 127     LogicInfo everything;
 128     everything.lock();
 129     return *this == everything;
 130   }
 131
 132   /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
 133   bool hasNothing() const {
 134     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 135     LogicInfo nothing("");
 136     nothing.lock();
 137     return *this == nothing;
 138   }
 139
 140   /**
 141    * Is this a pure logic (only one "true" background theory).  Quantifiers
 142    * can exist in such logics though; to test for quantifier-free purity,
 143    * use "isPure(theory) && !isQuantified()".
 144    */
 145   bool isPure(theory::TheoryId theory) const {
 146     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 147     // the third and fourth conjucts are really just to rule out the misleading
 148     // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
 149     return isTheoryEnabled(theory) && !isSharingEnabled() &&
 150       ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
 151       ( isTrueTheory(theory) || d_sharingTheories == 0 );
 152   }
 153
 154   // these are for arithmetic
 155
 156   /** Are integers in this logic? */
 157   bool areIntegersUsed() const {
 158     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 159     CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether integers are used");
 160     return d_integers;
 161   }
 162   /** Are reals in this logic? */
 163   bool areRealsUsed() const {
 164     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 165     CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether reals are used");
 166     return d_reals;
 167   }
 168   /** Does this logic only linear arithmetic? */
 169   bool isLinear() const {
 170     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 171     CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's linear");
 172     return d_linear || d_differenceLogic;
 173   }
 174   /** Does this logic only permit difference reasoning? (implies linear) */
 175   bool isDifferenceLogic() const {
 176     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 177     CheckArgument(isTheoryEnabled(theory::THEORY_ARITH), *this, "Arithmetic not used in this LogicInfo; cannot ask whether it's difference logic");
 178     return d_differenceLogic;
 179   }
 180   /** Does this logic allow cardinality constraints? */
 181   bool hasCardinalityConstraints() const {
 182     CheckArgument(d_locked, *this, "This LogicInfo isn't locked yet, and cannot be queried");
 183     return d_cardinalityConstraints;
 184   }
 185
 186   // MUTATORS
 187
 188   /**
 189    * Initialize the LogicInfo with an SMT-LIB-like logic string.
 190    * Throws an IllegalArgumentException if the string can't be
 191    * interpreted.
 192    */
 193   void setLogicString(std::string logicString) throw(IllegalArgumentException);
 194
 195   /**
 196    * Enable all functionality.  All theories, plus quantifiers, will be
 197    * enabled.
 198    */
 199   void enableEverything();
 200
 201   /**
 202    * Disable all functionality.  The result will be a LogicInfo with
 203    * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
 204    */
 205   void disableEverything();
 206
 207   /**
 208    * Enable the given theory module.
 209    */
 210   void enableTheory(theory::TheoryId theory);
 211
 212   /**
 213    * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
 214    * be disabled (and if given here, the request will be silently ignored).
 215    */
 216   void disableTheory(theory::TheoryId theory);
 217
 218   /**
 219    * Quantifiers are a special case, since two theory modules handle them.
 220    */
 221   void enableQuantifiers() {
 222     enableTheory(theory::THEORY_QUANTIFIERS);
 223   }
 224
 225   /**
 226    * Quantifiers are a special case, since two theory modules handle them.
 227    */
 228   void disableQuantifiers() {
 229     disableTheory(theory::THEORY_QUANTIFIERS);
 230   }
 231
 232   // these are for arithmetic
 233
 234   /** Enable the use of integers in this logic. */
 235   void enableIntegers();
 236   /** Disable the use of integers in this logic. */
 237   void disableIntegers();
 238   /** Enable the use of reals in this logic. */
 239   void enableReals();
 240   /** Disable the use of reals in this logic. */
 241   void disableReals();
 242   /** Only permit difference arithmetic in this logic. */
 243   void arithOnlyDifference();
 244   /** Only permit linear arithmetic in this logic. */
 245   void arithOnlyLinear();
 246   /** Permit nonlinear arithmetic in this logic. */
 247   void arithNonLinear();
 248
 249   // LOCKING FUNCTIONALITY
 250
 251   /** Lock this LogicInfo, disabling further mutation and allowing queries */
 252   void lock() { d_locked = true; }
 253   /** Check whether this LogicInfo is locked, disallowing further mutation */
 254   bool isLocked() const { return d_locked; }
 255   /** Get a copy of this LogicInfo that is identical, but unlocked */
 256   LogicInfo getUnlockedCopy() const;
 257
 258   // COMPARISON
 259
 260   /** Are these two LogicInfos equal? */
 261   bool operator==(const LogicInfo& other) const {
 262     CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
 263     for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 264       if(d_theories[id] != other.d_theories[id]) {
 265         return false;
 266       }
 267     }
 268     CheckArgument(d_sharingTheories == other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
 269     if(isTheoryEnabled(theory::THEORY_ARITH)) {
 270       return
 271         d_integers == other.d_integers &&
 272         d_reals == other.d_reals &&
 273         d_linear == other.d_linear &&
 274         d_differenceLogic == other.d_differenceLogic;
 275     } else {
 276       return true;
 277     }
 278   }
 279   /** Are these two LogicInfos disequal? */
 280   bool operator!=(const LogicInfo& other) const {
 281     return !(*this == other);
 282   }
 283   /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
 284   bool operator>(const LogicInfo& other) const {
 285     return *this >= other && *this != other;
 286   }
 287   /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
 288   bool operator<(const LogicInfo& other) const {
 289     return *this <= other && *this != other;
 290   }
 291   /** Is this LogicInfo "less than or equal" the other? */
 292   bool operator<=(const LogicInfo& other) const {
 293     CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
 294     for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 295       if(d_theories[id] && !other.d_theories[id]) {
 296         return false;
 297       }
 298     }
 299     CheckArgument(d_sharingTheories <= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
 300     if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
 301       return
 302         (!d_integers || other.d_integers) &&
 303         (!d_reals || other.d_reals) &&
 304         (d_linear || !other.d_linear) &&
 305         (d_differenceLogic || !other.d_differenceLogic);
 306     } else {
 307       return true;
 308     }
 309   }
 310   /** Is this LogicInfo "greater than or equal" the other? */
 311   bool operator>=(const LogicInfo& other) const {
 312     CheckArgument(isLocked() && other.isLocked(), *this, "This LogicInfo isn't locked yet, and cannot be queried");
 313     for(theory::TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
 314       if(!d_theories[id] && other.d_theories[id]) {
 315         return false;
 316       }
 317     }
 318     CheckArgument(d_sharingTheories >= other.d_sharingTheories, *this, "LogicInfo internal inconsistency");
 319     if(isTheoryEnabled(theory::THEORY_ARITH) && other.isTheoryEnabled(theory::THEORY_ARITH)) {
 320       return
 321         (d_integers || !other.d_integers) &&
 322         (d_reals || !other.d_reals) &&
 323         (!d_linear || other.d_linear) &&
 324         (!d_differenceLogic || other.d_differenceLogic);
 325     } else {
 326       return true;
 327     }
 328   }
 329
 330   /** Are two LogicInfos comparable?  That is, is one of <= or > true? */
 331   bool isComparableTo(const LogicInfo& other) const {
 332     return *this <= other || *this >= other;
 333   }
 334
 335 };/* class LogicInfo */
 336
 337 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC;
 338
 339 }/* CVC4 namespace */
 340
 341 #endif /* __CVC4__LOGIC_INFO_H */