src/theory/logic_info.h

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