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 #include "theory/substitutions.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::EFFORT_STANDARD:
  35     os << "EFFORT_STANDARD"; break;
  36   case Theory::EFFORT_FULL:
  37     os << "EFFORT_FULL"; break;
  38   case Theory::EFFORT_COMBINATION:
  39     os << "EFFORT_COMBINATION"; break;
  40   case Theory::EFFORT_LAST_CALL:
  41     os << "EFFORT_LAST_CALL"; break;
  42   default:
  43       Unreachable();
  44   }
  45   return os;
  46 }/* ostream& operator<<(ostream&, Theory::Effort) */
  47
  48 Theory::~Theory() {
  49   StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
  50 }
  51
  52 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
  53
  54   Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
  55
  56   switch(mode) {
  57   case THEORY_OF_TYPE_BASED:
  58     // Constants, variables, 0-ary constructors
  59     if (node.isVar() || node.isConst()) {
  60       return theoryOf(node.getType());
  61     }
  62     // Equality is owned by the theory that owns the domain
  63     if (node.getKind() == kind::EQUAL) {
  64       return theoryOf(node[0].getType());
  65     }
  66     // Regular nodes are owned by the kind
  67     return kindToTheoryId(node.getKind());
  68     break;
  69   case THEORY_OF_TERM_BASED:
  70     // Variables
  71     if (node.isVar()) {
  72       if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
  73         // We treat the variables as uninterpreted
  74         return s_uninterpretedSortOwner;
  75       } else {
  76         // Except for the Boolean ones, which we just ignore anyhow
  77         return theory::THEORY_BOOL;
  78       }
  79     }
  80     // Constants
  81     if (node.isConst()) {
  82       // Constants go to the theory of the type
  83       return theoryOf(node.getType());
  84     }
  85     // Equality
  86     if (node.getKind() == kind::EQUAL) {
  87       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
  88       if (node[0].getKind() == kind::ITE) {
  89         return theoryOf(node[0].getType());
  90       }
  91       if (node[1].getKind() == kind::ITE) {
  92         return theoryOf(node[1].getType());
  93       }
  94       // If both sides belong to the same theory the choice is easy
  95       TheoryId T1 = theoryOf(node[0]);
  96       TheoryId T2 = theoryOf(node[1]);
  97       if (T1 == T2) {
  98         return T1;
  99       }
 100       TheoryId T3 = theoryOf(node[0].getType());
 101       // This is a case of
 102       // * x*y = f(z) -> UF
 103       // * x = c      -> UF
 104       // * f(x) = read(a, y) -> either UF or ARRAY
 105       // at least one of the theories has to be parametric, i.e. theory of the type is different
 106       // from the theory of the term
 107       if (T1 == T3) {
 108         return T2;
 109       }
 110       if (T2 == T3) {
 111         return T1;
 112       }
 113       // If both are parametric, we take the smaller one (arbitraty)
 114       return T1 < T2 ? T1 : T2;
 115     }
 116     // Regular nodes are owned by the kind
 117     return kindToTheoryId(node.getKind());
 118     break;
 119   default:
 120     Unreachable();
 121   }
 122 }
 123
 124 void Theory::addSharedTermInternal(TNode n) {
 125   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 126   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 127   d_sharedTerms.push_back(n);
 128   addSharedTerm(n);
 129 }
 130
 131 void Theory::computeCareGraph() {
 132   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 133   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 134     TNode a = d_sharedTerms[i];
 135     TypeNode aType = a.getType();
 136     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 137       TNode b = d_sharedTerms[j];
 138       if (b.getType() != aType) {
 139         // We don't care about the terms of different types
 140         continue;
 141       }
 142       switch (d_valuation.getEqualityStatus(a, b)) {
 143       case EQUALITY_TRUE_AND_PROPAGATED:
 144       case EQUALITY_FALSE_AND_PROPAGATED:
 145         // If we know about it, we should have propagated it, so we can skip
 146         break;
 147       default:
 148         // Let's split on it
 149         addCarePair(a, b);
 150         break;
 151       }
 152     }
 153   }
 154 }
 155
 156 void Theory::printFacts(std::ostream& os) const {
 157   unsigned i, n = d_facts.size();
 158   for(i = 0; i < n; i++){
 159     const Assertion& a_i = d_facts[i];
 160     Node assertion  = a_i;
 161     os << d_id << '[' << i << ']' << " " << assertion << endl;
 162   }
 163 }
 164
 165 void Theory::debugPrintFacts() const{
 166   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 167   printFacts(DebugChannel.getStream());
 168 }
 169
 170 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 171   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
 172   for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
 173     currentlyShared.insert (*i);
 174   }
 175   return currentlyShared;
 176 }
 177
 178
 179 void Theory::collectTerms(TNode n, set<Node>& termSet)
 180 {
 181   if (termSet.find(n) != termSet.end()) {
 182     return;
 183   }
 184   Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
 185   termSet.insert(n);
 186   if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
 187     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 188       collectTerms(*child_it, termSet);
 189     }
 190   }
 191 }
 192
 193
 194 void Theory::computeRelevantTerms(set<Node>& termSet)
 195 {
 196   // Collect all terms appearing in assertions
 197   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 198   for (; assert_it != assert_it_end; ++assert_it) {
 199     collectTerms(*assert_it, termSet);
 200   }
 201
 202   // Add terms that are shared terms
 203   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 204   for (; shared_it != shared_it_end; ++shared_it) {
 205     collectTerms(*shared_it, termSet);
 206   }
 207 }
 208
 209
 210 Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions)
 211 {
 212   if (in.getKind() == kind::EQUAL) {
 213     if (in[0].isVar() && !in[1].hasSubterm(in[0])) {
 214       outSubstitutions.addSubstitution(in[0], in[1]);
 215       return PP_ASSERT_STATUS_SOLVED;
 216     }
 217     if (in[1].isVar() && !in[0].hasSubterm(in[1])) {
 218       outSubstitutions.addSubstitution(in[1], in[0]);
 219       return PP_ASSERT_STATUS_SOLVED;
 220     }
 221     if (in[0].isConst() && in[1].isConst()) {
 222       if (in[0] != in[1]) {
 223         return PP_ASSERT_STATUS_CONFLICT;
 224       }
 225     }
 226   }
 227
 228   return PP_ASSERT_STATUS_UNSOLVED;
 229 }
 230
 231
 232 }/* CVC4::theory namespace */
 233 }/* CVC4 namespace */