src/theory/theory.cpp

   1 /*********************                                                        */
   2 /*! \file theory.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Tim King, Mathias Preiner
   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_facts(satContext),
  69       d_factsHead(satContext, 0),
  70       d_sharedTermsIndex(satContext, 0),
  71       d_careGraph(nullptr),
  72       d_decManager(nullptr),
  73       d_instanceName(name),
  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_equalityEngine(nullptr),
  81       d_allocEqualityEngine(nullptr),
  82       d_theoryState(nullptr),
  83       d_inferManager(nullptr),
  84       d_quantEngine(nullptr),
  85       d_pnm(pnm)
  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   // quantifiers engine may be null if not in quantified logic
 119   d_quantEngine = qe;
 120 }
 121
 122 void Theory::setDecisionManager(DecisionManager* dm)
 123 {
 124   Assert(d_decManager == nullptr);
 125   Assert(dm != nullptr);
 126   d_decManager = dm;
 127 }
 128
 129 void Theory::finishInitStandalone()
 130 {
 131   EeSetupInfo esi;
 132   if (needsEqualityEngine(esi))
 133   {
 134     // always associated with the same SAT context as the theory (d_satContext)
 135     d_allocEqualityEngine.reset(new eq::EqualityEngine(
 136         *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
 137     // use it as the official equality engine
 138     setEqualityEngine(d_allocEqualityEngine.get());
 139   }
 140   finishInit();
 141 }
 142
 143 TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
 144 {
 145   TheoryId tid = THEORY_BUILTIN;
 146   switch(mode) {
 147     case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
 148       // Constants, variables, 0-ary constructors
 149       if (node.isVar())
 150       {
 151         if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 152         {
 153           tid = THEORY_UF;
 154         }
 155         else
 156         {
 157           tid = Theory::theoryOf(node.getType());
 158         }
 159       }
 160       else if (node.getKind() == kind::EQUAL)
 161       {
 162         // Equality is owned by the theory that owns the domain
 163         tid = Theory::theoryOf(node[0].getType());
 164       }
 165       else
 166       {
 167         // Regular nodes are owned by the kind. Notice that constants are a
 168         // special case here, where the theory of the kind of a constant
 169         // always coincides with the type of that constant.
 170         tid = kindToTheoryId(node.getKind());
 171       }
 172       break;
 173     case options::TheoryOfMode::THEORY_OF_TERM_BASED:
 174       // Variables
 175       if (node.isVar())
 176       {
 177         if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
 178         {
 179           // We treat the variables as uninterpreted
 180           tid = s_uninterpretedSortOwner;
 181         }
 182         else
 183         {
 184           if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 185           {
 186             // Boolean vars go to UF
 187             tid = THEORY_UF;
 188           }
 189           else
 190           {
 191             // Except for the Boolean ones
 192             tid = THEORY_BOOL;
 193           }
 194         }
 195       }
 196       else if (node.getKind() == kind::EQUAL)
 197       {  // Equality
 198         // If one of them is an ITE, it's irelevant, since they will get
 199         // replaced out anyhow
 200         if (node[0].getKind() == kind::ITE)
 201         {
 202           tid = Theory::theoryOf(node[0].getType());
 203         }
 204         else if (node[1].getKind() == kind::ITE)
 205         {
 206           tid = Theory::theoryOf(node[1].getType());
 207         }
 208         else
 209         {
 210           TNode l = node[0];
 211           TNode r = node[1];
 212           TypeNode ltype = l.getType();
 213           TypeNode rtype = r.getType();
 214           if (ltype != rtype)
 215           {
 216             tid = Theory::theoryOf(l.getType());
 217           }
 218           else
 219           {
 220             // If both sides belong to the same theory the choice is easy
 221             TheoryId T1 = Theory::theoryOf(l);
 222             TheoryId T2 = Theory::theoryOf(r);
 223             if (T1 == T2)
 224             {
 225               tid = T1;
 226             }
 227             else
 228             {
 229               TheoryId T3 = Theory::theoryOf(ltype);
 230               // This is a case of
 231               // * x*y = f(z) -> UF
 232               // * x = c      -> UF
 233               // * f(x) = read(a, y) -> either UF or ARRAY
 234               // at least one of the theories has to be parametric, i.e. theory
 235               // of the type is different from the theory of the term
 236               if (T1 == T3)
 237               {
 238                 tid = T2;
 239               }
 240               else if (T2 == T3)
 241               {
 242                 tid = T1;
 243               }
 244               else
 245               {
 246                 // If both are parametric, we take the smaller one (arbitrary)
 247                 tid = T1 < T2 ? T1 : T2;
 248               }
 249             }
 250           }
 251         }
 252       }
 253       else
 254       {
 255         // Regular nodes are owned by the kind, which includes constants as a
 256         // special case.
 257         tid = kindToTheoryId(node.getKind());
 258       }
 259     break;
 260   default:
 261     Unreachable();
 262   }
 263   Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
 264   return tid;
 265 }
 266
 267 void Theory::notifySharedTerm(TNode n)
 268 {
 269   // do nothing
 270 }
 271
 272 void Theory::computeCareGraph() {
 273   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 274   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 275     TNode a = d_sharedTerms[i];
 276     TypeNode aType = a.getType();
 277     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 278       TNode b = d_sharedTerms[j];
 279       if (b.getType() != aType) {
 280         // We don't care about the terms of different types
 281         continue;
 282       }
 283       switch (d_valuation.getEqualityStatus(a, b)) {
 284       case EQUALITY_TRUE_AND_PROPAGATED:
 285       case EQUALITY_FALSE_AND_PROPAGATED:
 286         // If we know about it, we should have propagated it, so we can skip
 287         break;
 288       default:
 289         // Let's split on it
 290         addCarePair(a, b);
 291         break;
 292       }
 293     }
 294   }
 295 }
 296
 297 void Theory::printFacts(std::ostream& os) const {
 298   unsigned i, n = d_facts.size();
 299   for(i = 0; i < n; i++){
 300     const Assertion& a_i = d_facts[i];
 301     Node assertion  = a_i;
 302     os << d_id << '[' << i << ']' << " " << assertion << endl;
 303   }
 304 }
 305
 306 void Theory::debugPrintFacts() const{
 307   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 308   printFacts(DebugChannel.getStream());
 309 }
 310
 311 bool Theory::isLegalElimination(TNode x, TNode val)
 312 {
 313   Assert(x.isVar());
 314   if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
 315       || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 316   {
 317     return false;
 318   }
 319   if (expr::hasSubterm(val, x))
 320   {
 321     return false;
 322   }
 323   if (!val.getType().isSubtypeOf(x.getType()))
 324   {
 325     return false;
 326   }
 327   if (!options::produceModels())
 328   {
 329     // don't care about the model, we are fine
 330     return true;
 331   }
 332   // if there is a model object
 333   TheoryModel* tm = d_valuation.getModel();
 334   Assert(tm != nullptr);
 335   return tm->isLegalElimination(x, val);
 336 }
 337
 338 std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 339   std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
 340   for (shared_terms_iterator i = shared_terms_begin(),
 341            i_end = shared_terms_end(); i != i_end; ++i) {
 342     currentlyShared.insert (*i);
 343   }
 344   return currentlyShared;
 345 }
 346
 347 bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
 348 {
 349   // if we are using an equality engine, assert it to the model
 350   if (d_equalityEngine != nullptr)
 351   {
 352     if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
 353     {
 354       return false;
 355     }
 356   }
 357   // now, collect theory-specific value assigments
 358   return collectModelValues(m, termSet);
 359 }
 360
 361 void Theory::computeRelevantTerms(std::set<Node>& termSet)
 362 {
 363   // by default, there are no additional relevant terms
 364 }
 365
 366 bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 367 {
 368   return true;
 369 }
 370
 371 Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
 372                                         TrustSubstitutionMap& outSubstitutions)
 373 {
 374   TNode in = tin.getNode();
 375   if (in.getKind() == kind::EQUAL)
 376   {
 377     // (and (= x t) phi) can be replaced by phi[x/t] if
 378     // 1) x is a variable
 379     // 2) x is not in the term t
 380     // 3) x : T and t : S, then S <: T
 381     if (in[0].isVar() && isLegalElimination(in[0], in[1])
 382         && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
 383     {
 384       outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
 385       return PP_ASSERT_STATUS_SOLVED;
 386     }
 387     if (in[1].isVar() && isLegalElimination(in[1], in[0])
 388         && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
 389     {
 390       outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
 391       return PP_ASSERT_STATUS_SOLVED;
 392     }
 393     if (in[0].isConst() && in[1].isConst())
 394     {
 395       if (in[0] != in[1])
 396       {
 397         return PP_ASSERT_STATUS_CONFLICT;
 398       }
 399     }
 400   }
 401
 402   return PP_ASSERT_STATUS_UNSOLVED;
 403 }
 404
 405 std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
 406 {
 407   return make_pair(false, Node::null());
 408 }
 409
 410 void Theory::addCarePair(TNode t1, TNode t2) {
 411   if (d_careGraph) {
 412     d_careGraph->insert(CarePair(t1, t2, d_id));
 413   }
 414 }
 415
 416 void Theory::getCareGraph(CareGraph* careGraph) {
 417   Assert(careGraph != NULL);
 418
 419   Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
 420   TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
 421   d_careGraph = careGraph;
 422   computeCareGraph();
 423   d_careGraph = NULL;
 424 }
 425
 426 bool Theory::proofsEnabled() const
 427 {
 428   return d_pnm != nullptr;
 429 }
 430
 431 EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
 432 {
 433   // if not using an equality engine, then by default we don't know the status
 434   if (d_equalityEngine == nullptr)
 435   {
 436     return EQUALITY_UNKNOWN;
 437   }
 438   Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
 439   Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
 440
 441   // Check for equality (simplest)
 442   if (d_equalityEngine->areEqual(a, b))
 443   {
 444     // The terms are implied to be equal
 445     return EQUALITY_TRUE;
 446   }
 447
 448   // Check for disequality
 449   if (d_equalityEngine->areDisequal(a, b, false))
 450   {
 451     // The terms are implied to be dis-equal
 452     return EQUALITY_FALSE;
 453   }
 454
 455   // All other terms are unknown, which is conservative. A theory may override
 456   // this method if it knows more information.
 457   return EQUALITY_UNKNOWN;
 458 }
 459
 460 void Theory::check(Effort level)
 461 {
 462   // see if we are already done (as an optimization)
 463   if (done() && level < EFFORT_FULL)
 464   {
 465     return;
 466   }
 467   Assert(d_theoryState!=nullptr);
 468   // standard calls for resource, stats
 469   d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
 470   TimerStat::CodeTimer checkTimer(d_checkTime);
 471   Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
 472                         << std::endl;
 473   // pre-check at level
 474   if (preCheck(level))
 475   {
 476     // check aborted for a theory-specific reason
 477     return;
 478   }
 479   Assert(d_theoryState != nullptr);
 480   Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
 481   // process the pending fact queue
 482   while (!done() && !d_theoryState->isInConflict())
 483   {
 484     // Get the next assertion from the fact queue
 485     Assertion assertion = get();
 486     TNode fact = assertion.d_assertion;
 487     Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
 488                           << std::endl;
 489     bool polarity = fact.getKind() != kind::NOT;
 490     TNode atom = polarity ? fact : fact[0];
 491     // call the pre-notify method
 492     if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
 493     {
 494       // handled in theory-specific way that doesn't involve equality engine
 495       continue;
 496     }
 497     Trace("theory-check") << "Theory::assert " << fact << " " << d_id
 498                           << std::endl;
 499     // Theories that don't have an equality engine should always return true
 500     // for preNotifyFact
 501     Assert(d_equalityEngine != nullptr);
 502     // assert to the equality engine
 503     if (atom.getKind() == kind::EQUAL)
 504     {
 505       d_equalityEngine->assertEquality(atom, polarity, fact);
 506     }
 507     else
 508     {
 509       d_equalityEngine->assertPredicate(atom, polarity, fact);
 510     }
 511     Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
 512                           << std::endl;
 513     // notify the theory of the new fact, which is not internal
 514     notifyFact(atom, polarity, fact, false);
 515   }
 516   Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
 517   // post-check at level
 518   postCheck(level);
 519   Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
 520 }
 521
 522 bool Theory::preCheck(Effort level) { return false; }
 523
 524 void Theory::postCheck(Effort level) {}
 525
 526 bool Theory::preNotifyFact(
 527     TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
 528 {
 529   return false;
 530 }
 531
 532 void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
 533 {
 534 }
 535
 536 void Theory::preRegisterTerm(TNode node) {}
 537
 538 void Theory::addSharedTerm(TNode n)
 539 {
 540   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
 541                    << std::endl;
 542   Debug("theory::assertions")
 543       << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
 544   d_sharedTerms.push_back(n);
 545   // now call theory-specific method notifySharedTerm
 546   notifySharedTerm(n);
 547   // if we have an equality engine, add the trigger term
 548   if (d_equalityEngine != nullptr)
 549   {
 550     d_equalityEngine->addTriggerTerm(n, d_id);
 551   }
 552 }
 553
 554 eq::EqualityEngine* Theory::getEqualityEngine()
 555 {
 556   // get the assigned equality engine, which is a pointer stored in this class
 557   return d_equalityEngine;
 558 }
 559
 560 }/* CVC4::theory namespace */
 561 }/* CVC4 namespace */