libcvc4-dev 1.5-1 / usr / include / cvc4 / expr / expr.h

/*********************                                                        */
/** expr.h
 **
 ** Copyright 2010-2014  New York University and The University of Iowa,
 ** and as below.
 **
 ** This file automatically generated by:
 **
 **     ../../../../../src/expr/mkexpr ../../../../../src/expr/expr_template.h ../../../../../src/theory/builtin/kinds ../../../../../src/theory/booleans/kinds ../../../../../src/theory/uf/kinds ../../../../../src/theory/arith/kinds ../../../../../src/theory/bv/kinds ../../../../../src/theory/fp/kinds ../../../../../src/theory/arrays/kinds ../../../../../src/theory/datatypes/kinds ../../../../../src/theory/sep/kinds ../../../../../src/theory/sets/kinds ../../../../../src/theory/strings/kinds ../../../../../src/theory/quantifiers/kinds ../../../../../src/theory/idl/kinds
 **
 ** for the CVC4 project.
 **/

/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */

/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */
/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */

/* Edit the template file instead:                     */
/* ../../../../../src/expr/expr_template.h */

/*********************                                                        */
/*! \file expr_template.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Morgan Deters, Dejan Jovanovic, Christopher L. Conway
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
 ** in the top-level source directory) and their institutional affiliations.
 ** All rights reserved.  See the file COPYING in the top-level source
 ** directory for licensing information.\endverbatim
 **
 ** \brief Public-facing expression interface.
 **
 ** Public-facing expression interface.
 **/

#include <cvc4/cvc4_public.h>

// putting the constant-payload #includes up here allows circularity
// (some of them may require a completely-defined Expr type).  This
// way, those #includes can forward-declare some stuff to get Expr's
// getConst<> template instantiations correct, and then #include
// "expr.h" safely, then go on to completely declare their own stuff.

#include <cvc4/expr/uninterpreted_constant.h>
#include <cvc4/util/abstract_value.h>
#include <cvc4/expr/kind.h>
#include <cvc4/expr/chain.h>
#include <cvc4/expr/kind.h>
#include <cvc4/expr/predicate.h>
#include <cvc4/util/bool.h>
#include <cvc4/util/divisible.h>
#include <cvc4/util/subrange_bound.h>
#include <cvc4/util/rational.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/bitvector.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/util/floatingpoint.h>
#include <cvc4/expr/array_store_all.h>
#include <cvc4/expr/datatype.h>
#include <cvc4/expr/ascription_type.h>
#include <cvc4/util/tuple.h>
#include <cvc4/expr/record.h>
#include <cvc4/expr/emptyset.h>
#include <cvc4/util/regexp.h>
#include <cvc4/util/regexp.h>

#ifndef __CVC4__EXPR_H
#define __CVC4__EXPR_H

#include <stdint.h>
#include <iostream>
#include <iterator>

#include <string>

#include <cvc4/base/exception.h>
#include <cvc4/options/language.h>
#include <cvc4/util/hash.h>

// This is a hack, but an important one: if there's an error, the
// compiler directs the user to the template file instead of the
// generated one.  We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
#line 44 "../../../../../src/expr/expr_template.h"

namespace CVC4 {

// The internal expression representation
template <bool ref_count>
class NodeTemplate;

class NodeManager;

class Expr;
class ExprManager;
class SmtEngine;
class Type;
class TypeCheckingException;
class TypeCheckingExceptionPrivate;

namespace expr {
  namespace pickle {
    class Pickler;
  }/* CVC4::expr::pickle namespace */
}/* CVC4::expr namespace */

namespace prop {
  class TheoryProxy;
}/* CVC4::prop namespace */

struct ExprManagerMapCollection;

struct ExprHashFunction;

namespace smt {
  class SmtEnginePrivate;
}/* CVC4::smt namespace */

namespace expr {
  class ExportPrivate;
}/* CVC4::expr namespace */

/**
 * Exception thrown in the case of type-checking errors.
 */
class CVC4_PUBLIC TypeCheckingException : public Exception {

  friend class SmtEngine;
  friend class smt::SmtEnginePrivate;

private:

  /** The expression responsible for the error */
  Expr* d_expr;

protected:

  TypeCheckingException() throw() : Exception() {}
  TypeCheckingException(ExprManager* em,
                        const TypeCheckingExceptionPrivate* exc) throw();

public:

  TypeCheckingException(const Expr& expr, std::string message) throw();

