src/theory/theory.cpp

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