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