src/theory/theory_id.h

   1 /*********************                                                        */
   2 /*! \file theory_id.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Aina Niemetz, Dejan Jovanovic
   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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "cvc4_public.h"
  19
  20 #ifndef CVC4__THEORY__THEORY_ID_H
  21 #define CVC4__THEORY__THEORY_ID_H
  22
  23 #include <iostream>
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /**
  29  * IMPORTANT: The order of the theories is important. For example, strings
  30  *            depends on arith, quantifiers needs to come as the very last.
  31  *            Do not change this order.
  32  */
  33 enum TheoryId
  34 {
  35   THEORY_BUILTIN,
  36   THEORY_BOOL,
  37   THEORY_UF,
  38   THEORY_ARITH,
  39   THEORY_BV,
  40   THEORY_FP,
  41   THEORY_ARRAYS,
  42   THEORY_DATATYPES,
  43   THEORY_SEP,
  44   THEORY_SETS,
  45   THEORY_BAGS,
  46   THEORY_STRINGS,
  47   THEORY_QUANTIFIERS,
  48
  49   THEORY_LAST
  50 };
  51
  52 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
  53 const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
  54
  55 TheoryId& operator++(TheoryId& id) CVC4_PUBLIC;
  56
  57 std::ostream& operator<<(std::ostream& out, TheoryId theoryId);
  58
  59 std::string getStatsPrefix(TheoryId theoryId) CVC4_PUBLIC;
  60
  61 /**
  62  * A set of theories. Utilities for TheoryIdSet can be found below.
  63  */
  64 typedef uint32_t TheoryIdSet;
  65
  66 class TheoryIdSetUtil
  67 {
  68  public:
  69   /** A set of all theories */
  70   static const TheoryIdSet AllTheories = (1 << theory::THEORY_LAST) - 1;
  71
  72   /** Pops a first theory off the set */
  73   static TheoryId setPop(TheoryIdSet& set);
  74
  75   /** Returns the size of a set of theories */
  76   static size_t setSize(TheoryIdSet set);
  77
  78   /** Returns the index size of a set of theories */
  79   static size_t setIndex(TheoryId id, TheoryIdSet set);
  80
  81   /** Add the theory to the set. If no set specified, just returns a singleton
  82    * set */
  83   static TheoryIdSet setInsert(TheoryId theory, TheoryIdSet set = 0);
  84
  85   /** Add the theory to the set. If no set specified, just returns a singleton
  86    * set */
  87   static TheoryIdSet setRemove(TheoryId theory, TheoryIdSet set = 0);
  88
  89   /** Check if the set contains the theory */
  90   static bool setContains(TheoryId theory, TheoryIdSet set);
  91
  92   /** Set complement of a */
  93   static TheoryIdSet setComplement(TheoryIdSet a);
  94
  95   /** Set intersection of a and b */
  96   static TheoryIdSet setIntersection(TheoryIdSet a, TheoryIdSet b);
  97
  98   /** Set union of a and b */
  99   static TheoryIdSet setUnion(TheoryIdSet a, TheoryIdSet b);
 100
 101   /** Set difference of a and b */
 102   static TheoryIdSet setDifference(TheoryIdSet a, TheoryIdSet b);
 103
 104   /** Convert theorySet to string (for debugging) */
 105   static std::string setToString(TheoryIdSet theorySet);
 106 };
 107
 108 }  // namespace theory
 109 }  // namespace CVC4
 110 #endif