  /** Copy constructor */
  TypeCheckingException(const TypeCheckingException& t) throw();

  /** Destructor */
  ~TypeCheckingException() throw();

  /**
   * Get the Expr that caused the type-checking to fail.
   *
   * @return the expr
   */
  Expr getExpression() const throw();

  /**
   * Returns the message corresponding to the type-checking failure.
   * We prefer toStream() to toString() because that keeps the expr-depth
   * and expr-language settings present in the stream.
   */
  void toStream(std::ostream& out) const throw();

  friend class ExprManager;
};/* class TypeCheckingException */

/**
 * Exception thrown in case of failure to export
 */
class CVC4_PUBLIC ExportUnsupportedException : public Exception {
public:
  ExportUnsupportedException() throw():
    Exception("export unsupported") {
  }
  ExportUnsupportedException(const char* msg) throw():
    Exception(msg) {
  }
};/* class DatatypeExportUnsupportedException */

std::ostream& operator<<(std::ostream& out,
                         const TypeCheckingException& e) CVC4_PUBLIC;

/**
 * Output operator for expressions
 * @param out the stream to output to
 * @param e the expression to output
 * @return the stream
 */
std::ostream& operator<<(std::ostream& out, const Expr& e) CVC4_PUBLIC;

// for hash_maps, hash_sets..
struct ExprHashFunction {
  size_t operator()(CVC4::Expr e) const;
};/* struct ExprHashFunction */

/**
 * Class encapsulating CVC4 expressions and methods for constructing new
 * expressions.
 */
class CVC4_PUBLIC Expr {

  /** The internal expression representation */
  NodeTemplate<true>* d_node;

  /** The responsible expression manager */
  ExprManager* d_exprManager;

  /**
   * Constructor for internal purposes.
   *
   * @param em the expression manager that handles this expression
   * @param node the actual expression node pointer
   */
  Expr(ExprManager* em, NodeTemplate<true>* node);

public:

  /** Default constructor, makes a null expression. */
  Expr();

  /**
   * Copy constructor, makes a copy of a given expression
   *
   * @param e the expression to copy
   */
  Expr(const Expr& e);

  /** Destructor */
  ~Expr();

  /**
   * Assignment operator, makes a copy of the given expression. If the
   * expression managers of the two expressions differ, the expression of
   * the given expression will be used.
   *
   * @param e the expression to assign
   * @return the reference to this expression after assignment
   */
  Expr& operator=(const Expr& e);

  /**
   * Syntactic comparison operator. Returns true if expressions belong to the
   * same expression manager and are syntactically identical.
   *
   * @param e the expression to compare to
   * @return true if expressions are syntactically the same, false otherwise
   */
  bool operator==(const Expr& e) const;

  /**
   * Syntactic disequality operator.
   *
   * @param e the expression to compare to
   * @return true if expressions differ syntactically, false otherwise
   */
  bool operator!=(const Expr& e) const;

  /**
   * Order comparison operator. The only invariant on the order of expressions
   * is that the expressions that were created sooner will be smaller in the
   * ordering than all the expressions created later. Null expression is the
   * smallest element of the ordering. The behavior of the operator is
   * undefined if the expressions come from two different expression managers.
   *
   * @param e the expression to compare to
   * @return true if this expression is smaller than the given one
   */
  bool operator<(const Expr& e) const;

  /**
   * Order comparison operator. The only invariant on the order of expressions
   * is that the expressions that were created sooner will be smaller in the
   * ordering than all the expressions created later. Null expression is the
   * smallest element of the ordering. The behavior of the operator is
   * undefined if the expressions come from two different expression managers.
   *
   * @param e the expression to compare to
   * @return true if this expression is greater than the given one
   */
  bool operator>(const Expr& e) const;

  /**
   * Order comparison operator. The only invariant on the order of expressions
   * is that the expressions that were created sooner will be smaller in the
   * ordering than all the expressions created later. Null expression is the
   * smallest element of the ordering. The behavior of the operator is
   * undefined if the expressions come from two different expression managers.
   *
   * @param e the expression to compare to
   * @return true if this expression is smaller or equal to the given one
   */
  bool operator<=(const Expr& e) const { return !(*this > e); }

  /**
   * Order comparison operator. The only invariant on the order of expressions
   * is that the expressions that were created sooner will be smaller in the
   * ordering than all the expressions created later. Null expression is the
   * smallest element of the ordering. The behavior of the operator is
   * undefined if the expressions come from two different expression managers.
   *
   * @param e the expression to compare to
   * @return true if this expression is greater or equal to the given one
   */
  bool operator>=(const Expr& e) const { return !(*this < e); }

