diff options
Diffstat (limited to 'src')
54 files changed, 946 insertions, 641 deletions
diff --git a/src/Makefile b/src/Makefile new file mode 100644 index 000000000..e119c83d7 --- /dev/null +++ b/src/Makefile @@ -0,0 +1,5 @@ +topdir = .. +srcdir = src +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/Makefile.am b/src/Makefile.am index 1db9d9ecf..f429e8b2a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -15,9 +15,10 @@ LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ -INCLUDES = -I@srcdir@/include -I@srcdir@ +AM_CPPFLAGS = + -D__BUILDING_CVC4LIB \ + -I@srcdir@/include -I@srcdir@ AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB SUBDIRS = util expr context prop smt theory . parser main diff --git a/src/Makefile.in b/src/Makefile.in index 8f33fd330..38d59d02a 100644 --- a/src/Makefile.in +++ b/src/Makefile.in @@ -159,6 +159,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -287,9 +288,8 @@ top_srcdir = @top_srcdir@ # LIBCVC4_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ -INCLUDES = -I@srcdir@/include -I@srcdir@ +AM_CPPFLAGS = AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB SUBDIRS = util expr context prop smt theory . parser main lib_LTLIBRARIES = libcvc4.la libcvc4_la_LDFLAGS = -version-info $(LIBCVC4_VERSION) -release $(LIBCVC4_RELEASE) @@ -700,6 +700,8 @@ uninstall-am: uninstall-libLTLIBRARIES tags tags-recursive uninstall uninstall-am \ uninstall-libLTLIBRARIES + -D__BUILDING_CVC4LIB \ + -I@srcdir@/include -I@srcdir@ install-data-local: $(publicheaders) $(mkinstalldirs) $(DESTDIR)$(includedir)/cvc4 diff --git a/src/context/Makefile b/src/context/Makefile new file mode 100644 index 000000000..5286dd3ac --- /dev/null +++ b/src/context/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/context +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e38f7f4eb..b36d5e69c 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libcontext.la diff --git a/src/context/Makefile.in b/src/context/Makefile.in index 0e5281ca6..51069583d 100644 --- a/src/context/Makefile.in +++ b/src/context/Makefile.in @@ -52,7 +52,7 @@ CONFIG_CLEAN_FILES = CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libcontext_la_LIBADD = -am_libcontext_la_OBJECTS = context.lo +am_libcontext_la_OBJECTS = context.lo context_mm.lo libcontext_la_OBJECTS = $(am_libcontext_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -104,6 +104,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -215,13 +216,17 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libcontext.la libcontext_la_SOURCES = \ context.cpp \ - context.h + context.h \ + context_mm.cpp \ + context_mm.h all: all-am @@ -276,6 +281,7 @@ distclean-compile: -rm -f *.tab.c @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/context.Plo@am__quote@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/context_mm.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index 51f192f2a..3b4089b25 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -14,14 +14,13 @@ #include <cstdlib> #include <vector> #include <deque> +#include <new> #include "context/context_mm.h" #include "util/Assert.h" - namespace CVC4 { namespace context { - void ContextMemoryManager::newChunk() { // Increment index to chunk list @@ -30,16 +29,16 @@ void ContextMemoryManager::newChunk() { "Index should be at the end of the list"); // Create new chunk if no free chunk available - if (d_freePages.empty()) { + if (d_freeChunks.empty()) { d_chunkList.push_back((char*)malloc(chunkSizeBytes)); if (d_chunkList.back() == NULL) { - throw bad_alloc(); + throw std::bad_alloc(); } } // If there is a free chunk, use that else { - d_chunkList.push_back(d_freePages.back()); - d_freePages.pop_back(); + d_chunkList.push_back(d_freeChunks.back()); + d_freeChunks.pop_back(); } // Set up the current chunk pointers d_nextFree = d_chunkList.back(); @@ -47,30 +46,30 @@ void ContextMemoryManager::newChunk() { } -ContextMemoryManager() : d_indexChunkList(0) { +ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) { // Create initial chunk d_chunkList.push_back((char*)malloc(chunkSizeBytes)); d_nextFree = d_chunkList.back(); if (d_nextFree == NULL) { - throw bad_alloc; + throw std::bad_alloc(); } d_endChunk = d_nextFree + chunkSizeBytes; } -~ContextMemoryManager() { +ContextMemoryManager::~ContextMemoryManager() { // Delete all chunks while (!d_chunkList.empty()) { free(d_chunkList.back()); d_chunkList.pop_back(); } - while (!d_freePages.empty()) { - free(d_freePages.back()); - d_freePages.pop_back(); + while (!d_freeChunks.empty()) { + free(d_freeChunks.back()); + d_freeChunks.pop_back(); } } -void* newData(size_t size) { +void* ContextMemoryManager::newData(size_t size) { // Use next available free location in current chunk void* res = (void*)d_nextFree; d_nextFree += size; @@ -86,7 +85,7 @@ void* newData(size_t size) { } -void push() { +void ContextMemoryManager::push() { // Store current state on the stack d_nextFreeStack.push_back(d_nextFree); d_endChunkStack.push_back(d_endChunk); @@ -94,7 +93,7 @@ void push() { } -void pop() { +void ContextMemoryManager::pop() { // Restore state from stack d_nextFree = d_nextFreeStack.back(); d_nextFreeStack.pop_back(); @@ -103,7 +102,7 @@ void pop() { // Free all the new chunks since the last push while (d_indexChunkList > d_indexChunkListStack.back()) { - d_freePages.push_back(d_chunkList.back()); + d_freeChunks.push_back(d_chunkList.back()); d_chunkList.pop_back(); --d_indexChunkList; } @@ -111,12 +110,11 @@ void pop() { // Delete excess free chunks while (d_freeChunks.size() > maxFreeChunks) { - free(d_freePages.front()); - d_freePages.pop_front(); + free(d_freeChunks.front()); + d_freeChunks.pop_front(); } } }/* CVC4::context namespace */ - }/* CVC4 namespace */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 6b442d4a0..d48cbedc0 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -33,13 +33,13 @@ class ContextMemoryManager { /** * Memory in regions is allocated in chunks. This is the minimum chunk size */ - const unsigned chunkSizeBytes = 16384; // #bytes in each chunk + static const unsigned chunkSizeBytes = 16384; // #bytes in each chunk /** * A list of free chunks is maintained. This is the maximum number of * free chunks. */ - const unsigned maxFreeChunks = 100; + static const unsigned maxFreeChunks = 100; /** * List of all chunks that are currently active diff --git a/src/expr/Makefile b/src/expr/Makefile new file mode 100644 index 000000000..b661835a5 --- /dev/null +++ b/src/expr/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/expr +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index b8606e051..046281702 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libexpr.la @@ -10,7 +11,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ - expr_value.h \ + node_value.h \ node_manager.h \ expr_manager.h \ node_attribute.h \ @@ -19,6 +20,6 @@ libexpr_la_SOURCES = \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ - expr_value.cpp \ + node_value.cpp \ expr.cpp diff --git a/src/expr/Makefile.in b/src/expr/Makefile.in index 6b1555e6c..c7d99dc84 100644 --- a/src/expr/Makefile.in +++ b/src/expr/Makefile.in @@ -53,7 +53,7 @@ CONFIG_CLEAN_VPATH_FILES = LTLIBRARIES = $(noinst_LTLIBRARIES) libexpr_la_LIBADD = am_libexpr_la_OBJECTS = node.lo node_builder.lo node_manager.lo \ - expr_manager.lo expr_value.lo expr.lo + expr_manager.lo node_value.lo expr.lo libexpr_la_OBJECTS = $(am_libexpr_la_OBJECTS) DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir) depcomp = $(SHELL) $(top_srcdir)/config/depcomp @@ -105,6 +105,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -216,9 +217,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libexpr.la libexpr_la_SOURCES = \ attr_type.h \ @@ -226,7 +229,7 @@ libexpr_la_SOURCES = \ node.h \ node_builder.h \ expr.h \ - expr_value.h \ + node_value.h \ node_manager.h \ expr_manager.h \ node_attribute.h \ @@ -235,7 +238,7 @@ libexpr_la_SOURCES = \ node_builder.cpp \ node_manager.cpp \ expr_manager.cpp \ - expr_value.cpp \ + node_value.cpp \ expr.cpp all: all-am @@ -292,10 +295,10 @@ distclean-compile: @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/expr.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@ +@AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/node_value.Plo@am__quote@ .cpp.o: @am__fastdepCXX_TRUE@ $(CXXCOMPILE) -MT $@ -MD -MP -MF $(DEPDIR)/$*.Tpo -c -o $@ $< diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp deleted file mode 100644 index af064f43d..000000000 --- a/src/expr/expr_value.cpp +++ /dev/null @@ -1,103 +0,0 @@ -/********************* -*- C++ -*- */ -/** expr_value.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. - ** - ** An expression node. - ** - ** Instances of this class are generally referenced through - ** cvc4::Node rather than by pointer; cvc4::Node maintains the - ** reference count on ExprValue instances and - **/ - -#include "expr_value.h" -#include <sstream> - -using namespace std; - -namespace CVC4 { - -size_t ExprValue::next_id = 1; - -ExprValue::ExprValue() : - d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { -} - -uint64_t ExprValue::hash() const { - return computeHash<const_iterator>(d_kind, begin(), end()); -} - -ExprValue* ExprValue::inc() { - // FIXME multithreading - if(d_rc < MAX_RC) - ++d_rc; - return this; -} - -ExprValue* ExprValue::dec() { - // FIXME multithreading - if(d_rc < MAX_RC) - if(--d_rc == 0) { - // FIXME gc - return 0; - } - return this; -} - -ExprValue::iterator ExprValue::begin() { - return d_children; -} - -ExprValue::iterator ExprValue::end() { - return d_children + d_nchildren; -} - -ExprValue::iterator ExprValue::rbegin() { - return d_children + d_nchildren - 1; -} - -ExprValue::iterator ExprValue::rend() { - return d_children - 1; -} - -ExprValue::const_iterator ExprValue::begin() const { - return d_children; -} - -ExprValue::const_iterator ExprValue::end() const { - return d_children + d_nchildren; -} - -ExprValue::const_iterator ExprValue::rbegin() const { - return d_children + d_nchildren - 1; -} - -ExprValue::const_iterator ExprValue::rend() const { - return d_children - 1; -} - -string ExprValue::toString() const { - stringstream ss; - toStream(ss); - return ss.str(); -} - -void ExprValue::toStream(std::ostream& out) const { - out << "(" << Kind(d_kind); - if(d_kind == VARIABLE) { - out << ":" << this; - } else { - for(const_iterator i = begin(); i != end(); ++i) { - if(i != end()) - out << " "; - out << *i; - } - } - out << ")"; -} - -}/* CVC4 namespace */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 5ac02ca7c..624ab7337 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -12,6 +12,7 @@ #ifndef __CVC4__KIND_H #define __CVC4__KIND_H +#include "cvc4_config.h" #include <iostream> namespace CVC4 { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index be9ac995c..1a549973f 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr.cpp +/** node.cpp ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,7 +11,7 @@ **/ #include "expr/node.h" -#include "expr/expr_value.h" +#include "expr/node_value.h" #include "expr/node_builder.h" #include "util/Assert.h" @@ -22,26 +22,29 @@ using namespace std; namespace CVC4 { -ExprValue ExprValue::s_null; +NodeValue NodeValue::s_null; -Node Node::s_null(&ExprValue::s_null); +Node Node::s_null(&NodeValue::s_null); Node Node::null() { return s_null; } - bool Node::isNull() const { - return d_ev == &ExprValue::s_null; + return d_ev == &NodeValue::s_null; } Node::Node() : - d_ev(&ExprValue::s_null) { + d_ev(&NodeValue::s_null) { // No refcount needed } -Node::Node(ExprValue* ev) - : d_ev(ev) { +// FIXME: escape from type system convenient but is there a better +// way? Nodes conceptually don't change their expr values but of +// course they do modify the refcount. But it's nice to be able to +// support node_iterators over const NodeValue*. So.... hm. +Node::Node(const NodeValue* ev) + : d_ev(const_cast<NodeValue*>(ev)) { Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); d_ev->inc(); } @@ -57,7 +60,7 @@ Node::~Node() { d_ev->dec(); } -void Node::assignExprValue(ExprValue* ev) { +void Node::assignNodeValue(NodeValue* ev) { d_ev = ev; d_ev->inc(); } @@ -72,7 +75,7 @@ Node& Node::operator=(const Node& e) { return *this; } -ExprValue const* Node::operator->() const { +NodeValue const* Node::operator->() const { Assert(d_ev != NULL, "Expecting a non-NULL expression value!"); return d_ev; } @@ -83,35 +86,35 @@ uint64_t Node::hash() const { } Node Node::eqExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(EQUAL, *this, right); + return NodeManager::currentNM()->mkExpr(EQUAL, *this, right); } Node Node::notExpr() const { - return NodeManager::currentEM()->mkExpr(NOT, *this); + return NodeManager::currentNM()->mkExpr(NOT, *this); } Node Node::andExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(AND, *this, right); + return NodeManager::currentNM()->mkExpr(AND, *this, right); } Node Node::orExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(OR, *this, right); + return NodeManager::currentNM()->mkExpr(OR, *this, right); } Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { - return NodeManager::currentEM()->mkExpr(ITE, *this, thenpart, elsepart); + return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart); } Node Node::iffExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(IFF, *this, right); + return NodeManager::currentNM()->mkExpr(IFF, *this, right); } Node Node::impExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(IMPLIES, *this, right); + return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right); } Node Node::xorExpr(const Node& right) const { - return NodeManager::currentEM()->mkExpr(XOR, *this, right); + return NodeManager::currentNM()->mkExpr(XOR, *this, right); } }/* CVC4 namespace */ diff --git a/src/expr/node.h b/src/expr/node.h index 17d1c0111..5415a5b3c 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -10,6 +10,8 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ +#include "expr/node_value.h" + #ifndef __CVC4__NODE_H #define __CVC4__NODE_H @@ -32,38 +34,44 @@ inline std::ostream& operator<<(std::ostream&, const Node&); class NodeManager; namespace expr { - class ExprValue; + class NodeValue; }/* CVC4::expr namespace */ -using CVC4::expr::ExprValue; +using CVC4::expr::NodeValue; /** - * Encapsulation of an ExprValue pointer. The reference count is - * maintained in the ExprValue. + * Encapsulation of an NodeValue pointer. The reference count is + * maintained in the NodeValue. */ class Node { - friend class ExprValue; + friend class NodeValue; /** A convenient null-valued encapsulated pointer */ static Node s_null; - /** The referenced ExprValue */ - ExprValue* d_ev; + /** The referenced NodeValue */ + NodeValue* 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; + * Increments the reference count. + * + * FIXME: there's a type-system escape here to cast away the const, + * since the refcount needs to be updated. But conceptually Nodes + * don't change their arguments, and it's nice to have + * const_iterators over them. See notes in .cpp file for + * details. */ + explicit Node(const NodeValue*); + + template <unsigned> friend class NodeBuilder; friend class NodeManager; /** Access to the encapsulated expression. * @return the encapsulated expression. */ - ExprValue const* operator->() const; + NodeValue const* operator->() const; /** * Assigns the expression value and does reference counting. No assumptions are @@ -72,7 +80,15 @@ class Node { * * @param ev the expression value to assign */ - void assignExprValue(ExprValue* ev); + void assignNodeValue(NodeValue* ev); + + typedef NodeValue::iterator ev_iterator; + typedef NodeValue::const_iterator const_ev_iterator; + + inline ev_iterator ev_begin(); + inline ev_iterator ev_end(); + inline const_ev_iterator ev_begin() const; + inline const_ev_iterator ev_end() const; public: @@ -82,7 +98,7 @@ public: Node(const Node&); /** Destructor. Decrements the reference count and, if zero, - * collects the ExprValue. */ + * collects the NodeValue. */ ~Node(); bool operator==(const Node& e) const { return d_ev == e.d_ev; } @@ -117,8 +133,8 @@ public: static Node null(); - typedef Node* iterator; - typedef Node const* const_iterator; + typedef NodeValue::node_iterator iterator; + typedef NodeValue::node_iterator const_iterator; inline iterator begin(); inline iterator end(); @@ -134,7 +150,7 @@ public: }/* CVC4 namespace */ -#include "expr/expr_value.h" +#include "expr/node_value.h" namespace CVC4 { @@ -159,6 +175,22 @@ inline void Node::toStream(std::ostream& out) const { d_ev->toStream(out); } +inline Node::ev_iterator Node::ev_begin() { + return d_ev->ev_begin(); +} + +inline Node::ev_iterator Node::ev_end() { + return d_ev->ev_end(); +} + +inline Node::const_ev_iterator Node::ev_begin() const { + return d_ev->ev_begin(); +} + +inline Node::const_ev_iterator Node::ev_end() const { + return d_ev->ev_end(); +} + inline Node::iterator Node::begin() { return d_ev->begin(); } diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp index 7d30ff4e3..0a36421f2 100644 --- a/src/expr/node_builder.cpp +++ b/src/expr/node_builder.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_builder.cpp +/** node_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 @@ -11,214 +11,7 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/expr_value.h" +#include "expr/node_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<Node> (); - 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; -} - -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<Node>* v = new vector<Node> (); - 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<Node>* v = new vector<Node> (); - 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 index 5be3c284d..63048c1ac 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_builder.h +/** node_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 @@ -14,68 +14,90 @@ #include <vector> #include <cstdlib> +#include <stdint.h> + +namespace CVC4 { + static const unsigned default_nchild_thresh = 10; + + template <unsigned nchild_thresh = default_nchild_thresh> + class NodeBuilder; + + class NodeManager; +}/* CVC4 namespace */ -#include "expr/node_manager.h" #include "expr/kind.h" #include "util/Assert.h" +#include "expr/node_value.h" namespace CVC4 { -class AndExprBuilder; -class OrExprBuilder; -class PlusExprBuilder; -class MinusExprBuilder; -class MultExprBuilder; +class AndNodeBuilder; +class OrNodeBuilder; +class PlusNodeBuilder; +class MinusNodeBuilder; +class MultNodeBuilder; +template <unsigned nchild_thresh> class NodeBuilder { - NodeManager* d_em; + unsigned d_size; - Kind d_kind; + uint64_t d_hash; + + NodeManager* d_nm; // 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<Node>* u_vec; - } d_children; - - void addChild(const Node& e) { addChild(e.d_ev); } - void addChild(ExprValue*); - NodeBuilder& collapse(); + NodeValue *d_ev; + NodeValue d_inlineEv; + NodeValue *d_childrenStorage[nchild_thresh]; - typedef ExprValue** ev_iterator; - typedef ExprValue const** const_ev_iterator; + bool evIsAllocated() { + return d_ev->d_nchildren > nchild_thresh; + } - ev_iterator ev_begin() { - return d_children.u_arr; + template <unsigned N> + bool evIsAllocated(const NodeBuilder<N>& nb) { + return nb.d_ev->d_nchildren > N; } - ev_iterator ev_end() { - return d_children.u_arr + d_nchildren; + bool evNeedsToBeAllocated() { + return d_ev->d_nchildren == d_size; } - NodeBuilder& reset(const ExprValue*); + // realloc in the default way + void realloc(); + + // realloc to a specific size + void realloc(size_t toSize, bool copy = true); + + void allocateEvIfNecessaryForAppend() { + if(EXPECT_FALSE( evNeedsToBeAllocated() )) { + realloc(); + } + } public: - NodeBuilder(); - NodeBuilder(Kind k); - NodeBuilder(const Node&); - NodeBuilder(const NodeBuilder&); + inline NodeBuilder(); + inline NodeBuilder(Kind k); + inline NodeBuilder(const NodeBuilder<nchild_thresh>& nb); + template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb); + inline NodeBuilder(NodeManager* nm); + inline NodeBuilder(NodeManager* nm, Kind k); + inline ~NodeBuilder(); - NodeBuilder(NodeManager*); - NodeBuilder(NodeManager*, Kind k); - NodeBuilder(NodeManager*, const Node&); - NodeBuilder(NodeManager*, const NodeBuilder&); + typedef NodeValue::ev_iterator iterator; + typedef NodeValue::const_ev_iterator const_iterator; - ~NodeBuilder(); + iterator begin() { return d_ev->ev_begin(); } + iterator end() { return d_ev->ev_end(); } + const_iterator begin() const { return d_ev->ev_begin(); } + const_iterator end() const { return d_ev->ev_end(); } // Compound expression constructors + /* NodeBuilder& eqExpr(const Node& right); NodeBuilder& notExpr(); NodeBuilder& andExpr(const Node& right); @@ -84,230 +106,413 @@ public: NodeBuilder& iffExpr(const Node& right); NodeBuilder& impExpr(const Node& right); NodeBuilder& xorExpr(const Node& right); + */ - /* TODO design: these modify NodeBuilder */ + /* 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); } + */ + + /* + 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); + + NodeBuilder& operator<<(const Kind& k) { + Assert(d_ev->d_kind == UNDEFINED_KIND); + d_ev->d_kind = k; + return *this; + } + + NodeBuilder& operator<<(const Node& n) { + return append(n); + } // For pushing sequences of children - NodeBuilder& append(const std::vector<Node>& children) { return append(children.begin(), children.end()); } - NodeBuilder& append(Node child) { return append(&child, (&child) + 1); } - template <class Iterator> 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; + NodeBuilder& append(const std::vector<Node>& children) { + return append(children.begin(), children.end()); + } + + NodeBuilder& append(const Node& n) { + allocateEvIfNecessaryForAppend(); + NodeValue* ev = n.d_ev; + d_hash = NodeValue::computeHash(d_hash, ev); + ev->inc(); + d_ev->d_children[d_ev->d_nchildren++] = ev; + return *this; + } + + template <class Iterator> + NodeBuilder& append(const Iterator& begin, const Iterator& end) { + for(Iterator i = begin; i != end; ++i) { + append(*i); + } + return *this; + } + + void crop() { + if(EXPECT_FALSE( evIsAllocated() ) && d_size > d_ev->d_nchildren) { + d_ev = (NodeValue*) + std::realloc(d_ev, sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = d_ev->d_nchildren) )); + } + } + + // not const + operator Node(); + + /* + AndNodeBuilder operator&&(Node); + OrNodeBuilder operator||(Node); + PlusNodeBuilder operator+ (Node); + PlusNodeBuilder operator- (Node); + MultNodeBuilder operator* (Node); + + friend class AndNodeBuilder; + friend class OrNodeBuilder; + friend class PlusNodeBuilder; + friend class MultNodeBuilder; + */ };/* class NodeBuilder */ -class AndExprBuilder { +#if 0 +class AndNodeBuilder { NodeBuilder d_eb; public: - AndExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + AndNodeBuilder(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); + AndNodeBuilder& operator&&(Node); + OrNodeBuilder operator||(Node); operator NodeBuilder() { return d_eb; } -};/* class AndExprBuilder */ +};/* class AndNodeBuilder */ -class OrExprBuilder { +class OrNodeBuilder { NodeBuilder d_eb; public: - OrExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + OrNodeBuilder(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); + AndNodeBuilder operator&&(Node); + OrNodeBuilder& operator||(Node); operator NodeBuilder() { return d_eb; } -};/* class OrExprBuilder */ +};/* class OrNodeBuilder */ -class PlusExprBuilder { +class PlusNodeBuilder { NodeBuilder d_eb; public: - PlusExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + PlusNodeBuilder(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); + PlusNodeBuilder& operator+(Node); + PlusNodeBuilder& operator-(Node); + MultNodeBuilder operator*(Node); operator NodeBuilder() { return d_eb; } -};/* class PlusExprBuilder */ +};/* class PlusNodeBuilder */ -class MultExprBuilder { +class MultNodeBuilder { NodeBuilder d_eb; public: - MultExprBuilder(const NodeBuilder& eb) : d_eb(eb) { + MultNodeBuilder(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); + PlusNodeBuilder operator+(Node); + PlusNodeBuilder operator-(Node); + MultNodeBuilder& operator*(Node); operator NodeBuilder() { return d_eb; } -};/* class MultExprBuilder */ - -template <class Iterator> -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!"); +};/* class MultNodeBuilder */ - // variables are permitted to be duplicates (from POV of the expression manager) - if(d_kind == VARIABLE) { - ev = new ExprValue; - ev->d_kind = d_kind; - ev->d_id = ExprValue::next_id++;// FIXME multithreading - return Node(ev); - } else { - if(d_nchildren <= nchild_thresh) { - hash = ExprValue::computeHash<ev_iterator>(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 without using an assignment operator - ev->d_children[nc++].assignExprValue(*i); - } - } else { - hash = ExprValue::computeHash<std::vector<Node>::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<Node>::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 AndNodeBuilder NodeBuilder::operator&&(Node e) { + return AndNodeBuilder(*this) && e; } -inline OrExprBuilder NodeBuilder::operator||(Node e) { - return OrExprBuilder(*this) || e; +inline OrNodeBuilder NodeBuilder::operator||(Node e) { + return OrNodeBuilder(*this) || e; } -inline PlusExprBuilder NodeBuilder::operator+ (Node e) { - return PlusExprBuilder(*this) + e; +inline PlusNodeBuilder NodeBuilder::operator+ (Node e) { + return PlusNodeBuilder(*this) + e; } -inline PlusExprBuilder NodeBuilder::operator- (Node e) { - return PlusExprBuilder(*this) - e; +inline PlusNodeBuilder NodeBuilder::operator- (Node e) { + return PlusNodeBuilder(*this) - e; } -inline MultExprBuilder NodeBuilder::operator* (Node e) { - return MultExprBuilder(*this) * e; +inline MultNodeBuilder NodeBuilder::operator* (Node e) { + return MultNodeBuilder(*this) * e; } -inline AndExprBuilder& AndExprBuilder::operator&&(Node e) { +inline AndNodeBuilder& AndNodeBuilder::operator&&(Node e) { d_eb.append(e); return *this; } -inline OrExprBuilder AndExprBuilder::operator||(Node e) { - return OrExprBuilder(d_eb.collapse()) || e; +inline OrNodeBuilder AndNodeBuilder::operator||(Node e) { + return OrNodeBuilder(d_eb.collapse()) || e; } -inline AndExprBuilder OrExprBuilder::operator&&(Node e) { - return AndExprBuilder(d_eb.collapse()) && e; +inline AndNodeBuilder OrNodeBuilder::operator&&(Node e) { + return AndNodeBuilder(d_eb.collapse()) && e; } -inline OrExprBuilder& OrExprBuilder::operator||(Node e) { +inline OrNodeBuilder& OrNodeBuilder::operator||(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator+(Node e) { +inline PlusNodeBuilder& PlusNodeBuilder::operator+(Node e) { d_eb.append(e); return *this; } -inline PlusExprBuilder& PlusExprBuilder::operator-(Node e) { +inline PlusNodeBuilder& PlusNodeBuilder::operator-(Node e) { d_eb.append(e.uMinusExpr()); return *this; } -inline MultExprBuilder PlusExprBuilder::operator*(Node e) { - return MultExprBuilder(d_eb.collapse()) * e; +inline MultNodeBuilder PlusNodeBuilder::operator*(Node e) { + return MultNodeBuilder(d_eb.collapse()) * e; } -inline PlusExprBuilder MultExprBuilder::operator+(Node e) { - return MultExprBuilder(d_eb.collapse()) + e; +inline PlusNodeBuilder MultNodeBuilder::operator+(Node e) { + return MultNodeBuilder(d_eb.collapse()) + e; } -inline PlusExprBuilder MultExprBuilder::operator-(Node e) { - return MultExprBuilder(d_eb.collapse()) - e; +inline PlusNodeBuilder MultNodeBuilder::operator-(Node e) { + return MultNodeBuilder(d_eb.collapse()) - e; } -inline MultExprBuilder& MultExprBuilder::operator*(Node e) { +inline MultNodeBuilder& MultNodeBuilder::operator*(Node e) { d_eb.append(e); return *this; } +#endif /* 0 */ + +}/* CVC4 namespace */ + +#include "expr/node.h" +#include "expr/node_manager.h" + +// template implementations + +namespace CVC4 { + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder() : + d_size(nchild_thresh), + d_nm(NodeManager::currentNM()), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) {} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(Kind k) : + d_size(nchild_thresh), + d_nm(NodeManager::currentNM()), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) { + + d_inlineEv.d_kind = k; +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<nchild_thresh>& nb) : + d_size(nchild_thresh), + d_nm(nb.d_nm), + d_used(nb.d_used), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) { + + if(evIsAllocated(nb)) { + realloc(nb->d_size, false); + std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end()); + } else { + std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end()); + } +} + +template <unsigned nchild_thresh> +template <unsigned N> +inline NodeBuilder<nchild_thresh>::NodeBuilder(const NodeBuilder<N>& nb) : + d_size(nchild_thresh), + d_nm(NodeManager::currentNM()), + d_used(nb.d_used), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) { + + if(nb.d_ev->d_nchildren > nchild_thresh) { + realloc(nb.d_size, false); + std::copy(d_ev->begin(), nb.d_ev->begin(), nb.d_ev->end()); + } else { + std::copy(d_inlineEv.begin(), nb.d_ev->begin(), nb.d_ev->end()); + } +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm) : + d_size(nchild_thresh), + d_nm(nm), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage(0) {} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::NodeBuilder(NodeManager* nm, Kind k) : + d_size(nchild_thresh), + d_nm(nm), + d_used(false), + d_ev(&d_inlineEv), + d_inlineEv(0), + d_childrenStorage() { + + d_inlineEv.d_kind = k; +} + +template <unsigned nchild_thresh> +inline NodeBuilder<nchild_thresh>::~NodeBuilder() { + for(iterator i = begin(); + i != end(); + ++i) { + (*i)->dec(); + } + if(evIsAllocated()) { + free(d_ev); + } +} + +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::realloc() { + if(EXPECT_FALSE( evIsAllocated() )) { + d_ev = (NodeValue*) + std::realloc(d_ev, + sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) )); + } else { + d_ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + ( sizeof(NodeValue*) * (d_size *= 2) )); + d_ev->d_id = 0; + d_ev->d_rc = 0; + d_ev->d_kind = d_inlineEv.d_kind; + d_ev->d_nchildren = nchild_thresh; + std::copy(d_ev->d_children, + d_inlineEv.d_children, + d_inlineEv.d_children + nchild_thresh); + } +} + +template <unsigned nchild_thresh> +void NodeBuilder<nchild_thresh>::realloc(size_t toSize, bool copy) { + Assert( d_size < toSize ); + + if(EXPECT_FALSE( evIsAllocated() )) { + d_ev = (NodeValue*) + std::realloc(d_ev, sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = toSize) )); + } else { + d_ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + + ( sizeof(NodeValue*) * (d_size = toSize) )); + d_ev->d_id = 0; + d_ev->d_rc = 0; + d_ev->d_kind = d_inlineEv.d_kind; + d_ev->d_nchildren = nchild_thresh; + if(copy) { + std::copy(d_ev->d_children, + d_inlineEv.d_children, + d_inlineEv.d_children + nchild_thresh); + } + } +} + +template <unsigned nchild_thresh> +NodeBuilder<nchild_thresh>::operator Node() {// not const + Assert(d_ev->d_kind != UNDEFINED_KIND, + "Can't make an expression of an undefined kind!"); + Assert(! d_used, "This NodeBuilder has already been used!"); + + // implementation differs depending on whether the expression value + // was malloc'ed or not + + if(EXPECT_FALSE( evIsAllocated() )) { + NodeValue *ev = d_nm->lookupNoInsert(d_hash, d_ev); + if(ev != d_ev) { + // expression already exists in node manager + return Node(ev); + } + + // otherwise create the canonical expression value for this node + crop(); + d_used = true; + ev = d_ev; + d_ev = NULL; + // this inserts into the NodeManager; + // return the result of lookup() in case another thread beat us to it + return d_nm->lookup(d_hash, ev); + } + + NodeValue *ev = d_nm->lookupNoInsert(d_hash, &d_inlineEv); + if(ev != &d_inlineEv) { + // expression already exists in node manager + return Node(ev); + } + + // otherwise create the canonical expression value for this node + ev = (NodeValue*) + std::malloc(sizeof(NodeValue) + + ( sizeof(NodeValue*) * d_inlineEv.d_nchildren) ); + ev->d_nchildren = d_ev->d_nchildren; + ev->d_kind = d_ev->d_kind; + ev->d_id = NodeValue::next_id++;// FIXME multithreading + ev->d_rc = 0; + d_used = true; + d_ev = NULL; + + // this inserts into the NodeManager; + // return the result of lookup() in case another thread beat us to it + return d_nm->lookup(d_hash, ev); +} }/* CVC4 namespace */ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 8da87c9eb..ab52b9f40 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_manager.cpp +/** node_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 @@ -18,76 +18,116 @@ 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!"); +Node NodeManager::lookup(uint64_t hash, NodeValue* ev) { + Assert(this != NULL, "Whoops, we have a bad expression manager!"); hash_t::iterator i = d_hash.find(hash); if(i == d_hash.end()) { // insert std::vector<Node> v; + Node e(ev); v.push_back(e); d_hash.insert(std::make_pair(hash, v)); return e; } else { for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) { - if(e.getKind() != j->getKind()) + if(ev->getKind() != j->getKind()) { continue; + } - if(e.numChildren() != j->numChildren()) + if(ev->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) + NodeValue::const_iterator c1 = ev->ev_begin(); + NodeValue::iterator c2 = j->d_ev->ev_begin(); + for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) { + if((*c1).d_ev != (*c2).d_ev) { break; + } } - if(c1 != e.end() || c2 != j->end()) + if(c1 != ev->ev_end() || c2 != j->end()) { continue; + } return *j; } // didn't find it, insert std::vector<Node> v; + Node e(ev); v.push_back(e); d_hash.insert(std::make_pair(hash, v)); return e; } } +NodeValue* NodeManager::lookupNoInsert(uint64_t hash, NodeValue* ev) { + Assert(this != NULL, "Whoops, we have a bad expression manager!"); + hash_t::iterator i = d_hash.find(hash); + if(i == d_hash.end()) { + return NULL; + } else { + for(std::vector<Node>::iterator j = i->second.begin(); j != i->second.end(); ++j) { + if(ev->getKind() != j->getKind()) { + continue; + } + + if(ev->numChildren() != j->numChildren()) { + continue; + } + + NodeValue::const_iterator c1 = ev->ev_begin(); + NodeValue::iterator c2 = j->d_ev->ev_begin(); + for(; c1 != ev->ev_end() && c2 != j->d_ev->ev_end(); ++c1, ++c2) { + if((*c1).d_ev != (*c2).d_ev) { + break; + } + } + + if(c1 != ev->ev_end() || c2 != j->end()) { + continue; + } + + return j->d_ev; + } + // didn't find it + return 0; + } +} + // general expression-builders Node NodeManager::mkExpr(Kind kind) { - return NodeBuilder(this, kind); + return NodeBuilder<>(this, kind); } Node NodeManager::mkExpr(Kind kind, const Node& child1) { - return NodeBuilder(this, kind) << child1; + return NodeBuilder<>(this, kind) << child1; } Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) { - return NodeBuilder(this, kind) << child1 << 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; + 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; + 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; + return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5; } // N-ary version Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) { - return NodeBuilder(this, kind).append(children); + return NodeBuilder<>(this, kind).append(children); } Node NodeManager::mkVar() { - return NodeBuilder(this, VARIABLE); + return NodeBuilder<>(this, VARIABLE); } }/* CVC4 namespace */ diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 6c20b29e8..3a28a22ff 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -20,22 +20,20 @@ namespace CVC4 { -namespace expr { - class ExprBuilder; -}/* CVC4::expr namespace */ - class NodeManager { static __thread NodeManager* s_current; - friend class CVC4::NodeBuilder; + template <unsigned> friend class CVC4::NodeBuilder; typedef std::map<uint64_t, std::vector<Node> > hash_t; hash_t d_hash; - Node lookup(uint64_t hash, const Node& e); + Node lookup(uint64_t hash, const Node& e) { return lookup(hash, e.d_ev); } + Node lookup(uint64_t hash, NodeValue* e); + NodeValue* lookupNoInsert(uint64_t hash, NodeValue* e); public: - static NodeManager* currentEM() { return s_current; } + static NodeManager* currentNM() { return s_current; } // general expression-builders Node mkExpr(Kind kind); @@ -50,20 +48,20 @@ public: // variables are special, because duplicates are permitted Node mkVar(); - // TODO: these use the current EM (but must be renamed) + // TODO: these use the current NM (but must be renamed) /* static Node mkExpr(Kind kind) - { currentEM()->mkExpr(kind); } + { currentNM()->mkExpr(kind); } static Node mkExpr(Kind kind, Node child1); - { currentEM()->mkExpr(kind, child1); } + { currentNM()->mkExpr(kind, child1); } static Node mkExpr(Kind kind, Node child1, Node child2); - { currentEM()->mkExpr(kind, child1, child2); } + { currentNM()->mkExpr(kind, child1, child2); } static Node mkExpr(Kind kind, Node child1, Node child2, Node child3); - { currentEM()->mkExpr(kind, child1, child2, child3); } + { currentNM()->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); } + { currentNM()->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); } + { currentNM()->mkExpr(kind, child1, child2, child3, child4, child5); } */ // do we want a varargs one? perhaps not.. diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp new file mode 100644 index 000000000..7af2cd2b5 --- /dev/null +++ b/src/expr/node_value.cpp @@ -0,0 +1,147 @@ +/********************* -*- C++ -*- */ +/** node_value.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. + ** + ** An expression node. + ** + ** Instances of this class are generally referenced through + ** cvc4::Node rather than by pointer; cvc4::Node maintains the + ** reference count on NodeValue instances and + **/ + +#include "node_value.h" +#include <sstream> + +using namespace std; + +namespace CVC4 { + +size_t NodeValue::next_id = 1; + +NodeValue::NodeValue() : + d_id(0), d_rc(MAX_RC), d_kind(NULL_EXPR), d_nchildren(0) { +} + +NodeValue::NodeValue(int) : + d_id(0), d_rc(0), d_kind(unsigned(UNDEFINED_KIND)), d_nchildren(0) { +} + +NodeValue::~NodeValue() { + for(ev_iterator i = ev_begin(); i != ev_end(); ++i) { + (*i)->dec(); + } +} + +uint64_t NodeValue::hash() const { + return computeHash(d_kind, ev_begin(), ev_end()); +} + +NodeValue* NodeValue::inc() { + // FIXME multithreading + if(d_rc < MAX_RC) + ++d_rc; + return this; +} + +NodeValue* NodeValue::dec() { + // FIXME multithreading + if(d_rc < MAX_RC) { + if(--d_rc == 0) { + // FIXME gc + return 0; + } + } + return this; +} + +NodeValue::iterator NodeValue::begin() { + return node_iterator(d_children); +} + +NodeValue::iterator NodeValue::end() { + return node_iterator(d_children + d_nchildren); +} + +NodeValue::iterator NodeValue::rbegin() { + return node_iterator(d_children + d_nchildren - 1); +} + +NodeValue::iterator NodeValue::rend() { + return node_iterator(d_children - 1); +} + +NodeValue::const_iterator NodeValue::begin() const { + return const_node_iterator(d_children); +} + +NodeValue::const_iterator NodeValue::end() const { + return const_node_iterator(d_children + d_nchildren); +} + +NodeValue::const_iterator NodeValue::rbegin() const { + return const_node_iterator(d_children + d_nchildren - 1); +} + +NodeValue::const_iterator NodeValue::rend() const { + return const_node_iterator(d_children - 1); +} + +NodeValue::ev_iterator NodeValue::ev_begin() { + return d_children; +} + +NodeValue::ev_iterator NodeValue::ev_end() { + return d_children + d_nchildren; +} + +NodeValue::ev_iterator NodeValue::ev_rbegin() { + return d_children + d_nchildren - 1; +} + +NodeValue::ev_iterator NodeValue::ev_rend() { + return d_children - 1; +} + +NodeValue::const_ev_iterator NodeValue::ev_begin() const { + return d_children; +} + +NodeValue::const_ev_iterator NodeValue::ev_end() const { + return d_children + d_nchildren; +} + +NodeValue::const_ev_iterator NodeValue::ev_rbegin() const { + return d_children + d_nchildren - 1; +} + +NodeValue::const_ev_iterator NodeValue::ev_rend() const { + return d_children - 1; +} + +string NodeValue::toString() const { + stringstream ss; + toStream(ss); + return ss.str(); +} + +void NodeValue::toStream(std::ostream& out) const { + out << "(" << Kind(d_kind); + if(d_kind == VARIABLE) { + out << ":" << this; + } else { + for(const_iterator i = begin(); i != end(); ++i) { + if(i != end()) { + out << " "; + } + out << *i; + } + } + out << ")"; +} + +}/* CVC4 namespace */ diff --git a/src/expr/expr_value.h b/src/expr/node_value.h index 25fada4af..9bdbb7f8c 100644 --- a/src/expr/expr_value.h +++ b/src/expr/node_value.h @@ -1,5 +1,5 @@ /********************* -*- C++ -*- */ -/** expr_value.h +/** node_value.h ** This file is part of the CVC4 prototype. ** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -11,15 +11,15 @@ ** ** Instances of this class are generally referenced through ** cvc4::Node rather than by pointer; cvc4::Node maintains the - ** reference count on ExprValue instances and + ** reference count on NodeValue instances and **/ -/* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ +/* this must be above the check for __CVC4__EXPR__NODE_VALUE_H */ /* to resolve a circular dependency */ -#include "expr/node.h" +//#include "expr/node.h" -#ifndef __CVC4__EXPR__EXPR_VALUE_H -#define __CVC4__EXPR__EXPR_VALUE_H +#ifndef __CVC4__EXPR__NODE_VALUE_H +#define __CVC4__EXPR__NODE_VALUE_H #include "cvc4_config.h" #include <stdint.h> @@ -30,17 +30,18 @@ namespace CVC4 { class Node; -class NodeBuilder; +template <unsigned> class NodeBuilder; +class NodeManager; namespace expr { /** - * This is an ExprValue. + * This is an NodeValue. */ -class ExprValue { +class NodeValue { /** A convenient null-valued expression value */ - static ExprValue s_null; + static NodeValue s_null; /** Maximum reference count possible. Used for sticky * reference-counting. Should be (1 << num_bits(d_rc)) - 1 */ @@ -61,25 +62,32 @@ class ExprValue { unsigned d_nchildren : 16; /** Variable number of child nodes */ - Node d_children[0]; + NodeValue *d_children[0]; // todo add exprMgr ref in debug case friend class CVC4::Node; - friend class CVC4::NodeBuilder; + template <unsigned> friend class CVC4::NodeBuilder; + friend class CVC4::NodeManager; - ExprValue* inc(); - ExprValue* dec(); + NodeValue* inc(); + NodeValue* dec(); static size_t next_id; /** Private default constructor for the null value. */ - ExprValue(); + NodeValue(); + + /** Private default constructor for the NodeBuilder. */ + NodeValue(int); + + /** Destructor decrements the ref counts of its children */ + ~NodeValue(); /** * Computes the hash over the given iterator span of children, and the * root hash. The iterator should be either over a range of Node or pointers - * to ExprValue. + * to NodeValue. * @param hash the initial value for the hash * @param begin the begining of the range * @param end the end of the range @@ -87,11 +95,55 @@ class ExprValue { */ template<typename const_iterator_type> static uint64_t computeHash(uint64_t hash, const_iterator_type begin, const_iterator_type end) { - for(const_iterator_type i = begin; i != end; ++i) - hash = ((hash << 3) | ((hash & 0xE000000000000000ull) >> 61)) ^ (*i)->getId(); + for(const_iterator_type i = begin; i != end; ++i) { + hash = computeHash(hash, *i); + } return hash; } + static uint64_t computeHash(uint64_t hash, const NodeValue* ev) { + return ( (hash << 3) | ((hash & 0xE000000000000000ull) >> 61) ) ^ ev->getId(); + } + + typedef NodeValue** ev_iterator; + typedef NodeValue const* const* const_ev_iterator; + + ev_iterator ev_begin(); + ev_iterator ev_end(); + ev_iterator ev_rbegin(); + ev_iterator ev_rend(); + + const_ev_iterator ev_begin() const; + const_ev_iterator ev_end() const; + const_ev_iterator ev_rbegin() const; + const_ev_iterator ev_rend() const; + + class node_iterator { + const_ev_iterator d_i; + public: + node_iterator(const_ev_iterator i) : d_i(i) {} + + inline Node operator*(); + + bool operator==(const node_iterator& i) { + return d_i == i.d_i; + } + + bool operator!=(const node_iterator& i) { + return d_i != i.d_i; + } + + node_iterator& operator++() { + ++d_i; + return *this; + } + + node_iterator operator++(int) { + return node_iterator(d_i++); + } + }; + typedef node_iterator const_node_iterator; + public: /** Hash this expression. * @return the hash value of this expression. */ @@ -99,8 +151,8 @@ public: // Iterator support - typedef Node* iterator; - typedef Node const* const_iterator; + typedef node_iterator iterator; + typedef node_iterator const_iterator; iterator begin(); iterator end(); @@ -113,7 +165,8 @@ public: const_iterator rend() const; unsigned getId() const { return d_id; } - unsigned getKind() const { return (Kind) d_kind; } + Kind getKind() const { return (Kind) d_kind; } + unsigned numChildren() const { return d_nchildren; } std::string toString() const; void toStream(std::ostream& out) const; }; @@ -121,4 +174,16 @@ public: }/* CVC4::expr namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__EXPR__EXPR_VALUE_H */ +#include "expr/node.h" + +namespace CVC4 { +namespace expr { + +inline Node NodeValue::node_iterator::operator*() { + return Node(*d_i); +} + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__EXPR__NODE_VALUE_H */ diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index a42ae28fb..f1877781f 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -10,6 +10,9 @@ ** [[ Add file-specific comments here ]] **/ +#ifndef __CVC4_CONFIG_H +#define __CVC4_CONFIG_H + #if defined _WIN32 || defined __CYGWIN__ # ifdef BUILDING_DLL # ifdef __GNUC__ @@ -35,3 +38,9 @@ #define EXPECT_TRUE(x) __builtin_expect( (x), true) #define EXPECT_FALSE(x) __builtin_expect( (x), false) #define NORETURN __attribute__ ((noreturn)) + +#ifndef NULL +# define NULL ((void*) 0) +#endif + +#endif /* __CVC4_CONFIG_H */ diff --git a/src/main/Makefile b/src/main/Makefile new file mode 100644 index 000000000..686674906 --- /dev/null +++ b/src/main/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/main +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 6b8ea928c..f5b76fcfb 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,6 +1,6 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = bin_PROGRAMS = cvc4 diff --git a/src/main/Makefile.in b/src/main/Makefile.in index ba924109e..26ea81859 100644 --- a/src/main/Makefile.in +++ b/src/main/Makefile.in @@ -106,6 +106,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -217,9 +218,10 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = cvc4_SOURCES = \ main.cpp \ getopt.cpp \ diff --git a/src/parser/Makefile b/src/parser/Makefile new file mode 100644 index 000000000..1ea7edf5d --- /dev/null +++ b/src/parser/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/parser +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index e54d4aa2d..7f1ddce1f 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,9 +15,10 @@ LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB SUBDIRS = smt cvc diff --git a/src/parser/Makefile.in b/src/parser/Makefile.in index b2e066f8d..859329834 100644 --- a/src/parser/Makefile.in +++ b/src/parser/Makefile.in @@ -168,6 +168,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -296,9 +297,11 @@ top_srcdir = @top_srcdir@ # LIBCVC4PARSER_RELEASE = @CVC4_LIBRARY_RELEASE_CODE@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB SUBDIRS = smt cvc nobase_lib_LTLIBRARIES = libcvc4parser.la libcvc4parser_la_LDFLAGS = $(ANTLR_LDFLAGS) diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 2d3033a59..1baaf2139 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -133,10 +133,10 @@ void AntlrParser::rethrow(antlr::SemanticException& e, string new_message) LT(0).get()->getColumn()); } -Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, const vector< - Kind>& kinds) { +Expr AntlrParser::createPrecedenceExpr(const vector<Expr>& exprs, + const vector<Kind>& kinds) { Assert( exprs.size() > 0, "Expected non-empty vector expr"); - Assert( vectors.size() + 1 == exprs.size(), "Expected kinds to match exprs"); + Assert( kinds.size() + 1 == exprs.size(), "Expected kinds to match exprs"); return createPrecedenceExpr(exprs, kinds, 0, exprs.size() - 1); } diff --git a/src/parser/cvc/Makefile b/src/parser/cvc/Makefile new file mode 100644 index 000000000..c91554a47 --- /dev/null +++ b/src/parser/cvc/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/parser/cvc +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index 6fb9689de..666c408cf 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsercvc.la diff --git a/src/parser/cvc/Makefile.in b/src/parser/cvc/Makefile.in index cbab2fd5c..57db98f0b 100644 --- a/src/parser/cvc/Makefile.in +++ b/src/parser/cvc/Makefile.in @@ -108,6 +108,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -219,9 +220,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../../include -I@srcdir@/../.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsercvc.la ANTLR_TOKEN_STUFF = \ @srcdir@/generated/CvcVocabularyTokenTypes.hpp \ diff --git a/src/parser/smt/Makefile b/src/parser/smt/Makefile new file mode 100644 index 000000000..aa3e74236 --- /dev/null +++ b/src/parser/smt/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/parser/smt +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index c3273f501..6f5f1bfd4 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsersmt.la diff --git a/src/parser/smt/Makefile.in b/src/parser/smt/Makefile.in index 281d2152b..2e9350486 100644 --- a/src/parser/smt/Makefile.in +++ b/src/parser/smt/Makefile.in @@ -108,6 +108,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -219,9 +220,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4PARSERLIB \ + -I@srcdir@/../../include -I@srcdir@/../.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4PARSERLIB noinst_LTLIBRARIES = libparsersmt.la ANTLR_TOKEN_STUFF = \ @srcdir@/generated/SmtVocabularyTokenTypes.hpp \ diff --git a/src/prop/Makefile b/src/prop/Makefile new file mode 100644 index 000000000..79fe1084b --- /dev/null +++ b/src/prop/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/prop +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 715e79d16..3473de30f 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libprop.la diff --git a/src/prop/Makefile.in b/src/prop/Makefile.in index 6d4e7f0b5..311d3f8c7 100644 --- a/src/prop/Makefile.in +++ b/src/prop/Makefile.in @@ -142,6 +142,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -253,9 +254,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libprop.la libprop_la_SOURCES = \ prop_engine.cpp \ diff --git a/src/prop/minisat/Makefile b/src/prop/minisat/Makefile new file mode 100644 index 000000000..49512a1cd --- /dev/null +++ b/src/prop/minisat/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/prop/minisat +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index f066f8669..609c25dd7 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ diff --git a/src/prop/minisat/Makefile.in b/src/prop/minisat/Makefile.in index a2cc36300..a54518c74 100644 --- a/src/prop/minisat/Makefile.in +++ b/src/prop/minisat/Makefile.in @@ -104,6 +104,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -215,9 +216,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ core/Solver.C \ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 166546a2c..caf87428b 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -34,7 +34,7 @@ void PropEngine::addVars(Node e) { Debug("prop") << "adding vars to " << e << endl; for(Node::iterator i = e.begin(); i != e.end(); ++i) { Debug("prop") << "expr " << *i << endl; - if(i->getKind() == VARIABLE) { + if((*i).getKind() == VARIABLE) { if(d_vars.find(*i) == d_vars.end()) { Var v = d_sat.newVar(); Debug("prop") << "adding var " << *i << " <--> " << v << endl; diff --git a/src/smt/Makefile b/src/smt/Makefile new file mode 100644 index 000000000..84a43ff39 --- /dev/null +++ b/src/smt/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/smt +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index b3637b6d9..bd75bacab 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libsmt.la diff --git a/src/smt/Makefile.in b/src/smt/Makefile.in index 7c60db89b..9647e51b9 100644 --- a/src/smt/Makefile.in +++ b/src/smt/Makefile.in @@ -104,6 +104,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -215,9 +216,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libsmt.la libsmt_la_SOURCES = \ smt_engine.cpp \ diff --git a/src/theory/Makefile b/src/theory/Makefile new file mode 100644 index 000000000..2a4a03491 --- /dev/null +++ b/src/theory/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/theory +builddir = $(topdir)/$(builds)/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index f8e9908c9..4eba7811c 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/Makefile.in b/src/theory/Makefile.in index 7af3f957c..d37387741 100644 --- a/src/theory/Makefile.in +++ b/src/theory/Makefile.in @@ -142,6 +142,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -253,9 +254,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libtheory.la libtheory_la_SOURCES = \ theory_engine.h \ diff --git a/src/theory/uf/Makefile b/src/theory/uf/Makefile new file mode 100644 index 000000000..524ff2009 --- /dev/null +++ b/src/theory/uf/Makefile @@ -0,0 +1,5 @@ +topdir = ../../.. +srcdir = src/theory/uf +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 11c9f536e..4b36d2fe8 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libuf.la diff --git a/src/theory/uf/Makefile.in b/src/theory/uf/Makefile.in index 4920e7a0c..dfb8ea932 100644 --- a/src/theory/uf/Makefile.in +++ b/src/theory/uf/Makefile.in @@ -90,6 +90,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -201,9 +202,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../../include -I@srcdir@/../.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../../include -I@srcdir@/../.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = all: all-am diff --git a/src/util/Makefile b/src/util/Makefile new file mode 100644 index 000000000..0bd2f197b --- /dev/null +++ b/src/util/Makefile @@ -0,0 +1,5 @@ +topdir = ../.. +srcdir = src/util +builddir = $(topdir)/builds/$(srcdir) + +include $(topdir)/Makefile.subdir diff --git a/src/util/Makefile.am b/src/util/Makefile.am index b6c116a6d..316c747de 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -1,6 +1,7 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la diff --git a/src/util/Makefile.in b/src/util/Makefile.in index 61768f933..5627e01a9 100644 --- a/src/util/Makefile.in +++ b/src/util/Makefile.in @@ -105,6 +105,7 @@ CXX = @CXX@ CXXCPP = @CXXCPP@ CXXDEPMODE = @CXXDEPMODE@ CXXFLAGS = @CXXFLAGS@ +CXXTEST = @CXXTEST@ CXXTESTGEN = @CXXTESTGEN@ CYGPATH_W = @CYGPATH_W@ DEFS = @DEFS@ @@ -216,9 +217,11 @@ target_vendor = @target_vendor@ top_build_prefix = @top_build_prefix@ top_builddir = @top_builddir@ top_srcdir = @top_srcdir@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. + AM_CXXFLAGS = -Wall -fvisibility=hidden -AM_CPPFLAGS = -D__BUILDING_CVC4LIB noinst_LTLIBRARIES = libutil.la libutil_la_SOURCES = \ Assert.h \ |