src/theory/theory.cpp

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