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