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/theory_options.h"
  27 #include "smt/smt_statistics_registry.h"
  28 #include "theory/ext_theory.h"
  29 #include "theory/quantifiers_engine.h"
  30 #include "theory/substitutions.h"
  31 #include "theory/theory_rewriter.h"
  32
  33 using namespace std;
  34
  35 namespace CVC4 {
  36 namespace theory {
  37
  38 /** Default value for the uninterpreted sorts is the UF theory */
  39 TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
  40
  41 std::ostream& operator<<(std::ostream& os, Theory::Effort level){
  42   switch(level){
  43   case Theory::EFFORT_STANDARD:
  44     os << "EFFORT_STANDARD"; break;
  45   case Theory::EFFORT_FULL:
  46     os << "EFFORT_FULL"; break;
  47   case Theory::EFFORT_COMBINATION:
  48     os << "EFFORT_COMBINATION"; break;
  49   case Theory::EFFORT_LAST_CALL:
  50     os << "EFFORT_LAST_CALL"; break;
  51   default:
  52       Unreachable();
  53   }
  54   return os;
  55 }/* ostream& operator<<(ostream&, Theory::Effort) */
  56
  57 Theory::Theory(TheoryId id,
  58                context::Context* satContext,
  59                context::UserContext* userContext,
  60                OutputChannel& out,
  61                Valuation valuation,
  62                const LogicInfo& logicInfo,
  63                ProofNodeManager* pnm,
  64                std::string name)
  65     : d_id(id),
  66       d_satContext(satContext),
  67       d_userContext(userContext),
  68       d_logicInfo(logicInfo),
  69       d_pnm(pnm),
  70       d_facts(satContext),
  71       d_factsHead(satContext, 0),
  72       d_sharedTermsIndex(satContext, 0),
  73       d_careGraph(NULL),
  74       d_quantEngine(NULL),
  75       d_decManager(nullptr),
  76       d_instanceName(name),
  77       d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
  78       d_computeCareGraphTime(getStatsPrefix(id) + name
  79                              + "::computeCareGraphTime"),
  80       d_sharedTerms(satContext),
  81       d_out(&out),
  82       d_valuation(valuation),
  83       d_equalityEngine(nullptr),
  84       d_allocEqualityEngine(nullptr),
  85       d_theoryState(nullptr),
  86       d_proofsEnabled(false)
  87 {
  88   smtStatisticsRegistry()->registerStat(&d_checkTime);
  89   smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
  90 }
  91
  92 Theory::~Theory() {
  93   smtStatisticsRegistry()->unregisterStat(&d_checkTime);
  94   smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
  95 }
  96
  97 bool Theory::needsEqualityEngine(EeSetupInfo& esi)
  98 {
  99   // by default, this theory does not use an (official) equality engine
 100   return false;
 101 }
 102
 103 void Theory::setEqualityEngine(eq::EqualityEngine* ee)
 104 {
 105   // set the equality engine pointer
 106   d_equalityEngine = ee;
 107   if (d_theoryState != nullptr)
 108   {
 109     d_theoryState->setEqualityEngine(ee);
 110   }
 111 }
 112 void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
 113 {
 114   Assert(d_quantEngine == nullptr);
 115   d_quantEngine = qe;
 116 }
 117
 118 void Theory::setDecisionManager(DecisionManager* dm)
 119 {
 120   Assert(d_decManager == nullptr);
 121   Assert(dm != nullptr);
 122   d_decManager = dm;
 123 }
 124
 125 void Theory::finishInitStandalone()
 126 {
 127   EeSetupInfo esi;
 128   if (needsEqualityEngine(esi))
 129   {
 130     // always associated with the same SAT context as the theory (d_satContext)
 131     d_allocEqualityEngine.reset(new eq::EqualityEngine(
 132         *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
 133     // use it as the official equality engine
 134     setEqualityEngine(d_allocEqualityEngine.get());
 135   }
 136   finishInit();
 137 }
 138
 139 TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
 140 {
 141   TheoryId tid = THEORY_BUILTIN;
 142   switch(mode) {
 143     case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
 144       // Constants, variables, 0-ary constructors
 145       if (node.isVar())
 146       {
 147         if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 148         {
 149           tid = THEORY_UF;
 150         }
 151         else
 152         {
 153           tid = Theory::theoryOf(node.getType());
 154         }
 155       }
 156       else if (node.isConst())
 157       {
 158         tid = Theory::theoryOf(node.getType());
 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
 168         tid = kindToTheoryId(node.getKind());
 169       }
 170       break;
 171     case options::TheoryOfMode::THEORY_OF_TERM_BASED:
 172       // Variables
 173       if (node.isVar())
 174       {
 175         if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
 176         {
 177           // We treat the variables as uninterpreted
 178           tid = s_uninterpretedSortOwner;
 179         }
 180         else
 181         {
 182           if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 183           {
 184             // Boolean vars go to UF
 185             tid = THEORY_UF;
 186           }
 187           else
 188           {
 189             // Except for the Boolean ones
 190             tid = THEORY_BOOL;
 191           }
 192         }
 193       }
 194       else if (node.isConst())
 195       {
 196         // Constants go to the theory of the type
 197         tid = Theory::theoryOf(node.getType());
 198       }
 199       else if (node.getKind() == kind::EQUAL)
 200       {  // Equality
 201         // If one of them is an ITE, it's irelevant, since they will get
 202         // replaced out anyhow
 203         if (node[0].getKind() == kind::ITE)
 204         {
 205           tid = Theory::theoryOf(node[0].getType());
 206         }
 207         else if (node[1].getKind() == kind::ITE)
 208         {
 209           tid = Theory::theoryOf(node[1].getType());
 210         }
 211         else
 212         {
 213           TNode l = node[0];
 214           TNode r = node[1];
 215           TypeNode ltype = l.getType();
 216           TypeNode rtype = r.getType();
 217           if (ltype != rtype)
 218           {
 219             tid = Theory::theoryOf(l.getType());
 220           }
 221           else
 222           {
 223             // If both sides belong to the same theory the choice is easy
 224             TheoryId T1 = Theory::theoryOf(l);
 225             TheoryId T2 = Theory::theoryOf(r);
 226             if (T1 == T2)
 227             {
 228               tid = T1;
 229             }
 230             else
 231             {
 232               TheoryId T3 = Theory::theoryOf(ltype);
 233               // This is a case of
 234               // * x*y = f(z) -> UF
 235               // * x = c      -> UF
 236               // * f(x) = read(a, y) -> either UF or ARRAY
 237               // at least one of the theories has to be parametric, i.e. theory
 238               // of the type is different from the theory of the term
 239               if (T1 == T3)
 240               {
 241                 tid = T2;
 242               }
 243               else if (T2 == T3)
 244               {
 245                 tid = T1;
 246               }
 247               else
 248               {
 249                 // If both are parametric, we take the smaller one (arbitrary)
 250                 tid = T1 < T2 ? T1 : T2;
 251               }
 252             }
 253           }
 254         }
 255       }
 256       else
 257       {
 258         // Regular nodes are owned by the kind
 259         tid = kindToTheoryId(node.getKind());
 260       }
 261     break;
 262   default:
 263     Unreachable();
 264   }
 265   Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
 266   return tid;
 267 }
 268
 269 void Theory::addSharedTermInternal(TNode n) {
 270   Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 271   Debug("theory::assertions") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << endl;
 272   d_sharedTerms.push_back(n);
 273   addSharedTerm(n);
 274 }
 275
 276 void Theory::computeCareGraph() {
 277   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 278   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 279     TNode a = d_sharedTerms[i];
 280     TypeNode aType = a.getType();
 281     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 282       TNode b = d_sharedTerms[j];
 283       if (b.getType() != aType) {
 284         // We don't care about the terms of different types
 285         continue;
 286       }
 287       switch (d_valuation.getEqualityStatus(a, b)) {
 288       case EQUALITY_TRUE_AND_PROPAGATED:
 289       case EQUALITY_FALSE_AND_PROPAGATED:
 290         // If we know about it, we should have propagated it, so we can skip
 291         break;
 292       default:
 293         // Let's split on it
 294         addCarePair(a, b);
 295         break;
 296       }
 297     }
 298   }
 299 }
 300
 301 void Theory::printFacts(std::ostream& os) const {
 302   unsigned i, n = d_facts.size();
 303   for(i = 0; i < n; i++){
 304     const Assertion& a_i = d_facts[i];
 305     Node assertion  = a_i;
 306     os << d_id << '[' << i << ']' << " " << assertion << endl;
 307   }
 308 }
 309
 310 void Theory::debugPrintFacts() const{
 311   DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
 312   printFacts(DebugChannel.getStream());
 313 }
 314
 315 bool Theory::isLegalElimination(TNode x, TNode val)
 316 {
 317   Assert(x.isVar());
 318   if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
 319       || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
 320   {
 321     return false;
 322   }
 323   if (expr::hasSubterm(val, x))
 324   {
 325     return false;
 326   }
 327   if (!val.getType().isSubtypeOf(x.getType()))
 328   {
 329     return false;
 330   }
 331   if (!options::produceModels())
 332   {
 333     // don't care about the model, we are fine
 334     return true;
 335   }
 336   // if there is a model object
 337   TheoryModel* tm = d_valuation.getModel();
 338   Assert(tm != nullptr);
 339   return tm->isLegalElimination(x, val);
 340 }
 341
 342 std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
 343   std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
 344   for (shared_terms_iterator i = shared_terms_begin(),
 345            i_end = shared_terms_end(); i != i_end; ++i) {
 346     currentlyShared.insert (*i);
 347   }
 348   return currentlyShared;
 349 }
 350
 351 bool Theory::collectModelInfo(TheoryModel* m)
 352 {
 353   std::set<Node> termSet;
 354   // Compute terms appearing in assertions and shared terms
 355   computeRelevantTerms(termSet);
 356   // if we are using an equality engine, assert it to the model
 357   if (d_equalityEngine != nullptr)
 358   {
 359     if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
 360     {
 361       return false;
 362     }
 363   }
 364   // now, collect theory-specific value assigments
 365   return collectModelValues(m, termSet);
 366 }
 367
 368 void Theory::collectTerms(TNode n,
 369                           set<Kind>& irrKinds,
 370                           set<Node>& termSet) const
 371 {
 372   if (termSet.find(n) != termSet.end()) {
 373     return;
 374   }
 375   Kind nk = n.getKind();
 376   if (irrKinds.find(nk) == irrKinds.end())
 377   {
 378     Trace("theory::collectTerms")
 379         << "Theory::collectTerms: adding " << n << endl;
 380     termSet.insert(n);
 381   }
 382   if (nk == kind::NOT || nk == kind::EQUAL || !isLeaf(n))
 383   {
 384     for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
 385       collectTerms(*child_it, irrKinds, termSet);
 386     }
 387   }
 388 }
 389
 390 void Theory::computeRelevantTermsInternal(std::set<Node>& termSet,
 391                                           std::set<Kind>& irrKinds,
 392                                           bool includeShared) const
 393 {
 394   // Collect all terms appearing in assertions
 395   irrKinds.insert(kind::EQUAL);
 396   irrKinds.insert(kind::NOT);
 397   context::CDList<Assertion>::const_iterator assert_it = facts_begin(), assert_it_end = facts_end();
 398   for (; assert_it != assert_it_end; ++assert_it) {
 399     collectTerms(*assert_it, irrKinds, termSet);
 400   }
 401
 402   if (!includeShared) return;
 403
 404   // Add terms that are shared terms
 405   set<Kind> kempty;
 406   context::CDList<TNode>::const_iterator shared_it = shared_terms_begin(), shared_it_end = shared_terms_end();
 407   for (; shared_it != shared_it_end; ++shared_it) {
 408     collectTerms(*shared_it, kempty, termSet);
 409   }
 410 }
 411
 412 void Theory::computeRelevantTerms(std::set<Node>& termSet, bool includeShared)
 413 {
 414   std::set<Kind> irrKinds;
 415   computeRelevantTermsInternal(termSet, irrKinds, includeShared);
 416 }
 417
 418 bool Theory::collectModelValues(TheoryModel* m, std::set<Node>& termSet)
 419 {
 420   return true;
 421 }
 422
 423 Theory::PPAssertStatus Theory::ppAssert(TNode in,
 424                                         SubstitutionMap& outSubstitutions)
 425 {
 426   if (in.getKind() == kind::EQUAL)
 427   {
 428     // (and (= x t) phi) can be replaced by phi[x/t] if
 429     // 1) x is a variable
 430     // 2) x is not in the term t
 431     // 3) x : T and t : S, then S <: T
 432     if (in[0].isVar() && isLegalElimination(in[0], in[1])
 433         && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
 434     {
 435       outSubstitutions.addSubstitution(in[0], in[1]);
 436       return PP_ASSERT_STATUS_SOLVED;
 437     }
 438     if (in[1].isVar() && isLegalElimination(in[1], in[0])
 439         && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
 440     {
 441       outSubstitutions.addSubstitution(in[1], in[0]);
 442       return PP_ASSERT_STATUS_SOLVED;
 443     }
 444     if (in[0].isConst() && in[1].isConst())
 445     {
 446       if (in[0] != in[1])
 447       {
 448         return PP_ASSERT_STATUS_CONFLICT;
 449       }
 450     }
 451   }
 452
 453   return PP_ASSERT_STATUS_UNSOLVED;
 454 }
 455
 456 std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
 457 {
 458   return make_pair(false, Node::null());
 459 }
 460
 461 void Theory::addCarePair(TNode t1, TNode t2) {
 462   if (d_careGraph) {
 463     d_careGraph->insert(CarePair(t1, t2, d_id));
 464   }
 465 }
 466
 467 void Theory::getCareGraph(CareGraph* careGraph) {
 468   Assert(careGraph != NULL);
 469
 470   Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
 471   TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
 472   d_careGraph = careGraph;
 473   computeCareGraph();
 474   d_careGraph = NULL;
 475 }
 476
 477 eq::EqualityEngine* Theory::getEqualityEngine()
 478 {
 479   // get the assigned equality engine, which is a pointer stored in this class
 480   return d_equalityEngine;
 481 }
 482
 483 }/* CVC4::theory namespace */
 484 }/* CVC4 namespace */