src/theory/builtin/theory_builtin.h

   1 /*********************                                                        */
   2 /*! \file theory_builtin.h
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): barrett
   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 Built-in theory.
  15  **
  16  ** Built-in theory.
  17  **/
  18
  19 #include "cvc4_private.h"
  20
  21 #ifndef __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
  22 #define __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H
  23
  24 #include "theory/theory.h"
  25
  26 namespace CVC4 {
  27 namespace theory {
  28 namespace builtin {
  29
  30 class TheoryBuiltin : public Theory {
  31 public:
  32   TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) :
  33     Theory(THEORY_BUILTIN, c, out, valuation) {}
  34   Node simplify(TNode in, Substitutions& outSubstitutions);
  35   Node getValue(TNode n);
  36   std::string identify() const { return std::string("TheoryBuiltin"); }
  37 };/* class TheoryBuiltin */
  38
  39 }/* CVC4::theory::builtin namespace */
  40 }/* CVC4::theory namespace */
  41 }/* CVC4 namespace */
  42
  43 #endif /* __CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */