src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Clark Barrett, Dejan Jovanovic
   6  ** Minor contributors (to current version): Andrew Reynolds, Tim King
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Base for theory interface.
  13  **
  14  ** Base for theory interface.
  15  **/
  16
  17 #include "theory/theory.h"
  18 #include "util/cvc4_assert.h"
  19 #include "theory/quantifiers_engine.h"
  20
  21 #include <vector>
  22
  23 using namespace std;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27
  28 /** Default value for the uninterpreted sorts is the UF theory */
  29 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
  30
  31 /** By default, we use the type based theoryOf */
  32 TheoryOfMode Theory::s_theoryOfMode = THEORY_OF_TYPE_BASED;
  33
  34 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  35   switch(level){
  36   case Theory::EFFORT_STANDARD:
  37     os << "EFFORT_STANDARD"; break;
  38   case Theory::EFFORT_FULL:
  39     os << "EFFORT_FULL"; break;
  40   case Theory::EFFORT_COMBINATION:
  41     os << "EFFORT_COMBINATION"; break;
  42   case Theory::EFFORT_LAST_CALL:
  43     os << "EFFORT_LAST_CALL"; break;
  44   default:
  45       Unreachable();
  46   }
  47   return os;
  48 }/* ostream& operator<<(ostream&, Theory::Effort) */
  49
  50 Theory::~Theory() {
  51   StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
  52 }
  53
  54 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
  55
  56   Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
  57
  58   switch(mode) {
  59   case THEORY_OF_TYPE_BASED:
  60     // Constants, variables, 0-ary constructors
  61     if (node.isVar() || node.isConst()) {
  62       return theoryOf(node.getType());
  63     }
  64     // Equality is owned by the theory that owns the domain
  65     if (node.getKind() == kind::EQUAL) {
  66       return theoryOf(node[0].getType());
  67     }
  68     // Regular nodes are owned by the kind
  69     return kindToTheoryId(node.getKind());
  70     break;
  71   case THEORY_OF_TERM_BASED:
  72     // Variables
  73     if (node.isVar()) {
  74       if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
  75         // We treat the varibables as uninterpreted
  76         return s_uninterpretedSortOwner;
  77       } else {
  78         // Except for the Boolean ones, which we just ignore anyhow
  79         return theory::THEORY_BOOL;
  80       }
  81     }
  82     // Constants
  83     if (node.isConst()) {
  84       // Constants go to the theory of the type
  85       return theoryOf(node.getType());
  86     }
  87     // Equality
  88     if (node.getKind() == kind::EQUAL) {
  89       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
  90       if (node[0].getKind() == kind::ITE) {
  91         return theoryOf(node[0].getType());
  92       }
  93       if (node[1].getKind() == kind::ITE) {
  94         return theoryOf(node[1].getType());
  95       }
  96       // If both sides belong to the same theory the choice is easy
  97       TheoryId T1 = theoryOf(node[0]);
  98       TheoryId T2 = theoryOf(node[1]);
  99       if (T1 == T2) {
 100         return T1;
 101       }
 102       TheoryId T3 = theoryOf(node[0].getType());
 103       // This is a case of
 104       // * x*y = f(z) -> UF
 105       // * x = c      -> UF
 106       // * f(x) = read(a, y) -> either UF or ARRAY
 107       // at least one of the theories has to be parametric, i.e. theory of the type is different
 108       // from the theory of the term
 109       if (T1 == T3) {
 110         return T2;
 111       }
 112       if (T2 == T3) {
 113         return T1;
 114       }
 115       // If both are parametric, we take the smaller one (arbitraty)
 116       return T1 < T2 ? T1 : T2;
 117     }
 118     // Regular nodes are owned by the kind
 119     return kindToTheoryId(node.getKind());
 120     break;
 121   default:
 122     Unreachable();
 123   }
 124 }
 125
 126 void Theory::addSharedTermInternal(TNode n) {
 127   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 128   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 129   d_sharedTerms.push_back(n);
 130   addSharedTerm(n);
 131 }
 132
 133 void Theory::computeCareGraph() {
 134   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 135   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 136     TNode a = d_sharedTerms[i];
 137     TypeNode aType = a.getType();
 138     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 139       TNode b = d_sharedTerms[j];
 140       if (b.getType() != aType) {
 141         // We don't care about the terms of different types
 142         continue;
 143       }
 144       switch (d_valuation.getEqualityStatus(a, b)) {
 145       case EQUALITY_TRUE_AND_PROPAGATED:
 146       case EQUALITY_FALSE_AND_PROPAGATED:
 147         // If we know about it, we should have propagated it, so we can skip
 148         break;
 149       default:
 150         // Let's split on it
 151         addCarePair(a, b);
 152         break;
 153       }
 154     }
 155   }
 156 }
 157
 158 void Theory::printFacts(std::ostream& os) const {
 159   unsigned i, n = d_facts.size();
 160   for(i = 0; i < n; i++){
 161     const Assertion& a_i = d_facts[i];
 162     Node assertion  = a_i;
 163     os << d_id << '[' << i << ']' << " " << assertion << endl;
 164   }
 165 }
 166
 167 void Theory::debugPrintFacts() const{
 168   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 169   printFacts(DebugChannel.getStream());
 170 }
 171
 172 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 173   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
 174   for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
 175     currentlyShared.insert (*i);
 176   }
 177   return currentlyShared;
 178 }
 179
 180
 181 void Theory::collectTerms(TNode n, set<Node>& termSet)
 182 {
 183   if (termSet.find(n) != termSet.end()) {
 184     return;
 185   }
 186   Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
 187   termSet.insert(n);
 188   if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
 189     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 190       collectTerms(*child_it, termSet);
 191     }
 192   }
 193 }
 194
 195
 196 void Theory::computeRelevantTerms(set<Node>& termSet)
 197 {
 198   // Collect all terms appearing in assertions
 199   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 200   for (; assert_it != assert_it_end; ++assert_it) {
 201     collectTerms(*assert_it, termSet);
 202   }
 203
 204   // Add terms that are shared terms
 205   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 206   for (; shared_it != shared_it_end; ++shared_it) {
 207     collectTerms(*shared_it, termSet);
 208   }
 209 }
 210
 211
 212 }/* CVC4::theory namespace */
 213 }/* CVC4 namespace */