Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Morgan Deters, Andrew Reynolds, Tim King
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * A class giving information about a logic (group of theory modules and
      14                 :            :  * configuration information).
      15                 :            :  */
      16                 :            : 
      17                 :            : #include "cvc5_public.h"
      18                 :            : 
      19                 :            : #ifndef CVC5__LOGIC_INFO_H
      20                 :            : #define CVC5__LOGIC_INFO_H
      21                 :            : 
      22                 :            : #include <cvc5/cvc5_export.h>
      23                 :            : 
      24                 :            : #include <string>
      25                 :            : #include <vector>
      26                 :            : 
      27                 :            : #include "theory/theory_id.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      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 cvc5.  Typically, when cvc5's SolverEngine
      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 cvc5 will only ever need to access a const reference to an
      40                 :            :  * instance of this class.  Such an instance is generally set by the
      41                 :            :  * SolverEngine when setLogic() is called.  However, mutating member functions
      42                 :            :  * are also provided by this class so that it can be used as a more general
      43                 :            :  * mechanism (e.g., for communicating to the SolverEngine which theories should
      44                 :            :  * be used, rather than having to provide an SMT-LIB string).
      45                 :            :  */
      46                 :            : class CVC5_EXPORT LogicInfo
      47                 :            : {
      48                 :            :   mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
      49                 :            :   std::vector<bool> d_theories; /**< set of active theories */
      50                 :            :   size_t d_sharingTheories; /**< count of theories that need sharing */
      51                 :            : 
      52                 :            :   /** are integers used in this logic? */
      53                 :            :   bool d_integers;
      54                 :            :   /** are reals used in this logic? */
      55                 :            :   bool d_reals;
      56                 :            :   /** transcendentals in this logic? */
      57                 :            :   bool d_transcendentals;
      58                 :            :   /** linear-only arithmetic in this logic? */
      59                 :            :   bool d_linear;
      60                 :            :   /** difference-only arithmetic in this logic? */
      61                 :            :   bool d_differenceLogic;
      62                 :            :   /** cardinality constraints in this logic? */
      63                 :            :   bool d_cardinalityConstraints;
      64                 :            :   /** higher-order constraints in this logic? */
      65                 :            :   bool d_higherOrder;
      66                 :            : 
      67                 :            :   bool d_locked; /**< is this LogicInfo instance locked (and thus immutable)? */
      68                 :            : 
      69                 :            :   /**
      70                 :            :    * Returns true iff this is a "true" theory (one that must be worried
      71                 :            :    * about for sharing
      72                 :            :    */
      73                 :    5516400 :   static inline bool isTrueTheory(theory::TheoryId theory) {
      74         [ +  + ]:    5516400 :     switch(theory) {
      75                 :    1311760 :     case theory::THEORY_BUILTIN:
      76                 :            :     case theory::THEORY_BOOL:
      77                 :            :     case theory::THEORY_QUANTIFIERS:
      78                 :    1311760 :       return false;
      79                 :    4204640 :     default:
      80                 :    4204640 :       return true;
      81                 :            :     }
      82                 :            :   }
      83                 :            : 
      84                 :            : public:
      85                 :            : 
      86                 :            :   /**
      87                 :            :    * Constructs a LogicInfo for the most general logic (quantifiers, all
      88                 :            :    * background theory modules, ...).
      89                 :            :    */
      90                 :            :   LogicInfo();
      91                 :            : 
      92                 :            :   /**
      93                 :            :    * Construct a LogicInfo from an SMT-LIB-like logic string.
      94                 :            :    * Throws an IllegalArgumentException if the logic string cannot
      95                 :            :    * be interpreted.
      96                 :            :    */
      97                 :            :   LogicInfo(std::string logicString);
      98                 :            : 
      99                 :            :   /**
     100                 :            :    * Construct a LogicInfo from an SMT-LIB-like logic string.
     101                 :            :    * Throws an IllegalArgumentException if the logic string cannot
     102                 :            :    * be interpreted.
     103                 :            :    */
     104                 :            :   LogicInfo(const char* logicString);
     105                 :            : 
     106                 :            :   // ACCESSORS
     107                 :            : 
     108                 :            :   /**
     109                 :            :    * Get an SMT-LIB-like logic string.  These are only guaranteed to
     110                 :            :    * be SMT-LIB-compliant if an SMT-LIB-compliant string was used in
     111                 :            :    * the constructor and no mutating functions were called.
     112                 :            :    */
     113                 :            :   std::string getLogicString() const;
     114                 :            : 
     115                 :            :   /** Is sharing enabled for this logic? */
     116                 :            :   bool isSharingEnabled() const;
     117                 :            : 
     118                 :            :   /** Is the given theory module active in this logic? */
     119                 :            :   bool isTheoryEnabled(theory::TheoryId theory) const;
     120                 :            : 
     121                 :            :   /** Is this a quantified logic? */
     122                 :            :   bool isQuantified() const;
     123                 :            : 
     124                 :            :   /** Is this a logic that includes the all-inclusive logic?
     125                 :            :    *
     126                 :            :    * @return Yields true if the logic corresponds to "ALL" or its super
     127                 :            :    * set including , such as "HO_ALL".
     128                 :            :    */
     129                 :            :   bool hasEverything() const;
     130                 :            : 
     131                 :            :   /** Is this the all-exclusive logic?  (Here, that means propositional logic) */
     132                 :            :   bool hasNothing() const;
     133                 :            : 
     134                 :            :   /**
     135                 :            :    * Is this a pure logic (only one "true" background theory).  Quantifiers
     136                 :            :    * can exist in such logics though; to test for quantifier-free purity,
     137                 :            :    * use "isPure(theory) && !isQuantified()".
     138                 :            :    */
     139                 :            :   bool isPure(theory::TheoryId theory) const;
     140                 :            : 
     141                 :            :   // these are for arithmetic
     142                 :            : 
     143                 :            :   /** Are integers in this logic? */
     144                 :            :   bool areIntegersUsed() const;
     145                 :            : 
     146                 :            :   /** Are reals in this logic? */
     147                 :            :   bool areRealsUsed() const;
     148                 :            : 
     149                 :            :   /** Are transcendentals in this logic? */
     150                 :            :   bool areTranscendentalsUsed() const;
     151                 :            : 
     152                 :            :   /** Does this logic only linear arithmetic? */
     153                 :            :   bool isLinear() const;
     154                 :            : 
     155                 :            :   /** Does this logic only permit difference reasoning? (implies linear) */
     156                 :            :   bool isDifferenceLogic() const;
     157                 :            : 
     158                 :            :   /** Does this logic allow cardinality constraints? */
     159                 :            :   bool hasCardinalityConstraints() const;
     160                 :            : 
     161                 :            :   /** Is this a higher order logic? */
     162                 :            :   bool isHigherOrder() const;
     163                 :            : 
     164                 :            :   // MUTATORS
     165                 :            : 
     166                 :            :   /**
     167                 :            :    * Initialize the LogicInfo with an SMT-LIB-like logic string.
     168                 :            :    * Throws an IllegalArgumentException if the string can't be
     169                 :            :    * interpreted.
     170                 :            :    */
     171                 :            :   void setLogicString(std::string logicString);
     172                 :            : 
     173                 :            :   /**
     174                 :            :    * Enable all functionality.  All theories, plus quantifiers, will be
     175                 :            :    * enabled.
     176                 :            :    *
     177                 :            :    * @param enableHigherOrder Whether HOL should be enable together with the
     178                 :            :    * above.
     179                 :            :    */
     180                 :            :   void enableEverything(bool enableHigherOrder = false);
     181                 :            : 
     182                 :            :   /**
     183                 :            :    * Disable all functionality.  The result will be a LogicInfo with
     184                 :            :    * the BUILTIN and BOOLEAN theories enabled only ("QF_SAT").
     185                 :            :    */
     186                 :            :   void disableEverything();
     187                 :            : 
     188                 :            :   /**
     189                 :            :    * Enable the given theory module.
     190                 :            :    */
     191                 :            :   void enableTheory(theory::TheoryId theory);
     192                 :            : 
     193                 :            :   /**
     194                 :            :    * Disable the given theory module.  THEORY_BUILTIN and THEORY_BOOL cannot
     195                 :            :    * be disabled (and if given here, the request will be silently ignored).
     196                 :            :    */
     197                 :            :   void disableTheory(theory::TheoryId theory);
     198                 :            : 
     199                 :            :   /**
     200                 :            :    * Quantifiers are a special case, since two theory modules handle them.
     201                 :            :    */
     202                 :      36589 :   void enableQuantifiers() {
     203                 :      36589 :     enableTheory(theory::THEORY_QUANTIFIERS);
     204                 :      36589 :   }
     205                 :            : 
     206                 :            :   /**
     207                 :            :    * Quantifiers are a special case, since two theory modules handle them.
     208                 :            :    */
     209                 :      72816 :   void disableQuantifiers() {
     210                 :      72816 :     disableTheory(theory::THEORY_QUANTIFIERS);
     211                 :      72815 :   }
     212                 :            : 
     213                 :            :   /**
     214                 :            :    * Enable everything that is needed for sygus with respect to this logic info.
     215                 :            :    * This means enabling quantifiers, datatypes, UF, integers, and higher order.
     216                 :            :    */
     217                 :            :   void enableSygus();
     218                 :            :   /**
     219                 :            :    * Enable everything that is needed for separation logic. This means enabling
     220                 :            :    * the theories of separation logic, UF and sets.
     221                 :            :    */
     222                 :            :   void enableSeparationLogic();
     223                 :            : 
     224                 :            :   // these are for arithmetic
     225                 :            : 
     226                 :            :   /** Enable the use of integers in this logic. */
     227                 :            :   void enableIntegers();
     228                 :            :   /** Disable the use of integers in this logic. */
     229                 :            :   void disableIntegers();
     230                 :            :   /** Enable the use of reals in this logic. */
     231                 :            :   void enableReals();
     232                 :            :   /** Disable the use of reals in this logic. */
     233                 :            :   void disableReals();
     234                 :            :   /** Enable the use of transcendentals in this logic. */
     235                 :            :   void arithTranscendentals();
     236                 :            :   /** Only permit difference arithmetic in this logic. */
     237                 :            :   void arithOnlyDifference();
     238                 :            :   /** Only permit linear arithmetic in this logic. */
     239                 :            :   void arithOnlyLinear();
     240                 :            :   /** Permit nonlinear arithmetic in this logic. */
     241                 :            :   void arithNonLinear();
     242                 :            : 
     243                 :            :   // for cardinality constraints
     244                 :            : 
     245                 :            :   /** Enable the use of cardinality constraints in this logic. */
     246                 :            :   void enableCardinalityConstraints();
     247                 :            :   /** Disable the use of cardinality constraints in this logic. */
     248                 :            :   void disableCardinalityConstraints();
     249                 :            : 
     250                 :            :   // for higher-order
     251                 :            : 
     252                 :            :   /** Enable the use of higher-order in this logic. */
     253                 :            :   void enableHigherOrder();
     254                 :            :   /** Disable the use of higher-order in this logic. */
     255                 :            :   void disableHigherOrder();
     256                 :            : 
     257                 :            :   // LOCKING FUNCTIONALITY
     258                 :            : 
     259                 :            :   /** Lock this LogicInfo, disabling further mutation and allowing queries */
     260                 :     362542 :   void lock() { d_locked = true; }
     261                 :            :   /** Check whether this LogicInfo is locked, disallowing further mutation */
     262                 :     399194 :   bool isLocked() const { return d_locked; }
     263                 :            :   /** Get a copy of this LogicInfo that is identical, but unlocked */
     264                 :            :   LogicInfo getUnlockedCopy() const;
     265                 :            : 
     266                 :            :   // COMPARISON
     267                 :            : 
     268                 :            :   /** Are these two LogicInfos equal? */
     269                 :            :   bool operator==(const LogicInfo& other) const;
     270                 :            : 
     271                 :            :   /** Are these two LogicInfos disequal? */
     272                 :       1708 :   bool operator!=(const LogicInfo& other) const {
     273                 :       1708 :     return !(*this == other);
     274                 :            :   }
     275                 :            : 
     276                 :            :   /** Is this LogicInfo "greater than" (does it contain everything and more) the other? */
     277                 :       1174 :   bool operator>(const LogicInfo& other) const {
     278 [ +  + ][ +  + ]:       1174 :     return *this >= other && *this != other;
     279                 :            :   }
     280                 :            : 
     281                 :            :   /** Is this LogicInfo "less than" (does it contain strictly less) the other? */
     282                 :       1174 :   bool operator<(const LogicInfo& other) const {
     283 [ +  + ][ +  + ]:       1174 :     return *this <= other && *this != other;
     284                 :            :   }
     285                 :            :   /** Is this LogicInfo "less than or equal" the other? */
     286                 :            :   bool operator<=(const LogicInfo& other) const;
     287                 :            : 
     288                 :            :   /** Is this LogicInfo "greater than or equal" the other? */
     289                 :            :   bool operator>=(const LogicInfo& other) const;
     290                 :            : 
     291                 :            :   /** Are two LogicInfos comparable?  That is, is one of <= or > true? */
     292                 :       1174 :   bool isComparableTo(const LogicInfo& other) const {
     293 [ +  + ][ +  + ]:       1174 :     return *this <= other || *this >= other;
     294                 :            :   }
     295                 :            : 
     296                 :            :  private:
     297                 :            :   /**
     298                 :            :    * Checks if the given theory has already been registered.
     299                 :            :    * If the theory is found to be a duplicate, throws an Exception
     300                 :            :    * indicating that the theory with the provided ID is already registered.
     301                 :            :    *
     302                 :            :    * @param theory The identifier of the theory to be checked.
     303                 :            :    * @param id The ID string associated with the theory for error reporting.
     304                 :            :    * @throws cvc5::internal::Exception if the theory is already registered.
     305                 :            :    */
     306                 :            :   void checkDuplicateTheory(theory::TheoryId theory, const char* id);
     307                 :            : 
     308                 :            : }; /* class LogicInfo */
     309                 :            : 
     310                 :            : std::ostream& operator<<(std::ostream& out, const LogicInfo& logic);
     311                 :            : 
     312                 :            : }  // namespace cvc5::internal
     313                 :            : 
     314                 :            : #endif /* CVC5__LOGIC_INFO_H */