src/theory/theory_engine.h

   1 /*********************                                                        */
   2 /*! \file theory_engine.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: taking, dejan
   6  ** Minor contributors (to current version): cconway, barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief The theory engine
  15  **
  16  ** The theory engine.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY_ENGINE_H
  22 #define __CVC4__THEORY_ENGINE_H
  23
  24 #include <deque>
  25 #include <vector>
  26 #include <utility>
  27
  28 #include "expr/node.h"
  29 #include "prop/prop_engine.h"
  30 #include "theory/shared_term_manager.h"
  31 #include "theory/theory.h"
  32 #include "theory/rewriter.h"
  33 #include "theory/substitutions.h"
  34 #include "theory/valuation.h"
  35 #include "util/options.h"
  36 #include "util/stats.h"
  37 #include "util/hash.h"
  38 #include "util/cache.h"
  39
  40 namespace CVC4 {
  41
  42 // In terms of abstraction, this is below (and provides services to)
  43 // PropEngine.
  44
  45 /**
  46  * This is essentially an abstraction for a collection of theories.  A
  47  * TheoryEngine provides services to a PropEngine, making various
  48  * T-solvers look like a single unit to the propositional part of
  49  * CVC4.
  50  */
  51 class TheoryEngine {
  52
  53   /** Associated PropEngine engine */
  54   prop::PropEngine* d_propEngine;
  55
  56   /** Our context */
  57   context::Context* d_context;
  58
  59   /** A table of from theory IDs to theory pointers */
  60   theory::Theory* d_theoryTable[theory::THEORY_LAST];
  61
  62   /**
  63    * A bitmap of theories that are "active" for the current run.  We
  64    * mark a theory active when we firt see a term or type belonging to
  65    * it.  This is important because we can optimize for single-theory
  66    * runs (no sharing), can reduce the cost of walking the DAG on
  67    * registration, etc.
  68    */
  69   bool d_theoryIsActive[theory::THEORY_LAST];
  70
  71   /**
  72    * The count of active theories in the d_theoryIsActive bitmap.
  73    */
  74   size_t d_activeTheories;
  75
  76   /**
  77    * Need the registration infrastructure when theory sharing is on
  78    * (>=2 active theories) or when the sole active theory has
  79    * requested it.
  80    */
  81   bool d_needRegistration;
  82
  83   /**
  84    * The type of the simplification cache.
  85    */
  86   typedef Cache<Node, std::pair<Node, theory::Substitutions>, NodeHashFunction> SimplifyCache;
  87
  88   /**
  89    * A cache for simplification.
  90    */
  91   SimplifyCache d_simplifyCache;
  92
  93   /**
  94    * An output channel for Theory that passes messages
  95    * back to a TheoryEngine.
  96    */
  97   class EngineOutputChannel : public theory::OutputChannel {
  98
  99     friend class TheoryEngine;
 100
 101     TheoryEngine* d_engine;
 102     context::Context* d_context;
 103     context::CDO<Node> d_conflictNode;
 104     context::CDO<Node> d_explanationNode;
 105
 106     /**
 107      * Literals that are propagated by the theory. Note that these are TNodes.
 108      * The theory can only propagate nodes that have an assigned literal in the
 109      * sat solver and are hence referenced in the SAT solver.
 110      */
 111     std::vector<TNode> d_propagatedLiterals;
 112
 113     /** Time spent in newFact() (largely spent doing term registration) */
 114     KEEP_STATISTIC(TimerStat,
 115                    d_newFactTimer,
 116                    "theory::newFactTimer");
 117
 118   public:
 119
 120     EngineOutputChannel(TheoryEngine* engine, context::Context* context) :
 121       d_engine(engine),
 122       d_context(context),
 123       d_conflictNode(context),
 124       d_explanationNode(context) {
 125     }
 126
 127     void newFact(TNode n);
 128
 129     void conflict(TNode conflictNode, bool safe)
 130       throw(theory::Interrupted, AssertionException) {
 131       Debug("theory") << "EngineOutputChannel::conflict("
 132                       << conflictNode << ")" << std::endl;
 133       d_conflictNode = conflictNode;
 134       ++(d_engine->d_statistics.d_statConflicts);
 135       if(safe) {
 136         throw theory::Interrupted();
 137       }
 138     }
 139
 140     void propagate(TNode lit, bool)
 141       throw(theory::Interrupted, AssertionException) {
 142       Debug("theory") << "EngineOutputChannel::propagate("
 143                       << lit << ")" << std::endl;
 144       d_propagatedLiterals.push_back(lit);
 145       ++(d_engine->d_statistics.d_statPropagate);
 146     }
 147
 148     void lemma(TNode node, bool)
 149       throw(theory::Interrupted, AssertionException) {
 150       Debug("theory") << "EngineOutputChannel::lemma("
 151                       << node << ")" << std::endl;
 152       ++(d_engine->d_statistics.d_statLemma);
 153       d_engine->newLemma(node);
 154     }
 155
 156     void explanation(TNode explanationNode, bool)
 157       throw(theory::Interrupted, AssertionException) {
 158       Debug("theory") << "EngineOutputChannel::explanation("
 159                       << explanationNode << ")" << std::endl;
 160       d_explanationNode = explanationNode;
 161       ++(d_engine->d_statistics.d_statExplanation);
 162     }
 163
 164     void setIncomplete()
 165       throw(theory::Interrupted, AssertionException) {
 166       d_engine->d_incomplete = true;
 167     }
 168   };/* class EngineOutputChannel */
 169
 170   EngineOutputChannel d_theoryOut;
 171
 172   /** Pointer to Shared Term Manager */
 173   SharedTermManager* d_sharedTermManager;
 174
 175   /**
 176    * Whether or not theory registration is on.  May not be safe to
 177    * turn off with some theories.
 178    */
 179   bool d_theoryRegistration;
 180
 181   /**
 182    * Debugging flag to ensure that shutdown() is called before the
 183    * destructor.
 184    */
 185   bool d_hasShutDown;
 186
 187   /**
 188    * True if a theory has notified us of incompleteness (at this
 189    * context level or below).
 190    */
 191   context::CDO<bool> d_incomplete;
 192
 193   /**
 194    * Replace ITE forms in a node.
 195    */
 196   Node removeITEs(TNode t);
 197
 198   /**
 199    * Mark a theory active if it's not already.
 200    */
 201   void markActive(theory::TheoryId th) {
 202     if(!d_theoryIsActive[th]) {
 203       d_theoryIsActive[th] = true;
 204       if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) {
 205         if(++d_activeTheories == 1) {
 206           // theory requests registration
 207           d_needRegistration = hasRegisterTerm(th);
 208         } else {
 209           // need it for sharing
 210           d_needRegistration = true;
 211         }
 212       }
 213       Notice() << "Theory " << th << " has been activated (registration is "
 214                << (d_needRegistration ? "on" : "off") << ")." << std::endl;
 215     }
 216   }
 217
 218   bool hasRegisterTerm(theory::TheoryId th) const;
 219
 220 public:
 221   /** The logic of the problem */
 222   std::string d_logic;
 223
 224   /** Constructs a theory engine */
 225   TheoryEngine(context::Context* ctxt);
 226
 227   /** Destroys a theory engine */
 228   ~TheoryEngine();
 229
 230   /**
 231    * Adds a theory. Only one theory per TheoryId can be present, so if
 232    * there is another theory it will be deleted.
 233    */
 234   template <class TheoryClass>
 235   void addTheory() {
 236     TheoryClass* theory =
 237       new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
 238     d_theoryTable[theory->getId()] = theory;
 239     d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
 240   }
 241
 242   SharedTermManager* getSharedTermManager() {
 243     return d_sharedTermManager;
 244   }
 245
 246   void setPropEngine(prop::PropEngine* propEngine) {
 247     Assert(d_propEngine == NULL);
 248     d_propEngine = propEngine;
 249   }
 250
 251   /**
 252    * Get a pointer to the underlying propositional engine.
 253    */
 254   prop::PropEngine* getPropEngine() const {
 255     return d_propEngine;
 256   }
 257
 258   /**
 259    * Return whether or not we are incomplete (in the current context).
 260    */
 261   bool isIncomplete() {
 262     return d_incomplete;
 263   }
 264
 265   /**
 266    * This is called at shutdown time by the SmtEngine, just before
 267    * destruction.  It is important because there are destruction
 268    * ordering issues between PropEngine and Theory.
 269    */
 270   void shutdown() {
 271     // Set this first; if a Theory shutdown() throws an exception,
 272     // at least the destruction of the TheoryEngine won't confound
 273     // matters.
 274     d_hasShutDown = true;
 275
 276     // Shutdown all the theories
 277     for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
 278       if(d_theoryTable[theoryId]) {
 279         d_theoryTable[theoryId]->shutdown();
 280       }
 281     }
 282
 283     theory::Rewriter::shutdown();
 284   }
 285
 286   /**
 287    * Get the theory associated to a given Node.
 288    *
 289    * @returns the theory, or NULL if the TNode is
 290    * of built-in type.
 291    */
 292   inline theory::Theory* theoryOf(TNode node) {
 293     return d_theoryTable[theory::Theory::theoryOf(node)];
 294   }
 295
 296   /**
 297    * Get the theory associated to a given Node.
 298    *
 299    * @returns the theory, or NULL if the TNode is
 300    * of built-in type.
 301    */
 302   inline theory::Theory* theoryOf(const TypeNode& typeNode) {
 303     return d_theoryTable[theory::Theory::theoryOf(typeNode)];
 304   }
 305
 306   /**
 307    * Preprocess a node.  This involves ITE removal and theory-specific
 308    * rewriting.
 309    *
 310    * @param n the node to preprocess
 311    */
 312   Node preprocess(TNode n);
 313
 314   /**
 315    * Preregister a Theory atom with the responsible theory (or
 316    * theories).
 317    */
 318   void preRegister(TNode preprocessed);
 319
 320   /**
 321    * Assert the formula to the appropriate theory.
 322    * @param node the assertion
 323    */
 324   inline void assertFact(TNode node) {
 325     Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl<<d_logic<<std::endl;
 326
 327     // Mark it as asserted in this context
 328     //
 329     // [MGD] removed for now, this appears to have a nontrivial
 330     // performance penalty
 331     // node.setAttribute(theory::Asserted(), true);
 332
 333     // Get the atom
 334     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 335
 336     // Again, equality is a special case
 337     if (atom.getKind() == kind::EQUAL) {
 338       if(d_logic == "QF_AX") {
 339         //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n";
 340         d_theoryTable[theory::THEORY_ARRAY]->assertFact(node);
 341       } else {
 342         theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]);
 343         Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl;
 344         d_theoryTable[theoryLHS]->assertFact(node);
 345 //      theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]);
 346 //      if (theoryLHS != theoryRHS) {
 347 //        Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl;
 348 //        d_theoryTable[theoryRHS]->assertFact(node);
 349 //      }
 350 //      theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType());
 351 //      if (typeTheory!= theoryLHS && typeTheory != theoryRHS) {
 352 //        Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl;
 353 //        d_theoryTable[typeTheory]->assertFact(node);
 354 //      }
 355       }
 356     } else {
 357       theory::Theory* theory = theoryOf(atom);
 358       Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
 359       theory->assertFact(node);
 360     }
 361   }
 362
 363   /**
 364    * Check all (currently-active) theories for conflicts.
 365    * @param effort the effort level to use
 366    */
 367   bool check(theory::Theory::Effort effort);
 368
 369   /**
 370    * Calls staticLearning() on all theories, accumulating their
 371    * combined contributions in the "learned" builder.
 372    */
 373   void staticLearning(TNode in, NodeBuilder<>& learned);
 374
 375   /**
 376    * Calls simplify() on all theories, accumulating their combined
 377    * contributions in the "outSubstitutions" vector.
 378    */
 379   Node simplify(TNode in, theory::Substitutions& outSubstitutions);
 380
 381   /**
 382    * Calls presolve() on all active theories and returns true
 383    * if one of the theories discovers a conflict.
 384    */
 385   bool presolve();
 386
 387   /**
 388    * Calls notifyRestart() on all active theories.
 389    */
 390   void notifyRestart();
 391
 392   inline const std::vector<TNode>& getPropagatedLiterals() const {
 393     return d_theoryOut.d_propagatedLiterals;
 394   }
 395
 396   void clearPropagatedLiterals() {
 397     d_theoryOut.d_propagatedLiterals.clear();
 398   }
 399
 400   inline void newLemma(TNode node) {
 401     d_propEngine->assertLemma(preprocess(node));
 402   }
 403
 404   /**
 405    * Returns the last conflict (if any).
 406    */
 407   inline Node getConflict() {
 408     return d_theoryOut.d_conflictNode;
 409   }
 410
 411   void propagate();
 412
 413   inline Node getExplanation(TNode node, theory::Theory* theory) {
 414     theory->explain(node);
 415     return d_theoryOut.d_explanationNode;
 416   }
 417
 418   inline Node getExplanation(TNode node) {
 419     d_theoryOut.d_explanationNode = Node::null();
 420     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 421     if (atom.getKind() == kind::EQUAL) {
 422       if(d_logic == "QF_AX") {
 423         //Debug("theory")<< "TheoryEngine::assertFact QF_AX logic; everything goes to Arrays \n";
 424         d_theoryTable[theory::THEORY_ARRAY]->explain(node);
 425       } else {
 426         theoryOf(atom[0])->explain(node);
 427       }
 428     } else {
 429       theoryOf(atom)->explain(node);
 430     }
 431     Assert(!d_theoryOut.d_explanationNode.get().isNull());
 432     return d_theoryOut.d_explanationNode;
 433   }
 434
 435   Node getValue(TNode node);
 436
 437 private:
 438   class Statistics {
 439   public:
 440     IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation;
 441     Statistics():
 442       d_statConflicts("theory::conflicts", 0),
 443       d_statPropagate("theory::propagate", 0),
 444       d_statLemma("theory::lemma", 0),
 445       d_statAugLemma("theory::aug_lemma", 0),
 446       d_statExplanation("theory::explanation", 0) {
 447       StatisticsRegistry::registerStat(&d_statConflicts);
 448       StatisticsRegistry::registerStat(&d_statPropagate);
 449       StatisticsRegistry::registerStat(&d_statLemma);
 450       StatisticsRegistry::registerStat(&d_statAugLemma);
 451       StatisticsRegistry::registerStat(&d_statExplanation);
 452     }
 453
 454     ~Statistics() {
 455       StatisticsRegistry::unregisterStat(&d_statConflicts);
 456       StatisticsRegistry::unregisterStat(&d_statPropagate);
 457       StatisticsRegistry::unregisterStat(&d_statLemma);
 458       StatisticsRegistry::unregisterStat(&d_statAugLemma);
 459       StatisticsRegistry::unregisterStat(&d_statExplanation);
 460     }
 461   };/* class TheoryEngine::Statistics */
 462   Statistics d_statistics;
 463
 464 };/* class TheoryEngine */
 465
 466 }/* CVC4 namespace */
 467
 468 #endif /* __CVC4__THEORY_ENGINE_H */