src/expr/expr_manager_template.h

   1 /*********************                                                        */
   2 /*! \file expr_manager_template.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: cconway, mdeters
   6  ** Minor contributors (to current version): taking
   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 Public-facing expression manager interface.
  15  **
  16  ** Public-facing expression manager interface.
  17  **/
  18
  19 #include "cvc4_public.h"
  20
  21 #ifndef __CVC4__EXPR_MANAGER_H
  22 #define __CVC4__EXPR_MANAGER_H
  23
  24 #include <vector>
  25
  26 #include "expr/kind.h"
  27 #include "expr/type.h"
  28 #include "expr/expr.h"
  29
  30 ${includes}
  31
  32 // This is a hack, but an important one: if there's an error, the
  33 // compiler directs the user to the template file instead of the
  34 // generated one.  We don't want the user to modify the generated one,
  35 // since it'll get overwritten on a later build.
  36 #line 37 "${template}"
  37
  38 namespace CVC4 {
  39
  40 class Expr;
  41 class SmtEngine;
  42 class NodeManager;
  43
  44 namespace context {
  45   class Context;
  46 }/* CVC4::context namespace */
  47
  48 class CVC4_PUBLIC ExprManager {
  49 private:
  50   /** The context */
  51   context::Context* d_ctxt;
  52
  53   /** The internal node manager */
  54   NodeManager* d_nodeManager;
  55
  56   /**
  57    * Returns the internal node manager.  This should only be used by
  58    * internal users, i.e. the friend classes.
  59    */
  60   NodeManager* getNodeManager() const;
  61
  62   /**
  63    * Returns the internal Context.  Used by internal users, i.e. the
  64    * friend classes.
  65    */
  66   context::Context* getContext() const;
  67
  68   /**
  69    * SmtEngine will use all the internals, so it will grab the
  70    * NodeManager.
  71    */
  72   friend class SmtEngine;
  73
  74   /** ExprManagerScope reaches in to get the NodeManager */
  75   friend class ExprManagerScope;
  76
  77 public:
  78
  79   /**
  80    * Creates an expression manager.
  81    */
  82   ExprManager();
  83
  84   /**
  85    * Destroys the expression manager. No will be deallocated at this point, so
  86    * any expression references that used to be managed by this expression
  87    * manager and are left-over are bad.
  88    */
  89   ~ExprManager();
  90
  91   /** Get the type for booleans */
  92   BooleanType booleanType() const;
  93
  94   /** Get the type for sorts. */
  95   KindType kindType() const;
  96
  97   /** Get the type for reals. */
  98   RealType realType() const;
  99
 100   /** Get the type for integers */
 101   IntegerType integerType() const;
 102
 103   /**
 104    * Make a unary expression of a given kind (NOT, BVNOT, ...).
 105    * @param child1 kind the kind of expression
 106    * @return the expression
 107    */
 108   Expr mkExpr(Kind kind, const Expr& child1);
 109
 110   /**
 111    * Make a binary expression of a given kind (AND, PLUS, ...).
 112    * @param kind the kind of expression
 113    * @param child1 the first child of the new expression
 114    * @param child2 the second child of the new expression
 115    * @return the expression
 116    */
 117   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2);
 118
 119   /**
 120    * Make a 3-ary expression of a given kind (AND, PLUS, ...).
 121    * @param kind the kind of expression
 122    * @param child1 the first child of the new expression
 123    * @param child2 the second child of the new expression
 124    * @param child3 the third child of the new expression
 125    * @return the expression
 126    */
 127   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 128               const Expr& child3);
 129
 130   /**
 131    * Make a 4-ary expression of a given kind (AND, PLUS, ...).
 132    * @param kind the kind of expression
 133    * @param child1 the first child of the new expression
 134    * @param child2 the second child of the new expression
 135    * @param child3 the third child of the new expression
 136    * @param child4 the fourth child of the new expression
 137    * @return the expression
 138    */
 139   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 140               const Expr& child3, const Expr& child4);
 141
 142   /**
 143    * Make a 5-ary expression of a given kind (AND, PLUS, ...).
 144    * @param kind the kind of expression
 145    * @param child1 the first child of the new expression
 146    * @param child2 the second child of the new expression
 147    * @param child3 the third child of the new expression
 148    * @param child4 the fourth child of the new expression
 149    * @param child5 the fifth child of the new expression
 150    * @return the expression
 151    */
 152   Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2,
 153               const Expr& child3, const Expr& child4, const Expr& child5);
 154
 155   /**
 156    * Make an n-ary expression of given kind given a vector of it's children
 157    * @param kind the kind of expression to build
 158    * @param children the subexpressions
 159    * @return the n-ary expression
 160    */
 161   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 162
 163   /**
 164    * Make an n-ary expression of given tre operator to appply and a vector of
 165    * it's children
 166    * @param opExpr the operator expression
 167    * @param children the subexpressions
 168    * @return the n-ary expression
 169    */
 170   Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
 171
 172   /** Create a constant of type T */
 173   template <class T>
 174   Expr mkConst(const T&);
 175
 176   /** Create an Expr by applying an associative operator to the children.
 177    * If <code>children.size()</code> is greater than the max arity for
 178    * <code>kind</code>, then the expression will be broken up into
 179    * suitably-sized chunks, taking advantage of the associativity of
 180    * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
 181    * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
 182    * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>.
 183    * The order of the arguments will be preserved in a left-to-right
 184    * traversal of the resulting tree.
 185    */
 186   Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
 187
 188
 189   /** Make a function type from domain to range. */
 190   FunctionType mkFunctionType(const Type& domain, const Type& range);
 191
 192   /**
 193    * Make a function type with input types from argTypes.
 194    * <code>argTypes</code> must have at least one element.
 195    */
 196   FunctionType mkFunctionType(const std::vector<Type>& argTypes, const Type& range);
 197
 198   /**
 199    * Make a function type with input types from
 200    * <code>sorts[0..sorts.size()-2]</code> and result type
 201    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
 202    * at least 2 elements.
 203    */
 204   FunctionType mkFunctionType(const std::vector<Type>& sorts);
 205
 206   /**
 207    * Make a predicate type with input types from
 208    * <code>sorts</code>. The result with be a function type with range
 209    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
 210    * element.
 211    */
 212   FunctionType mkPredicateType(const std::vector<Type>& sorts);
 213
 214   /**
 215    * Make a tuple type with types from
 216    * <code>types[0..types.size()-1]</code>.  <code>types</code> must
 217    * have at least 2 elements.
 218    */
 219   TupleType mkTupleType(const std::vector<Type>& types);
 220
 221   /** Make a type representing a bit-vector of the given size */
 222   BitVectorType mkBitVectorType(unsigned size) const;
 223
 224   /** Make the type of arrays with the given parameterization */
 225   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 226
 227   /** Make a new sort with the given name. */
 228   SortType mkSort(const std::string& name) const;
 229
 230   /** Get the type of an expression */
 231   Type getType(const Expr& e, bool check = false)
 232     throw (TypeCheckingException);
 233
 234   // variables are special, because duplicates are permitted
 235   Expr mkVar(const std::string& name, const Type& type);
 236   Expr mkVar(const Type& type);
 237
 238   /** Returns the minimum arity of the given kind. */
 239   static unsigned minArity(Kind kind);
 240
 241   /** Returns the maximum arity of the given kind. */
 242   static unsigned maxArity(Kind kind);
 243 };
 244
 245 ${mkConst_instantiations}
 246
 247 }/* CVC4 namespace */
 248
 249 #endif /* __CVC4__EXPR_MANAGER_H */