  /**
   * Get the ID of this expression (used for the comparison operators).
   *
   * @return an identifier uniquely identifying the value this
   * expression holds.
   */
  unsigned long getId() const;

  /**
   * Returns the kind of the expression (AND, PLUS ...).
   *
   * @return the kind of the expression
   */
  Kind getKind() const;

  /**
   * Returns the number of children of this expression.
   *
   * @return the number of children
   */
  size_t getNumChildren() const;

  /**
   * Returns the i'th child of this expression.
   *
   * @param i the index of the child to retrieve
   * @return the child
   */
  Expr operator[](unsigned i) const;

  /**
   * Returns the children of this Expr.
   */
  std::vector<Expr> getChildren() const {
    return std::vector<Expr>(begin(), end());
  }

  /**
   * Returns the Boolean negation of this Expr.
   */
  Expr notExpr() const;

  /**
   * Returns the conjunction of this expression and
   * the given expression.
   */
  Expr andExpr(const Expr& e) const;

  /**
   * Returns the disjunction of this expression and
   * the given expression.
   */
  Expr orExpr(const Expr& e) const;

  /**
   * Returns the exclusive disjunction of this expression and
   * the given expression.
   */
  Expr xorExpr(const Expr& e) const;

  /**
   * Returns the Boolean equivalence of this expression and
   * the given expression.
   */
  Expr iffExpr(const Expr& e) const;

  /**
   * Returns the implication of this expression and
   * the given expression.
   */
  Expr impExpr(const Expr& e) const;

  /**
   * Returns the if-then-else expression with this expression
   * as the Boolean condition and the given expressions as
   * the "then" and "else" expressions.
   */
  Expr iteExpr(const Expr& then_e, const Expr& else_e) const;

  /**
   * Iterator type for the children of an Expr.
   */
  class const_iterator : public std::iterator<std::input_iterator_tag, Expr> {
    ExprManager* d_exprManager;
    void* d_iterator;

    explicit const_iterator(ExprManager*, void*);

    friend class Expr;// to access void* constructor

  public:
    const_iterator();
    const_iterator(const const_iterator& it);
    const_iterator& operator=(const const_iterator& it);
    ~const_iterator();
    bool operator==(const const_iterator& it) const;
    bool operator!=(const const_iterator& it) const {
      return !(*this == it);
    }
    const_iterator& operator++();
    const_iterator operator++(int);
    Expr operator*() const;
  };/* class Expr::const_iterator */

  /**
   * Returns an iterator to the first child of this Expr.
   */
  const_iterator begin() const;

  /**
   * Returns an iterator to one-off-the-last child of this Expr.
   */
  const_iterator end() const;

  /**
   * Check if this is an expression that has an operator.
   *
   * @return true if this expression has an operator
   */
  bool hasOperator() const;

  /**
   * Get the operator of this expression.
   *
   * @throws IllegalArgumentException if it has no operator
   * @return the operator of this expression
   */
  Expr getOperator() const;

  /**
   * Get the type for this Expr and optionally do type checking.
   *
   * Initial type computation will be near-constant time if
   * type checking is not requested. Results are memoized, so that
   * subsequent calls to getType() without type checking will be
   * constant time.
   *
   * Initial type checking is linear in the size of the expression.
   * Again, the results are memoized, so that subsequent calls to
   * getType(), with or without type checking, will be constant
   * time.
   *
   * NOTE: A TypeCheckingException can be thrown even when type
   * checking is not requested. getType() will always return a
   * valid and correct type and, thus, an exception will be thrown
   * when no valid or correct type can be computed (e.g., if the
   * arguments to a bit-vector operation aren't bit-vectors). When
   * type checking is not requested, getType() will do the minimum
   * amount of checking required to return a valid result.
   *
   * @param check whether we should check the type as we compute it
   * (default: false)
   */
  Type getType(bool check = false) const throw (TypeCheckingException);

  /**
   * Substitute "replacement" in for "e".
   */
  Expr substitute(Expr e, Expr replacement) const;

  /**
   * Substitute "replacements" in for "exes".
   */
  Expr substitute(const std::vector<Expr> exes,
                  const std::vector<Expr>& replacements) const;

  /**
   * Substitute pairs of (ex,replacement) from the given map.
   */
  Expr substitute(const std::hash_map<Expr, Expr, ExprHashFunction> map) const;

