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