src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Tim King, Mathias Preiner, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 <iostream>
  20 #include <sstream>
  21 #include <string>
  22 #include <vector>
  23
  24 #include "base/check.h"
  25 #include "expr/node_algorithm.h"
  26 #include "options/smt_options.h"
  27 #include "options/theory_options.h"
  28 #include "smt/smt_statistics_registry.h"
  29 #include "theory/ext_theory.h"
  30 #include "theory/quantifiers_engine.h"
  31 #include "theory/substitutions.h"
  32 #include "theory/theory_rewriter.h"
  33
  34 using namespace std;
  35
  36 namespace CVC4 {
  37 namespace theory {
  38
  39 /** Default value for the uninterpreted sorts is the UF theory */
  40 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
  41
  42 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  43   switch(level){
  44   case Theory::EFFORT_STANDARD:
  45     os << "EFFORT_STANDARD"; break;
  46   case Theory::EFFORT_FULL:
  47     os << "EFFORT_FULL"; break;
  48   case Theory::EFFORT_LAST_CALL:
  49     os << "EFFORT_LAST_CALL"; break;
  50   default:
  51       Unreachable();
  52   }
  53   return os;
  54 }/* ostream& operator<<(ostream&, Theory::Effort) */
  55
  56 Theory::Theory(TheoryId id,
  57                context::Context* satContext,
  58                context::UserContext* userContext,
  59                OutputChannel& out,
  60                Valuation valuation,
  61                const LogicInfo& logicInfo,
  62                ProofNodeManager* pnm,
  63                std::string name)
  64     : d_id(id),
  65       d_satContext(satContext),
  66       d_userContext(userContext),
  67       d_logicInfo(logicInfo),
  68       d_pnm(pnm),
  69       d_facts(satContext),
  70       d_factsHead(satContext, 0),
  71       d_sharedTermsIndex(satContext, 0),
  72       d_careGraph(NULL),
  73       d_quantEngine(NULL),
  74       d_decManager(nullptr),
  75       d_instanceName(name),
  76       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
  77       d_computeCareGraphTime(getStatsPrefix(id) + name
  78                              + "::computeCareGraphTime"),
  79       d_sharedTerms(satContext),
  80       d_out(&out),
  81       d_valuation(valuation),
  82       d_equalityEngine(nullptr),
  83       d_allocEqualityEngine(nullptr),
  84       d_theoryState(nullptr),
  85       d_inferManager(nullptr)
  86 {
  87   smtStatisticsRegistry()->registerStat(&d_checkTime);
  88   smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
  89 }
  90
  91 Theory::~Theory() {
  92   smtStatisticsRegistry()->unregisterStat(&d_checkTime);
  93   smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
  94 }
  95
  96 bool Theory::needsEqualityEngine(EeSetupInfo& esi)
  97 {
  98   // by default, this theory does not use an (official) equality engine
  99   return false;
 100 }
 101
 102 void Theory::setEqualityEngine(eq::EqualityEngine* ee)
 103 {
 104   // set the equality engine pointer
 105   d_equalityEngine = ee;
 106   if (d_theoryState != nullptr)
 107   {
 108     d_theoryState->setEqualityEngine(ee);
 109   }
 110   if (d_inferManager != nullptr)
 111   {
 112     d_inferManager->setEqualityEngine(ee);
 113   }
 114 }
 115
 116 void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
 117 {
 118   Assert(d_quantEngine == nullptr);
 119   // quantifiers engine may be null if not in quantified logic
 120   d_quantEngine = qe;
 121 }
 122
 123 void Theory::setDecisionManager(DecisionManager* dm)
 124 {
 125   Assert(d_decManager == nullptr);
 126   Assert(dm != nullptr);
 127   d_decManager = dm;
 128 }
 129
 130 void Theory::finishInitStandalone()
 131 {
 132   EeSetupInfo esi;
 133   if (needsEqualityEngine(esi))
 134   {
 135     // always associated with the same SAT context as the theory (d_satContext)
 136     d_allocEqualityEngine.reset(new eq::EqualityEngine(
 137         *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
 138     // use it as the official equality engine
 139     setEqualityEngine(d_allocEqualityEngine.get());
 140   }
 141   finishInit();
 142 }
 143
 144 TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
 145 {
 146   TheoryId tid = THEORY_BUILTIN;
 147   switch(mode) {
 148     case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
 149       // Constants, variables, 0-ary constructors
 150       if (node.isVar())
 151       {
 152         if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 153         {
 154           tid = THEORY_UF;
 155         }
 156         else
 157         {
 158           tid = Theory::theoryOf(node.getType());
 159         }
 160       }
 161       else if (node.isConst())
 162       {
 163         tid = Theory::theoryOf(node.getType());
 164       }
 165       else if (node.getKind() == kind::EQUAL)
 166       {
 167         // Equality is owned by the theory that owns the domain
 168         tid = Theory::theoryOf(node[0].getType());
 169       }
 170       else
 171       {
 172         // Regular nodes are owned by the kind
 173         tid = kindToTheoryId(node.getKind());
 174       }
 175       break;
 176     case options::TheoryOfMode::THEORY_OF_TERM_BASED:
 177       // Variables
 178       if (node.isVar())
 179       {
 180         if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
 181         {
 182           // We treat the variables as uninterpreted
 183           tid = s_uninterpretedSortOwner;
 184         }
 185         else
 186         {
 187           if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 188           {
 189             // Boolean vars go to UF
 190             tid = THEORY_UF;
 191           }
 192           else
 193           {
 194             // Except for the Boolean ones
 195             tid = THEORY_BOOL;
 196           }
 197         }
 198       }
 199       else if (node.isConst())
 200       {
 201         // Constants go to the theory of the type
 202         tid = Theory::theoryOf(node.getType());
 203       }
 204       else if (node.getKind() == kind::EQUAL)
 205       {  // Equality
 206         // If one of them is an ITE, it's irelevant, since they will get
 207         // replaced out anyhow
 208         if (node[0].getKind() == kind::ITE)
 209         {
 210           tid = Theory::theoryOf(node[0].getType());
 211         }
 212         else if (node[1].getKind() == kind::ITE)
 213         {
 214           tid = Theory::theoryOf(node[1].getType());
 215         }
 216         else
 217         {
 218           TNode l = node[0];
 219           TNode r = node[1];
 220           TypeNode ltype = l.getType();
 221           TypeNode rtype = r.getType();
 222           if (ltype != rtype)
 223           {
 224             tid = Theory::theoryOf(l.getType());
 225           }
 226           else
 227           {
 228             // If both sides belong to the same theory the choice is easy
 229             TheoryId T1 = Theory::theoryOf(l);
 230             TheoryId T2 = Theory::theoryOf(r);
 231             if (T1 == T2)
 232             {
 233               tid = T1;
 234             }
 235             else
 236             {
 237               TheoryId T3 = Theory::theoryOf(ltype);
 238               // This is a case of
 239               // * x*y = f(z) -> UF
 240               // * x = c      -> UF
 241               // * f(x) = read(a, y) -> either UF or ARRAY
 242               // at least one of the theories has to be parametric, i.e. theory
 243               // of the type is different from the theory of the term
 244               if (T1 == T3)
 245               {
 246                 tid = T2;
 247               }
 248               else if (T2 == T3)
 249               {
 250                 tid = T1;
 251               }
 252               else
 253               {
 254                 // If both are parametric, we take the smaller one (arbitrary)
 255                 tid = T1 < T2 ? T1 : T2;
 256               }
 257             }
 258           }
 259         }
 260       }
 261       else
 262       {
 263         // Regular nodes are owned by the kind
 264         tid = kindToTheoryId(node.getKind());
 265       }
 266     break;
 267   default:
 268     Unreachable();
 269   }
 270   Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
 271   return tid;
 272 }
 273
 274 void Theory::notifySharedTerm(TNode n)
 275 {
 276   // TODO (project #39): this will move to addSharedTerm, as every theory with
 277   // an equality does this in their notifySharedTerm method.
 278   // if we have an equality engine, add the trigger term
 279   if (d_equalityEngine != nullptr)
 280   {
 281     d_equalityEngine->addTriggerTerm(n, d_id);
 282   }
 283 }
 284
 285 void Theory::computeCareGraph() {
 286   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 287   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 288     TNode a = d_sharedTerms[i];
 289     TypeNode aType = a.getType();
 290     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 291       TNode b = d_sharedTerms[j];
 292       if (b.getType() != aType) {
 293         // We don't care about the terms of different types
 294         continue;
 295       }
 296       switch (d_valuation.getEqualityStatus(a, b)) {
 297       case EQUALITY_TRUE_AND_PROPAGATED:
 298       case EQUALITY_FALSE_AND_PROPAGATED:
 299         // If we know about it, we should have propagated it, so we can skip
 300         break;
 301       default:
 302         // Let's split on it
 303         addCarePair(a, b);
 304         break;
 305       }
 306     }
 307   }
 308 }
 309
 310 void Theory::printFacts(std::ostream& os) const {
 311   unsigned i, n = d_facts.size();
 312   for(i = 0; i < n; i++){
 313     const Assertion& a_i = d_facts[i];
 314     Node assertion  = a_i;
 315     os << d_id << '[' << i << ']' << " " << assertion << endl;
 316   }
 317 }
 318
 319 void Theory::debugPrintFacts() const{
 320   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 321   printFacts(DebugChannel.getStream());
 322 }
 323
 324 bool Theory::isLegalElimination(TNode x, TNode val)
 325 {
 326   Assert(x.isVar());
 327   if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
 328       || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 329   {
 330     return false;
 331   }
 332   if (expr::hasSubterm(val, x))
 333   {
 334     return false;
 335   }
 336   if (!val.getType().isSubtypeOf(x.getType()))
 337   {
 338     return false;
 339   }
 340   if (!options::produceModels())
 341   {
 342     // don't care about the model, we are fine
 343     return true;
 344   }
 345   // if there is a model object
 346   TheoryModel* tm = d_valuation.getModel();
 347   Assert(tm != nullptr);
 348   return tm->isLegalElimination(x, val);
 349 }
 350
 351 std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 352   std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
 353   for (shared_terms_iterator i = shared_terms_begin(),
 354            i_end = shared_terms_end(); i != i_end; ++i) {
 355     currentlyShared.insert (*i);
 356   }
 357   return currentlyShared;
 358 }
 359
 360 bool Theory::collectModelInfo(TheoryModel* m)
 361 {
 362   // NOTE: the computation of termSet will be moved to model manager
 363   // and passed as an argument to collectModelInfo.
 364   std::set<Node> termSet;
 365   // Compute terms appearing in assertions and shared terms
 366   TheoryModel* tm = d_valuation.getModel();
 367   Assert(tm != nullptr);
 368   const std::set<Kind>& irrKinds = tm->getIrrelevantKinds();
 369   computeAssertedTerms(termSet, irrKinds, true);
 370   // Compute additional relevant terms (theory-specific)
 371   computeRelevantTerms(termSet);
 372   // if we are using an equality engine, assert it to the model
 373   if (d_equalityEngine != nullptr)
 374   {
 375     if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
 376     {
 377       return false;
 378     }
 379   }
 380   // now, collect theory-specific value assigments
 381   return collectModelValues(m, termSet);
 382 }
 383
 384 void Theory::collectTerms(TNode n,
 385                           const std::set<Kind>& irrKinds,
 386                           set<Node>& termSet) const
 387 {
 388   if (termSet.find(n) != termSet.end()) {
 389     return;
 390   }
 391   Kind nk = n.getKind();
 392   if (irrKinds.find(nk) == irrKinds.end())
 393   {
 394     Trace("theory::collectTerms")
 395         << "Theory::collectTerms: adding " << n << endl;
 396     termSet.insert(n);
 397   }
 398   if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
 399   {
 400     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 401       collectTerms(*child_it, irrKinds, termSet);
 402     }
 403   }
 404 }
 405
 406 void Theory::computeAssertedTerms(std::set<Node>& termSet,
 407                                   const std::set<Kind>& irrKinds,
 408                                   bool includeShared) const
 409 {
 410   // Collect all terms appearing in assertions
 411   context::CDList<Assertion>::const_iterator assert_it = facts_begin(),
 412                                              assert_it_end = facts_end();
 413   for (; assert_it != assert_it_end; ++assert_it)
 414   {
 415     collectTerms(*assert_it, irrKinds, termSet);
 416   }
 417
 418   if (!includeShared)
 419   {
 420     return;
 421   }
 422   // Add terms that are shared terms
 423   std::set<Kind> kempty;
 424   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(),
 425                                          shared_it_end = shared_terms_end();
 426   for (; shared_it != shared_it_end; ++shared_it)
 427   {
 428     collectTerms(*shared_it, kempty, termSet);
 429   }
 430 }
 431
 432 void Theory::computeRelevantTerms(std::set<Node>& termSet)
 433 {
 434   // by default, there are no additional relevant terms
 435 }
 436
 437 bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 438 {
 439   return true;
 440 }
 441
 442 Theory::PPAssertStatus Theory::ppAssert(TNode in,
 443                                         SubstitutionMap& outSubstitutions)
 444 {
 445   if (in.getKind() == kind::EQUAL)
 446   {
 447     // (and (= x t) phi) can be replaced by phi[x/t] if
 448     // 1) x is a variable
 449     // 2) x is not in the term t
 450     // 3) x : T and t : S, then S <: T
 451     if (in[0].isVar() && isLegalElimination(in[0], in[1])
 452         && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
 453     {
 454       outSubstitutions.addSubstitution(in[0], in[1]);
 455       return PP_ASSERT_STATUS_SOLVED;
 456     }
 457     if (in[1].isVar() && isLegalElimination(in[1], in[0])
 458         && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
 459     {
 460       outSubstitutions.addSubstitution(in[1], in[0]);
 461       return PP_ASSERT_STATUS_SOLVED;
 462     }
 463     if (in[0].isConst() && in[1].isConst())
 464     {
 465       if (in[0] != in[1])
 466       {
 467         return PP_ASSERT_STATUS_CONFLICT;
 468       }
 469     }
 470   }
 471
 472   return PP_ASSERT_STATUS_UNSOLVED;
 473 }
 474
 475 std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
 476 {
 477   return make_pair(false, Node::null());
 478 }
 479
 480 void Theory::addCarePair(TNode t1, TNode t2) {
 481   if (d_careGraph) {
 482     d_careGraph->insert(CarePair(t1, t2, d_id));
 483   }
 484 }
 485
 486 void Theory::getCareGraph(CareGraph* careGraph) {
 487   Assert(careGraph != NULL);
 488
 489   Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
 490   TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
 491   d_careGraph = careGraph;
 492   computeCareGraph();
 493   d_careGraph = NULL;
 494 }
 495
 496 EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
 497 {
 498   // if not using an equality engine, then by default we don't know the status
 499   if (d_equalityEngine == nullptr)
 500   {
 501     return EQUALITY_UNKNOWN;
 502   }
 503   Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
 504
 505   // Check for equality (simplest)
 506   if (d_equalityEngine->areEqual(a, b))
 507   {
 508     // The terms are implied to be equal
 509     return EQUALITY_TRUE;
 510   }
 511
 512   // Check for disequality
 513   if (d_equalityEngine->areDisequal(a, b, false))
 514   {
 515     // The terms are implied to be dis-equal
 516     return EQUALITY_FALSE;
 517   }
 518
 519   // All other terms are unknown, which is conservative. A theory may override
 520   // this method if it knows more information.
 521   return EQUALITY_UNKNOWN;
 522 }
 523
 524 void Theory::check(Effort level)
 525 {
 526   // see if we are already done (as an optimization)
 527   if (done() && level < EFFORT_FULL)
 528   {
 529     return;
 530   }
 531   Assert(d_theoryState!=nullptr);
 532   // standard calls for resource, stats
 533   d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
 534   TimerStat::CodeTimer checkTimer(d_checkTime);
 535   // pre-check at level
 536   if (preCheck(level))
 537   {
 538     // check aborted for a theory-specific reason
 539     return;
 540   }
 541   // process the pending fact queue
 542   while (!done() && !d_theoryState->isInConflict())
 543   {
 544     // Get the next assertion from the fact queue
 545     Assertion assertion = get();
 546     TNode fact = assertion.d_assertion;
 547     bool polarity = fact.getKind() != kind::NOT;
 548     TNode atom = polarity ? fact : fact[0];
 549     // call the pre-notify method
 550     if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
 551     {
 552       // handled in theory-specific way that doesn't involve equality engine
 553       continue;
 554     }
 555     // Theories that don't have an equality engine should always return true
 556     // for preNotifyFact
 557     Assert(d_equalityEngine != nullptr);
 558     // assert to the equality engine
 559     if (atom.getKind() == kind::EQUAL)
 560     {
 561       d_equalityEngine->assertEquality(atom, polarity, fact);
 562     }
 563     else
 564     {
 565       d_equalityEngine->assertPredicate(atom, polarity, fact);
 566     }
 567     // notify the theory of the new fact, which is not internal
 568     notifyFact(atom, polarity, fact, false);
 569   }
 570   // post-check at level
 571   postCheck(level);
 572 }
 573
 574 bool Theory::preCheck(Effort level) { return false; }
 575
 576 void Theory::postCheck(Effort level) {}
 577
 578 bool Theory::preNotifyFact(
 579     TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
 580 {
 581   return false;
 582 }
 583
 584 void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
 585 {
 586 }
 587
 588 void Theory::preRegisterTerm(TNode node) {}
 589
 590 void Theory::addSharedTerm(TNode n)
 591 {
 592   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
 593                    << std::endl;
 594   Debug("theory::assertions")
 595       << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
 596   d_sharedTerms.push_back(n);
 597   // now call theory-specific method notifySharedTerm
 598   notifySharedTerm(n);
 599 }
 600
 601 eq::EqualityEngine* Theory::getEqualityEngine()
 602 {
 603   // get the assigned equality engine, which is a pointer stored in this class
 604   return d_equalityEngine;
 605 }
 606
 607 }/* CVC4::theory namespace */
 608 }/* CVC4 namespace */