diff options
author | Morgan Deters <mdeters@gmail.com> | 2009-11-24 21:03:35 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2009-11-24 21:03:35 +0000 |
commit | 811158832b74e3b101af2c7473f4e11a41377dd4 (patch) | |
tree | 07c55ab126dd7eb24239b615c987a490b182c8a6 /src/expr | |
parent | f6968899de4d27c5bc986c3ac89972fbbe35c361 (diff) |
configure option adjustments as per 11/24 meeting; various fixes and improvements
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/expr.cpp | 2 | ||||
-rw-r--r-- | src/expr/expr.h | 103 | ||||
-rw-r--r-- | src/expr/expr_attribute.h | 2 | ||||
-rw-r--r-- | src/expr/expr_builder.cpp | 85 | ||||
-rw-r--r-- | src/expr/expr_builder.h | 8 | ||||
-rw-r--r-- | src/expr/expr_manager.h | 2 | ||||
-rw-r--r-- | src/expr/expr_value.h | 2 | ||||
-rw-r--r-- | src/expr/kind.h | 4 |
8 files changed, 186 insertions, 22 deletions
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index f1b334ff8..e25cf8595 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -10,7 +10,7 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#include "cvc4_expr.h" +#include "expr/expr.h" #include "expr_value.h" #include "expr_builder.h" diff --git a/src/expr/expr.h b/src/expr/expr.h new file mode 100644 index 000000000..d99708991 --- /dev/null +++ b/src/expr/expr.h @@ -0,0 +1,103 @@ +/********************* -*- 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 skolemExpr(int i) const; + Expr substExpr(const std::vector<Expr>& oldTerms, + const std::vector<Expr>& newTerms) 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 */ diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h index b44c9af6f..03140c4eb 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -17,7 +17,7 @@ #include <stdint.h> #include "config.h" #include "context/context.h" -#include "cvc4_expr.h" +#include "expr/expr.h" namespace CVC4 { namespace expr { diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index c5f366654..bf572cfbc 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -38,7 +38,7 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { } ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { - cvc4assert(!d_used); + Assert( !d_used ); if(d_nchildren > nchild_thresh) { d_children.u_vec = new vector<Expr>(); @@ -74,59 +74,104 @@ ExprBuilder::~ExprBuilder() { // Compound expression constructors ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { - if(d_kind != UNDEFINED_KIND && d_kind != EQUAL) + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != EQUAL )) { collapse(); - d_kind = EQUAL; + d_kind = EQUAL; + } + addChild(right); return *this; } ExprBuilder& ExprBuilder::notExpr() { - if(d_kind != UNDEFINED_KIND) - collapse(); + Assert( d_kind != UNDEFINED_KIND ); + collapse(); d_kind = NOT; return *this; } // avoid double-negatives ExprBuilder& ExprBuilder::negate() { - if(d_kind == NOT) + if(EXPECT_FALSE( d_kind == NOT )) return reset(d_children.u_arr[0]); - if(d_kind != UNDEFINED_KIND) - collapse(); + Assert( d_kind != UNDEFINED_KIND ); + collapse(); d_kind = NOT; return *this; } ExprBuilder& ExprBuilder::andExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(d_kind != AND) { + collapse(); + d_kind = AND; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::orExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != OR )) { + collapse(); + d_kind = OR; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = ITE; + addChild(thenpart); + addChild(elsepart); + return *this; } ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != IFF )) { + collapse(); + d_kind = IFF; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::impExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = IMPLIES; + addChild(right); + return *this; } ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != XOR )) { + collapse(); + d_kind = XOR; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::skolemExpr(int i) { -} - -ExprBuilder& ExprBuilder::substExpr(const std::vector<Expr>& oldTerms, - const std::vector<Expr>& newTerms) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = SKOLEM; + //addChild(i);//FIXME: int constant + return *this; } // "Stream" expression constructor syntax ExprBuilder& ExprBuilder::operator<<(const Kind& op) { + return *this; } ExprBuilder& ExprBuilder::operator<<(const Expr& child) { + return *this; } void ExprBuilder::addChild(const Expr& e) { @@ -182,21 +227,27 @@ void ExprBuilder::collapse() { // not const ExprBuilder::operator Expr() { + // FIXME } -AndExprBuilder ExprBuilder::operator&&(Expr) { +AndExprBuilder ExprBuilder::operator&&(Expr e) { + return AndExprBuilder(*this) && e; } -OrExprBuilder ExprBuilder::operator||(Expr) { +OrExprBuilder ExprBuilder::operator||(Expr e) { + return OrExprBuilder(*this) || e; } -PlusExprBuilder ExprBuilder::operator+ (Expr) { +PlusExprBuilder ExprBuilder::operator+ (Expr e) { + return PlusExprBuilder(*this) + e; } -PlusExprBuilder ExprBuilder::operator- (Expr) { +PlusExprBuilder ExprBuilder::operator- (Expr e) { + return PlusExprBuilder(*this) - e; } -MultExprBuilder ExprBuilder::operator* (Expr) { +MultExprBuilder ExprBuilder::operator* (Expr e) { + return MultExprBuilder(*this) * e; } }/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 07d069a9e..97f18ca6d 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -109,6 +109,8 @@ class AndExprBuilder { public: + AndExprBuilder(const ExprBuilder&); + AndExprBuilder& operator&&(Expr); OrExprBuilder operator||(Expr); @@ -121,6 +123,8 @@ class OrExprBuilder { public: + OrExprBuilder(const ExprBuilder&); + AndExprBuilder operator&&(Expr); OrExprBuilder& operator||(Expr); @@ -133,6 +137,8 @@ class PlusExprBuilder { public: + PlusExprBuilder(const ExprBuilder&); + PlusExprBuilder& operator+(Expr); PlusExprBuilder& operator-(Expr); MultExprBuilder operator*(Expr); @@ -146,6 +152,8 @@ class MultExprBuilder { public: + MultExprBuilder(const ExprBuilder&); + PlusExprBuilder operator+(Expr); PlusExprBuilder operator-(Expr); MultExprBuilder& operator*(Expr); diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 802cfe9c0..e3fbd91bf 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -13,7 +13,7 @@ #define __CVC4__EXPR_MANAGER_H #include <vector> -#include "cvc4_expr.h" +#include "expr/expr.h" #include "kind.h" namespace CVC4 { diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index e0451f7a6..0b97dfdae 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -16,7 +16,7 @@ /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ /* to resolve a circular dependency */ -#include "cvc4_expr.h" +#include "expr/expr.h" #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H diff --git a/src/expr/kind.h b/src/expr/kind.h index 98cc7e2e3..db25d914e 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -36,12 +36,14 @@ enum Kind { AND, IFF, + IMPLIES, OR, XOR, /* from arith */ PLUS, - MINUS + MINUS, + MULT };/* enum Kind */ |