diff options
Diffstat (limited to 'src/include/cvc4_expr.h')
-rw-r--r-- | src/include/cvc4_expr.h | 100 |
1 files changed, 0 insertions, 100 deletions
diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h deleted file mode 100644 index 863097123..000000000 --- a/src/include/cvc4_expr.h +++ /dev/null @@ -1,100 +0,0 @@ -/********************* -*- C++ -*- */ -/** cvc4_expr.h - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information. - ** - ** Reference-counted encapsulation of a pointer to an expression. - **/ - -#ifndef __CVC4_EXPR_H -#define __CVC4_EXPR_H - -#include <vector> -#include <stdint.h> - -#include "cvc4_config.h" -#include "expr/kind.h" - -namespace CVC4 { - -namespace expr { - class ExprValue; -}/* CVC4::expr namespace */ - -using CVC4::expr::ExprValue; - -/** - * Encapsulation of an ExprValue pointer. The reference count is - * maintained in the ExprValue. - */ -class CVC4_PUBLIC Expr { - /** A convenient null-valued encapsulated pointer */ - static Expr s_null; - - /** The referenced ExprValue */ - ExprValue* d_ev; - - /** This constructor is reserved for use by the Expr package; one - * must construct an Expr using one of the build mechanisms of the - * Expr package. - * - * Increments the reference count. */ - explicit Expr(ExprValue*); - - typedef Expr* iterator; - typedef Expr const* const_iterator; - - friend class ExprBuilder; - -public: - CVC4_PUBLIC Expr(const Expr&); - - /** Destructor. Decrements the reference count and, if zero, - * collects the ExprValue. */ - CVC4_PUBLIC ~Expr(); - - Expr& operator=(const Expr&) CVC4_PUBLIC; - - /** Access to the encapsulated expression. - * @return the encapsulated expression. */ - ExprValue* operator->() const CVC4_PUBLIC; - - uint64_t hash() const; - - Expr eqExpr(const Expr& right) const; - Expr notExpr() const; - Expr negate() const; // avoid double-negatives - Expr andExpr(const Expr& right) const; - Expr orExpr(const Expr& right) const; - Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; - Expr iffExpr(const Expr& right) const; - Expr impExpr(const Expr& right) const; - Expr xorExpr(const Expr& right) const; - - Expr plusExpr(const Expr& right) const; - Expr uMinusExpr() const; - Expr multExpr(const Expr& right) const; - - inline Kind getKind() const; - - static Expr null() { return s_null; } - -};/* class Expr */ - -}/* CVC4 namespace */ - -#include "expr/expr_value.h" - -namespace CVC4 { - -inline Kind Expr::getKind() const { - return Kind(d_ev->d_kind); -} - -}/* CVC4 namespace */ - -#endif /* __CVC4_EXPR_H */ |