src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: ajreynol, dejan
   6  ** Minor contributors (to current version): taking
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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/quantifiers/instantiator_default.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 /** By default, we use the type based theoryOf */
  33 TheoryOfMode Theory::s_theoryOfMode = THEORY_OF_TYPE_BASED;
  34
  35 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  36   switch(level){
  37   case Theory::EFFORT_STANDARD:
  38     os << "EFFORT_STANDARD"; break;
  39   case Theory::EFFORT_FULL:
  40     os << "EFFORT_FULL"; break;
  41   case Theory::EFFORT_COMBINATION:
  42     os << "EFFORT_COMBINATION"; break;
  43   case Theory::EFFORT_LAST_CALL:
  44     os << "EFFORT_LAST_CALL"; break;
  45   default:
  46       Unreachable();
  47   }
  48   return os;
  49 }/* ostream& operator<<(ostream&, Theory::Effort) */
  50
  51 Theory::~Theory() {
  52   if(d_inst != NULL) {
  53     delete d_inst;
  54     d_inst = NULL;
  55   }
  56
  57   StatisticsRegistry::unregisterStat(&d_computeCareGraphTime);
  58 }
  59
  60 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
  61
  62   Trace("theory::internal") << "theoryOf(" << node << ")" << std::endl;
  63
  64   switch(mode) {
  65   case THEORY_OF_TYPE_BASED:
  66     // Constants, variables, 0-ary constructors
  67     if (node.isVar() || node.isConst()) {
  68       return theoryOf(node.getType());
  69     }
  70     // Equality is owned by the theory that owns the domain
  71     if (node.getKind() == kind::EQUAL) {
  72       return theoryOf(node[0].getType());
  73     }
  74     // Regular nodes are owned by the kind
  75     return kindToTheoryId(node.getKind());
  76     break;
  77   case THEORY_OF_TERM_BASED:
  78     // Variables
  79     if (node.isVar()) {
  80       if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
  81         // We treat the varibables as uninterpreted
  82         return s_uninterpretedSortOwner;
  83       } else {
  84         // Except for the Boolean ones, which we just ignore anyhow
  85         return theory::THEORY_BOOL;
  86       }
  87     }
  88     // Constants
  89     if (node.isConst()) {
  90       // Constants go to the theory of the type
  91       return theoryOf(node.getType());
  92     }
  93     // Equality
  94     if (node.getKind() == kind::EQUAL) {
  95       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
  96       if (node[0].getKind() == kind::ITE) {
  97         return theoryOf(node[0].getType());
  98       }
  99       if (node[1].getKind() == kind::ITE) {
 100         return theoryOf(node[1].getType());
 101       }
 102       // If both sides belong to the same theory the choice is easy
 103       TheoryId T1 = theoryOf(node[0]);
 104       TheoryId T2 = theoryOf(node[1]);
 105       if (T1 == T2) {
 106         return T1;
 107       }
 108       TheoryId T3 = theoryOf(node[0].getType());
 109       // This is a case of
 110       // * x*y = f(z) -> UF
 111       // * x = c      -> UF
 112       // * f(x) = read(a, y) -> either UF or ARRAY
 113       // at least one of the theories has to be parametric, i.e. theory of the type is different
 114       // from the theory of the term
 115       if (T1 == T3) {
 116         return T2;
 117       }
 118       if (T2 == T3) {
 119         return T1;
 120       }
 121       // If both are parametric, we take the smaller one (arbitraty)
 122       return T1 < T2 ? T1 : T2;
 123     }
 124     // Regular nodes are owned by the kind
 125     return kindToTheoryId(node.getKind());
 126     break;
 127   default:
 128     Unreachable();
 129   }
 130 }
 131
 132 void Theory::addSharedTermInternal(TNode n) {
 133   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 134   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 135   d_sharedTerms.push_back(n);
 136   addSharedTerm(n);
 137 }
 138
 139 void Theory::computeCareGraph() {
 140   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 141   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 142     TNode a = d_sharedTerms[i];
 143     TypeNode aType = a.getType();
 144     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 145       TNode b = d_sharedTerms[j];
 146       if (b.getType() != aType) {
 147         // We don't care about the terms of different types
 148         continue;
 149       }
 150       switch (d_valuation.getEqualityStatus(a, b)) {
 151       case EQUALITY_TRUE_AND_PROPAGATED:
 152       case EQUALITY_FALSE_AND_PROPAGATED:
 153         // If we know about it, we should have propagated it, so we can skip
 154         break;
 155       default:
 156         // Let's split on it
 157         addCarePair(a, b);
 158         break;
 159       }
 160     }
 161   }
 162 }
 163
 164 void Theory::printFacts(std::ostream& os) const {
 165   unsigned i, n = d_facts.size();
 166   for(i = 0; i < n; i++){
 167     const Assertion& a_i = d_facts[i];
 168     Node assertion  = a_i;
 169     os << d_id << '[' << i << ']' << " " << assertion << endl;
 170   }
 171 }
 172
 173 void Theory::debugPrintFacts() const{
 174   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 175   printFacts(DebugChannel.getStream());
 176 }
 177
 178 Instantiator::Instantiator(context::Context* c, QuantifiersEngine* qe, Theory* th) :
 179   d_quantEngine(qe),
 180   d_th(th) {
 181 }
 182
 183 Instantiator::~Instantiator() {
 184 }
 185
 186 void Instantiator::resetInstantiationRound(Theory::Effort effort) {
 187   for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
 188     if(isActiveStrategy(d_instStrategies[i])) {
 189       d_instStrategies[i]->processResetInstantiationRound(effort);
 190     }
 191   }
 192   processResetInstantiationRound(effort);
 193 }
 194
 195 int Instantiator::doInstantiation(Node f, Theory::Effort effort, int e ) {
 196   if( getQuantifierActive(f) ) {
 197     int status = process(f, effort, e );
 198     if(d_instStrategies.empty()) {
 199       Debug("inst-engine-inst") << "There are no instantiation strategies allocated." << endl;
 200     } else {
 201       for(int i = 0; i < (int) d_instStrategies.size(); ++i) {
 202         if(isActiveStrategy(d_instStrategies[i])) {
 203           Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl;
 204           //call the instantiation strategy's process method
 205           int s_status = d_instStrategies[i]->process( f, effort, e );
 206           Debug("inst-engine-inst") << "  -> status is " << s_status << endl;
 207           InstStrategy::updateStatus(status, s_status);
 208         } else {
 209           Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " is not active." << endl;
 210         }
 211       }
 212     }
 213     return status;
 214   } else {
 215     Debug("inst-engine-inst") << "We have no constraints from this quantifier." << endl;
 216     return InstStrategy::STATUS_SAT;
 217   }
 218 }
 219
 220 //void Instantiator::doInstantiation(int effort) {
 221 //  d_status = InstStrategy::STATUS_SAT;
 222 //  for( int q = 0; q < d_quantEngine->getNumQuantifiers(); ++q ) {
 223 //    Node f = d_quantEngine->getQuantifier(q);
 224 //    if( d_quantEngine->getActive(f) && hasConstraintsFrom(f) ) {
 225 //      int d_quantStatus = process( f, effort );
 226 //      InstStrategy::updateStatus( d_status, d_quantStatus );
 227 //      for( int i = 0; i < (int)d_instStrategies.size(); ++i ) {
 228 //        if( isActiveStrategy( d_instStrategies[i] ) ) {
 229 //          Debug("inst-engine-inst") << d_instStrategies[i]->identify() << " process " << effort << endl;
 230 //          //call the instantiation strategy's process method
 231 //          d_quantStatus = d_instStrategies[i]->process( f, effort );
 232 //          Debug("inst-engine-inst") << "  -> status is " << d_quantStatus << endl;
 233 //          InstStrategy::updateStatus( d_status, d_quantStatus );
 234 //        }
 235 //      }
 236 //    }
 237 //  }
 238 //}
 239
 240 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 241   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
 242   for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
 243     currentlyShared.insert (*i);
 244   }
 245   return currentlyShared;
 246 }
 247
 248
 249 void Theory::collectTerms(TNode n, set<Node>& termSet)
 250 {
 251   if (termSet.find(n) != termSet.end()) {
 252     return;
 253   }
 254   Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
 255   termSet.insert(n);
 256   if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
 257     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 258       collectTerms(*child_it, termSet);
 259     }
 260   }
 261 }
 262
 263
 264 void Theory::computeRelevantTerms(set<Node>& termSet)
 265 {
 266   // Collect all terms appearing in assertions
 267   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 268   for (; assert_it != assert_it_end; ++assert_it) {
 269     collectTerms(*assert_it, termSet);
 270   }
 271
 272   // Add terms that are shared terms
 273   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 274   for (; shared_it != shared_it_end; ++shared_it) {
 275     collectTerms(*shared_it, termSet);
 276   }
 277 }
 278
 279
 280 }/* CVC4::theory namespace */
 281 }/* CVC4 namespace */