src/theory/theory.cpp

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