src/theory/theory_engine.h

   1 /*********************                                                        */
   2 /** theory_engine.h
   3  ** Original author: mdeters
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** The theory engine.
  14  **/
  15
  16 #ifndef __CVC4__THEORY_ENGINE_H
  17 #define __CVC4__THEORY_ENGINE_H
  18
  19 #include "expr/node.h"
  20 #include "theory/theory.h"
  21
  22 namespace CVC4 {
  23
  24 class SmtEngine;
  25
  26 // In terms of abstraction, this is below (and provides services to)
  27 // PropEngine.
  28
  29 /**
  30  * This is essentially an abstraction for a collection of theories.  A
  31  * TheoryEngine provides services to a PropEngine, making various
  32  * T-solvers look like a single unit to the propositional part of
  33  * CVC4.
  34  */
  35 class TheoryEngine {
  36
  37   SmtEngine* d_smt;
  38
  39 public:
  40
  41   /**
  42    * Construct a theory engine.
  43    */
  44   TheoryEngine(SmtEngine* smt) : d_smt(smt) {
  45   }
  46
  47   /**
  48    * Get the theory associated to a given Node.
  49    */
  50   CVC4::theory::Theory* theoryOf(const Node& n);
  51
  52 };/* class TheoryEngine */
  53
  54 }/* CVC4 namespace */
  55
  56 #endif /* __CVC4__THEORY_ENGINE_H */