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   /**
  58    * Returns true iff this is a "true" theory (one that must be worried
  59    * about for sharing
  60    */
  61   static inline bool isTrueTheory(theory::TheoryId theory) {
  62     switch(theory) {
  63     case theory::THEORY_BUILTIN:
  64     case theory::THEORY_BOOL:
  65     case theory::THEORY_QUANTIFIERS:
  66     case theory::THEORY_REWRITERULES:
  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   // ACCESSORS
  89
  90   /**
  91    * Get an SMT-LIB-like logic string.  These are only guaranteed to
  92    * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
  93    * the constructor and no mutating functions were called.
  94    */
  95   std::string getLogicString() const;
  96
  97   /** Is sharing enabled for this logic? */
  98   bool isSharingEnabled() const { return d_sharingTheories > 1; }
  99   /** Is the given theory module active in this logic? */
 100   bool isTheoryEnabled(theory::TheoryId theory) const { return d_theories[theory]; }
 101
 102   /** Is this a quantified logic? */
 103   bool isQuantified() const {
 104     return isTheoryEnabled(theory::THEORY_QUANTIFIERS) || isTheoryEnabled(theory::THEORY_REWRITERULES);
 105   }
 106
 107   /**
 108    * Is this a pure logic (only one "true" background theory).  Quantifiers
 109    * can exist in such logics though; to test for quantifier-free purity,
 110    * use "isPure(theory) && !isQuantified()".
 111    */
 112   bool isPure(theory::TheoryId theory) const {
 113     // the third conjuct is really just to rule out the misleading case where you ask
 114     // isPure(THEORY_BOOL) and get true even in e.g. QF_LIA
 115     return isTheoryEnabled(theory) && !isSharingEnabled() &&
 116       ( !isTrueTheory(theory) || d_sharingTheories == 1 );
 117   }
 118
 119   // these are for arithmetic
 120
 121   /** Are integers in this logic? */
 122   bool areIntegersUsed() const { return d_integers; }
 123   /** Are reals in this logic? */
 124   bool areRealsUsed() const { return d_reals; }
 125   /** Does this logic only linear arithmetic? */
 126   bool isLinear() const { return d_linear || d_differenceLogic; }
 127   /** Does this logic only permit difference reasoning? (implies linear) */
 128   bool isDifferenceLogic() const { return d_differenceLogic; }
 129
 130   // MUTATORS
 131
 132   /**
 133    * Initialize the LogicInfo with an SMT-LIB-like logic string.
 134    * Throws an IllegalArgumentException if the string can't be
 135    * interpreted.
 136    */
 137   void setLogicString(std::string logicString) throw(IllegalArgumentException);
 138
 139   /**
 140    * Enable the given theory module.
 141    */
 142   void enableTheory(theory::TheoryId theory);
 143
 144   /**
 145    * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
 146    * be disabled (and if given here, the request will be silently ignored).
 147    */
 148   void disableTheory(theory::TheoryId theory);
 149
 150   /**
 151    * Quantifiers are a special case, since two theory modules handle them.
 152    */
 153   void enableQuantifiers() {
 154     enableTheory(theory::THEORY_QUANTIFIERS);
 155     enableTheory(theory::THEORY_REWRITERULES);
 156   }
 157
 158   /**
 159    * Quantifiers are a special case, since two theory modules handle them.
 160    */
 161   void disableQuantifiers() {
 162     disableTheory(theory::THEORY_QUANTIFIERS);
 163     disableTheory(theory::THEORY_REWRITERULES);
 164   }
 165
 166   // these are for arithmetic
 167
 168   /** Enable the use of integers in this logic. */
 169   void enableIntegers();
 170   /** Disable the use of integers in this logic. */
 171   void disableIntegers();
 172   /** Enable the use of reals in this logic. */
 173   void enableReals();
 174   /** Disable the use of reals in this logic. */
 175   void disableReals();
 176   /** Only permit difference arithmetic in this logic. */
 177   void arithOnlyDifference();
 178   /** Only permit linear arithmetic in this logic. */
 179   void arithOnlyLinear();
 180   /** Permit nonlinear arithmetic in this logic. */
 181   void arithNonLinear();
 182
 183 };/* class LogicInfo */
 184
 185 }/* CVC4 namespace */
 186
 187 #endif /* __CVC4__LOGIC_INFO_H */
 188