src/theory/theory_engine.h

   1 /*********************                                                        */
   2 /*! \file theory_engine.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: dejan, taking
   6  ** Minor contributors (to current version): cconway
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010  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 "expr/node.h"
  25 #include "theory/theory.h"
  26 #include "theory/theoryof_table.h"
  27
  28 #include "prop/prop_engine.h"
  29 #include "theory/shared_term_manager.h"
  30 #include "theory/builtin/theory_builtin.h"
  31 #include "theory/booleans/theory_bool.h"
  32 #include "theory/uf/theory_uf.h"
  33 #include "theory/uf/tim/theory_uf_tim.h"
  34 #include "theory/uf/morgan/theory_uf_morgan.h"
  35 #include "theory/arith/theory_arith.h"
  36 #include "theory/arrays/theory_arrays.h"
  37 #include "theory/bv/theory_bv.h"
  38
  39 #include "util/options.h"
  40 #include "util/stats.h"
  41
  42 namespace CVC4 {
  43
  44 // In terms of abstraction, this is below (and provides services to)
  45 // PropEngine.
  46
  47 /**
  48  * This is essentially an abstraction for a collection of theories.  A
  49  * TheoryEngine provides services to a PropEngine, making various
  50  * T-solvers look like a single unit to the propositional part of
  51  * CVC4.
  52  */
  53 class TheoryEngine {
  54
  55   /** Associated PropEngine engine */
  56   prop::PropEngine* d_propEngine;
  57
  58   /** A table of Kinds to pointers to Theory */
  59   theory::TheoryOfTable d_theoryOfTable;
  60
  61   /** Tag for the "registerTerm()-has-been-called" flag on Nodes */
  62   struct Registered {};
  63   /** The "registerTerm()-has-been-called" flag on Nodes */
  64   typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr;
  65
  66   /**
  67    * An output channel for Theory that passes messages
  68    * back to a TheoryEngine.
  69    */
  70   class EngineOutputChannel : public theory::OutputChannel {
  71
  72     friend class TheoryEngine;
  73
  74     TheoryEngine* d_engine;
  75     context::Context* d_context;
  76     context::CDO<Node> d_conflictNode;
  77     context::CDO<Node> d_explanationNode;
  78
  79     /**
  80      * Literals that are propagated by the theory. Note that these are TNodes.
  81      * The theory can only propagate nodes that have an assigned literal in the
  82      * sat solver and are hence referenced in the SAT solver.
  83      */
  84     std::vector<TNode> d_propagatedLiterals;
  85
  86   public:
  87
  88     EngineOutputChannel(TheoryEngine* engine, context::Context* context) :
  89       d_engine(engine),
  90       d_context(context),
  91       d_conflictNode(context),
  92       d_explanationNode(context){
  93     }
  94
  95     void newFact(TNode n);
  96
  97     void conflict(TNode conflictNode, bool safe) throw(theory::Interrupted, AssertionException) {
  98       Debug("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
  99       d_conflictNode = conflictNode;
 100       ++(d_engine->d_statistics.d_statConflicts);
 101       if(safe) {
 102         throw theory::Interrupted();
 103       }
 104     }
 105
 106     void propagate(TNode lit, bool) throw(theory::Interrupted, AssertionException) {
 107       d_propagatedLiterals.push_back(lit);
 108       ++(d_engine->d_statistics.d_statPropagate);
 109     }
 110
 111     void lemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
 112       ++(d_engine->d_statistics.d_statLemma);
 113       d_engine->newLemma(node);
 114     }
 115     void augmentingLemma(TNode node, bool) throw(theory::Interrupted, AssertionException) {
 116       ++(d_engine->d_statistics.d_statAugLemma);
 117       d_engine->newAugmentingLemma(node);
 118     }
 119     void explanation(TNode explanationNode, bool) throw(theory::Interrupted, AssertionException) {
 120       d_explanationNode = explanationNode;
 121       ++(d_engine->d_statistics.d_statExplanation);
 122     }
 123   };
 124
 125
 126
 127   EngineOutputChannel d_theoryOut;
 128
 129   /** Pointer to Shared Term Manager */
 130   SharedTermManager* d_sharedTermManager;
 131
 132   theory::builtin::TheoryBuiltin* d_builtin;
 133   theory::booleans::TheoryBool* d_bool;
 134   theory::uf::TheoryUF* d_uf;
 135   theory::arith::TheoryArith* d_arith;
 136   theory::arrays::TheoryArrays* d_arrays;
 137   theory::bv::TheoryBV* d_bv;
 138
 139   /**
 140    * Debugging flag to ensure that shutdown() is called before the
 141    * destructor.
 142    */
 143   bool d_hasShutDown;
 144
 145   /**
 146    * Check whether a node is in the pre-rewrite cache or not.
 147    */
 148   static bool inPreRewriteCache(TNode n, bool topLevel) throw() {
 149     return theory::Theory::inPreRewriteCache(n, topLevel);
 150   }
 151
 152   /**
 153    * Get the value of the pre-rewrite cache (or Node::null()) if there is
 154    * none).
 155    */
 156   static Node getPreRewriteCache(TNode n, bool topLevel) throw() {
 157     return theory::Theory::getPreRewriteCache(n, topLevel);
 158   }
 159
 160   /**
 161    * Set the value of the pre-rewrite cache.  v cannot be a null Node.
 162    */
 163   static void setPreRewriteCache(TNode n, bool topLevel, TNode v) throw() {
 164     return theory::Theory::setPreRewriteCache(n, topLevel, v);
 165   }
 166
 167   /**
 168    * Check whether a node is in the post-rewrite cache or not.
 169    */
 170   static bool inPostRewriteCache(TNode n, bool topLevel) throw() {
 171     return theory::Theory::inPostRewriteCache(n, topLevel);
 172   }
 173
 174   /**
 175    * Get the value of the post-rewrite cache (or Node::null()) if there is
 176    * none).
 177    */
 178   static Node getPostRewriteCache(TNode n, bool topLevel) throw() {
 179     return theory::Theory::getPostRewriteCache(n, topLevel);
 180   }
 181
 182   /**
 183    * Set the value of the post-rewrite cache.  v cannot be a null Node.
 184    */
 185   static void setPostRewriteCache(TNode n, bool topLevel, TNode v) throw() {
 186     return theory::Theory::setPostRewriteCache(n, topLevel, v);
 187   }
 188
 189   /**
 190    * This is the top rewrite entry point, called during preprocessing.
 191    * It dispatches to the proper theories to rewrite the given Node.
 192    */
 193   Node rewrite(TNode in, bool topLevel = true);
 194
 195   /**
 196    * Replace ITE forms in a node.
 197    */
 198   Node removeITEs(TNode t);
 199
 200 public:
 201
 202   /**
 203    * Construct a theory engine.
 204    */
 205   TheoryEngine(context::Context* ctxt, const Options* opts) :
 206     d_propEngine(NULL),
 207     d_theoryOut(this, ctxt),
 208     d_hasShutDown(false),
 209     d_statistics() {
 210
 211     d_sharedTermManager = new SharedTermManager(this, ctxt);
 212
 213     d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
 214     d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
 215     switch(opts->uf_implementation) {
 216     case Options::TIM:
 217       d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
 218       break;
 219     case Options::MORGAN:
 220       d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
 221       break;
 222     default:
 223       Unhandled(opts->uf_implementation);
 224     }
 225     d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
 226     d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
 227     d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
 228
 229     d_sharedTermManager->registerTheory(d_builtin);
 230     d_sharedTermManager->registerTheory(d_bool);
 231     d_sharedTermManager->registerTheory(d_uf);
 232     d_sharedTermManager->registerTheory(d_arith);
 233     d_sharedTermManager->registerTheory(d_arrays);
 234     d_sharedTermManager->registerTheory(d_bv);
 235
 236     d_theoryOfTable.registerTheory(d_builtin);
 237     d_theoryOfTable.registerTheory(d_bool);
 238     d_theoryOfTable.registerTheory(d_uf);
 239     d_theoryOfTable.registerTheory(d_arith);
 240     d_theoryOfTable.registerTheory(d_arrays);
 241     d_theoryOfTable.registerTheory(d_bv);
 242   }
 243
 244   ~TheoryEngine() {
 245     Assert(d_hasShutDown);
 246
 247     delete d_bv;
 248     delete d_arrays;
 249     delete d_arith;
 250     delete d_uf;
 251     delete d_bool;
 252     delete d_builtin;
 253
 254     delete d_sharedTermManager;
 255   }
 256
 257   SharedTermManager* getSharedTermManager() {
 258     return d_sharedTermManager;
 259   }
 260
 261   void setPropEngine(prop::PropEngine* propEngine) {
 262     Assert(d_propEngine == NULL);
 263     d_propEngine = propEngine;
 264   }
 265
 266   /**
 267    * This is called at shutdown time by the SmtEngine, just before
 268    * destruction.  It is important because there are destruction
 269    * ordering issues between PropEngine and Theory.
 270    */
 271   void shutdown() {
 272     // Set this first; if a Theory shutdown() throws an exception,
 273     // at least the destruction of the TheoryEngine won't confound
 274     // matters.
 275     d_hasShutDown = true;
 276
 277     d_builtin->shutdown();
 278     d_bool->shutdown();
 279     d_uf->shutdown();
 280     d_arith->shutdown();
 281     d_arrays->shutdown();
 282     d_bv->shutdown();
 283   }
 284
 285   /**
 286    * Get the theory associated to a given TypeNode.
 287    *
 288    * @returns the theory owning the type
 289    */
 290   theory::Theory* theoryOf(TypeNode t);
 291
 292   /**
 293    * Get the theory associated to a given Node.
 294    *
 295    * @returns the theory, or NULL if the TNode is
 296    * of built-in type.
 297    */
 298   theory::Theory* theoryOf(TNode n);
 299
 300   /**
 301    * Preprocess a node.  This involves theory-specific rewriting, then
 302    * calling preRegisterTerm() on what's left over.
 303    * @param n the node to preprocess
 304    */
 305   Node preprocess(TNode n);
 306
 307   /**
 308    * Assert the formula to the apropriate theory.
 309    * @param node the assertion
 310    */
 311   inline void assertFact(TNode node) {
 312     Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 313     theory::Theory* theory =
 314       node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
 315     if(theory != NULL) {
 316       theory->assertFact(node);
 317     }
 318   }
 319
 320   /**
 321    * Check all (currently-active) theories for conflicts.
 322    * @param effort the effort level to use
 323    */
 324   inline bool check(theory::Theory::Effort effort)
 325   {
 326     d_theoryOut.d_conflictNode = Node::null();
 327     d_theoryOut.d_propagatedLiterals.clear();
 328     // Do the checking
 329     try {
 330       //d_builtin->check(effort);
 331       //d_bool->check(effort);
 332       d_uf->check(effort);
 333       d_arith->check(effort);
 334       d_arrays->check(effort);
 335       d_bv->check(effort);
 336     } catch(const theory::Interrupted&) {
 337       Debug("theory") << "TheoryEngine::check() => conflict" << std::endl;
 338     }
 339     // Return wheather we have a conflict
 340     return d_theoryOut.d_conflictNode.get().isNull();
 341   }
 342
 343   inline const std::vector<TNode>& getPropagatedLiterals() const {
 344     return d_theoryOut.d_propagatedLiterals;
 345   }
 346
 347   void clearPropagatedLiterals() {
 348     d_theoryOut.d_propagatedLiterals.clear();
 349   }
 350
 351   inline void newLemma(TNode node) {
 352     d_propEngine->assertLemma(node);
 353   }
 354
 355   inline void newAugmentingLemma(TNode node) {
 356     Node preprocessed = preprocess(node);
 357     d_propEngine->assertFormula(preprocessed);
 358   }
 359
 360   /**
 361    * Returns the last conflict (if any).
 362    */
 363   inline Node getConflict() {
 364     return d_theoryOut.d_conflictNode;
 365   }
 366
 367   inline void propagate() {
 368     d_theoryOut.d_propagatedLiterals.clear();
 369     // Do the propagation
 370     //d_builtin->propagate(theory::Theory::FULL_EFFORT);
 371     //d_bool->propagate(theory::Theory::FULL_EFFORT);
 372     d_uf->propagate(theory::Theory::FULL_EFFORT);
 373     d_arith->propagate(theory::Theory::FULL_EFFORT);
 374     d_arrays->propagate(theory::Theory::FULL_EFFORT);
 375     //d_bv->propagate(theory::Theory::FULL_EFFORT);
 376   }
 377
 378   inline Node getExplanation(TNode node, theory::Theory* theory) {
 379     theory->explain(node);
 380     return d_theoryOut.d_explanationNode;
 381   }
 382
 383   inline Node getExplanation(TNode node){
 384     d_theoryOut.d_explanationNode = Node::null();
 385     theory::Theory* theory =
 386               node.getKind() == kind::NOT ? theoryOf(node[0]) : theoryOf(node);
 387     theory->explain(node);
 388     return d_theoryOut.d_explanationNode;
 389   }
 390
 391 private:
 392   class Statistics {
 393   public:
 394     IntStat d_statConflicts, d_statPropagate, d_statLemma, d_statAugLemma, d_statExplanation;
 395     Statistics():
 396       d_statConflicts("theory::conflicts",0),
 397       d_statPropagate("theory::propagate",0),
 398       d_statLemma("theory::lemma",0),
 399       d_statAugLemma("theory::aug_lemma", 0),
 400       d_statExplanation("theory::explanation", 0)
 401     {
 402       StatisticsRegistry::registerStat(&d_statConflicts);
 403       StatisticsRegistry::registerStat(&d_statPropagate);
 404       StatisticsRegistry::registerStat(&d_statLemma);
 405       StatisticsRegistry::registerStat(&d_statAugLemma);
 406       StatisticsRegistry::registerStat(&d_statExplanation);
 407     }
 408
 409     ~Statistics() {
 410       StatisticsRegistry::unregisterStat(&d_statConflicts);
 411       StatisticsRegistry::unregisterStat(&d_statPropagate);
 412       StatisticsRegistry::unregisterStat(&d_statLemma);
 413       StatisticsRegistry::unregisterStat(&d_statAugLemma);
 414       StatisticsRegistry::unregisterStat(&d_statExplanation);
 415     }
 416   };
 417   Statistics d_statistics;
 418
 419 };/* class TheoryEngine */
 420
 421 }/* CVC4 namespace */
 422
 423 #endif /* __CVC4__THEORY_ENGINE_H */