src/expr/expr_manager_template.h

   1 /*********************                                                        */
   2 /*! \file expr_manager_template.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Morgan Deters, Andrew Reynolds, Dejan Jovanovic
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Public-facing expression manager interface
  13  **
  14  ** Public-facing expression manager interface.
  15  **/
  16
  17 #include "cvc4_public.h"
  18
  19 #ifndef CVC4__EXPR_MANAGER_H
  20 #define CVC4__EXPR_MANAGER_H
  21
  22 #include <vector>
  23
  24 #include "expr/expr.h"
  25 #include "expr/kind.h"
  26 #include "expr/type.h"
  27 #include "util/statistics.h"
  28
  29 ${includes}
  30
  31 // This is a hack, but an important one: if there's an error, the
  32 // compiler directs the user to the template file instead of the
  33 // generated one.  We don't want the user to modify the generated one,
  34 // since it'll get overwritten on a later build.
  35 #line 36 "${template}"
  36
  37 namespace CVC4 {
  38
  39 namespace api {
  40 class Solver;
  41 }
  42
  43 class Expr;
  44 class SmtEngine;
  45 class NodeManager;
  46 class Options;
  47 class IntStat;
  48 struct ExprManagerMapCollection;
  49 class ResourceManager;
  50
  51 class CVC4_PUBLIC ExprManager {
  52  private:
  53   friend api::Solver;
  54   /** The internal node manager */
  55   NodeManager* d_nodeManager;
  56
  57   /** Counts of expressions and variables created of a given kind */
  58   IntStat* d_exprStatisticsVars[LAST_TYPE + 1];
  59   IntStat* d_exprStatistics[kind::LAST_KIND];
  60
  61   /**
  62    * Returns the internal node manager.  This should only be used by
  63    * internal users, i.e. the friend classes.
  64    */
  65   NodeManager* getNodeManager() const;
  66
  67   /**
  68    * SmtEngine will use all the internals, so it will grab the
  69    * NodeManager.
  70    */
  71   friend class SmtEngine;
  72
  73   /** ExprManagerScope reaches in to get the NodeManager */
  74   friend class ExprManagerScope;
  75
  76   /** NodeManager reaches in to get the NodeManager */
  77   friend class NodeManager;
  78
  79   // undefined, private copy constructor and assignment op (disallow copy)
  80   ExprManager(const ExprManager&) = delete;
  81   ExprManager& operator=(const ExprManager&) = delete;
  82   /** Creates an expression manager. */
  83   ExprManager();
  84  public:
  85   /**
  86    * Destroys the expression manager. No will be deallocated at this point, so
  87    * any expression references that used to be managed by this expression
  88    * manager and are left-over are bad.
  89    */
  90   ~ExprManager();
  91
  92   /** Get the type for booleans */
  93   BooleanType booleanType() const;
  94
  95   /** Get the type for strings. */
  96   StringType stringType() const;
  97
  98   /** Get the type for regular expressions. */
  99   RegExpType regExpType() const;
 100
 101   /** Get the type for reals. */
 102   RealType realType() const;
 103
 104   /** Get the type for integers */
 105   IntegerType integerType() const;
 106
 107   /** Get the type for rounding modes */
 108   RoundingModeType roundingModeType() const;
 109
 110   /**
 111    * Make a unary expression of a given kind (NOT, BVNOT, ...).
 112    * @param kind the kind of expression
 113    * @param child1 kind the kind of expression
 114    * @return the expression
 115    */
 116   Expr mkExpr(Kind kind, Expr child1);
 117
 118   /**
 119    * Make a binary expression of a given kind (AND, PLUS, ...).
 120    * @param kind the kind of expression
 121    * @param child1 the first child of the new expression
 122    * @param child2 the second child of the new expression
 123    * @return the expression
 124    */
 125   Expr mkExpr(Kind kind, Expr child1, Expr child2);
 126
 127   /**
 128    * Make a 3-ary expression of a given kind (AND, PLUS, ...).
 129    * @param kind the kind of expression
 130    * @param child1 the first child of the new expression
 131    * @param child2 the second child of the new expression
 132    * @param child3 the third child of the new expression
 133    * @return the expression
 134    */
 135   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3);
 136
 137   /**
 138    * Make a 4-ary expression of a given kind (AND, PLUS, ...).
 139    * @param kind the kind of expression
 140    * @param child1 the first child of the new expression
 141    * @param child2 the second child of the new expression
 142    * @param child3 the third child of the new expression
 143    * @param child4 the fourth child of the new expression
 144    * @return the expression
 145    */
 146   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4);
 147
 148   /**
 149    * Make a 5-ary expression of a given kind (AND, PLUS, ...).
 150    * @param kind the kind of expression
 151    * @param child1 the first child of the new expression
 152    * @param child2 the second child of the new expression
 153    * @param child3 the third child of the new expression
 154    * @param child4 the fourth child of the new expression
 155    * @param child5 the fifth child of the new expression
 156    * @return the expression
 157    */
 158   Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4,
 159               Expr child5);
 160
 161   /**
 162    * Make an n-ary expression of given kind given a vector of its
 163    * children
 164    *
 165    * @param kind the kind of expression to build
 166    * @param children the subexpressions
 167    * @return the n-ary expression
 168    */
 169   Expr mkExpr(Kind kind, const std::vector<Expr>& children);
 170
 171   /**
 172    * Make an n-ary expression of given kind given a first arg and
 173    * a vector of its remaining children (this can be useful where the
 174    * kind is parameterized operator, so the first arg is really an
 175    * arg to the kind to construct an operator)
 176    *
 177    * @param kind the kind of expression to build
 178    * @param child1 the first subexpression
 179    * @param otherChildren the remaining subexpressions
 180    * @return the n-ary expression
 181    */
 182   Expr mkExpr(Kind kind, Expr child1, const std::vector<Expr>& otherChildren);
 183
 184   /**
 185    * Make a nullary parameterized expression with the given operator.
 186    *
 187    * @param opExpr the operator expression
 188    * @return the nullary expression
 189    */
 190   Expr mkExpr(Expr opExpr);
 191
 192   /**
 193    * Make a unary parameterized expression with the given operator.
 194    *
 195    * @param opExpr the operator expression
 196    * @param child1 the subexpression
 197    * @return the unary expression
 198    */
 199   Expr mkExpr(Expr opExpr, Expr child1);
 200
 201   /**
 202    * Make a binary parameterized expression with the given operator.
 203    *
 204    * @param opExpr the operator expression
 205    * @param child1 the first subexpression
 206    * @param child2 the second subexpression
 207    * @return the binary expression
 208    */
 209   Expr mkExpr(Expr opExpr, Expr child1, Expr child2);
 210
 211   /**
 212    * Make a ternary parameterized expression with the given operator.
 213    *
 214    * @param opExpr the operator expression
 215    * @param child1 the first subexpression
 216    * @param child2 the second subexpression
 217    * @param child3 the third subexpression
 218    * @return the ternary expression
 219    */
 220   Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3);
 221
 222   /**
 223    * Make a quaternary parameterized expression with the given operator.
 224    *
 225    * @param opExpr the operator expression
 226    * @param child1 the first subexpression
 227    * @param child2 the second subexpression
 228    * @param child3 the third subexpression
 229    * @param child4 the fourth subexpression
 230    * @return the quaternary expression
 231    */
 232   Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4);
 233
 234   /**
 235    * Make a quinary parameterized expression with the given operator.
 236    *
 237    * @param opExpr the operator expression
 238    * @param child1 the first subexpression
 239    * @param child2 the second subexpression
 240    * @param child3 the third subexpression
 241    * @param child4 the fourth subexpression
 242    * @param child5 the fifth subexpression
 243    * @return the quinary expression
 244    */
 245   Expr mkExpr(Expr opExpr, Expr child1, Expr child2, Expr child3, Expr child4,
 246               Expr child5);
 247
 248   /**
 249    * Make an n-ary expression of given operator to apply and a vector
 250    * of its children
 251    *
 252    * @param opExpr the operator expression
 253    * @param children the subexpressions
 254    * @return the n-ary expression
 255    */
 256   Expr mkExpr(Expr opExpr, const std::vector<Expr>& children);
 257
 258   /** Create a constant of type T */
 259   template <class T>
 260   Expr mkConst(const T&);
 261
 262   /**
 263    * Create an Expr by applying an associative operator to the children.
 264    * If <code>children.size()</code> is greater than the max arity for
 265    * <code>kind</code>, then the expression will be broken up into
 266    * suitably-sized chunks, taking advantage of the associativity of
 267    * <code>kind</code>. For example, if kind <code>FOO</code> has max arity
 268    * 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
 269    * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
 270    * The order of the arguments will be preserved in a left-to-right
 271    * traversal of the resulting tree.
 272    */
 273   Expr mkAssociative(Kind kind, const std::vector<Expr>& children);
 274
 275   /**
 276    * Create an Expr by applying an binary left-associative operator to the
 277    * children. For example, mkLeftAssociative( f, { a, b, c } ) returns
 278    * f( f( a, b ), c ).
 279    */
 280   Expr mkLeftAssociative(Kind kind, const std::vector<Expr>& children);
 281   /**
 282    * Create an Expr by applying an binary right-associative operator to the
 283    * children. For example, mkRightAssociative( f, { a, b, c } ) returns
 284    * f( a, f( b, c ) ).
 285    */
 286   Expr mkRightAssociative(Kind kind, const std::vector<Expr>& children);
 287
 288   /** make chain
 289    *
 290    * Given a kind k and arguments t_1, ..., t_n, this returns the
 291    * conjunction of:
 292    *  (k t_1 t_2) .... (k t_{n-1} t_n)
 293    * It is expected that k is a kind denoting a predicate, and args is a list
 294    * of terms of size >= 2 such that the terms above are well-typed.
 295    */
 296   Expr mkChain(Kind kind, const std::vector<Expr>& children);
 297
 298   /**
 299    * Determine whether Exprs of a particular Kind have operators.
 300    * @returns true if Exprs of Kind k have operators.
 301    */
 302   static bool hasOperator(Kind k);
 303
 304   /**
 305    * Get the (singleton) operator of an OPERATOR-kinded kind.  The
 306    * returned Expr e will have kind BUILTIN, and calling
 307    * e.getConst<CVC4::Kind>() will yield k.
 308    */
 309   Expr operatorOf(Kind k);
 310
 311   /** Get a Kind from an operator expression */
 312   Kind operatorToKind(Expr e);
 313
 314   /** Make a function type from domain to range. */
 315   FunctionType mkFunctionType(Type domain, Type range);
 316
 317   /**
 318    * Make a function type with input types from argTypes.
 319    * <code>argTypes</code> must have at least one element.
 320    */
 321   FunctionType mkFunctionType(const std::vector<Type>& argTypes, Type range);
 322
 323   /**
 324    * Make a function type with input types from
 325    * <code>sorts[0..sorts.size()-2]</code> and result type
 326    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
 327    * at least 2 elements.
 328    */
 329   FunctionType mkFunctionType(const std::vector<Type>& sorts);
 330
 331   /**
 332    * Make a predicate type with input types from
 333    * <code>sorts</code>. The result with be a function type with range
 334    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
 335    * element.
 336    */
 337   FunctionType mkPredicateType(const std::vector<Type>& sorts);
 338
 339   /**
 340    * Make a symbolic expressiontype with types from
 341    * <code>types[0..types.size()-1]</code>.  <code>types</code> may
 342    * have any number of elements.
 343    */
 344   SExprType mkSExprType(const std::vector<Type>& types);
 345
 346   /** Make a type representing a floating-point type with the given parameters. */
 347   FloatingPointType mkFloatingPointType(unsigned exp, unsigned sig) const;
 348
 349   /** Make a type representing a bit-vector of the given size. */
 350   BitVectorType mkBitVectorType(unsigned size) const;
 351
 352   /** Make the type of arrays with the given parameterization. */
 353   ArrayType mkArrayType(Type indexType, Type constituentType) const;
 354
 355   /** Make the type of set with the given parameterization. */
 356   SetType mkSetType(Type elementType) const;
 357
 358   /** Make the type of sequence with the given parameterization. */
 359   SequenceType mkSequenceType(Type elementType) const;
 360
 361   /** Bits for use in mkSort() flags. */
 362   enum {
 363     SORT_FLAG_NONE = 0,
 364     SORT_FLAG_PLACEHOLDER = 1
 365   };/* enum */
 366
 367   /** Make a new sort with the given name. */
 368   SortType mkSort(const std::string& name, uint32_t flags = SORT_FLAG_NONE) const;
 369
 370   /** Make a sort constructor from a name and arity. */
 371   SortConstructorType mkSortConstructor(const std::string& name,
 372                                         size_t arity,
 373                                         uint32_t flags = SORT_FLAG_NONE) const;
 374
 375   /**
 376    * Get the type of an expression.
 377    *
 378    * Throws a TypeCheckingException on failures or if a Type cannot be
 379    * computed.
 380    */
 381   Type getType(Expr e, bool check = false);
 382
 383   /** Bits for use in mkVar() flags. */
 384   enum {
 385     VAR_FLAG_NONE = 0,
 386     VAR_FLAG_GLOBAL = 1,
 387     VAR_FLAG_DEFINED = 2
 388   };/* enum */
 389
 390   /**
 391    * Create a new, fresh variable.  This variable is guaranteed to be
 392    * distinct from every variable thus far in the ExprManager, even
 393    * if it shares a name with another; this is to support any kind of
 394    * scoping policy on top of ExprManager.  The SymbolTable class
 395    * can be used to store and lookup symbols by name, if desired.
 396    *
 397    * @param name a name to associate to the fresh new variable
 398    * @param type the type for the new variable
 399    * @param flags - VAR_FLAG_NONE - no flags;
 400    * VAR_FLAG_GLOBAL - whether this variable is to be
 401    * considered "global" or not.  Note that this information isn't
 402    * used by the ExprManager, but is passed on to the ExprManager's
 403    * event subscribers like the model-building service; if isGlobal
 404    * is true, this newly-created variable will still available in
 405    * models generated after an intervening pop.
 406    * VAR_FLAG_DEFINED - if this is to be a "defined" symbol, e.g., for
 407    * use with SmtEngine::defineFunction().  This keeps a declaration
 408    * from being emitted in API dumps (since a subsequent definition is
 409    * expected to be dumped instead).
 410    */
 411   Expr mkVar(const std::string& name, Type type, uint32_t flags = VAR_FLAG_NONE);
 412
 413   /**
 414    * Create a (nameless) new, fresh variable.  This variable is guaranteed
 415    * to be distinct from every variable thus far in the ExprManager.
 416    *
 417    * @param type the type for the new variable
 418    * @param flags - VAR_FLAG_GLOBAL - whether this variable is to be considered "global"
 419    * or not.  Note that this information isn't used by the ExprManager,
 420    * but is passed on to the ExprManager's event subscribers like the
 421    * model-building service; if isGlobal is true, this newly-created
 422    * variable will still available in models generated after an
 423    * intervening pop.
 424    */
 425   Expr mkVar(Type type, uint32_t flags = VAR_FLAG_NONE);
 426
 427   /**
 428    * Create a new, fresh variable for use in a binder expression
 429    * (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS).  It is
 430    * an error for this bound variable to exist outside of a binder,
 431    * and it should also only be used in a single binder expression.
 432    * That is, two distinct FORALL expressions should use entirely
 433    * disjoint sets of bound variables (however, a single FORALL
 434    * expression can be used in multiple places in a formula without
 435    * a problem).  This newly-created bound variable is guaranteed to
 436    * be distinct from every variable thus far in the ExprManager, even
 437    * if it shares a name with another; this is to support any kind of
 438    * scoping policy on top of ExprManager.  The SymbolTable class
 439    * can be used to store and lookup symbols by name, if desired.
 440    *
 441    * @param name a name to associate to the fresh new bound variable
 442    * @param type the type for the new bound variable
 443    */
 444   Expr mkBoundVar(const std::string& name, Type type);
 445
 446   /**
 447    * Create a (nameless) new, fresh variable for use in a binder
 448    * expression (the BOUND_VAR_LIST of a FORALL, EXISTS, LAMBDA, or WITNESS).
 449    * It is an error for this bound variable to exist outside of a
 450    * binder, and it should also only be used in a single binder
 451    * expression.  That is, two distinct FORALL expressions should use
 452    * entirely disjoint sets of bound variables (however, a single FORALL
 453    * expression can be used in multiple places in a formula without
 454    * a problem).  This newly-created bound variable is guaranteed to
 455    * be distinct from every variable thus far in the ExprManager.
 456    *
 457    * @param type the type for the new bound variable
 458    */
 459   Expr mkBoundVar(Type type);
 460
 461   /**
 462    * Create unique variable of type
 463    */
 464   Expr mkNullaryOperator( Type type, Kind k);
 465
 466   /** Get a reference to the statistics registry for this ExprManager */
 467   Statistics getStatistics() const;
 468
 469   /** Get a reference to the statistics registry for this ExprManager */
 470   SExpr getStatistic(const std::string& name) const;
 471
 472   /**
 473    * Flushes statistics for this ExprManager to a file descriptor. Safe to use
 474    * in a signal handler.
 475    */
 476   void safeFlushStatistics(int fd) const;
 477
 478   /** Export an expr to a different ExprManager */
 479   //static Expr exportExpr(const Expr& e, ExprManager* em);
 480   /** Export a type to a different ExprManager */
 481   static Type exportType(const Type& t, ExprManager* em, ExprManagerMapCollection& vmap);
 482
 483   /** Returns the minimum arity of the given kind. */
 484   static unsigned minArity(Kind kind);
 485
 486   /** Returns the maximum arity of the given kind. */
 487   static unsigned maxArity(Kind kind);
 488
 489   /** Whether a kind is n-ary. The test is based on n-ary kinds having their
 490    * maximal arity as the maximal possible number of children of a node.
 491    **/
 492   static bool isNAryKind(Kind fun);
 493 };/* class ExprManager */
 494
 495 ${mkConst_instantiations}
 496
 497 }/* CVC4 namespace */
 498
 499 #endif /* CVC4__EXPR_MANAGER_H */