src/theory/theory_id.cpp

   1 /*********************                                                        */
   2 /*! \file theory_id.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Aina Niemetz, 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 [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "theory/theory_id.h"
  19
  20 #include "base/check.h"
  21 #include "lib/ffs.h"
  22
  23 namespace CVC4 {
  24 namespace theory {
  25
  26 TheoryId& operator++(TheoryId& id)
  27 {
  28   return id = static_cast<TheoryId>(static_cast<int>(id) + 1);
  29 }
  30
  31 std::ostream& operator<<(std::ostream& out, TheoryId theoryId)
  32 {
  33   switch (theoryId)
  34   {
  35     case THEORY_BUILTIN: out << "THEORY_BUILTIN"; break;
  36     case THEORY_BOOL: out << "THEORY_BOOL"; break;
  37     case THEORY_UF: out << "THEORY_UF"; break;
  38     case THEORY_ARITH: out << "THEORY_ARITH"; break;
  39     case THEORY_BV: out << "THEORY_BV"; break;
  40     case THEORY_FP: out << "THEORY_FP"; break;
  41     case THEORY_ARRAYS: out << "THEORY_ARRAYS"; break;
  42     case THEORY_DATATYPES: out << "THEORY_DATATYPES"; break;
  43     case THEORY_SAT_SOLVER: out << "THEORY_SAT_SOLVER"; break;
  44     case THEORY_SEP: out << "THEORY_SEP"; break;
  45     case THEORY_SETS: out << "THEORY_SETS"; break;
  46     case THEORY_BAGS: out << "THEORY_BAGS"; break;
  47     case THEORY_STRINGS: out << "THEORY_STRINGS"; break;
  48     case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
  49
  50     default: out << "UNKNOWN_THEORY"; break;
  51   }
  52   return out;
  53 }
  54
  55 std::string getStatsPrefix(TheoryId theoryId)
  56 {
  57   switch (theoryId)
  58   {
  59     case THEORY_BUILTIN: return "theory::builtin"; break;
  60     case THEORY_BOOL: return "theory::bool"; break;
  61     case THEORY_UF: return "theory::uf"; break;
  62     case THEORY_ARITH: return "theory::arith"; break;
  63     case THEORY_BV: return "theory::bv"; break;
  64     case THEORY_FP: return "theory::fp"; break;
  65     case THEORY_ARRAYS: return "theory::arrays"; break;
  66     case THEORY_DATATYPES: return "theory::datatypes"; break;
  67     case THEORY_SEP: return "theory::sep"; break;
  68     case THEORY_SETS: return "theory::sets"; break;
  69     case THEORY_BAGS: return "theory::bags"; break;
  70     case THEORY_STRINGS: return "theory::strings"; break;
  71     case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
  72
  73     default: break;
  74   }
  75   return "unknown";
  76 }
  77
  78 TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
  79 {
  80   uint32_t i = ffs(set);  // Find First Set (bit)
  81   if (i == 0)
  82   {
  83     return THEORY_LAST;
  84   }
  85   TheoryId id = static_cast<TheoryId>(i - 1);
  86   set = setRemove(id, set);
  87   return id;
  88 }
  89
  90 size_t TheoryIdSetUtil::setSize(TheoryIdSet set)
  91 {
  92   size_t count = 0;
  93   while (setPop(set) != THEORY_LAST)
  94   {
  95     ++count;
  96   }
  97   return count;
  98 }
  99
 100 size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set)
 101 {
 102   Assert(setContains(id, set));
 103   size_t count = 0;
 104   while (setPop(set) != id)
 105   {
 106     ++count;
 107   }
 108   return count;
 109 }
 110
 111 TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set)
 112 {
 113   return set | (1 << theory);
 114 }
 115
 116 TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set)
 117 {
 118   return setDifference(set, setInsert(theory));
 119 }
 120
 121 bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set)
 122 {
 123   return set & (1 << theory);
 124 }
 125
 126 TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a)
 127 {
 128   return (~a) & AllTheories;
 129 }
 130
 131 TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b)
 132 {
 133   return a & b;
 134 }
 135
 136 TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b)
 137 {
 138   return a | b;
 139 }
 140
 141 TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b)
 142 {
 143   return (~b) & a;
 144 }
 145
 146 std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet)
 147 {
 148   std::stringstream ss;
 149   ss << "[";
 150   for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId)
 151   {
 152     TheoryId tid = static_cast<TheoryId>(theoryId);
 153     if (setContains(tid, theorySet))
 154     {
 155       ss << tid << " ";
 156     }
 157   }
 158   ss << "]";
 159   return ss.str();
 160 }
 161
 162 }  // namespace theory
 163 }  // namespace CVC4