src/expr/expr_manager.h

   1 /*********************                                           -*- C++ -*-  */
   2 /** expr_manager.h
   3  ** This file is part of the CVC4 prototype.
   4  ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
   5  ** Courant Institute of Mathematical Sciences
   6  ** New York University
   7  ** See the file COPYING in the top-level source directory for licensing
   8  ** information.
   9  **
  10  **/
  11
  12 #ifndef __CVC4_EXPR_MANAGER_H
  13 #define __CVC4_EXPR_MANAGER_H
  14
  15 #include <vector>
  16 #include "cvc4_expr.h"
  17 #include "core/kind.h"
  18
  19 namespace CVC4 {
  20
  21 class ExprManager {
  22   static __thread ExprManager* s_current;
  23
  24 public:
  25   static ExprManager* currentEM() { return s_current; }
  26
  27   // general expression-builders
  28   Expr mkExpr(Kind kind);
  29   Expr mkExpr(Kind kind, Expr child1);
  30   Expr mkExpr(Kind kind, Expr child1, Expr child2);
  31   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
  32   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
  33   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
  34   // N-ary version
  35   Expr mkExpr(Kind kind, std::vector<Expr> children);
  36
  37   // TODO: these use the current EM (but must be renamed)
  38   /*
  39   static Expr mkExpr(Kind kind)
  40   { currentEM()->mkExpr(kind); }
  41   static Expr mkExpr(Kind kind, Expr child1);
  42   { currentEM()->mkExpr(kind, child1); }
  43   static Expr mkExpr(Kind kind, Expr child1, Expr child2);
  44   { currentEM()->mkExpr(kind, child1, child2); }
  45   static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
  46   { currentEM()->mkExpr(kind, child1, child2, child3); }
  47   static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
  48   { currentEM()->mkExpr(kind, child1, child2, child3, child4); }
  49   static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5);
  50   { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); }
  51   */
  52
  53   // do we want a varargs one?  perhaps not..
  54 };
  55
  56 } /* CVC4 namespace */
  57
  58 #endif /* __CVC4_EXPR_MANAGER_H */