  /**
   * Returns the string representation of the expression.
   * @return a string representation of the expression
   */
  std::string toString() const;

  /**
   * Outputs the string representation of the expression to the stream.
   *
   * @param out the stream to serialize this expression to
   * @param toDepth the depth to which to print this expression, or -1
   * to print it fully
   * @param types set to true to ascribe types to the output
   * expressions (might break language compliance, but good for
   * debugging expressions)
   * @param dag the dagification threshold to use (0 == off)
   * @param language the language in which to output
   */
  void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1,
                OutputLanguage language = language::output::LANG_AUTO) const;

  /**
   * Check if this is a null expression.
   *
   * @return true if a null expression
   */
  bool isNull() const;

  /**
   * Check if this is an expression representing a variable.
   *
   * @return true if a variable expression
   */
  bool isVariable() const;

  /**
   * Check if this is an expression representing a constant.
   *
   * @return true if a constant expression
   */
  bool isConst() const;

  /* A note on isAtomic() and isAtomicFormula() (in CVC3 parlance)..
   *
   * It has been decided for now to hold off on implementations of
   * these functions, as they may only be needed in CNF conversion,
   * where it's pointless to do a lazy isAtomic determination by
   * searching through the DAG, and storing it, since the result will
   * only be used once.  For more details see the 4/27/2010 CVC4
   * developer's meeting notes at:
   *
   * http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
   */
  // bool containsDecision(); // is "atomic"
  // bool properlyContainsDecision(); // maybe not atomic but all children are

  /** Extract a constant of type T */
  template <class T>
  const T& getConst() const;

  /**
   * Returns the expression reponsible for this expression.
   */
  ExprManager* getExprManager() const;

  /**
   * Maps this Expr into one for a different ExprManager, using
   * variableMap for the translation and extending it with any new
   * mappings.
   */
  Expr exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap, uint32_t flags = 0) const;

  /**
   * Very basic pretty printer for Expr.
   * This is equivalent to calling e.getNode().printAst(...)
   * @param out output stream to print to.
   * @param indent number of spaces to indent the formula by.
   */
  void printAst(std::ostream& out, int indent = 0) const;

private:

  /**
   * Pretty printer for use within gdb
   * This is not intended to be used outside of gdb.
   * This writes to the ostream Warning() and immediately flushes
   * the ostream.
   */
  void debugPrint();

  /**
   * Returns the actual internal node.
   * @return the internal node
   */
  NodeTemplate<true> getNode() const throw();

  /**
   * Returns the actual internal node as a TNode.
   * @return the internal node
   */
  NodeTemplate<false> getTNode() const throw();

  // Friend to access the actual internal expr information and private methods
  friend class SmtEngine;
  friend class smt::SmtEnginePrivate;
  friend class ExprManager;
  friend class NodeManager;
  friend class TypeCheckingException;
  friend class expr::pickle::Pickler;
  friend class prop::TheoryProxy;
  friend class expr::ExportPrivate;
  friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
  template <bool ref_count> friend class NodeTemplate;

};/* class Expr */


#line 266 "../../../../../src/theory/builtin/kinds"
template <> ::CVC4::UninterpretedConstant const & Expr::getConst< ::CVC4::UninterpretedConstant >() const;

#line 276 "../../../../../src/theory/builtin/kinds"
template <> ::CVC4::AbstractValue const & Expr::getConst< ::CVC4::AbstractValue >() const;

#line 287 "../../../../../src/theory/builtin/kinds"
template <> ::CVC4::Kind const & Expr::getConst< ::CVC4::Kind >() const;

#line 306 "../../../../../src/theory/builtin/kinds"
template <> ::CVC4::Chain const & Expr::getConst< ::CVC4::Chain >() const;

#line 312 "../../../../../src/theory/builtin/kinds"
template <> ::CVC4::TypeConstant const & Expr::getConst< ::CVC4::TypeConstant >() const;

#line 339 "../../../../../src/theory/builtin/kinds"
template <> ::CVC4::Predicate const & Expr::getConst< ::CVC4::Predicate >() const;

#line 21 "../../../../../src/theory/booleans/kinds"
template <> bool const & Expr::getConst< bool >() const;

#line 30 "../../../../../src/theory/arith/kinds"
template <> ::CVC4::Divisible const & Expr::getConst< ::CVC4::Divisible >() const;

