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