src/theory/logic_info.h

   1 /*********************                                                        */
   2 /*! \file logic_info.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Tim King, Dejan Jovanovic
   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
  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   bool d_cardinalityConstraints; /**< cardinality constraints in this logic? */
  56
  57   bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
  58
  59   /**
  60    * Returns true iff this is a "true" theory (one that must be worried
  61    * about for sharing
  62    */
  63   static inline bool isTrueTheory(theory::TheoryId theory) {
  64     switch(theory) {
  65     case theory::THEORY_BUILTIN:
  66     case theory::THEORY_BOOL:
  67     case theory::THEORY_QUANTIFIERS:
  68       return false;
  69     default:
  70       return true;
  71     }
  72   }
  73
  74 public:
  75
  76   /**
  77    * Constructs a LogicInfo for the most general logic (quantifiers, all
  78    * background theory modules, ...).
  79    */
  80   LogicInfo();
  81
  82   /**
  83    * Construct a LogicInfo from an SMT-LIB-like logic string.
  84    * Throws an IllegalArgumentException if the logic string cannot
  85    * be interpreted.
  86    */
  87   LogicInfo(std::string logicString) throw(IllegalArgumentException);
  88
  89   /**
  90    * Construct a LogicInfo from an SMT-LIB-like logic string.
  91    * Throws an IllegalArgumentException if the logic string cannot
  92    * be interpreted.
  93    */
  94   LogicInfo(const char* logicString) throw(IllegalArgumentException);
  95
  96   // ACCESSORS
  97
  98   /**
  99    * Get an SMT-LIB-like logic string.  These are only guaranteed to
 100    * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
 101    * the constructor and no mutating functions were called.
 102    */
 103   std::string getLogicString() const;
 104
 105   /** Is sharing enabled for this logic? */
 106   bool isSharingEnabled() const;
 107
 108   /** Is the given theory module active in this logic? */
 109   bool isTheoryEnabled(theory::TheoryId theory) const;
 110
 111   /** Is this a quantified logic? */
 112   bool isQuantified() const;
 113
 114   /** Is this the all-inclusive logic? */
 115   bool hasEverything() const;
 116
 117   /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
 118   bool hasNothing() const;
 119
 120   /**
 121    * Is this a pure logic (only one "true" background theory).  Quantifiers
 122    * can exist in such logics though; to test for quantifier-free purity,
 123    * use "isPure(theory) && !isQuantified()".
 124    */
 125   bool isPure(theory::TheoryId theory) const;
 126
 127   // these are for arithmetic
 128
 129   /** Are integers in this logic? */
 130   bool areIntegersUsed() const;
 131
 132   /** Are reals in this logic? */
 133   bool areRealsUsed() const;
 134
 135   /** Does this logic only linear arithmetic? */
 136   bool isLinear() const;
 137
 138   /** Does this logic only permit difference reasoning? (implies linear) */
 139   bool isDifferenceLogic() const;
 140
 141   /** Does this logic allow cardinality constraints? */
 142   bool hasCardinalityConstraints() const;
 143
 144   // MUTATORS
 145
 146   /**
 147    * Initialize the LogicInfo with an SMT-LIB-like logic string.
 148    * Throws an IllegalArgumentException if the string can't be
 149    * interpreted.
 150    */
 151   void setLogicString(std::string logicString) throw(IllegalArgumentException);
 152
 153   /**
 154    * Enable all functionality.  All theories, plus quantifiers, will be
 155    * enabled.
 156    */
 157   void enableEverything();
 158
 159   /**
 160    * Disable all functionality.  The result will be a LogicInfo with
 161    * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
 162    */
 163   void disableEverything();
 164
 165   /**
 166    * Enable the given theory module.
 167    */
 168   void enableTheory(theory::TheoryId theory);
 169
 170   /**
 171    * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
 172    * be disabled (and if given here, the request will be silently ignored).
 173    */
 174   void disableTheory(theory::TheoryId theory);
 175
 176   /**
 177    * Quantifiers are a special case, since two theory modules handle them.
 178    */
 179   void enableQuantifiers() {
 180     enableTheory(theory::THEORY_QUANTIFIERS);
 181   }
 182
 183   /**
 184    * Quantifiers are a special case, since two theory modules handle them.
 185    */
 186   void disableQuantifiers() {
 187     disableTheory(theory::THEORY_QUANTIFIERS);
 188   }
 189
 190   // these are for arithmetic
 191
 192   /** Enable the use of integers in this logic. */
 193   void enableIntegers();
 194   /** Disable the use of integers in this logic. */
 195   void disableIntegers();
 196   /** Enable the use of reals in this logic. */
 197   void enableReals();
 198   /** Disable the use of reals in this logic. */
 199   void disableReals();
 200   /** Only permit difference arithmetic in this logic. */
 201   void arithOnlyDifference();
 202   /** Only permit linear arithmetic in this logic. */
 203   void arithOnlyLinear();
 204   /** Permit nonlinear arithmetic in this logic. */
 205   void arithNonLinear();
 206
 207   // LOCKING FUNCTIONALITY
 208
 209   /** Lock this LogicInfo, disabling further mutation and allowing queries */
 210   void lock() { d_locked = true; }
 211   /** Check whether this LogicInfo is locked, disallowing further mutation */
 212   bool isLocked() const { return d_locked; }
 213   /** Get a copy of this LogicInfo that is identical, but unlocked */
 214   LogicInfo getUnlockedCopy() const;
 215
 216   // COMPARISON
 217
 218   /** Are these two LogicInfos equal? */
 219   bool operator==(const LogicInfo& other) const;
 220
 221   /** Are these two LogicInfos disequal? */
 222   bool operator!=(const LogicInfo& other) const {
 223     return !(*this == other);
 224   }
 225
 226   /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
 227   bool operator>(const LogicInfo& other) const {
 228     return *this >= other && *this != other;
 229   }
 230
 231   /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
 232   bool operator<(const LogicInfo& other) const {
 233     return *this <= other && *this != other;
 234   }
 235   /** Is this LogicInfo "less than or equal" the other? */
 236   bool operator<=(const LogicInfo& other) const;
 237
 238   /** Is this LogicInfo "greater than or equal" the other? */
 239   bool operator>=(const LogicInfo& other) const;
 240
 241   /** Are two LogicInfos comparable?  That is, is one of <= or > true? */
 242   bool isComparableTo(const LogicInfo& other) const {
 243     return *this <= other || *this >= other;
 244   }
 245
 246 };/* class LogicInfo */
 247
 248 std::ostream& operator<<(std::ostream& out, const LogicInfo& logic) CVC4_PUBLIC;
 249
 250 }/* CVC4 namespace */
 251
 252 #endif /* __CVC4__LOGIC_INFO_H */