src/theory/theory_id.cpp

   1 /*********************                                                        */
   2 /*! \file theory_id.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Aina Niemetz, Tim King, 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 "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_STRINGS: out << "THEORY_STRINGS"; break;
  47     case THEORY_QUANTIFIERS: out << "THEORY_QUANTIFIERS"; break;
  48
  49     default: out << "UNKNOWN_THEORY"; break;
  50   }
  51   return out;
  52 }
  53
  54 std::string getStatsPrefix(TheoryId theoryId)
  55 {
  56   switch (theoryId)
  57   {
  58     case THEORY_BUILTIN: return "theory::builtin"; break;
  59     case THEORY_BOOL: return "theory::bool"; break;
  60     case THEORY_UF: return "theory::uf"; break;
  61     case THEORY_ARITH: return "theory::arith"; break;
  62     case THEORY_BV: return "theory::bv"; break;
  63     case THEORY_FP: return "theory::fp"; break;
  64     case THEORY_ARRAYS: return "theory::arrays"; break;
  65     case THEORY_DATATYPES: return "theory::datatypes"; break;
  66     case THEORY_SEP: return "theory::sep"; break;
  67     case THEORY_SETS: return "theory::sets"; break;
  68     case THEORY_STRINGS: return "theory::strings"; break;
  69     case THEORY_QUANTIFIERS: return "theory::quantifiers"; break;
  70
  71     default: break;
  72   }
  73   return "unknown";
  74 }
  75
  76 TheoryId TheoryIdSetUtil::setPop(TheoryIdSet& set)
  77 {
  78   uint32_t i = ffs(set);  // Find First Set (bit)
  79   if (i == 0)
  80   {
  81     return THEORY_LAST;
  82   }
  83   TheoryId id = static_cast<TheoryId>(i - 1);
  84   set = setRemove(id, set);
  85   return id;
  86 }
  87
  88 size_t TheoryIdSetUtil::setSize(TheoryIdSet set)
  89 {
  90   size_t count = 0;
  91   while (setPop(set) != THEORY_LAST)
  92   {
  93     ++count;
  94   }
  95   return count;
  96 }
  97
  98 size_t TheoryIdSetUtil::setIndex(TheoryId id, TheoryIdSet set)
  99 {
 100   Assert(setContains(id, set));
 101   size_t count = 0;
 102   while (setPop(set) != id)
 103   {
 104     ++count;
 105   }
 106   return count;
 107 }
 108
 109 TheoryIdSet TheoryIdSetUtil::setInsert(TheoryId theory, TheoryIdSet set)
 110 {
 111   return set | (1 << theory);
 112 }
 113
 114 TheoryIdSet TheoryIdSetUtil::setRemove(TheoryId theory, TheoryIdSet set)
 115 {
 116   return setDifference(set, setInsert(theory));
 117 }
 118
 119 bool TheoryIdSetUtil::setContains(TheoryId theory, TheoryIdSet set)
 120 {
 121   return set & (1 << theory);
 122 }
 123
 124 TheoryIdSet TheoryIdSetUtil::setComplement(TheoryIdSet a)
 125 {
 126   return (~a) & AllTheories;
 127 }
 128
 129 TheoryIdSet TheoryIdSetUtil::setIntersection(TheoryIdSet a, TheoryIdSet b)
 130 {
 131   return a & b;
 132 }
 133
 134 TheoryIdSet TheoryIdSetUtil::setUnion(TheoryIdSet a, TheoryIdSet b)
 135 {
 136   return a | b;
 137 }
 138
 139 TheoryIdSet TheoryIdSetUtil::setDifference(TheoryIdSet a, TheoryIdSet b)
 140 {
 141   return (~b) & a;
 142 }
 143
 144 std::string TheoryIdSetUtil::setToString(TheoryIdSet theorySet)
 145 {
 146   std::stringstream ss;
 147   ss << "[";
 148   for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++theoryId)
 149   {
 150     TheoryId tid = static_cast<TheoryId>(theoryId);
 151     if (setContains(tid, theorySet))
 152     {
 153       ss << tid << " ";
 154     }
 155   }
 156   ss << "]";
 157   return ss.str();
 158 }
 159
 160 }  // namespace theory
 161 }  // namespace CVC4