From: Dejan Jovanović Date: Thu, 10 Dec 2009 18:44:51 +0000 (+0000) Subject: killing expr into node... X-Git-Tag: cvc5-1.0.0~9380 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f79afa96e7e7176b974252dd05a9f7bdf70194e8;p=cvc5.git killing expr into node... --- diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 630850387..6ca68d35c 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -7,13 +7,13 @@ noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ attr_type.h \ attr_var_name.h \ - expr.h \ - expr_builder.h \ + node.h \ + node_builder.h \ expr_value.h \ - expr_manager.h \ - expr_attribute.h \ + node_manager.h \ + node_attribute.h \ kind.h \ - expr.cpp \ - expr_builder.cpp \ - expr_manager.cpp \ + node.cpp \ + node_builder.cpp \ + node_manager.cpp \ expr_value.cpp diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index 9d410cea8..de0bad1bd 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -52,7 +52,7 @@ CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libexpr_la_LIBADD = -am_libexpr_la_OBJECTS = expr.lo expr_builder.lo expr_manager.lo \ +am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \ expr_value.lo libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) @@ -223,15 +223,15 @@ noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ attr_type.h \ attr_var_name.h \ - expr.h \ - expr_builder.h \ + node.h \ + node_builder.h \ expr_value.h \ - expr_manager.h \ - expr_attribute.h \ + node_manager.h \ + node_attribute.h \ kind.h \ - expr.cpp \ - expr_builder.cpp \ - expr_manager.cpp \ + node.cpp \ + node_builder.cpp \ + node_manager.cpp \ expr_value.cpp all: all-am @@ -286,10 +286,10 @@ mostlyclean-compile: distclean-compile: -rm -f *.tab.c -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_builder.Plo@am__quote@ -@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_manager.Plo@am__quote@ @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr_value.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_builder.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_manager.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index 1d5e8eb0c..2e0a8b675 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -24,7 +24,7 @@ class Type; class Type_attr { public: enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles - typedef Type value_type;//Expr? + typedef Type value_type;//Node? static const Type_attr marker; }; diff --git a/src/expr/attr_var_name.h b/src/expr/attr_var_name.h index a0780d575..13a2ec36f 100644 --- a/src/expr/attr_var_name.h +++ b/src/expr/attr_var_name.h @@ -24,7 +24,7 @@ class VarName; class VarName_attr { public: enum { hash_value = 11 }; // could use typeid but then different on different machines/compiles - typedef Type value_type;//Expr? + typedef Type value_type;//Node? static const Type_attr marker; }; diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp deleted file mode 100644 index fa273dfa5..000000000 --- a/src/expr/expr.cpp +++ /dev/null @@ -1,115 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr.cpp - ** 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. - **/ - -#include "expr/expr.h" -#include "expr_value.h" -#include "expr_builder.h" -#include "util/Assert.h" - -using namespace CVC4::expr; - -namespace CVC4 { - -ExprValue ExprValue::s_null; - -Expr Expr::s_null(&ExprValue::s_null); - -bool Expr::isNull() const { - return d_ev == &ExprValue::s_null; -} - -Expr::Expr() : - d_ev(&ExprValue::s_null) { - // No refcount needed -} - -Expr::Expr(ExprValue* ev) - : d_ev(ev) { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - d_ev->inc(); -} - -Expr::Expr(const Expr& e) { - Assert(e.d_ev != NULL, "Expecting a non-NULL evpression value!"); - d_ev = e.d_ev; - d_ev->inc(); -} - -Expr::~Expr() { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - d_ev->dec(); -} - -void Expr::assignExprValue(ExprValue* ev) { - d_ev = ev; - d_ev->inc(); -} - -Expr& Expr::operator=(const Expr& e) { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - if(this != &e && d_ev != e.d_ev) { - d_ev->dec(); - d_ev = e.d_ev; - d_ev->inc(); - } - return *this; -} - -ExprValue const* Expr::operator->() const { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - return d_ev; -} - -uint64_t Expr::hash() const { - Assert(d_ev != NULL, "Expecting a non-NULL evpression value!"); - return d_ev->hash(); -} - -Expr Expr::eqExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(EQUAL, *this, right); -} - -Expr Expr::notExpr() const { - return ExprManager::currentEM()->mkExpr(NOT, *this); -} - -// FIXME: What does this do and why? -Expr Expr::negate() const { // avoid double-negatives - return ExprBuilder(*this).negate(); -} - - -Expr Expr::andExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(AND, *this, right); -} - -Expr Expr::orExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(OR, *this, right); -} - -Expr Expr::iteExpr(const Expr& thenpart, const Expr& elsepart) const { - return ExprManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); -} - -Expr Expr::iffExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(IFF, *this, right); -} - -Expr Expr::impExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(IMPLIES, *this, right); -} - -Expr Expr::xorExpr(const Expr& right) const { - return ExprManager::currentEM()->mkExpr(XOR, *this, right); -} - -}/* CVC4 namespace */ diff --git a/src/expr/expr.h b/src/expr/expr.h deleted file mode 100644 index 7440974d8..000000000 --- a/src/expr/expr.h +++ /dev/null @@ -1,181 +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 -#include -#include - -#include "cvc4_config.h" -#include "expr/kind.h" - -namespace CVC4 { - class Expr; -}/* CVC4 namespace */ - -namespace CVC4 { - -inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC; - -class ExprManager; - -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 { - - friend class ExprValue; - - /** 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*); - - friend class ExprBuilder; - friend class ExprManager; - - /** Access to the encapsulated expression. - * @return the encapsulated expression. */ - ExprValue const* operator->() const; - - /** - * Assigns the expression value and does reference counting. No assumptions are - * made on the expression, and should only be used if we know what we are - * doing. - * - * @param ev the expression value to assign - */ - void assignExprValue(ExprValue* ev); - -public: - - /** Default constructor, makes a null expression. */ - Expr(); - - Expr(const Expr&); - - /** Destructor. Decrements the reference count and, if zero, - * collects the ExprValue. */ - ~Expr(); - - bool operator==(const Expr& e) const { return d_ev == e.d_ev; } - bool operator!=(const Expr& e) const { return d_ev != e.d_ev; } - - /** - * We compare by expression ids so, keeping things deterministic and having - * that subexpressions have to be smaller than the enclosing expressions. - */ - inline bool operator<(const Expr& e) const; - - Expr& operator=(const Expr&); - - 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; - - inline size_t numChildren() const; - - static Expr null() { return s_null; } - - typedef Expr* iterator; - typedef Expr const* const_iterator; - - inline iterator begin(); - inline iterator end(); - inline const_iterator begin() const; - inline const_iterator end() const; - - void toString(std::ostream&) const; - - bool isNull() const; - -};/* class Expr */ - -}/* CVC4 namespace */ - -#include "expr/expr_value.h" - -namespace CVC4 { - -inline bool Expr::operator<(const Expr& e) const { - return d_ev->d_id < e.d_ev->d_id; -} - -inline std::ostream& operator<<(std::ostream& out, const Expr& e) { - e.toString(out); - return out; -} - -inline Kind Expr::getKind() const { - return Kind(d_ev->d_kind); -} - -inline void Expr::toString(std::ostream& out) const { - if(d_ev) - d_ev->toString(out); - else out << "null"; -} - -inline Expr::iterator Expr::begin() { - return d_ev->begin(); -} - -inline Expr::iterator Expr::end() { - return d_ev->end(); -} - -inline Expr::const_iterator Expr::begin() const { - return d_ev->begin(); -} - -inline Expr::const_iterator Expr::end() const { - return d_ev->end(); -} - -inline size_t Expr::numChildren() const { - return d_ev->d_nchildren; -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR_H */ diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h deleted file mode 100644 index b68a9d19d..000000000 --- a/src/expr/expr_attribute.h +++ /dev/null @@ -1,98 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_attribute.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. - ** - **/ - -#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H -#define __CVC4__EXPR__EXPR_ATTRIBUTE_H - -#include -#include "config.h" -#include "context/context.h" -#include "expr/expr.h" - -namespace CVC4 { -namespace expr { - -template -class AttrTables; - -// global (or TSS) -extern CDMap g_hash_bool; -extern CDMap g_hash_int; -extern CDMap g_hash_expr; -extern CDMap g_hash_ptr; - -template -class AttrTable; - -template <> -class AttrTable { -public: - class BitAccessor { - uint64_t& d_word; - unsigned d_bit; - public: - BitAccessor& operator=(bool b); - // continue... - }; - - // bool specialization - static CDMap *s_hash; - - template - BitAccessor& find(Expr e, const Attr&); - - template - bool find(Expr e, const Attr&) const; -}; - -template <> -class AttrTable { -public: - // int(egral) specialization - static CDMap *s_hash; - uint64_t& find(Expr); - uint64_t& find(Expr) const; -}; - -template -class AttrTable { - // pointer specialization - static CDMap *s_hash; -public: -}; - -template <> -class AttrTable { -public: - // Expr specialization - static CDMap *s_hash; - Expr find(Expr); -}; - -CDMap* AttrTable::s_hash = &g_hash_bool; -CDMap* AttrTable::s_hash = &g_hash_int; -CDMap* AttrTable::s_hash = &g_hash_expr; - -template -CDMap* AttrTable::s_hash = &g_hash_ptr; - -template -class AttributeTable { - typedef typename Attr::value_type value_type; - - AttrTable& d_table; - -}; - -}/* CVC4::expr namespace */ -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */ diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp deleted file mode 100644 index 10152a338..000000000 --- a/src/expr/expr_builder.cpp +++ /dev/null @@ -1,233 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_builder.cpp - ** 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. - ** - **/ - -#include "expr_builder.h" -#include "expr_manager.h" -#include "expr_value.h" -#include "util/output.h" - -using namespace std; - -namespace CVC4 { - -ExprBuilder::ExprBuilder() : - d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), - d_nchildren(0) { -} - -ExprBuilder::ExprBuilder(Kind k) : - d_em(ExprManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) { -} - -ExprBuilder::ExprBuilder(const Expr& e) : - d_em(ExprManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { - d_children.u_arr[0] = e.d_ev->inc();; -} - -ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { - this->~ExprBuilder(); - d_kind = Kind(ev->d_kind); - d_used = false; - d_nchildren = ev->d_nchildren; - for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i) - addChild(i->d_ev); - return *this; -} - -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) { - Assert( !d_used ); - - if(d_nchildren > nchild_thresh) { - d_children.u_vec = new vector (); - d_children.u_vec->reserve(d_nchildren + 5); - copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), - back_inserter(*d_children.u_vec)); - } else { - ev_iterator j = d_children.u_arr; - ExprValue* const * i = eb.d_children.u_arr; - ExprValue* const * i_end = i + eb.d_nchildren; - for(; i != i_end; ++i, ++j) - *j = (*i)->inc(); - } -} - -ExprBuilder::ExprBuilder(ExprManager* em) : - d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { -} - -ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : - d_em(em), d_kind(k), d_used(false), d_nchildren(0) { -} - -ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : - d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { - d_children.u_arr[0] = e.d_ev->inc(); -} - -ExprBuilder::~ExprBuilder() { - if(d_nchildren > nchild_thresh) { - delete d_children.u_vec; - } else { - ev_iterator i = d_children.u_arr; - ev_iterator i_end = d_children.u_arr + d_nchildren; - for(; i != i_end ; ++i) { - (*i)->dec(); - } - } -} - -// Compound expression constructors -ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { - Assert( d_kind != UNDEFINED_KIND ); - if(EXPECT_TRUE( d_kind != EQUAL )) { - collapse(); - d_kind = EQUAL; - } - addChild(right); - return *this; -} - -ExprBuilder& ExprBuilder::notExpr() { - Assert( d_kind != UNDEFINED_KIND ); - collapse(); - d_kind = NOT; - return *this; -} - -// avoid double-negatives -ExprBuilder& ExprBuilder::negate() { - if(EXPECT_FALSE( d_kind == NOT )) - return reset(d_children.u_arr[0]); 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; -} - -// "Stream" expression constructor syntax -ExprBuilder& ExprBuilder::operator<<(const Kind& op) { - d_kind = op; - return *this; -} - -ExprBuilder& ExprBuilder::operator<<(const Expr& child) { - addChild(child); - return *this; -} - -/** - * We keep the children either: - * (a) In the array of expression values if the number of children is less than - * nchild_thresh. Hence (last else) we increase the reference count. - * (b) If the number of children reaches the nchild_thresh, we allocate a vector - * for the children. Children are now expressions, so we also decrement the - * reference count for each child. - * (c) Otherwise we just add to the end of the vector. - */ -void ExprBuilder::addChild(ExprValue* ev) { - Assert(d_nchildren <= nchild_thresh || - d_nchildren == d_children.u_vec->size(), - "children count doesn't reflect the size of the vector!"); - Debug("expr") << "adding child ev " << ev << endl; - if(d_nchildren == nchild_thresh) { - Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; - vector* v = new vector (); - v->reserve(nchild_thresh + 5); - ExprValue** i = d_children.u_arr; - ExprValue** i_end = i + nchild_thresh; - for(;i != i_end; ++ i) { - v->push_back(Expr(*i)); - (*i)->dec(); - } - v->push_back(Expr(ev)); - d_children.u_vec = v; - ++d_nchildren; - } else if(d_nchildren > nchild_thresh) { - Debug("expr") << "over thresh " << d_nchildren - << " > " << nchild_thresh << endl; - d_children.u_vec->push_back(Expr(ev)); - // ++d_nchildren; no need for this - } else { - Debug("expr") << "under thresh " << d_nchildren - << " < " << nchild_thresh << endl; - d_children.u_arr[d_nchildren ++] = ev->inc(); - } -} - -ExprBuilder& ExprBuilder::collapse() { - if(d_nchildren == nchild_thresh) { - vector* v = new vector (); - v->reserve(nchild_thresh + 5); - // - Unreachable();// unimplemented - } - return *this; -} - -}/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h deleted file mode 100644 index 34e34bf6e..000000000 --- a/src/expr/expr_builder.h +++ /dev/null @@ -1,313 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_builder.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. - ** - **/ - -#ifndef __CVC4__EXPR_BUILDER_H -#define __CVC4__EXPR_BUILDER_H - -#include -#include - -#include "expr_manager.h" -#include "kind.h" -#include "util/Assert.h" - -namespace CVC4 { - -class AndExprBuilder; -class OrExprBuilder; -class PlusExprBuilder; -class MinusExprBuilder; -class MultExprBuilder; - -class ExprBuilder { - ExprManager* d_em; - - Kind d_kind; - - // initially false, when you extract the Expr this is set and you can't - // extract another - bool d_used; - - static const unsigned nchild_thresh = 10; - - unsigned d_nchildren; - union { - ExprValue* u_arr[nchild_thresh]; - std::vector* u_vec; - } d_children; - - void addChild(const Expr& e) { addChild(e.d_ev); } - void addChild(ExprValue*); - ExprBuilder& collapse(); - - typedef ExprValue** ev_iterator; - typedef ExprValue const** const_ev_iterator; - - ev_iterator ev_begin() { - return d_children.u_arr; - } - - ev_iterator ev_end() { - return d_children.u_arr + d_nchildren; - } - - ExprBuilder& reset(const ExprValue*); - -public: - - ExprBuilder(); - ExprBuilder(Kind k); - ExprBuilder(const Expr&); - ExprBuilder(const ExprBuilder&); - - ExprBuilder(ExprManager*); - ExprBuilder(ExprManager*, Kind k); - ExprBuilder(ExprManager*, const Expr&); - ExprBuilder(ExprManager*, const ExprBuilder&); - - ~ExprBuilder(); - - // Compound expression constructors - ExprBuilder& eqExpr(const Expr& right); - ExprBuilder& notExpr(); - ExprBuilder& negate(); // avoid double-negatives - ExprBuilder& andExpr(const Expr& right); - ExprBuilder& orExpr(const Expr& right); - ExprBuilder& iteExpr(const Expr& thenpart, const Expr& elsepart); - ExprBuilder& iffExpr(const Expr& right); - ExprBuilder& impExpr(const Expr& right); - ExprBuilder& xorExpr(const Expr& right); - - /* TODO design: these modify ExprBuilder */ - ExprBuilder& operator!() { return notExpr(); } - ExprBuilder& operator&&(const Expr& right) { return andExpr(right); } - ExprBuilder& operator||(const Expr& right) { return orExpr(right); } - - // "Stream" expression constructor syntax - ExprBuilder& operator<<(const Kind& op); - ExprBuilder& operator<<(const Expr& child); - - // For pushing sequences of children - ExprBuilder& append(const std::vector& children) { return append(children.begin(), children.end()); } - ExprBuilder& append(Expr child) { return append(&child, (&child) + 1); } - template ExprBuilder& append(const Iterator& begin, const Iterator& end); - - operator Expr();// not const - - AndExprBuilder operator&&(Expr); - OrExprBuilder operator||(Expr); - PlusExprBuilder operator+ (Expr); - PlusExprBuilder operator- (Expr); - MultExprBuilder operator* (Expr); - - friend class AndExprBuilder; - friend class OrExprBuilder; - friend class PlusExprBuilder; - friend class MultExprBuilder; -};/* class ExprBuilder */ - -class AndExprBuilder { - ExprBuilder d_eb; - -public: - - AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != AND) { - d_eb.collapse(); - d_eb.d_kind = AND; - } - } - - AndExprBuilder& operator&&(Expr); - OrExprBuilder operator||(Expr); - - operator ExprBuilder() { return d_eb; } - -};/* class AndExprBuilder */ - -class OrExprBuilder { - ExprBuilder d_eb; - -public: - - OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != OR) { - d_eb.collapse(); - d_eb.d_kind = OR; - } - } - - AndExprBuilder operator&&(Expr); - OrExprBuilder& operator||(Expr); - - operator ExprBuilder() { return d_eb; } - -};/* class OrExprBuilder */ - -class PlusExprBuilder { - ExprBuilder d_eb; - -public: - - PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != PLUS) { - d_eb.collapse(); - d_eb.d_kind = PLUS; - } - } - - PlusExprBuilder& operator+(Expr); - PlusExprBuilder& operator-(Expr); - MultExprBuilder operator*(Expr); - - operator ExprBuilder() { return d_eb; } - -};/* class PlusExprBuilder */ - -class MultExprBuilder { - ExprBuilder d_eb; - -public: - - MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) { - if(d_eb.d_kind != MULT) { - d_eb.collapse(); - d_eb.d_kind = MULT; - } - } - - PlusExprBuilder operator+(Expr); - PlusExprBuilder operator-(Expr); - MultExprBuilder& operator*(Expr); - - operator ExprBuilder() { return d_eb; } - -};/* class MultExprBuilder */ - -template -inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { - for(Iterator i = begin; i != end; ++i) - addChild(*i); - return *this; -} - -// not const -inline ExprBuilder::operator Expr() { - ExprValue *ev; - uint64_t hash; - - Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); - - // variables are permitted to be duplicates (from POV of the expression manager) - if(d_kind == VARIABLE) { - ev = new ExprValue; - hash = reinterpret_cast(ev); - } else { - if(d_nchildren <= nchild_thresh) { - hash = ExprValue::computeHash(d_kind, ev_begin(), ev_end()); - void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); - ev = new (space) ExprValue; - size_t nc = 0; - ev_iterator i = ev_begin(); - ev_iterator i_end = ev_end(); - for(; i != i_end; ++i) { - // The expressions in the allocated children are all 0, so we must - // construct it withouth using an assignment operator - ev->d_children[nc++].assignExprValue(*i); - } - } else { - hash = ExprValue::computeHash::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); - void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Expr)); - ev = new (space) ExprValue; - size_t nc = 0; - for(std::vector::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) - ev->d_children[nc++] = Expr(*i); - } - } - - ev->d_nchildren = d_nchildren; - ev->d_kind = d_kind; - ev->d_id = ExprValue::next_id++;// FIXME multithreading - ev->d_rc = 0; - Expr e(ev); - - return d_em->lookup(hash, e); -} - -inline AndExprBuilder ExprBuilder::operator&&(Expr e) { - return AndExprBuilder(*this) && e; -} - -inline OrExprBuilder ExprBuilder::operator||(Expr e) { - return OrExprBuilder(*this) || e; -} - -inline PlusExprBuilder ExprBuilder::operator+ (Expr e) { - return PlusExprBuilder(*this) + e; -} - -inline PlusExprBuilder ExprBuilder::operator- (Expr e) { - return PlusExprBuilder(*this) - e; -} - -inline MultExprBuilder ExprBuilder::operator* (Expr e) { - return MultExprBuilder(*this) * e; -} - -inline AndExprBuilder& AndExprBuilder::operator&&(Expr e) { - d_eb.append(e); - return *this; -} - -inline OrExprBuilder AndExprBuilder::operator||(Expr e) { - return OrExprBuilder(d_eb.collapse()) || e; -} - -inline AndExprBuilder OrExprBuilder::operator&&(Expr e) { - return AndExprBuilder(d_eb.collapse()) && e; -} - -inline OrExprBuilder& OrExprBuilder::operator||(Expr e) { - d_eb.append(e); - return *this; -} - -inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) { - d_eb.append(e); - return *this; -} - -inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) { - d_eb.append(e.negate()); - return *this; -} - -inline MultExprBuilder PlusExprBuilder::operator*(Expr e) { - return MultExprBuilder(d_eb.collapse()) * e; -} - -inline PlusExprBuilder MultExprBuilder::operator+(Expr e) { - return MultExprBuilder(d_eb.collapse()) + e; -} - -inline PlusExprBuilder MultExprBuilder::operator-(Expr e) { - return MultExprBuilder(d_eb.collapse()) - e; -} - -inline MultExprBuilder& MultExprBuilder::operator*(Expr e) { - d_eb.append(e); - return *this; -} - - -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR_BUILDER_H */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp deleted file mode 100644 index 3b5347301..000000000 --- a/src/expr/expr_manager.cpp +++ /dev/null @@ -1,93 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_manager.cpp - ** 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. - ** - ** Expression manager implementation. - **/ - -#include "expr_builder.h" -#include "expr_manager.h" -#include "expr/expr.h" - -namespace CVC4 { - -__thread ExprManager* ExprManager::s_current = 0; - -Expr ExprManager::lookup(uint64_t hash, const Expr& e) { - Assert(this != NULL, "Woops, we have a bad expression manager!"); - hash_t::iterator i = d_hash.find(hash); - if(i == d_hash.end()) { - // insert - std::vector v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } else { - for(std::vector::iterator j = i->second.begin(); j != i->second.end(); ++j) { - if(e.getKind() != j->getKind()) - continue; - - if(e.numChildren() != j->numChildren()) - continue; - - Expr::const_iterator c1 = e.begin(); - Expr::iterator c2 = j->begin(); - for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { - if(c1->d_ev != c2->d_ev) - break; - } - - if(c1 != e.end() || c2 != j->end()) - continue; - - return *j; - } - // didn't find it, insert - std::vector v; - v.push_back(e); - d_hash.insert(std::make_pair(hash, v)); - return e; - } -} - -// general expression-builders - -Expr ExprManager::mkExpr(Kind kind) { - return ExprBuilder(this, kind); -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { - return ExprBuilder(this, kind) << child1; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) { - return ExprBuilder(this, kind) << child1 << child2; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3) { - return ExprBuilder(this, kind) << child1 << child2 << child3; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4) { - return ExprBuilder(this, kind) << child1 << child2 << child3 << child4; -} - -Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5) { - return ExprBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; -} - -// N-ary version -Expr ExprManager::mkExpr(Kind kind, std::vector children) { - return ExprBuilder(this, kind).append(children); -} - -Expr ExprManager::mkVar() { - return ExprBuilder(this, VARIABLE); -} - -}/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h deleted file mode 100644 index 542d1040d..000000000 --- a/src/expr/expr_manager.h +++ /dev/null @@ -1,74 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_manager.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. - ** - **/ - -#ifndef __CVC4__EXPR_MANAGER_H -#define __CVC4__EXPR_MANAGER_H - -#include -#include - -#include "expr/expr.h" -#include "kind.h" - -namespace CVC4 { - -namespace expr { - class ExprBuilder; -}/* CVC4::expr namespace */ - -class CVC4_PUBLIC ExprManager { - static __thread ExprManager* s_current; - - friend class CVC4::ExprBuilder; - - typedef std::map > hash_t; - hash_t d_hash; - - Expr lookup(uint64_t hash, const Expr& e); - -public: - static ExprManager* currentEM() { return s_current; } - - // general expression-builders - Expr mkExpr(Kind kind); - Expr mkExpr(Kind kind, const Expr& child1); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4); - Expr mkExpr(Kind kind, const Expr& child1, const Expr& child2, const Expr& child3, const Expr& child4, const Expr& child5); - // N-ary version - Expr mkExpr(Kind kind, std::vector children); - - // variables are special, because duplicates are permitted - Expr mkVar(); - - // TODO: these use the current EM (but must be renamed) - /* - static Expr mkExpr(Kind kind) - { currentEM()->mkExpr(kind); } - static Expr mkExpr(Kind kind, Expr child1); - { currentEM()->mkExpr(kind, child1); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2); - { currentEM()->mkExpr(kind, child1, child2); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); - { currentEM()->mkExpr(kind, child1, child2, child3); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); - { currentEM()->mkExpr(kind, child1, child2, child3, child4); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); - { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } - */ - - // do we want a varargs one? perhaps not.. -}; - -}/* CVC4 namespace */ - -#endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index 17f3b64c3..9ce7c3e12 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -10,7 +10,7 @@ ** An expression node. ** ** Instances of this class are generally referenced through - ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the + ** cvc4::Node rather than by pointer; cvc4::Node maintains the ** reference count on ExprValue instances and **/ diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index b334e1c2d..10f09e565 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -10,13 +10,13 @@ ** An expression node. ** ** Instances of this class are generally referenced through - ** cvc4::Expr rather than by pointer; cvc4::Expr maintains the + ** cvc4::Node rather than by pointer; cvc4::Node maintains the ** reference count on ExprValue instances and **/ /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ /* to resolve a circular dependency */ -#include "expr/expr.h" +#include "expr/node.h" #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H @@ -27,8 +27,8 @@ namespace CVC4 { -class Expr; -class ExprBuilder; +class Node; +class NodeBuilder; namespace expr { @@ -49,7 +49,7 @@ class ExprValue { /** The ID (0 is reserved for the null value) */ unsigned d_id : 32; - /** The expression's reference count. @see cvc4::Expr. */ + /** The expression's reference count. @see cvc4::Node. */ unsigned d_rc : 8; /** Kind of the expression */ @@ -59,12 +59,12 @@ class ExprValue { unsigned d_nchildren : 16; /** Variable number of child nodes */ - Expr d_children[0]; + Node d_children[0]; // todo add exprMgr ref in debug case - friend class CVC4::Expr; - friend class CVC4::ExprBuilder; + friend class CVC4::Node; + friend class CVC4::NodeBuilder; ExprValue* inc(); ExprValue* dec(); @@ -76,7 +76,7 @@ class ExprValue { /** * Computes the hash over the given iterator span of children, and the - * root hash. The iterator should be either over a range of Expr or pointers + * root hash. The iterator should be either over a range of Node or pointers * to ExprValue. * @param hash the initial value for the hash * @param begin the begining of the range @@ -97,8 +97,8 @@ public: // Iterator support - typedef Expr* iterator; - typedef Expr const* const_iterator; + typedef Node* iterator; + typedef Node const* const_iterator; iterator begin(); iterator end(); diff --git a/src/expr/node.cpp b/src/expr/node.cpp new file mode 100644 index 000000000..22a905470 --- /dev/null +++ b/src/expr/node.cpp @@ -0,0 +1,115 @@ +/********************* -*- C++ -*- */ +/** expr.cpp + ** 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. + **/ + +#include "expr/node.h" +#include "expr/expr_value.h" +#include "expr/node_builder.h" +#include "util/Assert.h" + +using namespace CVC4::expr; + +namespace CVC4 { + +ExprValue ExprValue::s_null; + +Node Node::s_null(&ExprValue::s_null); + +bool Node::isNull() const { + return d_ev == &ExprValue::s_null; +} + +Node::Node() : + d_ev(&ExprValue::s_null) { + // No refcount needed +} + +Node::Node(ExprValue* ev) + : d_ev(ev) { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + d_ev->inc(); +} + +Node::Node(const Node& e) { + Assert(e.d_ev != NULL, "Expecting a non-NULL expression value!"); + d_ev = e.d_ev; + d_ev->inc(); +} + +Node::~Node() { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + d_ev->dec(); +} + +void Node::assignExprValue(ExprValue* ev) { + d_ev = ev; + d_ev->inc(); +} + +Node& Node::operator=(const Node& e) { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + if(this != &e && d_ev != e.d_ev) { + d_ev->dec(); + d_ev = e.d_ev; + d_ev->inc(); + } + return *this; +} + +ExprValue const* Node::operator->() const { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + return d_ev; +} + +uint64_t Node::hash() const { + Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); + return d_ev->hash(); +} + +Node Node::eqExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(EQUAL, *this, right); +} + +Node Node::notExpr() const { + return NodeManager::currentEM()->mkExpr(NOT, *this); +} + +// FIXME: What does this do and why? +Node Node::negate() const { // avoid double-negatives + return NodeBuilder(*this).negate(); +} + + +Node Node::andExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(AND, *this, right); +} + +Node Node::orExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(OR, *this, right); +} + +Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { + return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); +} + +Node Node::iffExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(IFF, *this, right); +} + +Node Node::impExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right); +} + +Node Node::xorExpr(const Node& right) const { + return NodeManager::currentEM()->mkExpr(XOR, *this, right); +} + +}/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h new file mode 100644 index 000000000..aec50000e --- /dev/null +++ b/src/expr/node.h @@ -0,0 +1,181 @@ +/********************* -*- 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 +#include +#include + +#include "cvc4_config.h" +#include "expr/kind.h" + +namespace CVC4 { + class Node; +}/* CVC4 namespace */ + +namespace CVC4 { + +inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC; + +class NodeManager; + +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 Node { + + friend class ExprValue; + + /** A convenient null-valued encapsulated pointer */ + static Node s_null; + + /** The referenced ExprValue */ + ExprValue* d_ev; + + /** This constructor is reserved for use by the Node package; one + * must construct an Node using one of the build mechanisms of the + * Node package. + * + * Increments the reference count. */ + explicit Node(ExprValue*); + + friend class NodeBuilder; + friend class NodeManager; + + /** Access to the encapsulated expression. + * @return the encapsulated expression. */ + ExprValue const* operator->() const; + + /** + * Assigns the expression value and does reference counting. No assumptions are + * made on the expression, and should only be used if we know what we are + * doing. + * + * @param ev the expression value to assign + */ + void assignExprValue(ExprValue* ev); + +public: + + /** Default constructor, makes a null expression. */ + Node(); + + Node(const Node&); + + /** Destructor. Decrements the reference count and, if zero, + * collects the ExprValue. */ + ~Node(); + + bool operator==(const Node& e) const { return d_ev == e.d_ev; } + bool operator!=(const Node& e) const { return d_ev != e.d_ev; } + + /** + * We compare by expression ids so, keeping things deterministic and having + * that subexpressions have to be smaller than the enclosing expressions. + */ + inline bool operator<(const Node& e) const; + + Node& operator=(const Node&); + + uint64_t hash() const; + + Node eqExpr(const Node& right) const; + Node notExpr() const; + Node negate() const; // avoid double-negatives + Node andExpr(const Node& right) const; + Node orExpr(const Node& right) const; + Node iteExpr(const Node& thenpart, const Node& elsepart) const; + Node iffExpr(const Node& right) const; + Node impExpr(const Node& right) const; + Node xorExpr(const Node& right) const; + + Node plusExpr(const Node& right) const; + Node uMinusExpr() const; + Node multExpr(const Node& right) const; + + inline Kind getKind() const; + + inline size_t numChildren() const; + + static Node null() { return s_null; } + + typedef Node* iterator; + typedef Node const* const_iterator; + + inline iterator begin(); + inline iterator end(); + inline const_iterator begin() const; + inline const_iterator end() const; + + void toString(std::ostream&) const; + + bool isNull() const; + +};/* class Node */ + +}/* CVC4 namespace */ + +#include "expr/expr_value.h" + +namespace CVC4 { + +inline bool Node::operator<(const Node& e) const { + return d_ev->d_id < e.d_ev->d_id; +} + +inline std::ostream& operator<<(std::ostream& out, const Node& e) { + e.toString(out); + return out; +} + +inline Kind Node::getKind() const { + return Kind(d_ev->d_kind); +} + +inline void Node::toString(std::ostream& out) const { + if(d_ev) + d_ev->toString(out); + else out << "null"; +} + +inline Node::iterator Node::begin() { + return d_ev->begin(); +} + +inline Node::iterator Node::end() { + return d_ev->end(); +} + +inline Node::const_iterator Node::begin() const { + return d_ev->begin(); +} + +inline Node::const_iterator Node::end() const { + return d_ev->end(); +} + +inline size_t Node::numChildren() const { + return d_ev->d_nchildren; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR_H */ diff --git a/src/expr/node_attribute.h b/src/expr/node_attribute.h new file mode 100644 index 000000000..b978f097d --- /dev/null +++ b/src/expr/node_attribute.h @@ -0,0 +1,98 @@ +/********************* -*- C++ -*- */ +/** expr_attribute.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. + ** + **/ + +#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H +#define __CVC4__EXPR__EXPR_ATTRIBUTE_H + +#include +#include "config.h" +#include "context/context.h" +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +template +class AttrTables; + +// global (or TSS) +extern CDMap g_hash_bool; +extern CDMap g_hash_int; +extern CDMap g_hash_expr; +extern CDMap g_hash_ptr; + +template +class AttrTable; + +template <> +class AttrTable { +public: + class BitAccessor { + uint64_t& d_word; + unsigned d_bit; + public: + BitAccessor& operator=(bool b); + // continue... + }; + + // bool specialization + static CDMap *s_hash; + + template + BitAccessor& find(Node e, const Attr&); + + template + bool find(Node e, const Attr&) const; +}; + +template <> +class AttrTable { +public: + // int(egral) specialization + static CDMap *s_hash; + uint64_t& find(Node); + uint64_t& find(Node) const; +}; + +template +class AttrTable { + // pointer specialization + static CDMap *s_hash; +public: +}; + +template <> +class AttrTable { +public: + // Node specialization + static CDMap *s_hash; + Node find(Node); +}; + +CDMap* AttrTable::s_hash = &g_hash_bool; +CDMap* AttrTable::s_hash = &g_hash_int; +CDMap* AttrTable::s_hash = &g_hash_expr; + +template +CDMap* AttrTable::s_hash = &g_hash_ptr; + +template +class AttributeTable { + typedef typename Attr::value_type value_type; + + AttrTable& d_table; + +}; + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */ diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp new file mode 100644 index 000000000..83d2ae41d --- /dev/null +++ b/src/expr/node_builder.cpp @@ -0,0 +1,233 @@ +/********************* -*- C++ -*- */ +/** expr_builder.cpp + ** 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. + ** + **/ + +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/expr_value.h" +#include "util/output.h" + +using namespace std; + +namespace CVC4 { + +NodeBuilder::NodeBuilder() : + d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), + d_nchildren(0) { +} + +NodeBuilder::NodeBuilder(Kind k) : + d_em(NodeManager::currentEM()), d_kind(k), d_used(false), d_nchildren(0) { +} + +NodeBuilder::NodeBuilder(const Node& e) : + d_em(NodeManager::currentEM()), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { + d_children.u_arr[0] = e.d_ev->inc();; +} + +NodeBuilder& NodeBuilder::reset(const ExprValue* ev) { + this->~NodeBuilder(); + d_kind = Kind(ev->d_kind); + d_used = false; + d_nchildren = ev->d_nchildren; + for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i) + addChild(i->d_ev); + return *this; +} + +NodeBuilder::NodeBuilder(const NodeBuilder& eb) : + d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), + d_nchildren(eb.d_nchildren) { + Assert( !d_used ); + + if(d_nchildren > nchild_thresh) { + d_children.u_vec = new vector (); + d_children.u_vec->reserve(d_nchildren + 5); + copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), + back_inserter(*d_children.u_vec)); + } else { + ev_iterator j = d_children.u_arr; + ExprValue* const * i = eb.d_children.u_arr; + ExprValue* const * i_end = i + eb.d_nchildren; + for(; i != i_end; ++i, ++j) + *j = (*i)->inc(); + } +} + +NodeBuilder::NodeBuilder(NodeManager* em) : + d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { +} + +NodeBuilder::NodeBuilder(NodeManager* em, Kind k) : + d_em(em), d_kind(k), d_used(false), d_nchildren(0) { +} + +NodeBuilder::NodeBuilder(NodeManager* em, const Node& e) : + d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) { + d_children.u_arr[0] = e.d_ev->inc(); +} + +NodeBuilder::~NodeBuilder() { + if(d_nchildren > nchild_thresh) { + delete d_children.u_vec; + } else { + ev_iterator i = d_children.u_arr; + ev_iterator i_end = d_children.u_arr + d_nchildren; + for(; i != i_end ; ++i) { + (*i)->dec(); + } + } +} + +// Compound expression constructors +NodeBuilder& NodeBuilder::eqExpr(const Node& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != EQUAL )) { + collapse(); + d_kind = EQUAL; + } + addChild(right); + return *this; +} + +NodeBuilder& NodeBuilder::notExpr() { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = NOT; + return *this; +} + +// avoid double-negatives +NodeBuilder& NodeBuilder::negate() { + if(EXPECT_FALSE( d_kind == NOT )) + return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = NOT; + return *this; +} + +NodeBuilder& NodeBuilder::andExpr(const Node& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(d_kind != AND) { + collapse(); + d_kind = AND; + } + addChild(right); + return *this; +} + +NodeBuilder& NodeBuilder::orExpr(const Node& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != OR )) { + collapse(); + d_kind = OR; + } + addChild(right); + return *this; +} + +NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = ITE; + addChild(thenpart); + addChild(elsepart); + return *this; +} + +NodeBuilder& NodeBuilder::iffExpr(const Node& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != IFF )) { + collapse(); + d_kind = IFF; + } + addChild(right); + return *this; +} + +NodeBuilder& NodeBuilder::impExpr(const Node& right) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = IMPLIES; + addChild(right); + return *this; +} + +NodeBuilder& NodeBuilder::xorExpr(const Node& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != XOR )) { + collapse(); + d_kind = XOR; + } + addChild(right); + return *this; +} + +// "Stream" expression constructor syntax +NodeBuilder& NodeBuilder::operator<<(const Kind& op) { + d_kind = op; + return *this; +} + +NodeBuilder& NodeBuilder::operator<<(const Node& child) { + addChild(child); + return *this; +} + +/** + * We keep the children either: + * (a) In the array of expression values if the number of children is less than + * nchild_thresh. Hence (last else) we increase the reference count. + * (b) If the number of children reaches the nchild_thresh, we allocate a vector + * for the children. Children are now expressions, so we also decrement the + * reference count for each child. + * (c) Otherwise we just add to the end of the vector. + */ +void NodeBuilder::addChild(ExprValue* ev) { + Assert(d_nchildren <= nchild_thresh || + d_nchildren == d_children.u_vec->size(), + "children count doesn't reflect the size of the vector!"); + Debug("expr") << "adding child ev " << ev << endl; + if(d_nchildren == nchild_thresh) { + Debug("expr") << "reached thresh " << nchild_thresh << ", copying" << endl; + vector* v = new vector (); + v->reserve(nchild_thresh + 5); + ExprValue** i = d_children.u_arr; + ExprValue** i_end = i + nchild_thresh; + for(;i != i_end; ++ i) { + v->push_back(Node(*i)); + (*i)->dec(); + } + v->push_back(Node(ev)); + d_children.u_vec = v; + ++d_nchildren; + } else if(d_nchildren > nchild_thresh) { + Debug("expr") << "over thresh " << d_nchildren + << " > " << nchild_thresh << endl; + d_children.u_vec->push_back(Node(ev)); + // ++d_nchildren; no need for this + } else { + Debug("expr") << "under thresh " << d_nchildren + << " < " << nchild_thresh << endl; + d_children.u_arr[d_nchildren ++] = ev->inc(); + } +} + +NodeBuilder& NodeBuilder::collapse() { + if(d_nchildren == nchild_thresh) { + vector* v = new vector (); + v->reserve(nchild_thresh + 5); + // + Unreachable();// unimplemented + } + return *this; +} + +}/* CVC4 namespace */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h new file mode 100644 index 000000000..be96c2e77 --- /dev/null +++ b/src/expr/node_builder.h @@ -0,0 +1,313 @@ +/********************* -*- C++ -*- */ +/** expr_builder.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. + ** + **/ + +#ifndef __CVC4__EXPR_BUILDER_H +#define __CVC4__EXPR_BUILDER_H + +#include +#include + +#include "expr/node_manager.h" +#include "expr/kind.h" +#include "util/Assert.h" + +namespace CVC4 { + +class AndExprBuilder; +class OrExprBuilder; +class PlusExprBuilder; +class MinusExprBuilder; +class MultExprBuilder; + +class NodeBuilder { + NodeManager* d_em; + + Kind d_kind; + + // initially false, when you extract the Node this is set and you can't + // extract another + bool d_used; + + static const unsigned nchild_thresh = 10; + + unsigned d_nchildren; + union { + ExprValue* u_arr[nchild_thresh]; + std::vector* u_vec; + } d_children; + + void addChild(const Node& e) { addChild(e.d_ev); } + void addChild(ExprValue*); + NodeBuilder& collapse(); + + typedef ExprValue** ev_iterator; + typedef ExprValue const** const_ev_iterator; + + ev_iterator ev_begin() { + return d_children.u_arr; + } + + ev_iterator ev_end() { + return d_children.u_arr + d_nchildren; + } + + NodeBuilder& reset(const ExprValue*); + +public: + + NodeBuilder(); + NodeBuilder(Kind k); + NodeBuilder(const Node&); + NodeBuilder(const NodeBuilder&); + + NodeBuilder(NodeManager*); + NodeBuilder(NodeManager*, Kind k); + NodeBuilder(NodeManager*, const Node&); + NodeBuilder(NodeManager*, const NodeBuilder&); + + ~NodeBuilder(); + + // Compound expression constructors + NodeBuilder& eqExpr(const Node& right); + NodeBuilder& notExpr(); + NodeBuilder& negate(); // avoid double-negatives + NodeBuilder& andExpr(const Node& right); + NodeBuilder& orExpr(const Node& right); + NodeBuilder& iteExpr(const Node& thenpart, const Node& elsepart); + NodeBuilder& iffExpr(const Node& right); + NodeBuilder& impExpr(const Node& right); + NodeBuilder& xorExpr(const Node& right); + + /* TODO design: these modify NodeBuilder */ + NodeBuilder& operator!() { return notExpr(); } + NodeBuilder& operator&&(const Node& right) { return andExpr(right); } + NodeBuilder& operator||(const Node& right) { return orExpr(right); } + + // "Stream" expression constructor syntax + NodeBuilder& operator<<(const Kind& op); + NodeBuilder& operator<<(const Node& child); + + // For pushing sequences of children + NodeBuilder& append(const std::vector& children) { return append(children.begin(), children.end()); } + NodeBuilder& append(Node child) { return append(&child, (&child) + 1); } + template NodeBuilder& append(const Iterator& begin, const Iterator& end); + + operator Node();// not const + + AndExprBuilder operator&&(Node); + OrExprBuilder operator||(Node); + PlusExprBuilder operator+ (Node); + PlusExprBuilder operator- (Node); + MultExprBuilder operator* (Node); + + friend class AndExprBuilder; + friend class OrExprBuilder; + friend class PlusExprBuilder; + friend class MultExprBuilder; +};/* class NodeBuilder */ + +class AndExprBuilder { + NodeBuilder d_eb; + +public: + + AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != AND) { + d_eb.collapse(); + d_eb.d_kind = AND; + } + } + + AndExprBuilder& operator&&(Node); + OrExprBuilder operator||(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class AndExprBuilder */ + +class OrExprBuilder { + NodeBuilder d_eb; + +public: + + OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != OR) { + d_eb.collapse(); + d_eb.d_kind = OR; + } + } + + AndExprBuilder operator&&(Node); + OrExprBuilder& operator||(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class OrExprBuilder */ + +class PlusExprBuilder { + NodeBuilder d_eb; + +public: + + PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != PLUS) { + d_eb.collapse(); + d_eb.d_kind = PLUS; + } + } + + PlusExprBuilder& operator+(Node); + PlusExprBuilder& operator-(Node); + MultExprBuilder operator*(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class PlusExprBuilder */ + +class MultExprBuilder { + NodeBuilder d_eb; + +public: + + MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + if(d_eb.d_kind != MULT) { + d_eb.collapse(); + d_eb.d_kind = MULT; + } + } + + PlusExprBuilder operator+(Node); + PlusExprBuilder operator-(Node); + MultExprBuilder& operator*(Node); + + operator NodeBuilder() { return d_eb; } + +};/* class MultExprBuilder */ + +template +inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) { + for(Iterator i = begin; i != end; ++i) + addChild(*i); + return *this; +} + +// not const +inline NodeBuilder::operator Node() { + ExprValue *ev; + uint64_t hash; + + Assert(d_kind != UNDEFINED_KIND, "Can't make an expression of an undefined kind!"); + + // variables are permitted to be duplicates (from POV of the expression manager) + if(d_kind == VARIABLE) { + ev = new ExprValue; + hash = reinterpret_cast(ev); + } else { + if(d_nchildren <= nchild_thresh) { + hash = ExprValue::computeHash(d_kind, ev_begin(), ev_end()); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); + ev = new (space) ExprValue; + size_t nc = 0; + ev_iterator i = ev_begin(); + ev_iterator i_end = ev_end(); + for(; i != i_end; ++i) { + // The expressions in the allocated children are all 0, so we must + // construct it withouth using an assignment operator + ev->d_children[nc++].assignExprValue(*i); + } + } else { + hash = ExprValue::computeHash::const_iterator>(d_kind, d_children.u_vec->begin(), d_children.u_vec->end()); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); + ev = new (space) ExprValue; + size_t nc = 0; + for(std::vector::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) + ev->d_children[nc++] = Node(*i); + } + } + + ev->d_nchildren = d_nchildren; + ev->d_kind = d_kind; + ev->d_id = ExprValue::next_id++;// FIXME multithreading + ev->d_rc = 0; + Node e(ev); + + return d_em->lookup(hash, e); +} + +inline AndExprBuilder NodeBuilder::operator&&(Node e) { + return AndExprBuilder(*this) && e; +} + +inline OrExprBuilder NodeBuilder::operator||(Node e) { + return OrExprBuilder(*this) || e; +} + +inline PlusExprBuilder NodeBuilder::operator+ (Node e) { + return PlusExprBuilder(*this) + e; +} + +inline PlusExprBuilder NodeBuilder::operator- (Node e) { + return PlusExprBuilder(*this) - e; +} + +inline MultExprBuilder NodeBuilder::operator* (Node e) { + return MultExprBuilder(*this) * e; +} + +inline AndExprBuilder& AndExprBuilder::operator&&(Node e) { + d_eb.append(e); + return *this; +} + +inline OrExprBuilder AndExprBuilder::operator||(Node e) { + return OrExprBuilder(d_eb.collapse()) || e; +} + +inline AndExprBuilder OrExprBuilder::operator&&(Node e) { + return AndExprBuilder(d_eb.collapse()) && e; +} + +inline OrExprBuilder& OrExprBuilder::operator||(Node e) { + d_eb.append(e); + return *this; +} + +inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { + d_eb.append(e); + return *this; +} + +inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { + d_eb.append(e.negate()); + return *this; +} + +inline MultExprBuilder PlusExprBuilder::operator*(Node e) { + return MultExprBuilder(d_eb.collapse()) * e; +} + +inline PlusExprBuilder MultExprBuilder::operator+(Node e) { + return MultExprBuilder(d_eb.collapse()) + e; +} + +inline PlusExprBuilder MultExprBuilder::operator-(Node e) { + return MultExprBuilder(d_eb.collapse()) - e; +} + +inline MultExprBuilder& MultExprBuilder::operator*(Node e) { + d_eb.append(e); + return *this; +} + + +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR_BUILDER_H */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp new file mode 100644 index 000000000..3c15aa9c4 --- /dev/null +++ b/src/expr/node_manager.cpp @@ -0,0 +1,93 @@ +/********************* -*- C++ -*- */ +/** expr_manager.cpp + ** 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. + ** + ** Expression manager implementation. + **/ + +#include "node_builder.h" +#include "node_manager.h" +#include "expr/node.h" + +namespace CVC4 { + +__thread NodeManager* NodeManager::s_current = 0; + +Node NodeManager::lookup(uint64_t hash, const Node& e) { + Assert(this != NULL, "Woops, we have a bad expression manager!"); + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.end()) { + // insert + std::vector v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } else { + for(std::vector::iterator j = i->second.begin(); j != i->second.end(); ++j) { + if(e.getKind() != j->getKind()) + continue; + + if(e.numChildren() != j->numChildren()) + continue; + + Node::const_iterator c1 = e.begin(); + Node::iterator c2 = j->begin(); + for(; c1 != e.end() && c2 != j->end(); ++c1, ++c2) { + if(c1->d_ev != c2->d_ev) + break; + } + + if(c1 != e.end() || c2 != j->end()) + continue; + + return *j; + } + // didn't find it, insert + std::vector v; + v.push_back(e); + d_hash.insert(std::make_pair(hash, v)); + return e; + } +} + +// general expression-builders + +Node NodeManager::mkExpr(Kind kind) { + return NodeBuilder(this, kind); +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1) { + return NodeBuilder(this, kind) << child1; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) { + return NodeBuilder(this, kind) << child1 << child2; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) { + return NodeBuilder(this, kind) << child1 << child2 << child3; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) { + return NodeBuilder(this, kind) << child1 << child2 << child3 << child4; +} + +Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) { + return NodeBuilder(this, kind) << child1 << child2 << child3 << child4 << child5; +} + +// N-ary version +Node NodeManager::mkExpr(Kind kind, std::vector children) { + return NodeBuilder(this, kind).append(children); +} + +Node NodeManager::mkVar() { + return NodeBuilder(this, VARIABLE); +} + +}/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h new file mode 100644 index 000000000..ca15d88b4 --- /dev/null +++ b/src/expr/node_manager.h @@ -0,0 +1,74 @@ +/********************* -*- C++ -*- */ +/** expr_manager.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. + ** + **/ + +#ifndef __CVC4__EXPR_MANAGER_H +#define __CVC4__EXPR_MANAGER_H + +#include +#include + +#include "node.h" +#include "kind.h" + +namespace CVC4 { + +namespace expr { + class ExprBuilder; +}/* CVC4::expr namespace */ + +class CVC4_PUBLIC NodeManager { + static __thread NodeManager* s_current; + + friend class CVC4::NodeBuilder; + + typedef std::map > hash_t; + hash_t d_hash; + + Node lookup(uint64_t hash, const Node& e); + +public: + static NodeManager* currentEM() { return s_current; } + + // general expression-builders + Node mkExpr(Kind kind); + Node mkExpr(Kind kind, const Node& child1); + Node mkExpr(Kind kind, const Node& child1, const Node& child2); + Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3); + Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4); + Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5); + // N-ary version + Node mkExpr(Kind kind, std::vector children); + + // variables are special, because duplicates are permitted + Node mkVar(); + + // TODO: these use the current EM (but must be renamed) + /* + static Node mkExpr(Kind kind) + { currentEM()->mkExpr(kind); } + static Node mkExpr(Kind kind, Node child1); + { currentEM()->mkExpr(kind, child1); } + static Node mkExpr(Kind kind, Node child1, Node child2); + { currentEM()->mkExpr(kind, child1, child2); } + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3); + { currentEM()->mkExpr(kind, child1, child2, child3); } + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4); + { currentEM()->mkExpr(kind, child1, child2, child3, child4); } + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5); + { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } + */ + + // do we want a varargs one? perhaps not.. +}; + +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/main/main.cpp b/src/main/main.cpp index d9d3988f1..c7e23aee2 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -22,7 +22,7 @@ #include "parser/parser.h" #include "parser/smt/smt_parser.h" #include "parser/cvc/cvc_parser.h" -#include "expr/expr_manager.h" +#include "expr/node_manager.h" #include "smt/smt_engine.h" #include "util/command.h" #include "util/output.h" @@ -53,7 +53,7 @@ int main(int argc, char *argv[]) { throw new Exception("Too many input files specified."); // Create the expression manager - ExprManager exprMgr; + NodeManager exprMgr; // Create the SmtEngine SmtEngine smt(&exprMgr, &options); diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 04a82f721..d81336b53 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -8,7 +8,6 @@ #include #include "antlr_parser.h" -#include "expr/expr_manager.h" #include "util/output.h" using namespace std; @@ -66,29 +65,29 @@ AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) : antlr::LLkParser(lexer, k) { } -Expr AntlrParser::getVariable(std::string var_name) { - Expr e = d_var_symbol_table.getObject(var_name); +Node AntlrParser::getVariable(std::string var_name) { + Node e = d_var_symbol_table.getObject(var_name); Debug("parser") << "getvar " << var_name << " gives " << e << endl; return e; } -Expr AntlrParser::getTrueExpr() const { +Node AntlrParser::getTrueExpr() const { return d_expr_manager->mkExpr(TRUE); } -Expr AntlrParser::getFalseExpr() const { +Node AntlrParser::getFalseExpr() const { return d_expr_manager->mkExpr(FALSE); } -Expr AntlrParser::newExpression(Kind kind, const Expr& child) { +Node AntlrParser::newExpression(Kind kind, const Node& child) { return d_expr_manager->mkExpr(kind, child); } -Expr AntlrParser::newExpression(Kind kind, const Expr& child_1, const Expr& child_2) { +Node AntlrParser::newExpression(Kind kind, const Node& child_1, const Node& child_2) { return d_expr_manager->mkExpr(kind, child_1, child_2); } -Expr AntlrParser::newExpression(Kind kind, const std::vector& children) { +Node AntlrParser::newExpression(Kind kind, const std::vector& children) { return d_expr_manager->mkExpr(kind, children); } @@ -113,7 +112,7 @@ void AntlrParser::setBenchmarkStatus(BenchmarkStatus status) { void AntlrParser::addExtraSorts(const std::vector& extra_sorts) { } -void AntlrParser::setExpressionManager(ExprManager* em) { +void AntlrParser::setExpressionManager(NodeManager* em) { d_expr_manager = em; } @@ -133,7 +132,7 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Expr AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< +Node AntlrParser::createPrecedenceExpr(const vector& exprs, const vector< Kind>& kinds) { return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } @@ -155,7 +154,7 @@ unsigned AntlrParser::findPivot(const std::vector& kinds, return pivot; } -Expr AntlrParser::createPrecedenceExpr(const std::vector& exprs, +Node AntlrParser::createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index) { if(start_index == end_index) @@ -163,8 +162,8 @@ Expr AntlrParser::createPrecedenceExpr(const std::vector& exprs, unsigned pivot = findPivot(kinds, start_index, end_index - 1); - Expr child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); - Expr child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); + Node child_1 = createPrecedenceExpr(exprs, kinds, start_index, pivot); + Node child_2 = createPrecedenceExpr(exprs, kinds, pivot + 1, end_index); return d_expr_manager->mkExpr(kinds[pivot], child_1, child_2); } diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index ad23d45f8..26f206e43 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -15,8 +15,8 @@ #include #include -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/node.h" +#include "expr/node_manager.h" #include "util/command.h" #include "util/Assert.h" #include "parser/symbol_table.h" @@ -48,7 +48,7 @@ public: * Set's the expression manager to use when creating/managing expression. * @param expr_manager the expression manager */ - void setExpressionManager(ExprManager* expr_manager); + void setExpressionManager(NodeManager* expr_manager); protected: @@ -89,7 +89,7 @@ protected: * @param var_name the name of the variable * @return the variable expression */ - Expr getVariable(std::string var_name); + Node getVariable(std::string var_name); /** * Types of symbols. @@ -113,40 +113,40 @@ protected: * Returns the true expression. * @return the true expression */ - Expr getTrueExpr() const; + Node getTrueExpr() const; /** * Returns the false expression. * @return the false expression */ - Expr getFalseExpr() const; + Node getFalseExpr() const; /** * Creates a new unary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param child the child */ - Expr newExpression(Kind kind, const Expr& child); + Node newExpression(Kind kind, const Node& child); /** * Creates a new binary CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Expr newExpression(Kind kind, const Expr& child_1, const Expr& child_2); + Node newExpression(Kind kind, const Node& child_1, const Node& child_2); /** * Creates a new CVC4 expression using the expression manager. * @param kind the kind of the expression * @param children the children of the expression */ - Expr newExpression(Kind kind, const std::vector& children); + Node newExpression(Kind kind, const std::vector& children); /** * Creates a new expression based on the given string of expressions and kinds. * The expression is created so that it respects the kinds precedence table. */ - Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds); + Node createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds); /** * Creates a new predicated over the given sorts. @@ -193,16 +193,16 @@ private: * Creates a new expression based on the given string of expressions and kinds. * The expression is created so that it respects the kinds precedence table. */ - Expr createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); + Node createPrecedenceExpr(const std::vector& exprs, const std::vector& kinds, unsigned start_index, unsigned end_index); /** The status of the benchmark */ BenchmarkStatus d_benchmark_status; /** The expression manager */ - ExprManager* d_expr_manager; + NodeManager* d_expr_manager; /** The symbol table lookup */ - SymbolTable d_var_symbol_table; + SymbolTable d_var_symbol_table; }; std::ostream& operator<<(std::ostream& out, AntlrParser::BenchmarkStatus status); diff --git a/src/parser/cvc/cvc_parser.cpp b/src/parser/cvc/cvc_parser.cpp index adeb5761d..2bb01007a 100644 --- a/src/parser/cvc/cvc_parser.cpp +++ b/src/parser/cvc/cvc_parser.cpp @@ -44,8 +44,8 @@ Command* CvcParser::parseNextCommand() throw(ParserException) { return cmd; } -Expr CvcParser::parseNextExpression() throw(ParserException) { - Expr result; +Node CvcParser::parseNextExpression() throw(ParserException) { + Node result; if(!done()) { try { result = d_antlr_parser->formula(); @@ -62,7 +62,7 @@ CvcParser::~CvcParser() { delete d_antlr_lexer; } -CvcParser::CvcParser(ExprManager*em, istream& input, const char* file_name) : +CvcParser::CvcParser(NodeManager*em, istream& input, const char* file_name) : Parser(em), d_input(input) { if(!d_input) { throw ParserException(string("Read error") + diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 625f2c381..812925b0b 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -34,7 +34,7 @@ options { */ command returns [CVC4::Command* cmd = 0] { - Expr f; + Node f; vector ids; } : ASSERT f = formula { cmd = new AssertCommand(f); } @@ -60,15 +60,15 @@ type : BOOLEAN ; -formula returns [CVC4::Expr formula] +formula returns [CVC4::Node formula] : formula = bool_formula ; -bool_formula returns [CVC4::Expr formula] +bool_formula returns [CVC4::Node formula] { - vector formulas; + vector formulas; vector kinds; - Expr f1, f2; + Node f1, f2; Kind k; } : f1 = primary_bool_formula { formulas.push_back(f1); } @@ -79,7 +79,7 @@ bool_formula returns [CVC4::Expr formula] } ; -primary_bool_formula returns [CVC4::Expr formula] +primary_bool_formula returns [CVC4::Node formula] : formula = bool_atom | NOT formula = primary_bool_formula { formula = newExpression(CVC4::NOT, formula); } | LPAREN formula = bool_formula RPAREN @@ -93,7 +93,7 @@ bool_operator returns [CVC4::Kind kind] | IFF { kind = CVC4::IFF; } ; -bool_atom returns [CVC4::Expr atom] +bool_atom returns [CVC4::Node atom] { string p; } diff --git a/src/parser/cvc/cvc_parser.h b/src/parser/cvc/cvc_parser.h index 9cb6b7594..07699916f 100644 --- a/src/parser/cvc/cvc_parser.h +++ b/src/parser/cvc/cvc_parser.h @@ -37,7 +37,7 @@ public: * @param input the input stream to parse * @param file_name the name of the file (for diagnostic output) */ - CvcParser(ExprManager* em, std::istream& input, const char* file_name = ""); + CvcParser(NodeManager* em, std::istream& input, const char* file_name = ""); /** * Destructor. @@ -57,7 +57,7 @@ public: * Parses the next complete expression of the stream. * @return the expression parsed */ - Expr parseNextExpression() throw(ParserException); + Node parseNextExpression() throw(ParserException); protected: diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 8d4af5ba1..c6d5bcb5c 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -28,7 +28,7 @@ using namespace std; namespace CVC4 { namespace parser { -Parser::Parser(ExprManager* em) : +Parser::Parser(NodeManager* em) : d_expr_manager(em), d_done(false) { } diff --git a/src/parser/parser.h b/src/parser/parser.h index 7755d65f0..7f63261c7 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -22,9 +22,9 @@ namespace CVC4 { // Forward declarations -class Expr; +class Node; class Command; -class ExprManager; +class NodeManager; namespace parser { @@ -44,7 +44,7 @@ public: * Construct the parser that uses the given expression manager. * @param em the expression manager. */ - Parser(ExprManager* em); + Parser(NodeManager* em); /** * Destructor. @@ -60,7 +60,7 @@ public: /** * Parse the next expression of the stream */ - virtual Expr parseNextExpression() throw (ParserException) = 0; + virtual Node parseNextExpression() throw (ParserException) = 0; /** * Check if we are done -- either the end of input has been reached. @@ -73,7 +73,7 @@ protected: void setDone(bool done = true); /** Expression manager the parser will be using */ - ExprManager* d_expr_manager; + NodeManager* d_expr_manager; /** Are we done */ bool d_done; diff --git a/src/parser/smt/smt_parser.cpp b/src/parser/smt/smt_parser.cpp index 65d36690c..411866540 100644 --- a/src/parser/smt/smt_parser.cpp +++ b/src/parser/smt/smt_parser.cpp @@ -41,8 +41,8 @@ Command* SmtParser::parseNextCommand() throw(ParserException) { return cmd; } -Expr SmtParser::parseNextExpression() throw(ParserException) { - Expr result; +Node SmtParser::parseNextExpression() throw(ParserException) { + Node result; if(!done()) { try { result = d_antlr_parser->an_formula(); @@ -59,7 +59,7 @@ SmtParser::~SmtParser() { delete d_antlr_lexer; } -SmtParser::SmtParser(ExprManager* em, istream& input, const char* file_name) : +SmtParser::SmtParser(NodeManager* em, istream& input, const char* file_name) : Parser(em), d_input(input) { if(!d_input) { throw ParserException(string("Read error") + diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index f68d783bc..c2f5c145b 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -60,7 +60,7 @@ pred_symb returns [std::string p] /** * Matches a propositional atom from the input. */ -prop_atom returns [CVC4::Expr atom] +prop_atom returns [CVC4::Node atom] { std::string p; } @@ -78,7 +78,7 @@ prop_atom returns [CVC4::Expr atom] * enclosed in brackets. The prop_atom rule from the original SMT grammar is inlined * here in order to get rid of the ugly antlr non-determinism warrnings. */ -an_atom returns [CVC4::Expr atom] +an_atom returns [CVC4::Node atom] : atom = prop_atom ; @@ -97,18 +97,18 @@ connective returns [CVC4::Kind kind] /** * Matches an annotated formula. */ -an_formula returns [CVC4::Expr formula] +an_formula returns [CVC4::Node formula] { Kind kind; - vector children; + vector children; } : formula = an_atom | LPAREN kind = connective an_formulas[children] RPAREN { formula = newExpression(kind, children); } ; -an_formulas[std::vector& formulas] +an_formulas[std::vector& formulas] { - Expr f; + Node f; } : ( f = an_formula { formulas.push_back(f); } )+ ; @@ -149,7 +149,7 @@ status returns [ AntlrParser::BenchmarkStatus status ] bench_attribute returns [ Command* smt_command = 0] { BenchmarkStatus b_status = SMT_UNKNOWN; - Expr formula; + Node formula; vector sorts; } : C_LOGIC IDENTIFIER diff --git a/src/parser/smt/smt_parser.h b/src/parser/smt/smt_parser.h index a68f0e783..7dedcd5b4 100644 --- a/src/parser/smt/smt_parser.h +++ b/src/parser/smt/smt_parser.h @@ -37,7 +37,7 @@ public: * @param input the input stream to parse * @param file_name the name of the file (for diagnostic output) */ - SmtParser(ExprManager* em, std::istream& input, const char* file_name = ""); + SmtParser(NodeManager* em, std::istream& input, const char* file_name = ""); /** * Destructor. @@ -57,7 +57,7 @@ public: * Parses the next complete expression of the stream. * @return the expression parsed */ - Expr parseNextExpression() throw(ParserException); + Node parseNextExpression() throw(ParserException); protected: diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 32532c734..2c4f0e8b7 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -16,8 +16,6 @@ #include #include -#include "expr/expr.h" - namespace __gnu_cxx { template<> struct hash { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2fb73cbed..166546a2c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -30,9 +30,9 @@ PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) : d_de(de), d_te(te), d_sat() { } -void PropEngine::addVars(Expr e) { +void PropEngine::addVars(Node e) { Debug("prop") << "adding vars to " << e << endl; - for(Expr::iterator i = e.begin(); i != e.end(); ++i) { + for(Node::iterator i = e.begin(); i != e.end(); ++i) { Debug("prop") << "expr " << *i << endl; if(i->getKind() == VARIABLE) { if(d_vars.find(*i) == d_vars.end()) { @@ -45,18 +45,18 @@ void PropEngine::addVars(Expr e) { } } -static void doAtom(SimpSolver* minisat, map* vars, Expr e, vec* c) { +static void doAtom(SimpSolver* minisat, map* vars, Node e, vec* c) { if(e.getKind() == VARIABLE) { - map::iterator v = vars->find(e); + map::iterator v = vars->find(e); Assert(v != vars->end()); c->push(Lit(v->second, false)); return; } if(e.getKind() == NOT) { Assert(e.numChildren() == 1); - Expr child = *e.begin(); + Node child = *e.begin(); Assert(child.getKind() == VARIABLE); - map::iterator v = vars->find(child); + map::iterator v = vars->find(child); Assert(v != vars->end()); c->push(Lit(v->second, true)); return; @@ -64,14 +64,14 @@ static void doAtom(SimpSolver* minisat, map* vars, Expr e, vec* Unhandled(); } -static void doClause(SimpSolver* minisat, map* vars, map* varsReverse, Expr e) { +static void doClause(SimpSolver* minisat, map* vars, map* varsReverse, Node e) { vec c; Debug("prop") << " " << e << endl; if(e.getKind() == VARIABLE || e.getKind() == NOT) { doAtom(minisat, vars, e, &c); } else { Assert(e.getKind() == OR); - for(Expr::iterator i = e.begin(); i != e.end(); ++i) { + for(Node::iterator i = e.begin(); i != e.end(); ++i) { Debug("prop") << " " << *i << endl; doAtom(minisat, vars, *i, &c); } @@ -86,12 +86,12 @@ static void doClause(SimpSolver* minisat, map* vars, map* minisat->addClause(c); } -void PropEngine::solve(Expr e) { +void PropEngine::solve(Node e) { Debug("prop") << "SOLVING " << e << endl; addVars(e); if(e.getKind() == AND) { Debug("prop") << "AND" << endl; - for(Expr::iterator i = e.begin(); i != e.end(); ++i) + for(Node::iterator i = e.begin(); i != e.end(); ++i) doClause(&d_sat, &d_vars, &d_varsReverse, *i); } else doClause(&d_sat, &d_vars, &d_varsReverse, e); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index a3355bf89..21a6669d7 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -13,7 +13,7 @@ #define __CVC4__PROP_ENGINE_H #include "cvc4_config.h" -#include "expr/expr.h" +#include "expr/node.h" #include "util/decision_engine.h" #include "theory/theory_engine.h" #include "prop/minisat/simp/SimpSolver.h" @@ -31,10 +31,10 @@ class PropEngine { DecisionEngine &d_de; TheoryEngine &d_te; CVC4::prop::minisat::SimpSolver d_sat; - std::map d_vars; - std::map d_varsReverse; + std::map d_vars; + std::map d_varsReverse; - void addVars(Expr); + void addVars(Node); public: /** @@ -45,7 +45,7 @@ public: /** * Converts to CNF if necessary. */ - void solve(Expr); + void solve(Node); };/* class PropEngine */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2e895cdc0..4ccdd07d0 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -19,12 +19,12 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } -Expr SmtEngine::preprocess(Expr e) { +Node SmtEngine::preprocess(Node e) { return e; } void SmtEngine::processAssertionList() { - for(std::vector::iterator i = d_assertions.begin(); + for(std::vector::iterator i = d_assertions.begin(); i != d_assertions.end(); ++i) d_expr = d_expr.isNull() ? *i : d_em->mkExpr(AND, d_expr, *i); @@ -41,23 +41,23 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEngine::addFormula(Expr e) { +void SmtEngine::addFormula(Node e) { d_assertions.push_back(e); } -Result SmtEngine::checkSat(Expr e) { +Result SmtEngine::checkSat(Node e) { e = preprocess(e); addFormula(e); return check(); } -Result SmtEngine::query(Expr e) { +Result SmtEngine::query(Node e) { e = preprocess(e); addFormula(e); return check(); } -Result SmtEngine::assertFormula(Expr e) { +Result SmtEngine::assertFormula(Node e) { e = preprocess(e); addFormula(e); return quickCheck(); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 30786511e..c4addc7dd 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -15,8 +15,8 @@ #include #include "cvc4_config.h" -#include "expr/expr.h" -#include "expr/expr_manager.h" +#include "expr/node.h" +#include "expr/node_manager.h" #include "util/result.h" #include "util/model.h" #include "util/options.h" @@ -45,16 +45,16 @@ class Command; class SmtEngine { /** Current set of assertions. */ // TODO: make context-aware to handle user-level push/pop. - std::vector d_assertions; + std::vector d_assertions; /** Our expression manager */ - ExprManager *d_em; + NodeManager *d_em; /** User-level options */ Options *d_opts; /** Expression built-up for handing off to the propagation engine */ - Expr d_expr; + Node d_expr; /** The decision engine */ DecisionEngine d_de; @@ -66,17 +66,17 @@ class SmtEngine { PropEngine d_prop; /** - * Pre-process an Expr. This is expected to be highly-variable, + * Pre-process an Node. This is expected to be highly-variable, * with a lot of "source-level configurability" to add multiple - * passes over the Expr. TODO: may need to specify a LEVEL of + * passes over the Node. TODO: may need to specify a LEVEL of * preprocessing (certain contexts need more/less ?). */ - Expr preprocess(Expr); + Node preprocess(Node); /** * Adds a formula to the current context. */ - void addFormula(Expr); + void addFormula(Node); /** * Full check of consistency in current context. Returns true iff @@ -101,10 +101,10 @@ public: /* * Construct an SmtEngine with the given expression manager and user options. */ - SmtEngine(ExprManager* em, Options* opts) throw() : + SmtEngine(NodeManager* em, Options* opts) throw() : d_em(em), d_opts(opts), - d_expr(Expr::null()), + d_expr(Node::null()), d_de(), d_te(), d_prop(d_de, d_te) { @@ -121,25 +121,25 @@ public: * literals and conjunction of literals. Returns false iff * inconsistent. */ - Result assertFormula(Expr); + Result assertFormula(Node); /** * Add a formula to the current context and call check(). Returns * true iff consistent. */ - Result query(Expr); + Result query(Node); /** * Add a formula to the current context and call check(). Returns * true iff consistent. */ - Result checkSat(Expr); + Result checkSat(Node); /** * Simplify a formula without doing "much" work. Requires assist * from the SAT Engine. */ - Expr simplify(Expr); + Node simplify(Node); /** * Get a (counter)model (only if preceded by a SAT or INVALID query. diff --git a/src/theory/theory.h b/src/theory/theory.h index 5e5f053a6..21124375a 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -12,7 +12,7 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include "expr/expr.h" +#include "expr/node.h" #include "util/literal.h" namespace CVC4 { @@ -46,9 +46,9 @@ public: static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** - * Prepare for an Expr. + * Prepare for an Node. */ - virtual void setup(Expr) = 0; + virtual void setup(Node) = 0; /** * Assert a literal in the current context. @@ -75,7 +75,7 @@ public: /** * Return an explanation for the literal (which was previously propagated by this theory).. */ - virtual Expr explain(Literal) = 0; + virtual Node explain(Literal) = 0; };/* class Theory */ diff --git a/src/util/command.cpp b/src/util/command.cpp index ed6b61703..0953a2ba2 100644 --- a/src/util/command.cpp +++ b/src/util/command.cpp @@ -7,7 +7,7 @@ #include "util/command.h" #include "smt/smt_engine.h" -#include "expr/expr.h" +#include "expr/node.h" #include "util/result.h" using namespace std; @@ -26,7 +26,7 @@ EmptyCommand::EmptyCommand(string name) : void EmptyCommand::invoke(SmtEngine* smt_engine) { } -AssertCommand::AssertCommand(const Expr& e) : +AssertCommand::AssertCommand(const Node& e) : d_expr(e) { } @@ -37,7 +37,7 @@ void AssertCommand::invoke(SmtEngine* smt_engine) { CheckSatCommand::CheckSatCommand() { } -CheckSatCommand::CheckSatCommand(const Expr& e) : +CheckSatCommand::CheckSatCommand(const Node& e) : d_expr(e) { } @@ -45,7 +45,7 @@ void CheckSatCommand::invoke(SmtEngine* smt_engine) { smt_engine->checkSat(d_expr); } -QueryCommand::QueryCommand(const Expr& e) : +QueryCommand::QueryCommand(const Node& e) : d_expr(e) { } diff --git a/src/util/command.h b/src/util/command.h index 31acbc43b..189872220 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -15,12 +15,12 @@ #include #include "cvc4_config.h" -#include "expr/expr.h" +#include "expr/node.h" namespace CVC4 { class SmtEngine; class Command; - class Expr; + class Node; }/* CVC4 namespace */ namespace CVC4 { @@ -46,9 +46,9 @@ private: class CVC4_PUBLIC AssertCommand : public Command { protected: - Expr d_expr; + Node d_expr; public: - AssertCommand(const Expr& e); + AssertCommand(const Node& e); void invoke(CVC4::SmtEngine* smt_engine); void toString(std::ostream& out) const; };/* class AssertCommand */ @@ -57,21 +57,21 @@ public: class CVC4_PUBLIC CheckSatCommand : public Command { public: CheckSatCommand(); - CheckSatCommand(const Expr& e); + CheckSatCommand(const Node& e); void invoke(SmtEngine* smt); void toString(std::ostream& out) const; protected: - Expr d_expr; + Node d_expr; };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { public: - QueryCommand(const Expr& e); + QueryCommand(const Node& e); void invoke(SmtEngine* smt); void toString(std::ostream& out) const; protected: - Expr d_expr; + Node d_expr; };/* class QueryCommand */ diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h index 5f1deee8a..ad70bec91 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_black.h @@ -1,4 +1,4 @@ -/* Black box testing of CVC4::Expr. */ +/* Black box testing of CVC4::Node. */ #include @@ -10,10 +10,10 @@ class ExprBlack : public CxxTest::TestSuite { public: void testNull() { - Expr::s_null; + Node::s_null; } void testCopyCtor() { - Expr e(Expr::s_null); + Node e(Node::s_null); } }; diff --git a/test/unit/expr/expr_white.h b/test/unit/expr/expr_white.h index 3da360126..6b48d66e6 100644 --- a/test/unit/expr/expr_white.h +++ b/test/unit/expr/expr_white.h @@ -1,4 +1,4 @@ -/* White box testing of CVC4::Expr. */ +/* White box testing of CVC4::Node. */ #include @@ -10,10 +10,10 @@ class ExprWhite : public CxxTest::TestSuite { public: void testNull() { - Expr::s_null; + Node::s_null; } void testCopyCtor() { - Expr e(Expr::s_null); + Node e(Node::s_null); } };