src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: taking
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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 Base for theory interface.
  15  **
  16  ** Base for theory interface.
  17  **/
  18
  19 #include "theory/theory.h"
  20 #include "util/Assert.h"
  21
  22 #include <vector>
  23
  24 using namespace std;
  25
  26 namespace CVC4 {
  27 namespace theory {
  28
  29 /** Default value for the uninterpreted sorts is the UF theory */
  30 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
  31
  32 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  33   switch(level){
  34   case Theory::MIN_EFFORT:
  35     os << "MIN_EFFORT"; break;
  36   case Theory::QUICK_CHECK:
  37     os << "QUICK_CHECK"; break;
  38   case Theory::STANDARD:
  39     os << "STANDARD"; break;
  40   case Theory::FULL_EFFORT:
  41     os << "FULL_EFFORT"; break;
  42   default:
  43       Unreachable();
  44   }
  45   return os;
  46 }/* ostream& operator<<(ostream&, Theory::Effort) */
  47
  48 void Theory::addSharedTermInternal(TNode n) {
  49   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
  50   d_sharedTerms.push_back(n);
  51   addSharedTerm(n);
  52 }
  53
  54 void Theory::computeCareGraph(CareGraph& careGraph) {
  55   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << std::endl;
  56   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
  57     TNode a = d_sharedTerms[i];
  58     TypeNode aType = a.getType();
  59     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
  60       TNode b = d_sharedTerms[j];
  61       if (b.getType() != aType) {
  62         // We don't care about the terms of different types
  63         continue;
  64       }
  65       switch (getEqualityStatus(a, b)) {
  66       case EQUALITY_TRUE_AND_PROPAGATED:
  67       case EQUALITY_FALSE_AND_PROPAGATED:
  68         // If we know about it, we should have propagated it, so we can skip
  69         break;
  70       default:
  71         // Let's split on it
  72         careGraph.push_back(CarePair(a, b, getId()));
  73         break;
  74       }
  75     }
  76   }
  77 }
  78
  79 }/* CVC4::theory namespace */
  80 }/* CVC4 namespace */