#line 49 "../../../../../src/theory/arith/kinds"
template <> ::CVC4::SubrangeBounds const & Expr::getConst< ::CVC4::SubrangeBounds >() const;

#line 62 "../../../../../src/theory/arith/kinds"
template <> ::CVC4::Rational const & Expr::getConst< ::CVC4::Rational >() const;

#line 15 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorSize const & Expr::getConst< ::CVC4::BitVectorSize >() const;

#line 24 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVector const & Expr::getConst< ::CVC4::BitVector >() const;

#line 85 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorBitOf const & Expr::getConst< ::CVC4::BitVectorBitOf >() const;

#line 91 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorExtract const & Expr::getConst< ::CVC4::BitVectorExtract >() const;

#line 97 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorRepeat const & Expr::getConst< ::CVC4::BitVectorRepeat >() const;

#line 103 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorZeroExtend const & Expr::getConst< ::CVC4::BitVectorZeroExtend >() const;

#line 109 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorSignExtend const & Expr::getConst< ::CVC4::BitVectorSignExtend >() const;

#line 115 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorRotateLeft const & Expr::getConst< ::CVC4::BitVectorRotateLeft >() const;

#line 121 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::BitVectorRotateRight const & Expr::getConst< ::CVC4::BitVectorRotateRight >() const;

#line 135 "../../../../../src/theory/bv/kinds"
template <> ::CVC4::IntToBitVector const & Expr::getConst< ::CVC4::IntToBitVector >() const;

#line 16 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPoint const & Expr::getConst< ::CVC4::FloatingPoint >() const;

#line 24 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::RoundingMode const & Expr::getConst< ::CVC4::RoundingMode >() const;

#line 41 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointSize const & Expr::getConst< ::CVC4::FloatingPointSize >() const;

#line 134 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToFPIEEEBitVector const & Expr::getConst< ::CVC4::FloatingPointToFPIEEEBitVector >() const;

#line 146 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToFPFloatingPoint const & Expr::getConst< ::CVC4::FloatingPointToFPFloatingPoint >() const;

#line 159 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToFPReal const & Expr::getConst< ::CVC4::FloatingPointToFPReal >() const;

#line 171 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToFPSignedBitVector const & Expr::getConst< ::CVC4::FloatingPointToFPSignedBitVector >() const;

#line 183 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToFPUnsignedBitVector const & Expr::getConst< ::CVC4::FloatingPointToFPUnsignedBitVector >() const;

#line 196 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToFPGeneric const & Expr::getConst< ::CVC4::FloatingPointToFPGeneric >() const;

#line 211 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToUBV const & Expr::getConst< ::CVC4::FloatingPointToUBV >() const;

#line 223 "../../../../../src/theory/fp/kinds"
template <> ::CVC4::FloatingPointToSBV const & Expr::getConst< ::CVC4::FloatingPointToSBV >() const;

#line 35 "../../../../../src/theory/arrays/kinds"
template <> ::CVC4::ArrayStoreAll const & Expr::getConst< ::CVC4::ArrayStoreAll >() const;

#line 41 "../../../../../src/theory/datatypes/kinds"
template <> ::CVC4::DatatypeIndexConstant const & Expr::getConst< ::CVC4::DatatypeIndexConstant >() const;

#line 73 "../../../../../src/theory/datatypes/kinds"
template <> ::CVC4::AscriptionType const & Expr::getConst< ::CVC4::AscriptionType >() const;

#line 88 "../../../../../src/theory/datatypes/kinds"
template <> ::CVC4::TupleUpdate const & Expr::getConst< ::CVC4::TupleUpdate >() const;

#line 96 "../../../../../src/theory/datatypes/kinds"
template <> ::CVC4::RecordUpdate const & Expr::getConst< ::CVC4::RecordUpdate >() const;

#line 18 "../../../../../src/theory/sets/kinds"
template <> ::CVC4::EmptySet const & Expr::getConst< ::CVC4::EmptySet >() const;

#line 61 "../../../../../src/theory/strings/kinds"
template <> ::CVC4::String const & Expr::getConst< ::CVC4::String >() const;

#line 67 "../../../../../src/theory/strings/kinds"
template <> ::CVC4::RegExp const & Expr::getConst< ::CVC4::RegExp >() const;


#line 557 "../../../../../src/expr/expr_template.h"

inline size_t ExprHashFunction::operator()(CVC4::Expr e) const {
  return (size_t) e.getId();
}

}/* CVC4 namespace */

#endif /* __CVC4__EXPR_H */