src/expr/expr_manager.h

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