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
  26 #include "expr/node.h"
  27 #include "prop/prop_engine.h"
  28 #include "theory/shared_term_manager.h"
  29 #include "theory/theory.h"
  30 #include "theory/rewriter.h"
  31 #include "theory/valuation.h"
  32 #include "util/options.h"
  33 #include "util/stats.h"
  34
  35 namespace CVC4 {
  36
  37 // In terms of abstraction, this is below (and provides services to)
  38 // PropEngine.
  39
  40 /**
  41  * This is essentially an abstraction for a collection of theories.  A
  42  * TheoryEngine provides services to a PropEngine, making various
  43  * T-solvers look like a single unit to the propositional part of
  44  * CVC4.
  45  */
  46 class TheoryEngine {
  47
  48   /** Associated PropEngine engine */
  49   prop::PropEngine* d_propEngine;
  50
  51   /** Our context */
  52   context::Context* d_context;
  53
  54   /** A table of from theory ifs to theory pointers */
  55   theory::Theory* d_theoryTable[theory::THEORY_LAST];
  56
  57   /**
  58    * An output channel for Theory that passes messages
  59    * back to a TheoryEngine.
  60    */
  61   class EngineOutputChannel : public theory::OutputChannel {
  62
  63     friend class TheoryEngine;
  64
  65     TheoryEngine* d_engine;
  66     context::Context* d_context;
  67     context::CDO<Node> d_conflictNode;
  68     context::CDO<Node> d_explanationNode;
  69
  70     /**
  71      * Literals that are propagated by the theory. Note that these are TNodes.
  72      * The theory can only propagate nodes that have an assigned literal in the
  73      * sat solver and are hence referenced in the SAT solver.
  74      */
  75     std::vector<TNode> d_propagatedLiterals;
  76
  77     /** Time spent in newFact() (largely spent doing term registration) */
  78     KEEP_STATISTIC(TimerStat,
  79                    d_newFactTimer,
  80                    "theory::newFactTimer");
  81
  82   public:
  83
  84     EngineOutputChannel(TheoryEngine* engine, context::Context* context) :
  85       d_engine(engine),
  86       d_context(context),
  87       d_conflictNode(context),
  88       d_explanationNode(context) {
  89     }
  90
  91     void newFact(TNode n);
  92
  93     void conflict(TNode conflictNode, bool safe)
  94       throw(theory::Interrupted, AssertionException) {
  95       Debug("theory") << "EngineOutputChannel::conflict("
  96                       << conflictNode << ")" << std::endl;
  97       d_conflictNode = conflictNode;
  98       ++(d_engine->d_statistics.d_statConflicts);
  99       if(safe) {
 100         throw theory::Interrupted();
 101       }
 102     }
 103
 104     void propagate(TNode lit, bool)
 105       throw(theory::Interrupted, AssertionException) {
 106       Debug("theory") << "EngineOutputChannel::propagate("
 107                       << lit << ")" << std::endl;
 108       d_propagatedLiterals.push_back(lit);
 109       ++(d_engine->d_statistics.d_statPropagate);
 110     }
 111
 112     void lemma(TNode node, bool)
 113       throw(theory::Interrupted, AssertionException) {
 114       Debug("theory") << "EngineOutputChannel::lemma("
 115                       << node << ")" << std::endl;
 116       ++(d_engine->d_statistics.d_statLemma);
 117       d_engine->newLemma(node);
 118     }
 119
 120     void explanation(TNode explanationNode, bool)
 121       throw(theory::Interrupted, AssertionException) {
 122       Debug("theory") << "EngineOutputChannel::explanation("
 123                       << explanationNode << ")" << std::endl;
 124       d_explanationNode = explanationNode;
 125       ++(d_engine->d_statistics.d_statExplanation);
 126     }
 127
 128     void setIncomplete()
 129       throw(theory::Interrupted, AssertionException) {
 130       d_engine->d_incomplete = true;
 131     }
 132   };/* class EngineOutputChannel */
 133
 134   EngineOutputChannel d_theoryOut;
 135
 136   /** Pointer to Shared Term Manager */
 137   SharedTermManager* d_sharedTermManager;
 138
 139   /**
 140    * Whether or not theory registration is on.  May not be safe to
 141    * turn off with some theories.
 142    */
 143   bool d_theoryRegistration;
 144
 145   /**
 146    * Debugging flag to ensure that shutdown() is called before the
 147    * destructor.
 148    */
 149   bool d_hasShutDown;
 150
 151   /**
 152    * True if a theory has notified us of incompleteness (at this
 153    * context level or below).
 154    */
 155   context::CDO<bool> d_incomplete;
 156
 157   /**
 158    * Replace ITE forms in a node.
 159    */
 160   Node removeITEs(TNode t);
 161
 162 public:
 163
 164   /**
 165    * Construct a theory engine.
 166    */
 167   TheoryEngine(context::Context* ctxt);
 168
 169   /**
 170    * Destroy a theory engine.
 171    */
 172   ~TheoryEngine();
 173
 174   /**
 175    * Adds a theory. Only one theory per theoryId can be present, so if there is another theory it will be deleted.
 176    */
 177   template <class TheoryClass>
 178   void addTheory() {
 179     TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this));
 180     d_theoryTable[theory->getId()] = theory;
 181     d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory));
 182   }
 183
 184   SharedTermManager* getSharedTermManager() {
 185     return d_sharedTermManager;
 186   }
 187
 188   void setPropEngine(prop::PropEngine* propEngine) {
 189     Assert(d_propEngine == NULL);
 190     d_propEngine = propEngine;
 191   }
 192
 193   /**
 194    * Get a pointer to the underlying propositional engine.
 195    */
 196   prop::PropEngine* getPropEngine() const {
 197     return d_propEngine;
 198   }
 199
 200   /**
 201    * Return whether or not we are incomplete (in the current context).
 202    */
 203   bool isIncomplete() {
 204     return d_incomplete;
 205   }
 206
 207   /**
 208    * This is called at shutdown time by the SmtEngine, just before
 209    * destruction.  It is important because there are destruction
 210    * ordering issues between PropEngine and Theory.
 211    */
 212   void shutdown() {
 213     // Set this first; if a Theory shutdown() throws an exception,
 214     // at least the destruction of the TheoryEngine won't confound
 215     // matters.
 216     d_hasShutDown = true;
 217
 218     // Shutdown all the theories
 219     for(unsigned theoryId = 0; theoryId < theory::THEORY_LAST; ++theoryId) {
 220       if(d_theoryTable[theoryId]) {
 221         d_theoryTable[theoryId]->shutdown();
 222       }
 223     }
 224
 225     theory::Rewriter::shutdown();
 226   }
 227
 228   /**
 229    * Get the theory associated to a given Node.
 230    *
 231    * @returns the theory, or NULL if the TNode is
 232    * of built-in type.
 233    */
 234   inline theory::Theory* theoryOf(TNode node) {
 235     return d_theoryTable[theory::Theory::theoryOf(node)];
 236   }
 237
 238   /**
 239    * Get the theory associated to a given Node.
 240    *
 241    * @returns the theory, or NULL if the TNode is
 242    * of built-in type.
 243    */
 244   inline theory::Theory* theoryOf(const TypeNode& typeNode) {
 245     return d_theoryTable[theory::Theory::theoryOf(typeNode)];
 246   }
 247
 248   /**
 249    * Preprocess a node.  This involves theory-specific rewriting, then
 250    * calling preRegisterTerm() on what's left over.
 251    * @param n the node to preprocess
 252    */
 253   Node preprocess(TNode n);
 254   void preRegister(TNode preprocessed);
 255
 256   /**
 257    * Assert the formula to the appropriate theory.
 258    * @param node the assertion
 259    */
 260   inline void assertFact(TNode node) {
 261     Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 262
 263     // Mark it as asserted in this context
 264     //
 265     // [MGD] removed for now, this appears to have a nontrivial
 266     // performance penalty
 267     // node.setAttribute(theory::Asserted(), true);
 268
 269     // Get the atom
 270     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 271
 272     // Again, equality is a special case
 273     if (atom.getKind() == kind::EQUAL) {
 274       theory::TheoryId theoryLHS = theory::Theory::theoryOf(atom[0]);
 275       Debug("theory") << "asserting " << node << " to " << theoryLHS << std::endl;
 276       d_theoryTable[theoryLHS]->assertFact(node);
 277 //      theory::TheoryId theoryRHS = theory::Theory::theoryOf(atom[1]);
 278 //      if (theoryLHS != theoryRHS) {
 279 //        Debug("theory") << "asserting " << node << " to " << theoryRHS << std::endl;
 280 //        d_theoryTable[theoryRHS]->assertFact(node);
 281 //      }
 282 //      theory::TheoryId typeTheory = theory::Theory::theoryOf(atom[0].getType());
 283 //      if (typeTheory!= theoryLHS && typeTheory != theoryRHS) {
 284 //        Debug("theory") << "asserting " << node << " to " << typeTheory << std::endl;
 285 //        d_theoryTable[typeTheory]->assertFact(node);
 286 //      }
 287     } else {
 288       theory::Theory* theory = theoryOf(atom);
 289       Debug("theory") << "asserting " << node << " to " << theory->getId() << std::endl;
 290       theory->assertFact(node);
 291     }
 292   }
 293
 294   /**
 295    * Check all (currently-active) theories for conflicts.
 296    * @param effort the effort level to use
 297    */
 298   bool check(theory::Theory::Effort effort);
 299
 300   /**
 301    * Calls staticLearning() on all active theories, accumulating their
 302    * combined contributions in the "learned" builder.
 303    */
 304   void staticLearning(TNode in, NodeBuilder<>& learned);
 305
 306   /**
 307    * Calls presolve() on all active theories and returns true
 308    * if one of the theories discovers a conflict.
 309    */
 310   bool presolve();
 311
 312   /**
 313    * Calls notifyRestart() on all active theories.
 314    */
 315   void notifyRestart();
 316
 317   inline const std::vector<TNode>& getPropagatedLiterals() const {
 318     return d_theoryOut.d_propagatedLiterals;
 319   }
 320
 321   void clearPropagatedLiterals() {
 322     d_theoryOut.d_propagatedLiterals.clear();
 323   }
 324
 325   inline void newLemma(TNode node) {
 326     d_propEngine->assertLemma(preprocess(node));
 327   }
 328
 329   /**
 330    * Returns the last conflict (if any).
 331    */
 332   inline Node getConflict() {
 333     return d_theoryOut.d_conflictNode;
 334   }
 335
 336   void propagate();
 337
 338   inline Node getExplanation(TNode node, theory::Theory* theory) {
 339     theory->explain(node);
 340     return d_theoryOut.d_explanationNode;
 341   }
 342
 343   inline Node getExplanation(TNode node) {
 344     d_theoryOut.d_explanationNode = Node::null();
 345     TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 346     if (atom.getKind() == kind::EQUAL) {
 347       theoryOf(atom[0])->explain(node);
 348     } else {
 349       theoryOf(atom)->explain(node);
 350     }
 351     Assert(!d_theoryOut.d_explanationNode.get().isNull());
 352     return d_theoryOut.d_explanationNode;
 353   }
 354
 355   Node getValue(TNode node);
 356
 357 private:
 358   class Statistics {
 359   public:
 360     IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation;
 361     Statistics():
 362       d_statConflicts("theory::conflicts", 0),
 363       d_statPropagate("theory::propagate", 0),
 364       d_statLemma("theory::lemma", 0),
 365       d_statAugLemma("theory::aug_lemma", 0),
 366       d_statExplanation("theory::explanation", 0)
 367     {
 368       StatisticsRegistry::registerStat(&d_statConflicts);
 369       StatisticsRegistry::registerStat(&d_statPropagate);
 370       StatisticsRegistry::registerStat(&d_statLemma);
 371       StatisticsRegistry::registerStat(&d_statAugLemma);
 372       StatisticsRegistry::registerStat(&d_statExplanation);
 373     }
 374
 375     ~Statistics() {
 376       StatisticsRegistry::unregisterStat(&d_statConflicts);
 377       StatisticsRegistry::unregisterStat(&d_statPropagate);
 378       StatisticsRegistry::unregisterStat(&d_statLemma);
 379       StatisticsRegistry::unregisterStat(&d_statAugLemma);
 380       StatisticsRegistry::unregisterStat(&d_statExplanation);
 381     }
 382   };
 383   Statistics d_statistics;
 384
 385 };/* class TheoryEngine */
 386
 387 }/* CVC4 namespace */
 388
 389 #endif /* __CVC4__THEORY_ENGINE_H */