src/expr/expr_manager.h

   1 /*
   2  * expr_manager.h
   3  *
   4  *  Created on: Dec 10, 2009
   5  *      Author: dejan
   6  */
   7
   8 #ifndef __CVC4__EXPR_MANAGER_H
   9 #define __CVC4__EXPR_MANAGER_H
  10
  11 #include "cvc4_config.h"
  12 #include "expr/kind.h"
  13 #include <vector>
  14
  15 namespace CVC4 {
  16
  17 class Expr;
  18 class NodeManager;
  19 class SmtEngine;
  20
  21 class CVC4_PUBLIC ExprManager {
  22
  23 public:
  24
  25   /**
  26    * Creates an expressio manager.
  27    */
  28   ExprManager();
  29
  30   /**
  31    * Destroys the expression manager. No will be deallocated at this point, so
  32    * any expression references that used to be managed by this expression
  33    * manager and are left-over are bad.
  34    */
  35   ~ExprManager();
  36
  37   /**
  38    * Make a unary expression of a given kind (TRUE, FALSE,...).
  39    * @param kind the kind of expression
  40    * @return the expression
  41    */
  42   Expr mkExpr(Kind kind);
  43
  44   /**
  45    * Make a unary expression of a given kind (NOT, BVNOT, ...).
  46    * @param kind the kind of expression
  47    * @return the expression
  48    */
  49   Expr mkExpr(Kind kind, const Expr& child1);
  50
  51   /**
  52    * Make a ternary expression of a given kind (AND, PLUS, ...).
  53    * @param kind the kind of expression
  54    * @return the expression
  55    */
  56   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
  57
  58   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
  59               const Expr& child3);
  60   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
  61               const Expr& child3, const Expr& child4);
  62   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
  63               const Expr& child3, const Expr& child4, const Expr& child5);
  64
  65   /**
  66    * Make an n-ary expression of given kind given a vector of it's children
  67    * @param kind the kind of expression to build
  68    * @param children the subexpressions
  69    * @return the n-ary expression
  70    */
  71   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
  72
  73   // variables are special, because duplicates are permitted
  74   Expr mkVar();
  75
  76 private:
  77
  78   /** The internal node manager */
  79   NodeManager* d_nm;
  80
  81   /**
  82    * Returns the internal node manager. This should only be used by internal
  83    * users, i.e. the friend classes.
  84    */
  85   NodeManager* getNodeManager() const;
  86
  87   /** SmtEngine will use all the internals, so it will grab the node manager */
  88   friend class SmtEngine;
  89 };
  90
  91 }
  92
  93 #endif /* __CVC4__EXPR_MANAGER_H */