src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Clark Barrett, Dejan Jovanovic, Tim King
   6  ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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
  19 #include <vector>
  20
  21 #include "base/cvc4_assert.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/substitutions.h"
  24 #include "theory/quantifiers_engine.h"
  25
  26
  27 using namespace std;
  28
  29 namespace CVC4 {
  30 namespace theory {
  31
  32 /** Default value for the uninterpreted sorts is the UF theory */
  33 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
  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(TheoryId id, context::Context* satContext, context::UserContext* userContext,
  52                OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo,
  53                SmtGlobals* globals, std::string name) throw()
  54     : d_id(id)
  55     , d_instanceName(name)
  56     , d_satContext(satContext)
  57     , d_userContext(userContext)
  58     , d_logicInfo(logicInfo)
  59     , d_facts(satContext)
  60     , d_factsHead(satContext, 0)
  61     , d_sharedTermsIndex(satContext, 0)
  62     , d_careGraph(NULL)
  63     , d_quantEngine(NULL)
  64     , d_checkTime(getFullInstanceName() + "::checkTime")
  65     , d_computeCareGraphTime(getFullInstanceName() + "::computeCareGraphTime")
  66     , d_sharedTerms(satContext)
  67     , d_out(&out)
  68     , d_valuation(valuation)
  69     , d_proofsEnabled(false)
  70     , d_globals(globals)
  71 {
  72   smtStatisticsRegistry()->registerStat(&d_checkTime);
  73   smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
  74 }
  75
  76 Theory::~Theory() {
  77   smtStatisticsRegistry()->unregisterStat(&d_checkTime);
  78   smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
  79 }
  80
  81 TheoryId Theory::theoryOf(TheoryOfMode mode, TNode node) {
  82   TheoryId tid = THEORY_BUILTIN;
  83   switch(mode) {
  84   case THEORY_OF_TYPE_BASED:
  85     // Constants, variables, 0-ary constructors
  86     if (node.isVar() || node.isConst()) {
  87       tid = Theory::theoryOf(node.getType());
  88     } else if (node.getKind() == kind::EQUAL) {
  89       // Equality is owned by the theory that owns the domain
  90       tid = Theory::theoryOf(node[0].getType());
  91     } else {
  92       // Regular nodes are owned by the kind
  93       tid = kindToTheoryId(node.getKind());
  94     }
  95     break;
  96   case THEORY_OF_TERM_BASED:
  97     // Variables
  98     if (node.isVar()) {
  99       if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL) {
 100         // We treat the variables as uninterpreted
 101         tid = s_uninterpretedSortOwner;
 102       } else {
 103         // Except for the Boolean ones, which we just ignore anyhow
 104         tid = theory::THEORY_BOOL;
 105       }
 106     } else if (node.isConst()) {
 107       // Constants go to the theory of the type
 108       tid = Theory::theoryOf(node.getType());
 109     } else if (node.getKind() == kind::EQUAL) { // Equality
 110       // If one of them is an ITE, it's irelevant, since they will get replaced out anyhow
 111       if (node[0].getKind() == kind::ITE) {
 112         tid = Theory::theoryOf(node[0].getType());
 113       } else if (node[1].getKind() == kind::ITE) {
 114         tid = Theory::theoryOf(node[1].getType());
 115       } else {
 116         TNode l = node[0];
 117         TNode r = node[1];
 118         TypeNode ltype = l.getType();
 119         TypeNode rtype = r.getType();
 120         if( ltype != rtype ){
 121           tid = Theory::theoryOf(l.getType());
 122         }else {
 123           // If both sides belong to the same theory the choice is easy
 124           TheoryId T1 = Theory::theoryOf(l);
 125           TheoryId T2 = Theory::theoryOf(r);
 126           if (T1 == T2) {
 127             tid = T1;
 128           } else {
 129             TheoryId T3 = Theory::theoryOf(ltype);
 130             // This is a case of
 131             // * x*y = f(z) -> UF
 132             // * x = c      -> UF
 133             // * f(x) = read(a, y) -> either UF or ARRAY
 134             // at least one of the theories has to be parametric, i.e. theory of the type is different
 135             // from the theory of the term
 136             if (T1 == T3) {
 137               tid = T2;
 138             } else if (T2 == T3) {
 139               tid = T1;
 140             } else {
 141               // If both are parametric, we take the smaller one (arbitrary)
 142               tid = T1 < T2 ? T1 : T2;
 143             }
 144           }
 145         }
 146       }
 147     } else {
 148       // Regular nodes are owned by the kind
 149       tid = kindToTheoryId(node.getKind());
 150     }
 151     break;
 152   default:
 153     Unreachable();
 154   }
 155   Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
 156   return tid;
 157 }
 158
 159 void Theory::addSharedTermInternal(TNode n) {
 160   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 161   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 162   d_sharedTerms.push_back(n);
 163   addSharedTerm(n);
 164 }
 165
 166 void Theory::computeCareGraph() {
 167   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 168   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 169     TNode a = d_sharedTerms[i];
 170     TypeNode aType = a.getType();
 171     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 172       TNode b = d_sharedTerms[j];
 173       if (b.getType() != aType) {
 174         // We don't care about the terms of different types
 175         continue;
 176       }
 177       switch (d_valuation.getEqualityStatus(a, b)) {
 178       case EQUALITY_TRUE_AND_PROPAGATED:
 179       case EQUALITY_FALSE_AND_PROPAGATED:
 180         // If we know about it, we should have propagated it, so we can skip
 181         break;
 182       default:
 183         // Let's split on it
 184         addCarePair(a, b);
 185         break;
 186       }
 187     }
 188   }
 189 }
 190
 191 void Theory::printFacts(std::ostream& os) const {
 192   unsigned i, n = d_facts.size();
 193   for(i = 0; i < n; i++){
 194     const Assertion& a_i = d_facts[i];
 195     Node assertion  = a_i;
 196     os << d_id << '[' << i << ']' << " " << assertion << endl;
 197   }
 198 }
 199
 200 void Theory::debugPrintFacts() const{
 201   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 202   printFacts(DebugChannel.getStream());
 203 }
 204
 205 std::hash_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 206   std::hash_set<TNode, TNodeHashFunction> currentlyShared;
 207   for(shared_terms_iterator i = shared_terms_begin(), i_end = shared_terms_end(); i != i_end; ++i){
 208     currentlyShared.insert (*i);
 209   }
 210   return currentlyShared;
 211 }
 212
 213
 214 void Theory::collectTerms(TNode n, set<Node>& termSet) const
 215 {
 216   if (termSet.find(n) != termSet.end()) {
 217     return;
 218   }
 219   Trace("theory::collectTerms") << "Theory::collectTerms: adding " << n << endl;
 220   termSet.insert(n);
 221   if (n.getKind() == kind::NOT || n.getKind() == kind::EQUAL || !isLeaf(n)) {
 222     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 223       collectTerms(*child_it, termSet);
 224     }
 225   }
 226 }
 227
 228
 229 void Theory::computeRelevantTerms(set<Node>& termSet) const
 230 {
 231   // Collect all terms appearing in assertions
 232   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 233   for (; assert_it != assert_it_end; ++assert_it) {
 234     collectTerms(*assert_it, termSet);
 235   }
 236
 237   // Add terms that are shared terms
 238   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 239   for (; shared_it != shared_it_end; ++shared_it) {
 240     collectTerms(*shared_it, termSet);
 241   }
 242 }
 243
 244
 245 Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstitutions)
 246 {
 247   if (in.getKind() == kind::EQUAL) {
 248     // (and (= x t) phi) can be replaced by phi[x/t] if
 249     // 1) x is a variable
 250     // 2) x is not in the term t
 251     // 3) x : T and t : S, then S <: T
 252     if (in[0].isVar() && !in[1].hasSubterm(in[0]) && (in[1].getType()).isSubtypeOf(in[0].getType()) ){
 253       outSubstitutions.addSubstitution(in[0], in[1]);
 254       return PP_ASSERT_STATUS_SOLVED;
 255     }
 256     if (in[1].isVar() && !in[0].hasSubterm(in[1]) && (in[0].getType()).isSubtypeOf(in[1].getType())){
 257       outSubstitutions.addSubstitution(in[1], in[0]);
 258       return PP_ASSERT_STATUS_SOLVED;
 259     }
 260     if (in[0].isConst() && in[1].isConst()) {
 261       if (in[0] != in[1]) {
 262         return PP_ASSERT_STATUS_CONFLICT;
 263       }
 264     }
 265   }
 266
 267   return PP_ASSERT_STATUS_UNSOLVED;
 268 }
 269
 270 std::pair<bool, Node> Theory::entailmentCheck(TNode lit,
 271                                               const EntailmentCheckParameters* params,
 272                                               EntailmentCheckSideEffects* out){
 273   return make_pair(false, Node::null());
 274 }
 275
 276 EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid)
 277   : d_tid(tid) {
 278 }
 279
 280 EntailmentCheckParameters::~EntailmentCheckParameters(){}
 281
 282 TheoryId EntailmentCheckParameters::getTheoryId() const {
 283   return d_tid;
 284 }
 285
 286 EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid)
 287   : d_tid(tid)
 288 {}
 289
 290 TheoryId EntailmentCheckSideEffects::getTheoryId() const {
 291   return d_tid;
 292 }
 293
 294 EntailmentCheckSideEffects::~EntailmentCheckSideEffects() {
 295 }
 296
 297 }/* CVC4::theory namespace */
 298 }/* CVC4 namespace */