src/theory/logic_info.h

   1 /*********************                                                        */
   2 /*! \file logic_info.h
   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 "cvc4_public.h"
  22
  23 #ifndef __CVC4__LOGIC_INFO_H
  24 #define __CVC4__LOGIC_INFO_H
  25
  26 #include <string>
  27 #include "expr/kind.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 LogicInfo {
  47   mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
  48   bool d_theories[theory::THEORY_LAST]; /**< 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
  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     case theory::THEORY_REWRITERULES:
  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   // ACCESSORS
  91
  92   /**
  93    * Get an SMT-LIB-like logic string.  These are only guaranteed to
  94    * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
  95    * the constructor and no mutating functions were called.
  96    */
  97   std::string getLogicString() const;
  98
  99   /** Is sharing enabled for this logic? */
 100   bool isSharingEnabled() const {
 101     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 102     return d_sharingTheories > 1;
 103   }
 104   /** Is the given theory module active in this logic? */
 105   bool isTheoryEnabled(theory::TheoryId theory) const {
 106     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 107     return d_theories[theory];
 108   }
 109
 110   /** Is this a quantified logic? */
 111   bool isQuantified() const {
 112     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 113     return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
 114   }
 115
 116   /**
 117    * Is this a pure logic (only one "true" background theory).  Quantifiers
 118    * can exist in such logics though; to test for quantifier-free purity,
 119    * use "isPure(theory) && !isQuantified()".
 120    */
 121   bool isPure(theory::TheoryId theory) const {
 122     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 123     // the third and fourth conjucts are really just to rule out the misleading
 124     // case where you ask isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
 125     return isTheoryEnabled(theory) && !isSharingEnabled() &&
 126       ( !isTrueTheory(theory) || d_sharingTheories == 1 ) &&
 127       ( isTrueTheory(theory) || d_sharingTheories == 0 );
 128   }
 129
 130   // these are for arithmetic
 131
 132   /** Are integers in this logic? */
 133   bool areIntegersUsed() const {
 134     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 135     return d_integers;
 136   }
 137   /** Are reals in this logic? */
 138   bool areRealsUsed() const {
 139     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 140     return d_reals;
 141   }
 142   /** Does this logic only linear arithmetic? */
 143   bool isLinear() const {
 144     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 145     return d_linear || d_differenceLogic;
 146   }
 147   /** Does this logic only permit difference reasoning? (implies linear) */
 148   bool isDifferenceLogic() const {
 149     Assert(d_locked, "This LogicInfo isn't locked yet, and cannot be queried");
 150     return d_differenceLogic;
 151   }
 152
 153   // MUTATORS
 154
 155   /**
 156    * Initialize the LogicInfo with an SMT-LIB-like logic string.
 157    * Throws an IllegalArgumentException if the string can't be
 158    * interpreted.
 159    */
 160   void setLogicString(std::string logicString) throw(IllegalArgumentException);
 161
 162   /**
 163    * Enable all functionality.  All theories, plus quantifiers, will be
 164    * enabled.
 165    */
 166   void enableEverything();
 167
 168   /**
 169    * Disable all functionality.  The result will be a LogicInfo with
 170    * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
 171    */
 172   void disableEverything();
 173
 174   /**
 175    * Enable the given theory module.
 176    */
 177   void enableTheory(theory::TheoryId theory);
 178
 179   /**
 180    * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
 181    * be disabled (and if given here, the request will be silently ignored).
 182    */
 183   void disableTheory(theory::TheoryId theory);
 184
 185   /**
 186    * Quantifiers are a special case, since two theory modules handle them.
 187    */
 188   void enableQuantifiers() {
 189     enableTheory(theory::THEORY_QUANTIFIERS);
 190     enableTheory(theory::THEORY_REWRITERULES);
 191   }
 192
 193   /**
 194    * Quantifiers are a special case, since two theory modules handle them.
 195    */
 196   void disableQuantifiers() {
 197     disableTheory(theory::THEORY_QUANTIFIERS);
 198     disableTheory(theory::THEORY_REWRITERULES);
 199   }
 200
 201   // these are for arithmetic
 202
 203   /** Enable the use of integers in this logic. */
 204   void enableIntegers();
 205   /** Disable the use of integers in this logic. */
 206   void disableIntegers();
 207   /** Enable the use of reals in this logic. */
 208   void enableReals();
 209   /** Disable the use of reals in this logic. */
 210   void disableReals();
 211   /** Only permit difference arithmetic in this logic. */
 212   void arithOnlyDifference();
 213   /** Only permit linear arithmetic in this logic. */
 214   void arithOnlyLinear();
 215   /** Permit nonlinear arithmetic in this logic. */
 216   void arithNonLinear();
 217
 218   // LOCKING FUNCTIONALITY
 219
 220   /** Lock this LogicInfo, disabling further mutation and allowing queries */
 221   void lock() { d_locked = true; }
 222   /** Check whether this LogicInfo is locked, disallowing further mutation */
 223   bool isLocked() const { return d_locked; }
 224   /** Get a copy of this LogicInfo that is identical, but unlocked */
 225   LogicInfo getUnlockedCopy() const;
 226
 227 };/* class LogicInfo */
 228
 229 }/* CVC4 namespace */
 230
 231 #endif /* __CVC4__LOGIC_INFO_H */
 232