From f79afa96e7e7176b974252dd05a9f7bdf70194e8 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Thu, 10 Dec 2009 18:44:51 +0000 Subject: [PATCH] killing expr into node... --- src/expr/Makefile.am | 14 +- src/expr/Makefile.in | 22 +-- src/expr/attr_type.h | 2 +- src/expr/attr_var_name.h | 2 +- src/expr/expr.cpp | 115 ----------- src/expr/expr_manager.cpp | 93 --------- src/expr/expr_value.cpp | 2 +- src/expr/expr_value.h | 22 +-- src/expr/node.cpp | 115 +++++++++++ src/expr/{expr.h => node.h} | 86 ++++----- .../{expr_attribute.h => node_attribute.h} | 22 +-- .../{expr_builder.cpp => node_builder.cpp} | 72 +++---- src/expr/{expr_builder.h => node_builder.h} | 178 +++++++++--------- src/expr/node_manager.cpp | 93 +++++++++ src/expr/{expr_manager.h => node_manager.h} | 42 ++--- src/main/main.cpp | 4 +- src/parser/antlr_parser.cpp | 25 ++- src/parser/antlr_parser.h | 26 +-- src/parser/cvc/cvc_parser.cpp | 6 +- src/parser/cvc/cvc_parser.g | 14 +- src/parser/cvc/cvc_parser.h | 4 +- src/parser/parser.cpp | 2 +- src/parser/parser.h | 10 +- src/parser/smt/smt_parser.cpp | 6 +- src/parser/smt/smt_parser.g | 14 +- src/parser/smt/smt_parser.h | 4 +- src/parser/symbol_table.h | 2 - src/prop/prop_engine.cpp | 20 +- src/prop/prop_engine.h | 10 +- src/smt/smt_engine.cpp | 12 +- src/smt/smt_engine.h | 30 +-- src/theory/theory.h | 8 +- src/util/command.cpp | 8 +- src/util/command.h | 16 +- test/unit/expr/expr_black.h | 6 +- test/unit/expr/expr_white.h | 6 +- 36 files changed, 555 insertions(+), 558 deletions(-) delete mode 100644 src/expr/expr.cpp delete mode 100644 src/expr/expr_manager.cpp create mode 100644 src/expr/node.cpp rename src/expr/{expr.h => node.h} (60%) rename src/expr/{expr_attribute.h => node_attribute.h} (83%) rename src/expr/{expr_builder.cpp => node_builder.cpp} (73%) rename src/expr/{expr_builder.h => node_builder.h} (52%) create mode 100644 src/expr/node_manager.cpp rename src/expr/{expr_manager.h => node_manager.h} (50%) 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_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_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/expr.h b/src/expr/node.h similarity index 60% rename from src/expr/expr.h rename to src/expr/node.h index 7440974d8..aec50000e 100644 --- a/src/expr/expr.h +++ b/src/expr/node.h @@ -21,14 +21,14 @@ #include "expr/kind.h" namespace CVC4 { - class Expr; + class Node; }/* CVC4 namespace */ namespace CVC4 { -inline std::ostream& operator<<(std::ostream&, const Expr&) CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream&, const Node&) CVC4_PUBLIC; -class ExprManager; +class NodeManager; namespace expr { class ExprValue; @@ -40,25 +40,25 @@ using CVC4::expr::ExprValue; * Encapsulation of an ExprValue pointer. The reference count is * maintained in the ExprValue. */ -class CVC4_PUBLIC Expr { +class CVC4_PUBLIC Node { friend class ExprValue; /** A convenient null-valued encapsulated pointer */ - static Expr s_null; + static Node 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. + /** 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 Expr(ExprValue*); + explicit Node(ExprValue*); - friend class ExprBuilder; - friend class ExprManager; + friend class NodeBuilder; + friend class NodeManager; /** Access to the encapsulated expression. * @return the encapsulated expression. */ @@ -76,49 +76,49 @@ class CVC4_PUBLIC Expr { public: /** Default constructor, makes a null expression. */ - Expr(); + Node(); - Expr(const Expr&); + Node(const Node&); /** Destructor. Decrements the reference count and, if zero, * collects the ExprValue. */ - ~Expr(); + ~Node(); - bool operator==(const Expr& e) const { return d_ev == e.d_ev; } - bool operator!=(const Expr& e) const { return d_ev != e.d_ev; } + 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 Expr& e) const; + inline bool operator<(const Node& e) const; - Expr& operator=(const Expr&); + Node& operator=(const Node&); 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; + 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; - Expr plusExpr(const Expr& right) const; - Expr uMinusExpr() const; - Expr multExpr(const Expr& 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 Expr null() { return s_null; } + static Node null() { return s_null; } - typedef Expr* iterator; - typedef Expr const* const_iterator; + typedef Node* iterator; + typedef Node const* const_iterator; inline iterator begin(); inline iterator end(); @@ -129,7 +129,7 @@ public: bool isNull() const; -};/* class Expr */ +};/* class Node */ }/* CVC4 namespace */ @@ -137,42 +137,42 @@ public: namespace CVC4 { -inline bool Expr::operator<(const Expr& e) const { +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 Expr& e) { +inline std::ostream& operator<<(std::ostream& out, const Node& e) { e.toString(out); return out; } -inline Kind Expr::getKind() const { +inline Kind Node::getKind() const { return Kind(d_ev->d_kind); } -inline void Expr::toString(std::ostream& out) const { +inline void Node::toString(std::ostream& out) const { if(d_ev) d_ev->toString(out); else out << "null"; } -inline Expr::iterator Expr::begin() { +inline Node::iterator Node::begin() { return d_ev->begin(); } -inline Expr::iterator Expr::end() { +inline Node::iterator Node::end() { return d_ev->end(); } -inline Expr::const_iterator Expr::begin() const { +inline Node::const_iterator Node::begin() const { return d_ev->begin(); } -inline Expr::const_iterator Expr::end() const { +inline Node::const_iterator Node::end() const { return d_ev->end(); } -inline size_t Expr::numChildren() const { +inline size_t Node::numChildren() const { return d_ev->d_nchildren; } diff --git a/src/expr/expr_attribute.h b/src/expr/node_attribute.h similarity index 83% rename from src/expr/expr_attribute.h rename to src/expr/node_attribute.h index b68a9d19d..b978f097d 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/node_attribute.h @@ -15,7 +15,7 @@ #include #include "config.h" #include "context/context.h" -#include "expr/expr.h" +#include "expr/node.h" namespace CVC4 { namespace expr { @@ -26,7 +26,7 @@ class AttrTables; // global (or TSS) extern CDMap g_hash_bool; extern CDMap g_hash_int; -extern CDMap g_hash_expr; +extern CDMap g_hash_expr; extern CDMap g_hash_ptr; template @@ -47,10 +47,10 @@ public: static CDMap *s_hash; template - BitAccessor& find(Expr e, const Attr&); + BitAccessor& find(Node e, const Attr&); template - bool find(Expr e, const Attr&) const; + bool find(Node e, const Attr&) const; }; template <> @@ -58,8 +58,8 @@ class AttrTable { public: // int(egral) specialization static CDMap *s_hash; - uint64_t& find(Expr); - uint64_t& find(Expr) const; + uint64_t& find(Node); + uint64_t& find(Node) const; }; template @@ -70,16 +70,16 @@ public: }; template <> -class AttrTable { +class AttrTable { public: - // Expr specialization - static CDMap *s_hash; - Expr find(Expr); + // 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; +CDMap* AttrTable::s_hash = &g_hash_expr; template CDMap* AttrTable::s_hash = &g_hash_ptr; diff --git a/src/expr/expr_builder.cpp b/src/expr/node_builder.cpp similarity index 73% rename from src/expr/expr_builder.cpp rename to src/expr/node_builder.cpp index 10152a338..83d2ae41d 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/node_builder.cpp @@ -9,46 +9,46 @@ ** **/ -#include "expr_builder.h" -#include "expr_manager.h" -#include "expr_value.h" +#include "expr/node_builder.h" +#include "expr/node_manager.h" +#include "expr/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), +NodeBuilder::NodeBuilder() : + d_em(NodeManager::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) { +NodeBuilder::NodeBuilder(Kind k) : + d_em(NodeManager::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) { +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();; } -ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { - this->~ExprBuilder(); +NodeBuilder& NodeBuilder::reset(const ExprValue* ev) { + this->~NodeBuilder(); 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) + for(Node::const_iterator i = ev->begin(); i != ev->end(); ++i) addChild(i->d_ev); return *this; } -ExprBuilder::ExprBuilder(const ExprBuilder& eb) : +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 = 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)); @@ -61,20 +61,20 @@ ExprBuilder::ExprBuilder(const ExprBuilder& eb) : } } -ExprBuilder::ExprBuilder(ExprManager* em) : +NodeBuilder::NodeBuilder(NodeManager* em) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : +NodeBuilder::NodeBuilder(NodeManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) { } -ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : +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(); } -ExprBuilder::~ExprBuilder() { +NodeBuilder::~NodeBuilder() { if(d_nchildren > nchild_thresh) { delete d_children.u_vec; } else { @@ -87,7 +87,7 @@ ExprBuilder::~ExprBuilder() { } // Compound expression constructors -ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { +NodeBuilder& NodeBuilder::eqExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != EQUAL )) { collapse(); @@ -97,7 +97,7 @@ ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::notExpr() { +NodeBuilder& NodeBuilder::notExpr() { Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = NOT; @@ -105,7 +105,7 @@ ExprBuilder& ExprBuilder::notExpr() { } // avoid double-negatives -ExprBuilder& ExprBuilder::negate() { +NodeBuilder& NodeBuilder::negate() { if(EXPECT_FALSE( d_kind == NOT )) return reset(d_children.u_arr[0]); Assert( d_kind != UNDEFINED_KIND ); collapse(); @@ -113,7 +113,7 @@ ExprBuilder& ExprBuilder::negate() { return *this; } -ExprBuilder& ExprBuilder::andExpr(const Expr& right) { +NodeBuilder& NodeBuilder::andExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(d_kind != AND) { collapse(); @@ -123,7 +123,7 @@ ExprBuilder& ExprBuilder::andExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::orExpr(const Expr& right) { +NodeBuilder& NodeBuilder::orExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != OR )) { collapse(); @@ -133,7 +133,7 @@ ExprBuilder& ExprBuilder::orExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { +NodeBuilder& NodeBuilder::iteExpr(const Node& thenpart, const Node& elsepart) { Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = ITE; @@ -142,7 +142,7 @@ ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { return *this; } -ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { +NodeBuilder& NodeBuilder::iffExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != IFF )) { collapse(); @@ -152,7 +152,7 @@ ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::impExpr(const Expr& right) { +NodeBuilder& NodeBuilder::impExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); collapse(); d_kind = IMPLIES; @@ -160,7 +160,7 @@ ExprBuilder& ExprBuilder::impExpr(const Expr& right) { return *this; } -ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { +NodeBuilder& NodeBuilder::xorExpr(const Node& right) { Assert( d_kind != UNDEFINED_KIND ); if(EXPECT_TRUE( d_kind != XOR )) { collapse(); @@ -171,12 +171,12 @@ ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { } // "Stream" expression constructor syntax -ExprBuilder& ExprBuilder::operator<<(const Kind& op) { +NodeBuilder& NodeBuilder::operator<<(const Kind& op) { d_kind = op; return *this; } -ExprBuilder& ExprBuilder::operator<<(const Expr& child) { +NodeBuilder& NodeBuilder::operator<<(const Node& child) { addChild(child); return *this; } @@ -190,28 +190,28 @@ ExprBuilder& ExprBuilder::operator<<(const Expr& child) { * reference count for each child. * (c) Otherwise we just add to the end of the vector. */ -void ExprBuilder::addChild(ExprValue* ev) { +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 (); + 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)); + v->push_back(Node(*i)); (*i)->dec(); } - v->push_back(Expr(ev)); + 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(Expr(ev)); + d_children.u_vec->push_back(Node(ev)); // ++d_nchildren; no need for this } else { Debug("expr") << "under thresh " << d_nchildren @@ -220,9 +220,9 @@ void ExprBuilder::addChild(ExprValue* ev) { } } -ExprBuilder& ExprBuilder::collapse() { +NodeBuilder& NodeBuilder::collapse() { if(d_nchildren == nchild_thresh) { - vector* v = new vector (); + vector* v = new vector (); v->reserve(nchild_thresh + 5); // Unreachable();// unimplemented diff --git a/src/expr/expr_builder.h b/src/expr/node_builder.h similarity index 52% rename from src/expr/expr_builder.h rename to src/expr/node_builder.h index 34e34bf6e..be96c2e77 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/node_builder.h @@ -15,8 +15,8 @@ #include #include -#include "expr_manager.h" -#include "kind.h" +#include "expr/node_manager.h" +#include "expr/kind.h" #include "util/Assert.h" namespace CVC4 { @@ -27,12 +27,12 @@ class PlusExprBuilder; class MinusExprBuilder; class MultExprBuilder; -class ExprBuilder { - ExprManager* d_em; +class NodeBuilder { + NodeManager* d_em; Kind d_kind; - // initially false, when you extract the Expr this is set and you can't + // initially false, when you extract the Node this is set and you can't // extract another bool d_used; @@ -41,12 +41,12 @@ class ExprBuilder { unsigned d_nchildren; union { ExprValue* u_arr[nchild_thresh]; - std::vector* u_vec; + std::vector* u_vec; } d_children; - void addChild(const Expr& e) { addChild(e.d_ev); } + void addChild(const Node& e) { addChild(e.d_ev); } void addChild(ExprValue*); - ExprBuilder& collapse(); + NodeBuilder& collapse(); typedef ExprValue** ev_iterator; typedef ExprValue const** const_ev_iterator; @@ -59,148 +59,148 @@ class ExprBuilder { return d_children.u_arr + d_nchildren; } - ExprBuilder& reset(const ExprValue*); + NodeBuilder& reset(const ExprValue*); public: - ExprBuilder(); - ExprBuilder(Kind k); - ExprBuilder(const Expr&); - ExprBuilder(const ExprBuilder&); + NodeBuilder(); + NodeBuilder(Kind k); + NodeBuilder(const Node&); + NodeBuilder(const NodeBuilder&); - ExprBuilder(ExprManager*); - ExprBuilder(ExprManager*, Kind k); - ExprBuilder(ExprManager*, const Expr&); - ExprBuilder(ExprManager*, const ExprBuilder&); + NodeBuilder(NodeManager*); + NodeBuilder(NodeManager*, Kind k); + NodeBuilder(NodeManager*, const Node&); + NodeBuilder(NodeManager*, const NodeBuilder&); - ~ExprBuilder(); + ~NodeBuilder(); // 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); } + 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 - ExprBuilder& operator<<(const Kind& op); - ExprBuilder& operator<<(const Expr& child); + NodeBuilder& operator<<(const Kind& op); + NodeBuilder& operator<<(const Node& 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); + 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 Expr();// not const + operator Node();// not const - AndExprBuilder operator&&(Expr); - OrExprBuilder operator||(Expr); - PlusExprBuilder operator+ (Expr); - PlusExprBuilder operator- (Expr); - MultExprBuilder operator* (Expr); + 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 ExprBuilder */ +};/* class NodeBuilder */ class AndExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - AndExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != AND) { d_eb.collapse(); d_eb.d_kind = AND; } } - AndExprBuilder& operator&&(Expr); - OrExprBuilder operator||(Expr); + AndExprBuilder& operator&&(Node); + OrExprBuilder operator||(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class AndExprBuilder */ class OrExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - OrExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) { if(d_eb.d_kind != OR) { d_eb.collapse(); d_eb.d_kind = OR; } } - AndExprBuilder operator&&(Expr); - OrExprBuilder& operator||(Expr); + AndExprBuilder operator&&(Node); + OrExprBuilder& operator||(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class OrExprBuilder */ class PlusExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - PlusExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + PlusExprBuilder(const NodeBuilder& 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); + PlusExprBuilder& operator+(Node); + PlusExprBuilder& operator-(Node); + MultExprBuilder operator*(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class PlusExprBuilder */ class MultExprBuilder { - ExprBuilder d_eb; + NodeBuilder d_eb; public: - MultExprBuilder(const ExprBuilder& eb) : d_eb(eb) { + MultExprBuilder(const NodeBuilder& 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); + PlusExprBuilder operator+(Node); + PlusExprBuilder operator-(Node); + MultExprBuilder& operator*(Node); - operator ExprBuilder() { return d_eb; } + operator NodeBuilder() { return d_eb; } };/* class MultExprBuilder */ template -inline ExprBuilder& ExprBuilder::append(const Iterator& begin, const Iterator& end) { +inline NodeBuilder& NodeBuilder::append(const Iterator& begin, const Iterator& end) { for(Iterator i = begin; i != end; ++i) addChild(*i); return *this; } // not const -inline ExprBuilder::operator Expr() { +inline NodeBuilder::operator Node() { ExprValue *ev; uint64_t hash; @@ -213,7 +213,7 @@ inline ExprBuilder::operator Expr() { } 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)); + void *space = std::calloc(1, sizeof(ExprValue) + d_nchildren * sizeof(Node)); ev = new (space) ExprValue; size_t nc = 0; ev_iterator i = ev_begin(); @@ -224,12 +224,12 @@ inline ExprBuilder::operator Expr() { 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)); + 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++] = Expr(*i); + for(std::vector::iterator i = d_children.u_vec->begin(); i != d_children.u_vec->end(); ++i) + ev->d_children[nc++] = Node(*i); } } @@ -237,72 +237,72 @@ inline ExprBuilder::operator Expr() { ev->d_kind = d_kind; ev->d_id = ExprValue::next_id++;// FIXME multithreading ev->d_rc = 0; - Expr e(ev); + Node e(ev); return d_em->lookup(hash, e); } -inline AndExprBuilder ExprBuilder::operator&&(Expr e) { +inline AndExprBuilder NodeBuilder::operator&&(Node e) { return AndExprBuilder(*this) && e; } -inline OrExprBuilder ExprBuilder::operator||(Expr e) { +inline OrExprBuilder NodeBuilder::operator||(Node e) { return OrExprBuilder(*this) || e; } -inline PlusExprBuilder ExprBuilder::operator+ (Expr e) { +inline PlusExprBuilder NodeBuilder::operator+ (Node e) { return PlusExprBuilder(*this) + e; } -inline PlusExprBuilder ExprBuilder::operator- (Expr e) { +inline PlusExprBuilder NodeBuilder::operator- (Node e) { return PlusExprBuilder(*this) - e; } -inline MultExprBuilder ExprBuilder::operator* (Expr e) { +inline MultExprBuilder NodeBuilder::operator* (Node e) { return MultExprBuilder(*this) * e; } -inline AndExprBuilder& AndExprBuilder::operator&&(Expr e) { +inline AndExprBuilder& AndExprBuilder::operator&&(Node e) { d_eb.append(e); return *this; } -inline OrExprBuilder AndExprBuilder::operator||(Expr e) { +inline OrExprBuilder AndExprBuilder::operator||(Node e) { return OrExprBuilder(d_eb.collapse()) || e; } -inline AndExprBuilder OrExprBuilder::operator&&(Expr e) { +inline AndExprBuilder OrExprBuilder::operator&&(Node e) { return AndExprBuilder(d_eb.collapse()) && e; } -inline OrExprBuilder& OrExprBuilder::operator||(Expr e) { +inline OrExprBuilder& OrExprBuilder::operator||(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator+(Expr e) { +inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator-(Expr e) { +inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { d_eb.append(e.negate()); return *this; } -inline MultExprBuilder PlusExprBuilder::operator*(Expr e) { +inline MultExprBuilder PlusExprBuilder::operator*(Node e) { return MultExprBuilder(d_eb.collapse()) * e; } -inline PlusExprBuilder MultExprBuilder::operator+(Expr e) { +inline PlusExprBuilder MultExprBuilder::operator+(Node e) { return MultExprBuilder(d_eb.collapse()) + e; } -inline PlusExprBuilder MultExprBuilder::operator-(Expr e) { +inline PlusExprBuilder MultExprBuilder::operator-(Node e) { return MultExprBuilder(d_eb.collapse()) - e; } -inline MultExprBuilder& MultExprBuilder::operator*(Expr e) { +inline MultExprBuilder& MultExprBuilder::operator*(Node e) { d_eb.append(e); return *this; } 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/expr_manager.h b/src/expr/node_manager.h similarity index 50% rename from src/expr/expr_manager.h rename to src/expr/node_manager.h index 542d1040d..ca15d88b4 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/node_manager.h @@ -15,7 +15,7 @@ #include #include -#include "expr/expr.h" +#include "node.h" #include "kind.h" namespace CVC4 { @@ -24,45 +24,45 @@ namespace expr { class ExprBuilder; }/* CVC4::expr namespace */ -class CVC4_PUBLIC ExprManager { - static __thread ExprManager* s_current; +class CVC4_PUBLIC NodeManager { + static __thread NodeManager* s_current; - friend class CVC4::ExprBuilder; + friend class CVC4::NodeBuilder; - typedef std::map > hash_t; + typedef std::map > hash_t; hash_t d_hash; - Expr lookup(uint64_t hash, const Expr& e); + Node lookup(uint64_t hash, const Node& e); public: - static ExprManager* currentEM() { return s_current; } + static NodeManager* 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); + 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 - Expr mkExpr(Kind kind, std::vector children); + Node mkExpr(Kind kind, std::vector children); // variables are special, because duplicates are permitted - Expr mkVar(); + Node mkVar(); // TODO: these use the current EM (but must be renamed) /* - static Expr mkExpr(Kind kind) + static Node mkExpr(Kind kind) { currentEM()->mkExpr(kind); } - static Expr mkExpr(Kind kind, Expr child1); + static Node mkExpr(Kind kind, Node child1); { currentEM()->mkExpr(kind, child1); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2); + static Node mkExpr(Kind kind, Node child1, Node child2); { currentEM()->mkExpr(kind, child1, child2); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3); + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3); { currentEM()->mkExpr(kind, child1, child2, child3); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4); + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4); { currentEM()->mkExpr(kind, child1, child2, child3, child4); } - static Expr mkExpr(Kind kind, Expr child1, Expr child2, Expr child3, Expr child4, Expr child5); + static Node mkExpr(Kind kind, Node child1, Node child2, Node child3, Node child4, Node child5); { currentEM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ 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); } }; -- 2.30.2