From 88b52c971b43248e6ceacf1c8140a06427d0418d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 5 Mar 2010 08:26:37 +0000 Subject: [PATCH] * public/private code untangled (smt/smt_engine.h no longer #includes expr/node.h). This removes the warnings we had during compilation, and heads off a number of potential linking errors due to improper inlining of private (library-only) stuff in client (out-of-library) code. * "configure" now takes some options as part of a "bare-option" build type (e.g., "./configure debug-coverage" or "./configure production-muzzle"). * split cdo.h, cdlist.h, cdmap.h, and cdset.h from context.h * split cdlist_black unit test from context_black * implement CDMap<>. * give ExprManagers ownership of the context (and have SmtEngine share that one) * fix main driver to properly report file-not-found * fix MemoryMappedInputBuffer class to report reasons for "errno"-returned system errors * src/expr/attribute.h: context-dependent attribute kinds now supported * test/unit/expr/node_white.h: context-dependent attribute tests * src/prop/cnf_conversion.h and associated parts of src/util/options.h and src/main/getopt.cpp: obsolete command-line option, removed. * src/util/Assert.h: assertions are now somewhat more useful (in debug builds, anyway) during stack unwinding. * test/unit/theory/theory_black.h: test context-dependent behavior of registerTerm() attribute for theories * src/expr/node_builder.h: formatting, fixes for arithmetic convenience node builders, check memory allocations * test/unit/expr/node_builder_black.h: add tessts for addition, subtraction, unary minus, and multiplication convenience node builders * src/expr/attribute.h: more comments * (various) code formatting, comment cleanup, added throws specifier to some destructors * contrib/code-checker: prototype perl script to test (some) code policy * contrib/indent-settings: command line for GNU indent to indent using CVC4 style (sort of; this is a work in progress) * COPYING: legal stuff * DESIGN_QUESTIONS: obsolete, removed --- COPYING | 57 ++- DESIGN_QUESTIONS | 82 ---- config/cvc4.m4 | 23 +- configure.ac | 4 +- contrib/code-checker | 96 +++++ contrib/indent-settings | 1 + src/context/Makefile.am | 7 +- src/context/cdlist.h | 222 ++++++++++ src/context/cdmap.h | 407 ++++++++++++++++++ src/context/cdo.h | 122 ++++++ src/context/cdset.h | 33 ++ src/context/context.cpp | 54 ++- src/context/context.h | 532 ++++++------------------ src/context/context_mm.cpp | 21 +- src/context/context_mm.h | 26 +- src/expr/attribute.h | 217 ++++++++-- src/expr/command.cpp | 2 +- src/expr/expr.cpp | 8 +- src/expr/expr_manager.cpp | 12 +- src/expr/expr_manager.h | 26 +- src/expr/node.h | 122 +++--- src/expr/node_builder.h | 145 +++++-- src/expr/node_manager.h | 54 ++- src/expr/node_value.h | 51 ++- src/main/getopt.cpp | 25 +- src/main/main.cpp | 2 +- src/main/util.cpp | 43 ++ src/parser/antlr_parser.cpp | 8 +- src/parser/memory_mapped_input_buffer.h | 36 +- src/parser/parser.cpp | 8 +- src/parser/parser_exception.h | 4 +- src/parser/symbol_table.h | 4 +- src/prop/cnf_conversion.h | 51 --- src/prop/cnf_stream.cpp | 8 +- src/smt/smt_engine.cpp | 53 ++- src/smt/smt_engine.h | 28 +- src/theory/uf/ecdata.h | 2 +- src/theory/uf/theory_uf.h | 1 + src/util/Assert.cpp | 16 + src/util/Assert.h | 53 ++- src/util/exception.h | 2 +- src/util/options.h | 5 - test/unit/Makefile.am | 1 + test/unit/context/cdlist_black.h | 72 ++++ test/unit/context/context_black.h | 45 +- test/unit/expr/node_black.h | 10 +- test/unit/expr/node_builder_black.h | 60 ++- test/unit/expr/node_white.h | 183 ++++++-- test/unit/theory/theory_black.h | 29 +- test/unit/theory/theory_uf_white.h | 92 ++-- 50 files changed, 2147 insertions(+), 1018 deletions(-) delete mode 100644 DESIGN_QUESTIONS create mode 100755 contrib/code-checker create mode 100644 contrib/indent-settings create mode 100644 src/context/cdlist.h create mode 100644 src/context/cdmap.h create mode 100644 src/context/cdo.h create mode 100644 src/context/cdset.h delete mode 100644 src/prop/cnf_conversion.h create mode 100644 test/unit/context/cdlist_black.h diff --git a/COPYING b/COPYING index 551f7fa37..3161a4784 100644 --- a/COPYING +++ b/COPYING @@ -1,13 +1,24 @@ -CVC4 is copyright (C) 2009 the ACSys research group at the Courant +CVC4 is copyright (C) 2009, 2010 the ACSys research group at the Courant Institute for Mathematical Sciences, New York University. All rights reserved. This is a prerelease version; distribution is restricted. --- Morgan Deters Mon, 02 Nov 2009 17:54:27 -0500 +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY +EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED +WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE +DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY +DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES +(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; +LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON +ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +-- Morgan Deters Thu, 04 Mar 2010 20:46:40 -0500 CVC4 incorporates MiniSat code, excluded from the above copyright. -See src/sat/minisat. +See src/sat/minisat. Its copyright: MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson @@ -30,3 +41,43 @@ See src/sat/minisat. OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +CVC4 incorporates the script "autogen.sh", excluded from the above copyright. +See autogen.sh. Its copyright: + + Copyright (c) 2005-2009 United States Government as represented by + the U.S. Army Research Laboratory. + + Redistribution and use in source and binary forms, with or without + modification, are permitted provided that the following conditions + are met: + + 1. Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + 2. Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + 3. The name of the author may not be used to endorse or promote + products derived from this software without specific prior written + permission. + + THIS SOFTWARE IS PROVIDED BY THE AUTHOR ``AS IS'' AND ANY EXPRESS + OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED + WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY + DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL + DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE + GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, + WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING + NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS + SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. + +CVC4 incorporates the script "doxygen.am", excluded from the above copyright. +See config/doxygen.am. Its copyright: + + Copyright (C) 2004 Oren Ben-Kiki + This file is distributed under the same terms as the Automake macro files. + diff --git a/DESIGN_QUESTIONS b/DESIGN_QUESTIONS deleted file mode 100644 index 0e8f50245..000000000 --- a/DESIGN_QUESTIONS +++ /dev/null @@ -1,82 +0,0 @@ -vc.h - -/* TODO provide way of querying whether you fall into a fragment / - * returning what fragment you're in */ - -decision_engine.h - - // TODO: design decision: decision engine should be notified of - // propagated lits, and also why(?) (so that it can make decisions - // based on the utility of various theories and various theory - // literals). How? Maybe TheoryEngine has a backdoor into - // DecisionEngine "behind the back" of the PropEngine? - -result.h - -// TODO: perhaps best to templatize Result on its Kind (SAT/Validity), -// but this requires doing the same for Prover and needs discussion. - -// TODO: subclass to provide models, etc. This is really just -// intended as a three-valued response code. - -expr_builder.h - - // TODO: store some flags here and install into attribute map when - // the expr is created? (we'd have to do that since we don't know - // it's hash code yet) - -expr_builder.h - - /* 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); } - -prover.h - -// TODO: SAT layer (esp. CNF- versus non-clausal solvers under the -// hood): use a type parameter and have check() delegate, or subclass -// Prover and override check()? -// -// Probably better than that is to have a configuration object that -// indicates which passes are desired. The configuration occurs -// elsewhere (and can even occur at runtime). A simple "pass manager" -// of sorts determines check()'s behavior. -// -// The CNF conversion can go on in PropEngine. - -prover.h - - /** (preprocessing) - * Pre-process an Expr. 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 - * preprocessing (certain contexts need more/less ?). - */ - -theory.h - - // TODO: these use the current EM (but must be renamed) - - // TODO design decision: instead of returning a set of literals - // here, perhaps we have an interface back into the prop engine - // where we assert directly. we might sometimes unknowingly assert - // something clearly inconsistent (esp. in a parallel context). - // This would allow the PropEngine to cancel our further work since - // we're already inconsistent---also could strategize dynamically on - // whether enough theory prop work has occurred. - virtual void propagate(Effort level = FULL_EFFORT) = 0; - - could provide a continuation (essentially) to propagate literals. - argument Propagator prop - class Propagator { - PropEngine d_pe; - public: - // may not return due to a longjmp (?) or perhaps an exception - // returns next continuation - Propagator operator()(Literal l); - }; - - -========================== -TODO: add throw() specifications diff --git a/config/cvc4.m4 b/config/cvc4.m4 index 1cde462b5..8106f1383 100644 --- a/config/cvc4.m4 +++ b/config/cvc4.m4 @@ -18,10 +18,25 @@ for ac_option do case $ac_option in -*|*=*) ;; - production|debug|default|competition) - ac_cvc4_build_profile_set=yes - AC_MSG_NOTICE([CVC4: building profile $ac_option]) - ac_option="--with-build=$ac_option" ;; + production|production-*|debug|debug-*|default|default-*|competition|competition-*) + ac_option_build=`expr "$ac_option" : '\([[^-]]*\)-\?'` + ac_cvc4_build_profile_set=yes + AC_MSG_NOTICE([CVC4: building profile $ac_option_build]) + for x in optimized assertions tracing muzzle coverage profiling; do + if expr "$ac_option" : '.*-no'$x'-\|.*-no'$x'$' >/dev/null; then + eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-$x\""' + fi + if expr "$ac_option" : '.*-'$x'-\|.*-'$x'$' >/dev/null; then + eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-$x\""' + fi + done + if expr "$ac_option" : '.*-nodebugsymbols-\|.*-nodebugsymbols$' >/dev/null; then + eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--disable-debug-symbols\""' + fi + if expr "$ac_option" : '.*-debugsymbols-\|.*-debugsymbols$' >/dev/null; then + eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"--enable-debug-symbols\""' + fi + ac_option="--with-build=$ac_option_build" esac eval 'ac_cvc4_rewritten_args="${ac_cvc4_rewritten_args+$ac_cvc4_rewritten_args }\"$ac_option\""' done diff --git a/configure.ac b/configure.ac index d75ce6309..0e08a0752 100644 --- a/configure.ac +++ b/configure.ac @@ -166,7 +166,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi ;; - debug) # Unoptimized, debug symbols, assertions, tracing + debug) # unoptimized, debug symbols, assertions, tracing CVC4CPPFLAGS=-DCVC4_DEBUG CVC4CXXFLAGS='-O0 -fno-inline -ggdb3' CVC4LDFLAGS= @@ -299,6 +299,7 @@ fi AC_MSG_RESULT([$enable_coverage]) if test "$enable_coverage" = yes; then + CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE" CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage" CVC4LDFLAGS="$CVC4LDFLAGS --coverage" fi @@ -316,6 +317,7 @@ fi AC_MSG_RESULT([$enable_profiling]) if test "$enable_profiling" = yes; then + CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING" CVC4CXXFLAGS="$CVC4CXXFLAGS -pg" CVC4LDFLAGS="$CVC4LDFLAGS -pg" fi diff --git a/contrib/code-checker b/contrib/code-checker new file mode 100755 index 000000000..a40dc61af --- /dev/null +++ b/contrib/code-checker @@ -0,0 +1,96 @@ +#!/usr/bin/perl -w + +use strict; + +while($#ARGV >= 0) { + my %FP; + my $file = shift @ARGV; + + local $/ = undef; + + open(FP, $file) || die "can't read $file"; + print "checking $file...\n"; + binmode FP; + my $buf = ; + close FP; + + print "file named incorrectly; use *.h: $file\n" if $file =~ /\.(hpp|H|hh)$/; + print "file named incorrectly; use *.cpp: $file\n" if $file =~ /\.(C|cc)$/; + if($file =~ /\.(h|hpp|H)$/) { + check_as_header($buf); + } elsif($file =~ /\.(h|cpp|C)$/) { + check_as_source($buf); + } else { + die "$file not checked (unknown type of file)"; + } + open(FP, "cpp -nostdinc \"$file\" 2>/dev/null |") || die "can't cpp $file"; + binmode FP; + $buf = ; + close FP; + + if($file =~ /\.(h|hpp|H)$/) { + check_as_header_cpp($buf); + } elsif($file =~ /\.(h|cpp|C)$/) { + check_as_source_cpp($buf); + } else { + die "$file not checked (unknown type of file)"; + } +} + +sub check_as_any { + my($buf) = @_; + + print "no file head comment\n" unless $buf =~ m,^/*\*\*\*,; +} + +sub check_as_header { + my($buf) = @_; + check_as_any($buf); +} + +sub check_as_source { + my($buf) = @_; + check_as_any($buf); +} + +sub check_as_any_cpp { + my($buf) = @_; + + print "need space between tokens ) and {\n" if $buf =~ /\)\{/; + print "need space between tokens 'const' and {\n" if $buf =~ /\bconst\{/; + print "need space between tokens ) and 'const'\n" if $buf =~ /\)const\b/; + print "need space between tokens 'template' and <\n" if $buf =~ /\btemplate +class CDList : public ContextObj { + /** + * d_list is a dynamic array of objects of type T. + */ + T* d_list; + + /** + * Whether to call the destructor when items are popped from the + * list. True by default, but can be set to false by setting the + * second argument in the constructor to false. + */ + bool d_callDestructor; + + /** + * Number of objects in d_list + */ + unsigned d_size; + + /** + * Allocated size of d_list. + */ + unsigned d_sizeAlloc; + + /** + * Implementation of mandatory ContextObj method save: simply copies the + * current size to a copy using the copy constructor (the pointer and the + * allocated size are *not* copied as they are not restored on a pop). + * The saved information is allocated using the ContextMemoryManager. + */ + ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDList(*this); + } + + /** + * Implementation of mandatory ContextObj method restore: simply restores the + * previous size. Note that the list pointer and the allocated size are not + * changed. + */ + void restore(ContextObj* data) { + if(d_callDestructor) { + unsigned size = ((CDList*)data)->d_size; + while(d_size != size) { + --d_size; + d_list[d_size].~T(); + } + } else { + d_size = ((CDList*)data)->d_size; + } + } + + /** + * Privae copy constructor used only by save above. d_list and d_sizeAlloc + * are not copied: only the base class information and d_size are needed in + * restore. + */ + CDList(const CDList& l) : + ContextObj(l), + d_list(NULL), + d_size(l.d_size), + d_sizeAlloc(0) { + } + + /** + * Reallocate the array with more space. + * Throws bad_alloc if memory allocation fails. + */ + void grow() { + if(d_list == NULL) { + // Allocate an initial list if one does not yet exist + d_sizeAlloc = 10; + d_list = (T*) malloc(sizeof(T) * d_sizeAlloc); + if(d_list == NULL) { + throw std::bad_alloc(); + } + } else { + // Allocate a new array with double the size + d_sizeAlloc *= 2; + T* tmpList = (T*) realloc(d_list, sizeof(T) * d_sizeAlloc); + if(tmpList == NULL) { + throw std::bad_alloc(); + } + d_list = tmpList; + } + } + +public: + /** + * Main constructor: d_list starts as NULL, size is 0 + */ + CDList(Context* context, bool callDestructor = true) + : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), + d_size(0), d_sizeAlloc(0) { } + + /** + * Destructor: delete the list + */ + ~CDList() throw() { + if(d_list != NULL) { + if(d_callDestructor) { + while(d_size != 0) { + --d_size; + d_list[d_size].~T(); + } + } + free(d_list); + } + } + + /** + * Return the current size of (i.e. valid number of objects in) the list + */ + unsigned size() const { return d_size; } + + + /** + * Return true iff there are no valid objects in the list. + */ + bool empty() const { return d_size == 0; } + + /** + * Add an item to the end of the list. + */ + void push_back(const T& data) { + makeCurrent(); + if(d_size == d_sizeAlloc) grow(); + ::new((void*)(d_list + d_size)) T(data); + ++ d_size; + } + + /** + * operator[]: return the ith item in the list + */ + const T& operator[](unsigned i) const { + Assert(i < d_size, "index out of bounds in CDList::operator[]"); + return d_list[i]; + } + + /** + * return the most recent item added to the list + */ + const T& back() const { + Assert(d_size > 0, "CDList::back() called on empty list"); + return d_list[d_size-1]; + } + + /** + * Iterator for CDList class. It has to be const because we don't allow + * items in the list to be changed. It's a straightforward wrapper around a + * pointer. Note that for efficiency, we implement only prefix increment and + * decrement. Also note that it's OK to create an iterator from an empty, + * uninitialized list, as begin() and end() will have the same value (NULL). + */ + class const_iterator { + friend class CDList; + T* d_it; + const_iterator(T* it) : d_it(it) {}; + public: + const_iterator() : d_it(NULL) {} + bool operator==(const const_iterator& i) const { return d_it == i.d_it; } + bool operator!=(const const_iterator& i) const { return d_it != i.d_it; } + const T& operator*() const { return *d_it; } + /** Prefix increment */ + const_iterator& operator++() { ++d_it; return *this; } + /** Prefix decrement */ + const_iterator& operator--() { --d_it; return *this; } + }; /* class const_iterator */ + + /** + * Returns an iterator pointing to the first item in the list. + */ + const_iterator begin() const { + return const_iterator(d_list); + } + + /** + * Returns an iterator pointing one past the last item in the list. + */ + const_iterator end() const { + return const_iterator(d_list + d_size); + } + +};/* class CDList */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDLIST_H */ diff --git a/src/context/cdmap.h b/src/context/cdmap.h new file mode 100644 index 000000000..994ff76b4 --- /dev/null +++ b/src/context/cdmap.h @@ -0,0 +1,407 @@ +/********************* */ +/** cdmap.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Context-dependent map class. Generic templated class for a map + ** which must be saved and restored as contexts are pushed and + ** popped. Requires that operator= be defined for the data class, + ** and operator== for the key class. For key types that don't have a + ** __gnu_cxx::hash<>, you should provide an explicit HashFcn. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDMAP_H +#define __CVC4__CONTEXT__CDMAP_H + +#include "context/context.h" +#include "util/Assert.h" + +#include +#include + +namespace CVC4 { +namespace context { + +// Auxiliary class: almost the same as CDO (see cdo.h), but on +// setNull() call it erases itself from the map. + +template > class CDMap; + +template > +class CDOmap : public ContextObj { + Key d_key; + Data d_data; + bool d_inMap; // whether the data must be in the map + CDMap* d_cdmap; + + // Doubly-linked list for keeping track of elements in order of insertion + CDOmap* d_prev; + CDOmap* d_next; + + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDOmap(*this); + } + + virtual void restore(ContextObj* data) { + CDOmap* p((CDOmap*) data); + if(p->d_inMap) { + d_data = p->d_data; + d_inMap = true; + } else { + // Erase itself from the map and put itself into trash. We cannot + // "delete this" here, because it will break context operations in + // a non-trivial way. + if(d_cdmap->d_map.count(d_key) > 0) { + d_cdmap->d_map.erase(d_key); + d_cdmap->d_trash.push_back(this); + } + + d_prev->d_next = d_next; + d_next->d_prev = d_prev; + + if(d_cdmap->d_first == this) { + d_cdmap->d_first = d_next; + + if(d_next == this) { + d_cdmap->d_first = NULL; + } + } + } + } + +public: + + CDOmap(Context* context, + CDMap* cdmap, + const Key& key, + const Data& data) : + ContextObj(context), + d_key(key), + d_inMap(false), + d_cdmap(cdmap) { + + set(data); + + CDOmap*& first = d_cdmap->d_first; + if(first == NULL) { + first = d_next = d_prev = this; + } else { + d_prev = first->d_prev; + d_next = first; + d_prev->d_next = first->d_prev = this; + } + } + + ~CDOmap() throw(AssertionException) {} + + void set(const Data& data) { + makeCurrent(); + d_data = data; + d_inMap = true; + } + + const Key& getKey() const { + return d_key; + } + + const Data& get() const { + return d_data; + } + + operator Data() { + return get(); + } + + CDOmap& operator=(const Data& data) { + set(data); + return *this; + } + + CDOmap* next() const { + if(d_next == d_cdmap->d_first) { + return NULL; + } else { + return d_next; + } + } +};/* class CDOmap */ + +// Dummy subclass of ContextObj to serve as our data class +class CDMapData : public ContextObj { + // befriend CDMap<> so that it can allocate us + template + friend class CDMap; + + ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDMapData(*this); + } + + void restore(ContextObj* data) {} + +public: + + CDMapData(Context* context) : ContextObj(context) {} + CDMapData(const ContextObj& co) : ContextObj(co) {} +}; + +/** + * Generic templated class for a map which must be saved and restored + * as contexts are pushed and popped. Requires that operator= be + * defined for the data class, and operator== for the key class. + */ +template +class CDMap : public ContextObj { + + friend class CDOmap; + + __gnu_cxx::hash_map*, HashFcn> d_map; + + // The vector of CDOmap objects to be destroyed + std::vector*> d_trash; + CDOmap* d_first; + Context* d_context; + + // Nothing to save; the elements take care of themselves + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDMapData(*this); + } + + // Similarly, nothing to restore + virtual void restore(ContextObj* data) {} + + // Destroy stale CDOmap objects from trash + void emptyTrash() { + for(typename std::vector*>::iterator + i = d_trash.begin(), iend = d_trash.end(); i != iend; ++i) { + /* + delete *i; + free(*i); + */ + } + d_trash.clear(); + } + +public: + + CDMap(Context* context) : + ContextObj(context), + d_first(NULL), + d_context(context) { + } + + ~CDMap() throw(AssertionException) { + // Delete all the elements and clear the map + for(typename __gnu_cxx::hash_map*, HashFcn>::iterator + i = d_map.begin(), iend = d_map.end(); i != iend; ++i) { + /* + delete (*i).second; + free((*i).second); + */ + } + d_map.clear(); + emptyTrash(); + } + + // The usual operators of map + + size_t size() const { + return d_map.size(); + } + + size_t count(const Key& k) const { + return d_map.count(k); + } + + typedef CDOmap& ElementReference; + + // If a key is not present, a new object is created and inserted + CDOmap& operator[](const Key& k) { + emptyTrash(); + + typename __gnu_cxx::hash_map*, HashFcn>::iterator + i(d_map.find(k)); + + CDOmap* obj; + if(i == d_map.end()) { // Create new object + obj = new(true) CDOmap(d_context, this, k, Data()); + d_map[k] = obj; + } else { + obj = (*i).second; + } + return *obj; + } + + void insert(const Key& k, const Data& d) { + emptyTrash(); + + typename __gnu_cxx::hash_map*, HashFcn>::iterator + i(d_map.find(k)); + + if(i == d_map.end()) { // Create new object + CDOmap* + obj(new(true) CDOmap(d_context, this, k, d)); + d_map[k] = obj; + } else { + (*i).second->set(d); + } + } + // FIXME: no erase(), too much hassle to implement efficiently... + + // Iterator for CDMap: points to pair&>; + // in most cases, this will be functionally similar to pair. + class iterator : public std::iterator, std::ptrdiff_t> { + + // Private members + typename __gnu_cxx::hash_map*, HashFcn>::const_iterator d_it; + + public: + + // Constructor from __gnu_cxx::hash_map + iterator(const typename __gnu_cxx::hash_map*, HashFcn>::const_iterator& i) : d_it(i) {} + + // Copy constructor + iterator(const iterator& i) : d_it(i.d_it) {} + + // Default constructor + iterator() {} + + // (Dis)equality + bool operator==(const iterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const iterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair operator*() const { + const std::pair*>& p(*d_it); + return std::pair(p.first, *p.second); + } + + // Who needs an operator->() for maps anyway?... + // It'd be nice, but not possible by design. + //std::pair* operator->() const { + // return &(operator*()); + //} + + // Prefix and postfix increment + iterator& operator++() { + ++d_it; + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const std::pair* d_pair; + public: + Proxy(const std::pair& p): d_pair(&p) {} + std::pair& operator*() { + return *d_pair; + } + };/* class CDMap<>::iterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the iterator. However, don't try to use Proxy for + // anything else. + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::iterator */ + + typedef iterator const_iterator; + + iterator begin() const { + return iterator(d_map.begin()); + } + + iterator end() const { + return iterator(d_map.end()); + } + + class orderedIterator { + const CDOmap* d_it; + + public: + + orderedIterator(const CDOmap* p) : d_it(p) {} + orderedIterator(const orderedIterator& i) : d_it(i.d_it) {} + + // Default constructor + orderedIterator() {} + + // (Dis)equality + bool operator==(const orderedIterator& i) const { + return d_it == i.d_it; + } + bool operator!=(const orderedIterator& i) const { + return d_it != i.d_it; + } + + // Dereference operators. + std::pair operator*() const { + return std::pair(d_it->getKey(), d_it->get()); + } + + // Prefix and postfix increment + orderedIterator& operator++() { + d_it = d_it->next(); + return *this; + } + + // Postfix increment: requires a Proxy object to hold the + // intermediate value for dereferencing + class Proxy { + const std::pair* d_pair; + + public: + + Proxy(const std::pair& p): d_pair(&p) {} + + std::pair& operator*() { + return *d_pair; + } + };/* class CDMap<>::orderedIterator::Proxy */ + + // Actual postfix increment: returns Proxy with the old value. + // Now, an expression like *i++ will return the current *i, and + // then advance the orderedIterator. However, don't try to use + // Proxy for anything else. + Proxy operator++(int) { + Proxy e(*(*this)); + ++(*this); + return e; + } + };/* class CDMap<>::orderedIterator */ + + orderedIterator orderedBegin() const { + return orderedIterator(d_first); + } + + orderedIterator orderedEnd() const { + return orderedIterator(NULL); + } + + iterator find(const Key& k) const { + return iterator(d_map.find(k)); + } + +};/* class CDMap<> */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDMAP_H */ diff --git a/src/context/cdo.h b/src/context/cdo.h new file mode 100644 index 000000000..6c30a70f4 --- /dev/null +++ b/src/context/cdo.h @@ -0,0 +1,122 @@ +/********************* */ +/** cdo.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** A context-dependent object. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDO_H +#define __CVC4__CONTEXT__CDO_H + +#include "context/context.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +/** + * Most basic template for context-dependent objects. Simply makes a copy + * (using the copy constructor) of class T when saving, and copies it back + * (using operator=) during restore. + */ +template +class CDO : public ContextObj { + + /** + * The data of type T being stored in this context-dependent object. + */ + T d_data; + + /** + * Implementation of mandatory ContextObj method save: simply copies the + * current data to a copy using the copy constructor. Memory is allocated + * using the ContextMemoryManager. + */ + virtual ContextObj* save(ContextMemoryManager* pCMM) { + return new(pCMM) CDO(*this); + } + + /** + * Implementation of mandatory ContextObj method restore: simply copies the + * saved data back from the saved copy using operator= for T. + */ + virtual void restore(ContextObj* pContextObj) { + d_data = ((CDO*) pContextObj)->d_data; + } + + /** + * Copy constructor - it's private to ensure it is only used by save(). + * Basic CDO objects, cannot be copied-they have to be unique. + */ + CDO(const CDO& cdo) : ContextObj(cdo), d_data(cdo.d_data) {} + + /** + * operator= for CDO is private to ensure CDO object is not copied. + */ + CDO& operator=(const CDO& cdo) {} + +public: + /** + * Main constructor - uses default constructor for T to create the initial + * value of d_data. + */ + CDO(Context* context) : ContextObj(context) {} + + /** + * Constructor from object of type T. Creates a ContextObj and sets the data + * to the given data value. Note that this value is only valid in the + * current Scope. If the Scope is popped, the value will revert to whatever + * is assigned by the default constructor for T + */ + CDO(Context* context, const T& data) : ContextObj(context) { + makeCurrent(); + d_data = data; + } + + /** + * Destructor - no need to do anything. + */ + ~CDO() throw() {} + + /** + * Set the data in the CDO. First call makeCurrent. + */ + void set(const T& data) { + makeCurrent(); + d_data = data; + } + + /** + * Get the current data from the CDO. Read-only. + */ + const T& get() const { return d_data; } + + /** + * For convenience, define operator T to be the same as get(). + */ + operator T() { return get(); } + + /** + * For convenience, define operator= that takes an object of type T. + */ + CDO& operator=(const T& data) { + set(data); + return *this; + } + +};/* class CDO */ + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDO_H */ diff --git a/src/context/cdset.h b/src/context/cdset.h new file mode 100644 index 000000000..48ad12daa --- /dev/null +++ b/src/context/cdset.h @@ -0,0 +1,33 @@ +/********************* */ +/** cdset.h + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Context-dependent set class. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__CONTEXT__CDSET_H +#define __CVC4__CONTEXT__CDSET_H + +#include "context/context.h" +#include "util/Assert.h" + +namespace CVC4 { +namespace context { + +template +class CDSet; + +}/* CVC4::context namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__CONTEXT__CDSET_H */ diff --git a/src/context/context.cpp b/src/context/context.cpp index 5ff377194..8e87741b5 100644 --- a/src/context/context.cpp +++ b/src/context/context.cpp @@ -29,7 +29,7 @@ Context::Context() : d_pCNOpre(NULL), d_pCNOpost(NULL) { } -Context::~Context() { +Context::~Context() throw(AssertionException) { // Delete all Scopes popto(0); @@ -38,13 +38,13 @@ Context::~Context() { // Clear ContextNotifyObj lists so there are no dangling pointers ContextNotifyObj* pCNO; - while (d_pCNOpre != NULL) { + while(d_pCNOpre != NULL) { pCNO = d_pCNOpre; pCNO->d_ppCNOprev = NULL; d_pCNOpre = pCNO->d_pCNOnext; pCNO->d_pCNOnext = NULL; } - while (d_pCNOpost != NULL) { + while(d_pCNOpost != NULL) { pCNO = d_pCNOpost; pCNO->d_ppCNOprev = NULL; d_pCNOpost = pCNO->d_pCNOnext; @@ -69,7 +69,7 @@ void Context::pop() { // Notify the (pre-pop) ContextNotifyObj objects ContextNotifyObj* pCNO = d_pCNOpre; - while (pCNO != NULL) { + while(pCNO != NULL) { pCNO->notify(); pCNO = pCNO->d_pCNOnext; } @@ -88,7 +88,7 @@ void Context::pop() { // Notify the (post-pop) ContextNotifyObj objects pCNO = d_pCNOpost; - while (pCNO != NULL) { + while(pCNO != NULL) { pCNO->notify(); pCNO = pCNO->d_pCNOnext; } @@ -99,8 +99,8 @@ void Context::pop() { void Context::popto(int toLevel) { // Pop scopes until there are none left or toLevel is reached - if (toLevel < 0) toLevel = 0; - while (toLevel < getLevel()) pop(); + if(toLevel < 0) toLevel = 0; + while(toLevel < getLevel()) pop(); } @@ -147,19 +147,17 @@ void ContextObj::update() { } -ContextObj* ContextObj::restoreAndContinue() -{ +ContextObj* ContextObj::restoreAndContinue() { // Variable to hold next object in list ContextObj* pContextObjNext; // Check the restore pointer. If NULL, this must be the bottom Scope - if (d_pContextObjRestore == NULL) { + if(d_pContextObjRestore == NULL) { Assert(d_pScope == d_pScope->getContext()->getBottomScope(), "Expected bottom scope"); pContextObjNext = d_pContextObjNext; // Nothing else to do - } - else { + } else { // Call restore to update the subclass data restore(d_pContextObjRestore); @@ -177,48 +175,48 @@ ContextObj* ContextObj::restoreAndContinue() } -ContextObj::ContextObj(Context* pContext) - : d_pContextObjRestore(NULL) -{ +ContextObj::ContextObj(Context* pContext) : + d_pContextObjRestore(NULL) { + Assert(pContext != NULL, "NULL context pointer"); + d_pScope = pContext->getBottomScope(); d_pScope->addToChain(this); } -ContextObj::~ContextObj() -{ +ContextObj::~ContextObj() throw(AssertionException) { for(;;) { - if (next() != NULL) { + if(next() != NULL) { next()->prev() = prev(); } *(prev()) = next(); - if (d_pContextObjRestore == NULL) break; + if(d_pContextObjRestore == NULL) { + break; + } restoreAndContinue(); } } ContextNotifyObj::ContextNotifyObj(Context* pContext, bool preNotify) { - if (preNotify) { + if(preNotify) { pContext->addNotifyObjPre(this); - } - else { + } else { pContext->addNotifyObjPost(this); } } -ContextNotifyObj::~ContextNotifyObj() -{ - if (d_pCNOnext != NULL) { + +ContextNotifyObj::~ContextNotifyObj() throw(AssertionException) { + if(d_pCNOnext != NULL) { d_pCNOnext->d_ppCNOprev = d_ppCNOprev; } - if (d_ppCNOprev != NULL) { + if(d_ppCNOprev != NULL) { *(d_ppCNOprev) = d_pCNOnext; } } -} /* CVC4::context namespace */ - +} /* CVC4::context namespace */ } /* CVC4 namespace */ diff --git a/src/context/context.h b/src/context/context.h index 6a35945b7..4e10347d7 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -20,6 +20,7 @@ #include "context/context_mm.h" #include "util/Assert.h" + #include #include #include @@ -32,28 +33,27 @@ class Scope; class ContextObj; class ContextNotifyObj; - /** - * A Context encapsulates all of the dynamic state of the system. Its main - * methods are push() and pop(). A call to push() saves the current state, - * and a call to pop() restores the state saved by the most recent call to - * push(). - * - * Objects which want to participate in this global save and restore - * mechanism must inherit from ContextObj (see below). - * - * For more flexible context-dependent behavior, objects may implement the - * ContextNotifyObj interface and simply get a notification when a pop has - * occurred. - * - * Context also uses a helper class called Scope which stores information - * specific to the portion of the Context since the last call to push() (see - * below). - * - * Memory allocation in Contexts is done with the help of the - * ContextMemoryManager. A copy is stored in each Scope object for quick - * access. - * - */ +/** + * A Context encapsulates all of the dynamic state of the system. Its main + * methods are push() and pop(). A call to push() saves the current state, + * and a call to pop() restores the state saved by the most recent call to + * push(). + * + * Objects which want to participate in this global save and restore + * mechanism must inherit from ContextObj (see below). + * + * For more flexible context-dependent behavior, objects may implement the + * ContextNotifyObj interface and simply get a notification when a pop has + * occurred. + * + * Context also uses a helper class called Scope which stores information + * specific to the portion of the Context since the last call to push() (see + * below). + * + * Memory allocation in Contexts is done with the help of the + * ContextMemoryManager. A copy is stored in each Scope object for quick + * access. + */ class Context { /** @@ -87,7 +87,7 @@ public: /** * Destructor: pop all scopes, delete ContextMemoryManager */ - ~Context(); + ~Context() throw(AssertionException); /** * Return the current (top) scope @@ -107,7 +107,7 @@ public: /** * Return the ContextMemoryManager associated with the context. */ - ContextMemoryManager* getCMM(){ return d_pCMM; } + ContextMemoryManager* getCMM() { return d_pCMM; } /** * Save the current state, create a new Scope @@ -182,15 +182,18 @@ public: * Constructor: Create a new Scope; set the level and the previous Scope * if any. */ - Scope(Context* pContext, ContextMemoryManager* pCMM, int level) - : d_pContext(pContext), d_pCMM(pCMM), d_level(level), - d_pContextObjList(NULL) { } + Scope(Context* pContext, ContextMemoryManager* pCMM, int level) : + d_pContext(pContext), + d_pCMM(pCMM), + d_level(level), + d_pContextObjList(NULL) { + } /** * Destructor: Restore all of the objects in ContextObjList. Defined inline * below. */ - ~Scope(); + ~Scope() throw(); /** * Get the Context for this Scope @@ -223,8 +226,9 @@ public: * Overload operator new for use with ContextMemoryManager to allow creation * of new Scope objects in the current memory region. */ - static void* operator new(size_t size, ContextMemoryManager* pCMM) - { return pCMM->newData(size); } + static void* operator new(size_t size, ContextMemoryManager* pCMM) { + return pCMM->newData(size); + } /** * Overload operator delete for Scope objects allocated using @@ -232,44 +236,44 @@ public: * automatically when the ContextMemoryManager pop() method is called. * Include both placement and standard delete for completeness. */ - static void operator delete(void* pMem, ContextMemoryManager* pCMM) { } - static void operator delete(void* pMem) { } + static void operator delete(void* pMem, ContextMemoryManager* pCMM) {} + static void operator delete(void* pMem) {} //FIXME: //! Check for memory leaks // void check(void); -}; /* class Scope */ - - /** - * This is an abstract base class from which all objects that are context-dependent - * should inherit. For any data structure that you want to have be - * automatically backtracked, do the following: - * 1. Create a class for the data structure that inherits from ContextObj - * 2. Implement save() - * The role of save() is to create a new ContexObj object that contains - * enough information to restore the object to its current state, even if - * it gets changed later. Note that save should call the (default) - * ContextObj Copy Constructor to copy the information in the base class. - * It is recommended that any memory allocated by save() should be done - * through the ContextMemoryManager. This way, it does not need to be - * explicitly freed when restore is called. However, it is only required - * that the ContextObj itself be allocated using the - * ContextMemoryManager. If other memory is allocated not using the - * ContextMemoryManager, it should be freed when restore() is called. In - * fact, any clean-up work on a saved object must be done by restore(). - * This is because the destructor is never called explicitly on saved - * objects. - * 3. Implement restore() - * The role of restore() is, given the ContextObj returned by a previous - * call to save(), to restore the current object to the state it was in - * when save() was called. Note that the implementation of restore does - * *not* need to worry about restoring the base class data. This is done - * automatically. Ideally, restore() should not have to free any memory - * as any memory allocated by save() should have been done using the - * ContextMemoryManager (see item 2 above). - * 4. In the subclass implementation, any time the state is about to be - * changed, first call makeCurrent(). - */ +};/* class Scope */ + +/** + * This is an abstract base class from which all objects that are context-dependent + * should inherit. For any data structure that you want to have be + * automatically backtracked, do the following: + * 1. Create a class for the data structure that inherits from ContextObj + * 2. Implement save() + * The role of save() is to create a new ContexObj object that contains + * enough information to restore the object to its current state, even if + * it gets changed later. Note that save should call the (default) + * ContextObj Copy Constructor to copy the information in the base class. + * It is recommended that any memory allocated by save() should be done + * through the ContextMemoryManager. This way, it does not need to be + * explicitly freed when restore is called. However, it is only required + * that the ContextObj itself be allocated using the + * ContextMemoryManager. If other memory is allocated not using the + * ContextMemoryManager, it should be freed when restore() is called. In + * fact, any clean-up work on a saved object must be done by restore(). + * This is because the destructor is never called explicitly on saved + * objects. + * 3. Implement restore() + * The role of restore() is, given the ContextObj returned by a previous + * call to save(), to restore the current object to the state it was in + * when save() was called. Note that the implementation of restore does + * *not* need to worry about restoring the base class data. This is done + * automatically. Ideally, restore() should not have to free any memory + * as any memory allocated by save() should have been done using the + * ContextMemoryManager (see item 2 above). + * 4. In the subclass implementation, any time the state is about to be + * changed, first call makeCurrent(). + */ class ContextObj { /** * Pointer to Scope in which this object was last modified. @@ -325,6 +329,7 @@ class ContextObj { ContextObj* restoreAndContinue(); protected: + /** * This is a method that must be implemented by all classes inheriting from * ContextObj. See the comment before the class declaration. @@ -341,57 +346,70 @@ protected: * This method checks if the object has been modified in this Scope yet. If * not, it calls update(). */ - void makeCurrent() { if (!(d_pScope->isCurrent())) update(); } + void makeCurrent() { + if(!(d_pScope->isCurrent())) { + update(); + } + } /** - * operator new using ContextMemoryManager (common case used by subclasses - * during save() ). No delete is required for memory allocated this way, - * since it is automatically released when the context is popped. Also note - * that allocations using this operator never have their destructor called, - * so any clean-up has to be done using the restore method. + * operator new using ContextMemoryManager (common case used by + * subclasses during save() ). No delete is required for memory + * allocated this way, since it is automatically released when the + * context is popped. Also note that allocations using this + * operator never have their destructor called, so any clean-up has + * to be done using the restore method. */ static void* operator new(size_t size, ContextMemoryManager* pCMM) { return pCMM->newData(size); } /** - * Corresponding placement delete. Note that this is provided just to - * satisfy the requirement that a placement delete should be provided for - * every placement new. It would only be called if a ContextObj Constructor - * throws an exception after a successful call to the above new operator. + * Corresponding placement delete. Note that this is provided just + * to satisfy the requirement that a placement delete should be + * provided for every placement new. It would only be called if a + * ContextObj constructor throws an exception after a successful + * call to the above new operator. */ - static void operator delete(void* pMem, ContextMemoryManager* pCMM) { } + static void operator delete(void* pMem, ContextMemoryManager* pCMM) {} public: + /** * Create a new ContextObj. The initial scope is set to the bottom - * scope of the Context. Note that in the common case, the copy constructor - * is called to create new ContextObj objects. The default copy constructor - * does the right thing, so we do not explicitly define it. + * scope of the Context. Note that in the common case, the copy + * constructor is called to create new ContextObj objects. The + * default copy constructor does the right thing, so we do not + * explicitly define it. */ ContextObj(Context* context); /** - * Destructor: Calls restore until restored to initial version. Also removes - * object from all Scope lists. Note that this doesn't actually free the - * memory allocated by the ContextMemoryManager for this object. This isn't - * done until the corresponding Scope is popped. + * Destructor: Calls restore until restored to initial version. + * Also removes object from all Scope lists. Note that this doesn't + * actually free the memory allocated by the ContextMemoryManager + * for this object. This isn't done until the corresponding Scope + * is popped. */ - virtual ~ContextObj(); + virtual ~ContextObj() throw(AssertionException); /** - * If you want to allocate a ContextObj object on the heap, use this special - * new operator. To free this memory, instead of "delete p", use - * "p->deleteSelf()". + * If you want to allocate a ContextObj object on the heap, use this + * special new operator. To free this memory, instead of + * "delete p", use "p->deleteSelf()". */ - static void* operator new(size_t size, bool) { return ::operator new(size); } + static void* operator new(size_t size, bool) { + return ::operator new(size); + } /** - * Corresponding placement delete. Note that this is provided for the - * compiler in case the ContextObj constructor throws an exception. The - * client can't call it. + * Corresponding placement delete. Note that this is provided for + * the compiler in case the ContextObj constructor throws an + * exception. The client can't call it. */ - static void operator delete(void* pMem, bool) { ::operator delete(pMem); } + static void operator delete(void* pMem, bool) { + ::operator delete(pMem); + } /** * Use this instead of delete to delete memory allocated using the special @@ -399,7 +417,9 @@ public: * function on memory allocated using the new that takes a * ContextMemoryManager as an argument. */ - void deleteSelf() { ::operator delete(this); } + void deleteSelf() { + ::operator delete(this); + } /** * Disable delete: objects allocated with new(ContextMemorymanager) should @@ -407,23 +427,23 @@ public: * calling deleteSelf(). */ static void operator delete(void* pMem) { - AlwaysAssert(false, "Not Allowed!"); + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); } -}; /* class ContextObj */ +};/* class ContextObj */ /** - * For more flexible context-dependent behavior than that provided by - * ContextObj, objects may implement the ContextNotifyObj interface and - * simply get a notification when a pop has occurred. See Context class for - * how to register a ContextNotifyObj with the Context (you can choose to - * have notification come before or after the ContextObj objects have been - * restored). + * For more flexible context-dependent behavior than that provided + * by ContextObj, objects may implement the ContextNotifyObj + * interface and simply get a notification when a pop has occurred. + * See Context class for how to register a ContextNotifyObj with the + * Context (you can choose to have notification come before or after + * the ContextObj objects have been restored). */ class ContextNotifyObj { /** - * Context is our friend so that when the Context is deleted, any remaining - * ContextNotifyObj can be removed from the Context list. + * Context is our friend so that when the Context is deleted, any + * remaining ContextNotifyObj can be removed from the Context list. */ friend class Context; @@ -451,18 +471,19 @@ class ContextNotifyObj { public: /** - * Constructor for ContextNotifyObj. Parameters are the context to which - * this notify object will be added, and a flag which, if true, tells the - * context to notify this object *before* the ContextObj objects are - * restored. Otherwise, the context notifies the object after the ContextObj - * objects are restored. The default is for notification after. + * Constructor for ContextNotifyObj. Parameters are the context to + * which this notify object will be added, and a flag which, if + * true, tells the context to notify this object *before* the + * ContextObj objects are restored. Otherwise, the context notifies + * the object after the ContextObj objects are restored. The + * default is for notification after. */ ContextNotifyObj(Context* pContext, bool preNotify = false); /** * Destructor: removes object from list */ - virtual ~ContextNotifyObj(); + virtual ~ContextNotifyObj() throw(AssertionException); /** * This is the method called to notify the object of a pop. It must be @@ -473,11 +494,11 @@ public: // Inline functions whose definitions had to be delayed: -inline Scope::~Scope() { +inline Scope::~Scope() throw() { // Call restore() method on each ContextObj object in the list. - // Note that it is the responsibility of restore() to return the next item in - // the list. - while (d_pContextObjList != NULL) { + // Note that it is the responsibility of restore() to return the + // next item in the list. + while(d_pContextObjList != NULL) { d_pContextObjList = d_pContextObjList->restoreAndContinue(); } } @@ -490,290 +511,7 @@ inline void Scope::addToChain(ContextObj* pContextObj) { d_pContextObjList = pContextObj; } - /** - * Most basic template for context-dependent objects. Simply makes a copy - * (using the copy constructor) of class T when saving, and copies it back - * (using operator=) during restore. - */ -template -class CDO :public ContextObj { - - /** - * The data of type T being stored in this context-dependent object. - */ - T d_data; - - /** - * Implementation of mandatory ContextObj method save: simply copies the - * current data to a copy using the copy constructor. Memory is allocated - * using the ContextMemoryManager. - */ - virtual ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDO(*this); - } - - /** - * Implementation of mandatory ContextObj method restore: simply copies the - * saved data back from the saved copy using operator= for T. - */ - virtual void restore(ContextObj* pContextObj) { - d_data = ((CDO*)pContextObj)->d_data; - } - - /** - * Copy constructor - it's private to ensure it is only used by save(). - * Basic CDO objects, cannot be copied-they have to be unique. - */ - CDO(const CDO& cdo): ContextObj(cdo), d_data(cdo.d_data) { } - - /** - * operator= for CDO is private to ensure CDO object is not copied. - */ - CDO& operator=(const CDO& cdo) {} - -public: - /** - * Main constructor - uses default constructor for T to create the initial - * value of d_data. - */ - CDO(Context* context) : ContextObj(context) {} - - /** - * Constructor from object of type T. Creates a ContextObj and sets the data - * to the given data value. Note that this value is only valid in the - * current Scope. If the Scope is popped, the value will revert to whatever - * is assigned by the default constructor for T - */ - CDO(Context* context, const T& data) : ContextObj(context) { - makeCurrent(); d_data = data; - } - - /** - * Destructor - no need to do anything. - */ - ~CDO() {} - - /** - * Set the data in the CDO. First call makeCurrent. - */ - void set(const T& data) { makeCurrent(); d_data = data; } - - /** - * Get the current data from the CDO. Read-only. - */ - const T& get() const { return d_data; } - - /** - * For convenience, define operator T to be the same as get(). - */ - operator T() { return get(); } - - /** - * For convenience, define operator= that takes an object of type T. - */ - CDO& operator=(const T& data) { set(data); return *this; } - -}; /* class CDO */ - - /** - * Generic context-dependent dynamic array. Note that for efficiency, this - * implementation makes the following assumptions: - * 1. Over time, objects are only added to the list. Objects are only - * removed when a pop restores the list to a previous state. - * 2. T objects can safely be copied using their copy constructor, - * operator=, and memcpy. - */ -template -class CDList :public ContextObj { - /** - * d_list is a dynamic array of objects of type T. - */ - T* d_list; - - /** - * Whether to call the destructor when items are popped from the - * list. True by default, but can be set to false by setting the - * second argument in the constructor to false. - */ - bool d_callDestructor; - - /** - * Number of objects in d_list - */ - unsigned d_size; - - /** - * Allocated size of d_list. - */ - unsigned d_sizeAlloc; - - /** - * Implementation of mandatory ContextObj method save: simply copies the - * current size to a copy using the copy constructor (the pointer and the - * allocated size are *not* copied as they are not restored on a pop). - * The saved information is allocated using the ContextMemoryManager. - */ - ContextObj* save(ContextMemoryManager* pCMM) { - return new(pCMM) CDList(*this); - } - - /** - * Implementation of mandatory ContextObj method restore: simply restores the - * previous size. Note that the list pointer and the allocated size are not - * changed. - */ - void restore(ContextObj* data) { - if (d_callDestructor) { - unsigned size = ((CDList*)data)->d_size; - while (d_size != size) { - --d_size; - d_list[d_size].~T(); - } - } - else { - d_size = ((CDList*)data)->d_size; - } - } - - /** - * Privae copy constructor used only by save above. d_list and d_sizeAlloc - * are not copied: only the base class information and d_size are needed in - * restore. - */ - CDList(const CDList& l): ContextObj(l), d_list(NULL), - d_size(l.d_size), d_sizeAlloc(0) { } - - /** - * Reallocate the array with more space. - * Throws bad_alloc if memory allocation fails. - */ - void grow() { - if (d_list == NULL) { - // Allocate an initial list if one does not yet exist - d_sizeAlloc = 10; - d_list = (T*)malloc(sizeof(T)*d_sizeAlloc); - if(d_list == NULL){ - throw std::bad_alloc(); - } - } - else { - // Allocate a new array with double the size - d_sizeAlloc *= 2; - T* tmpList = (T*)realloc(d_list, sizeof(T)*d_sizeAlloc); - if(tmpList == NULL){ - throw std::bad_alloc(); - } - d_list = tmpList; - } - } - -public: - /** - * Main constructor: d_list starts as NULL, size is 0 - */ - CDList(Context* context, bool callDestructor = true) - : ContextObj(context), d_list(NULL), d_callDestructor(callDestructor), - d_size(0), d_sizeAlloc(0) { } - - /** - * Destructor: delete the list - */ - ~CDList() { - if(d_list != NULL) { - if (d_callDestructor) { - while (d_size != 0) { - --d_size; - d_list[d_size].~T(); - } - } - delete d_list; - } - } - - /** - * Return the current size of (i.e. valid number of objects in) the list - */ - unsigned size() const { return d_size; } - - - /** - * Return true iff there are no valid objects in the list. - */ - bool empty() const { return d_size == 0; } - - /** - * Add an item to the end of the list. - */ - void push_back(const T& data) { - makeCurrent(); - if (d_size == d_sizeAlloc) grow(); - ::new((void*)(d_list + d_size)) T(data); - ++ d_size; - } - - /** - * operator[]: return the ith item in the list - */ - const T& operator[](unsigned i) const { - Assert(i < d_size, "index out of bounds in CDList::operator[]"); - return d_list[i]; - } - - /** - * return the most recent item added to the list - */ - const T& back() const { - Assert(d_size > 0, "CDList::back() called on empty list"); - return d_list[d_size-1]; - } - - /** - * Iterator for CDList class. It has to be const because we don't allow - * items in the list to be changed. It's a straightforward wrapper around a - * pointer. Note that for efficiency, we implement only prefix increment and - * decrement. Also note that it's OK to create an iterator from an empty, - * uninitialized list, as begin() and end() will have the same value (NULL). - */ - class const_iterator { - friend class CDList; - T* d_it; - const_iterator(T* it) : d_it(it) {}; - public: - const_iterator() : d_it(NULL) {} - bool operator==(const const_iterator& i) const { return d_it == i.d_it; } - bool operator!=(const const_iterator& i) const { return d_it != i.d_it; } - const T& operator*() const { return *d_it; } - /** Prefix increment */ - const_iterator& operator++() { ++d_it; return *this; } - /** Prefix decrement */ - const_iterator& operator--() { --d_it; return *this; } - }; /* class const_iterator */ - - /** - * Returns an iterator pointing to the first item in the list. - */ - const_iterator begin() const { - return const_iterator(d_list); - } - - /** - * Returns an iterator pointing one past the last item in the list. - */ - const_iterator end() const { - return const_iterator(d_list + d_size); - } - -}; /* class CDList */ - -template -class CDMap; - -template -class CDSet; - -} /* CVC4::context namespace */ - -} /* CVC4 namespace */ +}/* CVC4::context namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__CONTEXT__CONTEXT_H */ - diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index df7d82987..ab81c7486 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -32,9 +32,9 @@ void ContextMemoryManager::newChunk() { "Index should be at the end of the list"); // Create new chunk if no free chunk available - if (d_freeChunks.empty()) { + if(d_freeChunks.empty()) { d_chunkList.push_back((char*)malloc(chunkSizeBytes)); - if (d_chunkList.back() == NULL) { + if(d_chunkList.back() == NULL) { throw std::bad_alloc(); } } @@ -53,31 +53,32 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) { // Create initial chunk d_chunkList.push_back((char*)malloc(chunkSizeBytes)); d_nextFree = d_chunkList.back(); - if (d_nextFree == NULL) { + if(d_nextFree == NULL) { throw std::bad_alloc(); } d_endChunk = d_nextFree + chunkSizeBytes; } -ContextMemoryManager::~ContextMemoryManager() { +ContextMemoryManager::~ContextMemoryManager() throw() { // Delete all chunks - while (!d_chunkList.empty()) { + while(!d_chunkList.empty()) { free(d_chunkList.back()); d_chunkList.pop_back(); } - while (!d_freeChunks.empty()) { + while(!d_freeChunks.empty()) { free(d_freeChunks.back()); d_freeChunks.pop_back(); } } + void* ContextMemoryManager::newData(size_t size) { // Use next available free location in current chunk void* res = (void*)d_nextFree; d_nextFree += size; // Check if the request is too big for the chunk - if (d_nextFree > d_endChunk) { + if(d_nextFree > d_endChunk) { newChunk(); res = (void*)d_nextFree; d_nextFree += size; @@ -104,7 +105,7 @@ void ContextMemoryManager::pop() { d_endChunkStack.pop_back(); // Free all the new chunks since the last push - while (d_indexChunkList > d_indexChunkListStack.back()) { + while(d_indexChunkList > d_indexChunkListStack.back()) { d_freeChunks.push_back(d_chunkList.back()); d_chunkList.pop_back(); --d_indexChunkList; @@ -112,7 +113,7 @@ void ContextMemoryManager::pop() { d_indexChunkListStack.pop_back(); // Delete excess free chunks - while (d_freeChunks.size() > maxFreeChunks) { + while(d_freeChunks.size() > maxFreeChunks) { free(d_freeChunks.front()); d_freeChunks.pop_front(); } @@ -120,6 +121,4 @@ void ContextMemoryManager::pop() { } /* CVC4::context namespace */ - - } /* CVC4 namespace */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index c4e5aba4f..04b0c8167 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -25,17 +25,16 @@ namespace CVC4 { namespace context { - - /** - * Region-based memory manager for contexts. Calls to newData provide memory - * from the current region. This memory will persist until the entire - * region is deallocated (by calling pop). - * - * If push is called, the current region is deactivated and pushed on a - * stack, and a new current region is created. A subsequent call to pop - * releases the new region and restores the top region from the stack. - * - */ +/** + * Region-based memory manager for contexts. Calls to newData provide memory + * from the current region. This memory will persist until the entire + * region is deallocated (by calling pop). + * + * If push is called, the current region is deactivated and pushed on a + * stack, and a new current region is created. A subsequent call to pop + * releases the new region and restores the top region from the stack. + * + */ class ContextMemoryManager { /** @@ -102,6 +101,7 @@ class ContextMemoryManager { void newChunk(); public: + /** * Constructor - creates an initial region and an empty stack */ @@ -110,7 +110,7 @@ class ContextMemoryManager { /** * Destructor - deletes all memory in all regions */ - ~ContextMemoryManager(); + ~ContextMemoryManager() throw(); /** * Allocate size bytes from the current region @@ -128,7 +128,7 @@ class ContextMemoryManager { */ void pop(); -}; /* class ContextMemoryManager */ +};/* class ContextMemoryManager */ }/* CVC4::context namespace */ }/* CVC4 namespace */ diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 522427c03..285c7ce87 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -28,7 +28,7 @@ #include #include "config.h" -#include "context/context.h" +#include "context/cdmap.h" #include "expr/node.h" #include "expr/type.h" @@ -344,6 +344,25 @@ public: } };/* class AttrHash */ +/** + * A "CDAttrHash"---the hash table underlying + * attributes---is simply a context-dependent mapping of + * pair to value_type using our specialized + * hash function for these pairs. + */ +template +class CDAttrHash : + public CVC4::context::CDMap, + value_type, + AttrHashFcn> { +public: + CDAttrHash(context::Context* ctxt) : + context::CDMap, + value_type, + AttrHashFcn>(ctxt) { + } +}; + }/* CVC4::expr::attr namespace */ // ATTRIBUTE CLEANUP FUNCTIONS ================================================= @@ -353,7 +372,7 @@ namespace attr { /** Default cleanup for unmanaged Attribute<> */ template struct AttributeCleanupFcn { - inline void cleanup(const T&) {} + static inline void cleanup(const T&) {} }; /** Default cleanup for ManagedAttribute<> */ @@ -364,13 +383,13 @@ struct ManagedAttributeCleanupFcn { /** Specialization for T* */ template struct ManagedAttributeCleanupFcn { - inline void cleanup(T* p) { delete p; } + static inline void cleanup(T* p) { delete p; } }; /** Specialization for const T* */ template struct ManagedAttributeCleanupFcn { - inline void cleanup(const T* p) { delete p; } + static inline void cleanup(const T* p) { delete p; } }; }/* CVC4::expr::attr namespace */ @@ -388,13 +407,13 @@ struct ManagedAttributeCleanupFcn { * Node goes away. Useful, e.g., for pointer-valued attributes when * the values are "owned" by the table. * - * @param context_dependent whether this attribute kind is + * @param context_dep whether this attribute kind is * context-dependent */ template , - bool context_dependent = false> + bool context_dep = false> struct Attribute { /** The value type for this attribute. */ @@ -411,6 +430,11 @@ struct Attribute { */ static const bool has_default_value = false; + /** + * Expose this setting to the users of this Attribute kind. + */ + static const bool context_dependent = context_dep; + private: /** @@ -423,8 +447,8 @@ private: /** * An "attribute type" structure for boolean flags (special). */ -template -struct Attribute { +template +struct Attribute { /** The value type for this attribute; here, bool. */ typedef bool value_type; @@ -446,6 +470,11 @@ struct Attribute { */ static const bool default_value = false; + /** + * Expose this setting to the users of this Attribute kind. + */ + static const bool context_dependent = context_dep; + /** * Check that the ID is a valid ID for bool-valued attributes. Fail * an assert if not. Otherwise return the id. @@ -463,13 +492,28 @@ private: static const uint64_t s_id; }; -// FIXME make context-dependent +/** + * This is a context-dependent attribute kind (the only difference + * between CDAttribute<> and Attribute<> (with the fourth argument + * "true") is that you cannot supply a cleanup function (a no-op one + * is used). + */ template struct CDAttribute : public Attribute, true> {}; -// FIXME make context-dependent +/** + * This is a managed attribute kind (the only difference between + * ManagedAttribute<> and Attribute<> is the default cleanup function + * and the fact that ManagedAttributes cannot be context-dependent). + * In the default ManagedAttribute cleanup function, the value is + * destroyed with the delete operator. If the value is allocated with + * the array version of new[], an alternate cleanup function should be + * provided that uses array delete[]. It is an error to create a + * ManagedAttribute<> kind with a non-pointer value_type if you don't + * also supply a custom cleanup function. + */ template > @@ -484,29 +528,29 @@ namespace attr { * This is the last-attribute-assigner. IDs are not globally * unique; rather, they are unique for each table_value_type. */ -template +template struct LastAttributeId { static uint64_t s_id; }; /** Initially zero. */ -template -uint64_t LastAttributeId::s_id = 0; +template +uint64_t LastAttributeId::s_id = 0; }/* CVC4::expr::attr namespace */ /** Assign unique IDs to attributes at load time. */ -template -const uint64_t Attribute::s_id = - attr::LastAttributeId::table_value_type>::s_id++; +template +const uint64_t Attribute::s_id = + attr::LastAttributeId::table_value_type, context_dep>::s_id++; /** * Assign unique IDs to bool-valued attributes at load time, checking * that they are in range. */ -template -const uint64_t Attribute::s_id = - Attribute::checkID(attr::LastAttributeId::s_id++); +template +const uint64_t Attribute::s_id = + Attribute::checkID(attr::LastAttributeId::s_id++); // ATTRIBUTE MANAGER =========================================================== @@ -519,27 +563,44 @@ namespace attr { class AttributeManager { /** Underlying hash table for boolean-valued attributes */ - AttrHash d_bools; + AttrHash d_bools; /** Underlying hash table for integral-valued attributes */ - AttrHash d_ints; + AttrHash d_ints; /** Underlying hash table for node-valued attributes */ - AttrHash d_exprs; + AttrHash d_exprs; /** Underlying hash table for string-valued attributes */ AttrHash d_strings; /** Underlying hash table for pointer-valued attributes */ - AttrHash d_ptrs; + AttrHash d_ptrs; + + /** Underlying hash table for context-dependent boolean-valued attributes */ + CDAttrHash d_cdbools; + /** Underlying hash table for context-dependent integral-valued attributes */ + CDAttrHash d_cdints; + /** Underlying hash table for context-dependent node-valued attributes */ + CDAttrHash d_cdexprs; + /** Underlying hash table for context-dependent string-valued attributes */ + CDAttrHash d_cdstrings; + /** Underlying hash table for context-dependent pointer-valued attributes */ + CDAttrHash d_cdptrs; /** * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. */ - template + template friend struct getTable; public: /** Construct an attribute manager. */ - AttributeManager() {} + AttributeManager(context::Context* ctxt) : + d_cdbools(ctxt), + d_cdints(ctxt), + d_cdexprs(ctxt), + d_cdstrings(ctxt), + d_cdptrs(ctxt) { + } /** * Get a particular attribute on a particular node. @@ -619,12 +680,12 @@ namespace attr { * The getTable<> template provides (static) access to the * AttributeManager field holding the table. */ -template +template struct getTable; /** Access the "d_bools" member of AttributeManager. */ template <> -struct getTable { +struct getTable { typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_bools; @@ -636,7 +697,7 @@ struct getTable { /** Access the "d_ints" member of AttributeManager. */ template <> -struct getTable { +struct getTable { typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_ints; @@ -648,7 +709,7 @@ struct getTable { /** Access the "d_exprs" member of AttributeManager. */ template <> -struct getTable { +struct getTable { typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_exprs; @@ -660,7 +721,7 @@ struct getTable { /** Access the "d_strings" member of AttributeManager. */ template <> -struct getTable { +struct getTable { typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_strings; @@ -672,7 +733,7 @@ struct getTable { /** Access the "d_ptrs" member of AttributeManager. */ template -struct getTable { +struct getTable { typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -684,7 +745,7 @@ struct getTable { /** Access the "d_ptrs" member of AttributeManager. */ template -struct getTable { +struct getTable { typedef AttrHash table_type; static inline table_type& get(AttributeManager& am) { return am.d_ptrs; @@ -694,6 +755,78 @@ struct getTable { } }; +/** Access the "d_cdbools" member of AttributeManager. */ +template <> +struct getTable { + typedef CDAttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdbools; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdbools; + } +}; + +/** Access the "d_cdints" member of AttributeManager. */ +template <> +struct getTable { + typedef CDAttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdints; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdints; + } +}; + +/** Access the "d_cdexprs" member of AttributeManager. */ +template <> +struct getTable { + typedef CDAttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdexprs; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdexprs; + } +}; + +/** Access the "d_cdstrings" member of AttributeManager. */ +template <> +struct getTable { + typedef CDAttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdstrings; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdstrings; + } +}; + +/** Access the "d_cdptrs" member of AttributeManager. */ +template +struct getTable { + typedef CDAttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdptrs; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdptrs; + } +}; + +/** Access the "d_cdptrs" member of AttributeManager. */ +template +struct getTable { + typedef CDAttrHash table_type; + static inline table_type& get(AttributeManager& am) { + return am.d_cdptrs; + } + static inline const table_type& get(const AttributeManager& am) { + return am.d_cdptrs; + } +}; + }/* CVC4::expr::attr namespace */ // ATTRIBUTE MANAGER IMPLEMENTATIONS =========================================== @@ -707,9 +840,9 @@ typename AttrKind::value_type AttributeManager::getAttribute(TNode n, typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable::table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = getTable::get(*this); + const table_type& ah = getTable::get(*this); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n.d_nv)); if(i == ah.end()) { @@ -746,9 +879,9 @@ struct HasAttribute { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable::table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = getTable::get(*am); + const table_type& ah = getTable::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { @@ -771,9 +904,9 @@ struct HasAttribute { NodeValue* nv) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable::table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = getTable::get(*am); + const table_type& ah = getTable::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { @@ -788,9 +921,9 @@ struct HasAttribute { typename AttrKind::value_type& ret) { typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable::table_type table_type; + typedef typename getTable::table_type table_type; - const table_type& ah = getTable::get(*am); + const table_type& ah = getTable::get(*am); typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv)); if(i == ah.end()) { @@ -823,9 +956,9 @@ inline void AttributeManager::setAttribute(TNode n, typedef typename AttrKind::value_type value_type; typedef KindValueToTableValueMapping mapping; - typedef typename getTable::table_type table_type; + typedef typename getTable::table_type table_type; - table_type& ah = getTable::get(*this); + table_type& ah = getTable::get(*this); ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value); } diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 01f7205b2..934c405ad 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -21,7 +21,7 @@ using namespace std; namespace CVC4 { ostream& operator<<(ostream& out, const Command* command) { - if (command == NULL) { + if(command == NULL) { out << "null"; } else { command->toStream(out); diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 35bdc947a..b6348394c 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -60,7 +60,7 @@ Expr& Expr::operator=(const Expr& e) { } bool Expr::operator==(const Expr& e) const { - if(d_exprManager != e.d_exprManager){ + if(d_exprManager != e.d_exprManager) { return false; } Assert(d_node != NULL, "Unexpected NULL expression pointer!"); @@ -75,7 +75,7 @@ bool Expr::operator!=(const Expr& e) const { bool Expr::operator<(const Expr& e) const { Assert(d_node != NULL, "Unexpected NULL expression pointer!"); Assert(e.d_node != NULL, "Unexpected NULL expression pointer!"); - if(d_exprManager != e.d_exprManager){ + if(d_exprManager != e.d_exprManager) { return false; } return *d_node < *e.d_node; @@ -181,11 +181,11 @@ Expr BoolExpr::iteExpr(const Expr& then_e, const Expr& else_e) const { return d_exprManager->mkExpr(ITE, *this, then_e, else_e); } -void Expr::printAst(std::ostream & o, int indent) const{ +void Expr::printAst(std::ostream & o, int indent) const { getNode().printAst(o, indent); } -void Expr::debugPrint(){ +void Expr::debugPrint() { #ifndef CVC4_MUZZLE printAst(Warning()); Warning().flush(); diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 232a903e9..f0a35e5f1 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -25,17 +25,21 @@ #include "expr/type.h" #include "expr/node_manager.h" #include "expr/expr_manager.h" +#include "context/context.h" using namespace std; +using namespace CVC4::context; namespace CVC4 { ExprManager::ExprManager() : - d_nodeManager(new NodeManager()) { + d_ctxt(new Context), + d_nodeManager(new NodeManager(d_ctxt)) { } ExprManager::~ExprManager() { delete d_nodeManager; + delete d_ctxt; } const BooleanType* ExprManager::booleanType() const { @@ -136,4 +140,8 @@ NodeManager* ExprManager::getNodeManager() const { return d_nodeManager; } -} // End namespace CVC4 +Context* ExprManager::getContext() const { + return d_ctxt; +} + +}/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index f5edc5464..ff4e0db6b 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -30,6 +30,10 @@ class KindType; class SmtEngine; class NodeManager; +namespace context { + class Context; +}/* CVC4::context namespace */ + class CVC4_PUBLIC ExprManager { public: @@ -97,7 +101,7 @@ public: /** Make a function type with input types from argTypes. */ const FunctionType* - mkFunctionType(const std::vector& argTypes, + mkFunctionType(const std::vector& argTypes, const Type* range); /** Make a new sort with the given name. */ @@ -108,16 +112,28 @@ public: Expr mkVar(const Type* type); private: + /** The context */ + context::Context* d_ctxt; + /** The internal node manager */ NodeManager* d_nodeManager; - + /** - * Returns the internal node manager. This should only be used by internal - * users, i.e. the friend classes. + * Returns the internal node manager. This should only be used by + * internal users, i.e. the friend classes. */ NodeManager* getNodeManager() const; - /** SmtEngine will use all the internals, so it will grab the node manager */ + /** + * Returns the internal Context. Used by internal users, i.e. the + * friend classes. + */ + context::Context* getContext() const; + + /** + * SmtEngine will use all the internals, so it will grab the + * NodeManager. + */ friend class SmtEngine; /** ExprManagerScope reaches in to get the NodeManager */ diff --git a/src/expr/node.h b/src/expr/node.h index e4e57fc62..f9bbcb5a5 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -37,7 +37,8 @@ namespace CVC4 { class Type; class NodeManager; -template class NodeTemplate; +template +class NodeTemplate; /** * The Node class encapsulates the NodeValue with reference counting. @@ -64,7 +65,7 @@ class NodeValue; * maintained in the NodeValue if ref_count is true. * @param ref_count if true reference are counted in the NodeValue */ -template +template class NodeTemplate { /** @@ -94,11 +95,11 @@ class NodeTemplate { */ explicit NodeTemplate(const expr::NodeValue*); - friend class NodeTemplate ; - friend class NodeTemplate ; + friend class NodeTemplate; + friend class NodeTemplate; friend class NodeManager; - template + template friend class NodeBuilder; friend class ::CVC4::expr::attr::AttributeManager; @@ -152,7 +153,7 @@ public: * Destructor. If ref_count is true it will decrement the reference count * and, if zero, collect the NodeValue. */ - ~NodeTemplate() throw(); + ~NodeTemplate() throw(AssertionException); /** * Return the null node. @@ -389,8 +390,9 @@ private: * @param indent the numer of spaces */ static void indent(std::ostream& out, int indent) { - for(int i = 0; i < indent; i++) + for(int i = 0; i < indent; i++) { out << ' '; + } } };/* class NodeTemplate */ @@ -422,13 +424,13 @@ struct NodeHashFcn { } }; -template +template inline size_t NodeTemplate::getNumChildren() const { return d_nv->d_nchildren; } -template -template +template +template inline typename AttrKind::value_type NodeTemplate:: getAttribute(const AttrKind&) const { Assert( NodeManager::currentNM() != NULL, @@ -437,8 +439,8 @@ getAttribute(const AttrKind&) const { return NodeManager::currentNM()->getAttribute(*this, AttrKind()); } -template -template +template +template inline bool NodeTemplate:: hasAttribute(const AttrKind&) const { Assert( NodeManager::currentNM() != NULL, @@ -447,18 +449,18 @@ hasAttribute(const AttrKind&) const { return NodeManager::currentNM()->hasAttribute(*this, AttrKind()); } -template -template -inline bool NodeTemplate:: -hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const { +template +template +inline bool NodeTemplate::hasAttribute(const AttrKind&, + typename AttrKind::value_type& ret) const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" "Perhaps a public-facing function is missing a NodeManagerScope ?" ); return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); } -template -template +template +template inline void NodeTemplate:: setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { Assert( NodeManager::currentNM() != NULL, @@ -467,12 +469,12 @@ setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); } -template +template NodeTemplate NodeTemplate::s_null(&expr::NodeValue::s_null); ////FIXME: This function is a major hack! Should be changed ASAP ////TODO: Should use positive definition, i.e. what kinds are atomic. -template +template bool NodeTemplate::isAtomic() const { using namespace kind; switch(getKind()) { @@ -493,7 +495,7 @@ bool NodeTemplate::isAtomic() const { // 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. -template +template NodeTemplate::NodeTemplate(const expr::NodeValue* ev) : d_nv(const_cast (ev)) { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); @@ -504,7 +506,7 @@ NodeTemplate::NodeTemplate(const expr::NodeValue* ev) : // the code for these two "conversion/copy constructors" is identical, but // apparently we need both. see comment in the class. -template +template NodeTemplate::NodeTemplate(const NodeTemplate& e) { Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); d_nv = e.d_nv; @@ -513,7 +515,7 @@ NodeTemplate::NodeTemplate(const NodeTemplate& e) { } } -template +template NodeTemplate::NodeTemplate(const NodeTemplate& e) { Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!"); d_nv = e.d_nv; @@ -522,17 +524,17 @@ NodeTemplate::NodeTemplate(const NodeTemplate& e) { } } -template -NodeTemplate::~NodeTemplate() throw() { - DtorAssert(d_nv != NULL, "Expecting a non-NULL expression value!"); +template +NodeTemplate::~NodeTemplate() throw(AssertionException) { + Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); if(ref_count) { d_nv->dec(); } - DtorAssert(ref_count || d_nv->d_rc > 0, - "Temporary node pointing to an expired node"); + Assert(ref_count || d_nv->d_rc > 0, + "Temporary node pointing to an expired node"); } -template +template void NodeTemplate::assignNodeValue(expr::NodeValue* ev) { d_nv = ev; if(ref_count) { @@ -540,7 +542,7 @@ void NodeTemplate::assignNodeValue(expr::NodeValue* ev) { } } -template +template NodeTemplate& NodeTemplate:: operator=(const NodeTemplate& e) { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); @@ -557,7 +559,7 @@ operator=(const NodeTemplate& e) { return *this; } -template +template NodeTemplate& NodeTemplate:: operator=(const NodeTemplate& e) { Assert(d_nv != NULL, "Expecting a non-NULL expression value!"); @@ -574,54 +576,55 @@ operator=(const NodeTemplate& e) { return *this; } -template -NodeTemplate NodeTemplate::eqNode(const NodeTemplate< - ref_count>& right) const { +template +NodeTemplate +NodeTemplate::eqNode(const NodeTemplate& right) const { return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right); } -template +template NodeTemplate NodeTemplate::notNode() const { return NodeManager::currentNM()->mkNode(kind::NOT, *this); } -template -NodeTemplate NodeTemplate::andNode(const NodeTemplate< - ref_count>& right) const { +template +NodeTemplate +NodeTemplate::andNode(const NodeTemplate& right) const { return NodeManager::currentNM()->mkNode(kind::AND, *this, right); } -template -NodeTemplate NodeTemplate::orNode(const NodeTemplate< - ref_count>& right) const { +template +NodeTemplate +NodeTemplate::orNode(const NodeTemplate& right) const { return NodeManager::currentNM()->mkNode(kind::OR, *this, right); } -template -NodeTemplate NodeTemplate::iteNode(const NodeTemplate< - ref_count>& thenpart, const NodeTemplate& elsepart) const { +template +NodeTemplate +NodeTemplate::iteNode(const NodeTemplate& thenpart, + const NodeTemplate& elsepart) const { return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart); } -template -NodeTemplate NodeTemplate::iffNode(const NodeTemplate< - ref_count>& right) const { +template +NodeTemplate +NodeTemplate::iffNode(const NodeTemplate& right) const { return NodeManager::currentNM()->mkNode(kind::IFF, *this, right); } -template -NodeTemplate NodeTemplate::impNode(const NodeTemplate< - ref_count>& right) const { +template +NodeTemplate +NodeTemplate::impNode(const NodeTemplate& right) const { return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right); } -template -NodeTemplate NodeTemplate::xorNode(const NodeTemplate< - ref_count>& right) const { +template +NodeTemplate +NodeTemplate::xorNode(const NodeTemplate& right) const { return NodeManager::currentNM()->mkNode(kind::XOR, *this, right); } -template +template void NodeTemplate::printAst(std::ostream& out, int ind) const { indent(out, ind); out << '('; @@ -681,7 +684,8 @@ NodeTemplate NodeTemplate::getOperator() const { } /** - * Returns true if the node has an operator (i.e., it's not a variable or a constant). + * Returns true if the node has an operator (i.e., it's not a variable + * or a constant). */ template bool NodeTemplate::hasOperator() const { @@ -710,7 +714,7 @@ bool NodeTemplate::hasOperator() const { } } -template +template const Type* NodeTemplate::getType() const { Assert( NodeManager::currentNM() != NULL, "There is no current CVC4::NodeManager associated to this thread.\n" @@ -718,6 +722,7 @@ const Type* NodeTemplate::getType() const { return NodeManager::currentNM()->getType(*this); } +#ifdef CVC4_DEBUG /** * Pretty printer for use within gdb. This is not intended to be used * outside of gdb. This writes to the Warning() stream and immediately @@ -725,7 +730,9 @@ const Type* NodeTemplate::getType() const { * * Note that this function cannot be a template, since the compiler * won't instantiate it. Even if we explicitly instantiate. (Odd?) - * So we implement twice. + * So we implement twice. We mark as __attribute__((used)) so that + * GCC emits code for it even though static analysis indicates it's + * never called. * * Tim's Note: I moved this into the node.h file because this allows gdb * to find the symbol, and use it, which is the first standard this code needs @@ -740,6 +747,7 @@ static void __attribute__((used)) debugPrintTNode(const NodeTemplate& n) n.printAst(Warning(), 0); Warning().flush(); } +#endif /* CVC4_DEBUG */ }/* CVC4 namespace */ diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 4dc3c06d0..42ca9db2b 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -47,7 +47,6 @@ inline std::ostream& operator<<(std::ostream&, const NodeBuilder& class AndNodeBuilder; class OrNodeBuilder; class PlusNodeBuilder; -class MinusNodeBuilder; class MultNodeBuilder; template @@ -63,7 +62,7 @@ class NodeBuilder { // extract another bool d_used; - expr::NodeValue *d_nv; + expr::NodeValue* d_nv; expr::NodeValue d_inlineNv; expr::NodeValue *d_childrenStorage[nchild_thresh]; @@ -93,7 +92,7 @@ class NodeBuilder { } // dealloc: only call this with d_used == false and nvIsAllocated() - inline void dealloc() throw(); + inline void dealloc(); void crop() { Assert(!d_used, "NodeBuilder is one-shot only; attempt to access it after conversion"); @@ -101,6 +100,9 @@ class NodeBuilder { d_nv = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size = d_nv->d_nchildren) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } } } @@ -126,7 +128,7 @@ public: template inline NodeBuilder(const NodeBuilder& nb); inline NodeBuilder(NodeManager* nm); inline NodeBuilder(NodeManager* nm, Kind k); - inline ~NodeBuilder() throw(); + inline ~NodeBuilder(); typedef expr::NodeValue::iterator iterator; typedef expr::NodeValue::iterator const_iterator; @@ -223,9 +225,10 @@ public: friend class PlusNodeBuilder; friend class MultNodeBuilder; - //Yet 1 more example of how terrifying C++ is as a language - //This is needed for copy constructors of different sizes to access private fields - template friend class NodeBuilder; + // Yet 1 more example of how terrifying C++ is as a language + // This is needed for copy constructors of different sizes to access private fields + template + friend class NodeBuilder; };/* class NodeBuilder */ @@ -423,14 +426,24 @@ inline MultNodeBuilder PlusNodeBuilder::operator*(const NodeTemplate& n) { return MultNodeBuilder(Node(d_eb), n); } -/* -inline PlusNodeBuilder& PlusNodeBuilder::operator+(PlusNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder& PlusNodeBuilder::operator+(MultNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder& PlusNodeBuilder::operator-(PlusNodeBuilder& b) { return *this - Node(d_eb); } -inline PlusNodeBuilder& PlusNodeBuilder::operator-(MultNodeBuilder& b) { return *this - Node(d_eb); } -inline MultNodeBuilder PlusNodeBuilder::operator*(PlusNodeBuilder& b) { return *this * Node(d_eb); } -inline MultNodeBuilder PlusNodeBuilder::operator*(MultNodeBuilder& b) { return *this * Node(d_eb); } -*/ +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const PlusNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder& operator+(PlusNodeBuilder& a, const MultNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder&a, const PlusNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline PlusNodeBuilder& operator-(PlusNodeBuilder& a, const MultNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, const PlusNodeBuilder& b) { + return a * Node(b.d_eb); +} +inline MultNodeBuilder operator*(PlusNodeBuilder& a, const MultNodeBuilder& b) { + return a * Node(b.d_eb); +} template inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate& n) { @@ -439,7 +452,7 @@ inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate& n) { template inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate& n) { - return PlusNodeBuilder(Node(d_eb), n); + return PlusNodeBuilder(Node(d_eb), NodeManager::currentNM()->mkNode(kind::UMINUS, n)); } template @@ -448,14 +461,24 @@ inline MultNodeBuilder& MultNodeBuilder::operator*(const NodeTemplate& n) { return *this; } -/* -inline PlusNodeBuilder MultNodeBuilder::operator+(const PlusNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder MultNodeBuilder::operator+(const MultNodeBuilder& b) { return *this + Node(d_eb); } -inline PlusNodeBuilder MultNodeBuilder::operator-(const PlusNodeBuilder& b) { return *this - Node(d_eb); } -inline PlusNodeBuilder MultNodeBuilder::operator-(const MultNodeBuilder& b) { return *this - Node(d_eb); } -inline MultNodeBuilder& MultNodeBuilder::operator*(const PlusNodeBuilder& b) { return *this * Node(d_eb); } -inline MultNodeBuilder& MultNodeBuilder::operator*(const MultNodeBuilder& b) { return *this * Node(d_eb); } -*/ +inline PlusNodeBuilder operator+(MultNodeBuilder& a, const PlusNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder operator+(MultNodeBuilder& a, const MultNodeBuilder& b) { + return a + Node(b.d_eb); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, const PlusNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline PlusNodeBuilder operator-(MultNodeBuilder& a, const MultNodeBuilder& b) { + return a - Node(b.d_eb); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, const PlusNodeBuilder& b) { + return a * Node(b.d_eb); +} +inline MultNodeBuilder& operator*(MultNodeBuilder& a, const MultNodeBuilder& b) { + return a * Node(b.d_eb); +} template inline AndNodeBuilder operator&&(const NodeTemplate& a, const NodeTemplate& b) { @@ -502,6 +525,41 @@ inline OrNodeBuilder operator||(const NodeTemplate& a, const OrNodeBuilder& return a || Node(b.d_eb); } +template +inline PlusNodeBuilder operator+(const NodeTemplate& a, const PlusNodeBuilder& b) { + return a + Node(b.d_eb); +} + +template +inline PlusNodeBuilder operator+(const NodeTemplate& a, const MultNodeBuilder& b) { + return a + Node(b.d_eb); +} + +template +inline PlusNodeBuilder operator-(const NodeTemplate& a, const PlusNodeBuilder& b) { + return a - Node(b.d_eb); +} + +template +inline PlusNodeBuilder operator-(const NodeTemplate& a, const MultNodeBuilder& b) { + return a - Node(b.d_eb); +} + +template +inline MultNodeBuilder operator*(const NodeTemplate& a, const PlusNodeBuilder& b) { + return a * Node(b.d_eb); +} + +template +inline MultNodeBuilder operator*(const NodeTemplate& a, const MultNodeBuilder& b) { + return a * Node(b.d_eb); +} + +template +inline NodeTemplate operator-(const NodeTemplate& a) { + return NodeManager::currentNM()->mkNode(kind::UMINUS, a); +} + }/* CVC4 namespace */ #include "expr/node.h" @@ -611,7 +669,7 @@ inline NodeBuilder::NodeBuilder(NodeManager* nm, Kind k) : } template -inline NodeBuilder::~NodeBuilder() throw() { +inline NodeBuilder::~NodeBuilder() { if(!d_used) { // Warning("NodeBuilder unused at destruction\n"); // Commented above, as it happens a lot, for example with exceptions @@ -642,9 +700,15 @@ void NodeBuilder::realloc() { d_nv = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } } else { d_nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size *= 2) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; @@ -663,10 +727,16 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { d_nv = (expr::NodeValue*) std::realloc(d_nv, sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size = toSize) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } } else { d_nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * (d_size = toSize) )); + if(d_nv == NULL) { + throw std::bad_alloc(); + } d_nv->d_id = 0; d_nv->d_rc = 0; d_nv->d_kind = d_inlineNv.d_kind; @@ -682,12 +752,11 @@ void NodeBuilder::realloc(size_t toSize, bool copy) { } template -inline void NodeBuilder::dealloc() throw() { +inline void NodeBuilder::dealloc() { /* Prefer asserts to if() because usually these conditions have been * checked already, so we don't want to do a double-check in * production; these are just sanity checks for debug builds */ - DtorAssert(!d_used, - "Internal error: NodeBuilder: dealloc() called with d_used"); + Assert(!d_used, "Internal error: NodeBuilder: dealloc() called with d_used"); for(expr::NodeValue::nv_iterator i = d_nv->nv_begin(); i != d_nv->nv_end(); @@ -707,9 +776,12 @@ NodeBuilder::operator Node() const {// const version if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); - expr::NodeValue *nv = (expr::NodeValue*) + expr::NodeValue* nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + if(nv == NULL) { + throw std::bad_alloc(); + } nv->d_nchildren = 0; nv->d_kind = kind::VARIABLE; nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -736,6 +808,9 @@ NodeBuilder::operator Node() const {// const version nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * d_nv->d_nchildren )); + if(nv == NULL) { + throw std::bad_alloc(); + } nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading nv->d_rc = 0; nv->d_kind = d_nv->d_kind; @@ -767,6 +842,9 @@ NodeBuilder::operator Node() const {// const version ev = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(ev == NULL) { + throw std::bad_alloc(); + } ev->d_nchildren = d_inlineNv.d_nchildren; ev->d_kind = d_inlineNv.d_kind; ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -797,9 +875,12 @@ NodeBuilder::operator Node() {// not const if(d_nv->d_kind == kind::VARIABLE) { Assert(d_nv->d_nchildren == 0); - expr::NodeValue *nv = (expr::NodeValue*) + expr::NodeValue* nv = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + (sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren ));// FIXME :: WTF?? + if(nv == NULL) { + throw std::bad_alloc(); + } nv->d_nchildren = 0; nv->d_kind = kind::VARIABLE; nv->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -847,6 +928,9 @@ NodeBuilder::operator Node() {// not const ev = (expr::NodeValue*) std::malloc(sizeof(expr::NodeValue) + ( sizeof(expr::NodeValue*) * d_inlineNv.d_nchildren )); + if(ev == NULL) { + throw std::bad_alloc(); + } ev->d_nchildren = d_inlineNv.d_nchildren; ev->d_kind = d_inlineNv.d_kind; ev->d_id = expr::NodeValue::next_id++;// FIXME multithreading @@ -866,7 +950,6 @@ NodeBuilder::operator Node() {// not const template inline std::ostream& operator<<(std::ostream& out, const NodeBuilder& b) { - b.toStream(out); return out; } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 62bcc7516..c4f54727a 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -28,6 +28,7 @@ #include "expr/kind.h" #include "expr/expr.h" +#include "context/context.h" namespace CVC4 { @@ -51,7 +52,8 @@ class NodeManager { template friend class CVC4::NodeBuilder; - typedef __gnu_cxx::hash_set NodeValueSet; NodeValueSet d_nodeValueSet; @@ -61,10 +63,18 @@ class NodeManager { void poolInsert(expr::NodeValue* nv); friend class NodeManagerScope; + friend class expr::NodeValue; + + std::vector d_zombieList; + + inline void gc(expr::NodeValue* nv) { + Assert(nv->d_rc == 0); + d_zombieList.push_back(nv); + } public: - NodeManager() { + NodeManager(context::Context* ctxt) : d_attrManager(ctxt) { poolInsert( &expr::NodeValue::s_null ); } @@ -133,6 +143,26 @@ public: inline const Type* getType(TNode n); }; +/** + * Resource-acquisition-is-instantiation C++ idiom: create one of + * these "scope" objects to temporarily change the thread-specific + * notion of the "current" NodeManager for Node creation/deletion, + * etc. On destruction, the previous NodeManager pointer is restored. + * Therefore such objects should only be created and destroyed in a + * well-scoped manner (such as on the stack). + * + * This is especially useful on public-interface calls into the CVC4 + * library, where CVC4's notion of the "current" NodeManager should be + * set to match the calling context. See, for example, the + * implementations of public calls in the ExprManager and SmtEngine + * classes. + * + * You may create a NodeManagerScope with "new" and destroy it with + * "delete", or place it as a data member of an object that is, but if + * the scope of these new/delete pairs isn't properly maintained, the + * incorrect "current" NodeManager pointer may be restored after a + * delete. + */ class NodeManagerScope { NodeManager *d_oldNodeManager; @@ -143,22 +173,32 @@ public: Debug("current") << "node manager scope: " << NodeManager::s_current << "\n"; } - ~NodeManagerScope() throw() { + ~NodeManagerScope() { NodeManager::s_current = d_oldNodeManager; Debug("current") << "node manager scope: returning to " << NodeManager::s_current << "\n"; } }; /** - * A wrapper (essentially) for NodeManagerScope. Without this, we'd - * need Expr to be a friend of ExprManager. + * A wrapper (essentially) for NodeManagerScope. The current + * "NodeManager" pointer is set to this Expr's underlying + * ExpressionManager's NodeManager. When the ExprManagerScope is + * destroyed, the previous NodeManager is restored. + * + * This is especially useful on public-interface calls into the CVC4 + * library, where CVC4's notion of the "current" NodeManager should be + * set to match the calling context. See, for example, the + * implementations of public calls in the Expr class. + * + * Without this, we'd need Expr to be a friend of ExprManager. */ class ExprManagerScope { NodeManagerScope d_nms; public: inline ExprManagerScope(const Expr& e) : - d_nms(e.getExprManager() == NULL ? - NodeManager::currentNM() : e.getExprManager()->getNodeManager()) { + d_nms(e.getExprManager() == NULL + ? NodeManager::currentNM() + : e.getExprManager()->getNodeManager()) { } }; diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 523c5387b..bd74fd4d4 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -24,7 +24,7 @@ #include "cvc4_config.h" #include -#include "kind.h" +#include "expr/kind.h" #include #include @@ -98,7 +98,7 @@ class NodeValue { NodeValue(int); /** Destructor decrements the ref counts of its children */ - ~NodeValue() throw(); + ~NodeValue(); typedef NodeValue** nv_iterator; typedef NodeValue const* const* const_nv_iterator; @@ -150,16 +150,19 @@ public: } /** - * Hash this expression. + * Hash this NodeValue. For hash_maps, hash_sets, etc.. but this is + * for expr package internal use only at present! This is likely to + * be POORLY PERFORMING for other uses! For example, this gives + * collisions for all VARIABLEs. * @return the hash value of this expression. */ - size_t hash() const { + size_t internalHash() const { size_t hash = d_kind; const_nv_iterator i = nv_begin(); const_nv_iterator i_end = nv_end(); - while (i != i_end) { + while(i != i_end) { hash ^= (*i)->d_id + 0x9e3779b9 + (hash << 6) + (hash >> 2); - ++ i; + ++i; } return hash; } @@ -209,7 +212,27 @@ public: static inline Kind dKindToKind(unsigned d) { return (d == kindMask) ? kind::UNDEFINED_KIND : Kind(d); } -}; +};/* class NodeValue */ + +/** + * For hash_maps, hash_sets, etc.. but this is for expr package + * internal use only at present! This is likely to be POORLY + * PERFORMING for other uses! NodeValue::internalHash() will lead to + * collisions for all VARIABLEs. + */ +struct NodeValueInternalHashFcn { + inline size_t operator()(const NodeValue* nv) const { + return (size_t) nv->internalHash(); + } +};/* struct NodeValueHashFcn */ + +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ + +#include "node_manager.h" + +namespace CVC4 { +namespace expr { inline NodeValue::NodeValue() : d_id(0), @@ -225,7 +248,7 @@ inline NodeValue::NodeValue(int) : d_nchildren(0) { } -inline NodeValue::~NodeValue() throw() { +inline NodeValue::~NodeValue() { for(nv_iterator i = nv_begin(); i != nv_end(); ++i) { (*i)->dec(); } @@ -243,7 +266,10 @@ inline void NodeValue::dec() { if(EXPECT_TRUE( d_rc < MAX_RC )) { --d_rc; if(EXPECT_FALSE( d_rc == 0 )) { - // FIXME gc + Assert(NodeManager::currentNM() != NULL, + "No current NodeManager on destruction of NodeValue: " + "maybe a public CVC4 interface function is missing a NodeManagerScope ?"); + NodeManager::currentNM()->gc(this); } } } @@ -264,13 +290,6 @@ inline NodeValue::const_nv_iterator NodeValue::nv_end() const { return d_children + d_nchildren; } -// for hash_maps, hash_sets, ... -struct NodeValueHashFcn { - size_t operator()(const CVC4::expr::NodeValue* nv) const { - return (size_t)nv->hash(); - } -};/* struct NodeValueHashFcn */ - }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index baad6fe31..b319b7293 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -46,12 +46,6 @@ Languages currently supported as arguments to the -L / --lang option:\n\ smt | smtlib SMT-LIB format\n\ "; -static const char cnf_help[] = "\ -CNF conversions currently supported as arguments to the --cnf option:\n\ - direct put in equiv. CNF directly (exp. blow up in # clauses, no new vars)\n\ - var variable-introduction method (new vars, no exp. blow up in # clauses)\n\ -"; - /** * For the main getopt() routine, we need ways to switch on long * options without clashing with short option characters. This is an @@ -61,8 +55,7 @@ CNF conversions currently supported as arguments to the --cnf option:\n\ * any collision. */ enum OptionValue { - CNF = 256, /* no clash with char options */ - SMTCOMP, + SMTCOMP = 256, /* no clash with char options */ STATS, SEGV_NOSPIN, PARSE_ONLY, @@ -98,7 +91,6 @@ static struct option cmdlineOptions[] = { { "quiet" , no_argument , NULL, 'q' }, { "lang" , required_argument, NULL, 'L' }, { "debug" , required_argument, NULL, 'd' }, - { "cnf" , required_argument, NULL, CNF }, { "smtcomp" , no_argument , NULL, SMTCOMP }, { "stats" , no_argument , NULL, STATS }, { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }, @@ -179,21 +171,6 @@ throw(OptionException) { fputs(lang_help, stdout); exit(1); - case CNF: - if(!strcmp(optarg, "direct")) { - opts->d_cnfConversion = CNF_DIRECT_EXPONENTIAL; - break; - } else if(!strcmp(optarg, "var")) { - opts->d_cnfConversion = CNF_VAR_INTRODUCTION; - break; - } else if(strcmp(optarg, "help")) { - throw OptionException(string("unknown CNF conversion for --cnf: `") + - optarg + "'. Try --cnf help."); - } - - fputs(cnf_help, stdout); - exit(1); - case 'd': Debug.on(optarg); /* fall-through */ diff --git a/src/main/main.cpp b/src/main/main.cpp index 2eea56947..1da56b9f9 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -151,7 +151,7 @@ int runCvc4(int argc, char *argv[]) { } else { string filename = argv[firstArgIndex]; input = new ifstream(filename.c_str()); - if(input == NULL) { + if(!*input) { throw Exception("file does not exist or is unreadable: " + filename); } parser = Parser::getNewParser(&exprMgr, options.lang, *input, filename); diff --git a/src/main/util.cpp b/src/main/util.cpp index adb117b9d..a2b46513d 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -16,6 +16,7 @@ #include #include #include +#include #include #include @@ -63,6 +64,45 @@ void segv_handler(int sig, siginfo_t* info, void*) { #endif /* CVC4_DEBUG */ } +static terminate_handler default_terminator; + +void cvc4unexpected() { +#ifdef CVC4_DEBUG + fprintf(stderr, + "\n" + "CVC4 threw an \"unexpected\" exception (one that wasn't properly specified\n" + "in the throws() specifier for the throwing function).\n\n"); + if(segvNoSpin) { + fprintf(stderr, "No-spin requested.\n"); + set_terminate(default_terminator); + } else { + fprintf(stderr, "Spinning so that a debugger can be connected.\n"); + fprintf(stderr, "Try: gdb %s %u\n", progName, getpid()); + for(;;) { + sleep(60); + } + } +#else /* CVC4_DEBUG */ + fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n"); + set_terminate(default_terminator); +#endif /* CVC4_DEBUG */ +} + +void cvc4terminate() { +#ifdef CVC4_DEBUG + fprintf(stderr, + "\n" + "CVC4 was terminated by the C++ runtime.\n" + "Perhaps an exception was thrown during stack unwinding. (Don't do that.)\n"); + default_terminator(); +#else /* CVC4_DEBUG */ + fprintf(stderr, + "CVC4 was terminated by the C++ runtime.\n" + "Perhaps an exception was thrown during stack unwinding.\n"); + default_terminator(); +#endif /* CVC4_DEBUG */ +} + /** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */ void cvc4_init() throw() { struct sigaction act1; @@ -78,6 +118,9 @@ void cvc4_init() throw() { sigemptyset(&act2.sa_mask); if(sigaction(SIGSEGV, &act2, NULL)) throw Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); + + set_unexpected(cvc4unexpected); + default_terminator = set_terminate(cvc4terminate); } }/* CVC4::main namespace */ diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 6eb269bca..e2949286a 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -171,10 +171,10 @@ const Type* AntlrParser::predicateType(const std::vector& sorts) { Expr AntlrParser::mkVar(const std::string& name, const Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; - Assert( !isDeclared(name) ) ; + Assert( !isDeclared(name) ); Expr expr = d_exprManager->mkVar(type, name); d_varSymbolTable.bindName(name, expr); - Assert( isDeclared(name) ) ; + Assert( isDeclared(name) ); return expr; } @@ -192,10 +192,10 @@ AntlrParser::mkVars(const std::vector names, const Type* AntlrParser::newSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; - Assert( !isDeclared(name, SYM_SORT) ) ; + Assert( !isDeclared(name, SYM_SORT) ); const Type* type = d_exprManager->mkSort(name); d_sortTable.bindName(name, type); - Assert( isDeclared(name, SYM_SORT) ) ; + Assert( isDeclared(name, SYM_SORT) ); return type; } diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h index c92e62524..e1639a072 100644 --- a/src/parser/memory_mapped_input_buffer.h +++ b/src/parser/memory_mapped_input_buffer.h @@ -11,16 +11,19 @@ ** ANTLR input buffer from a memory-mapped file. **/ -#ifndef MEMORY_MAPPED_INPUT_BUFFER_H_ -#define MEMORY_MAPPED_INPUT_BUFFER_H_ +#ifndef __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H +#define __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H + +#include +#include #include -#include #include +#include -#include #include #include + #include #include "util/Assert.h" @@ -33,32 +36,34 @@ class MemoryMappedInputBuffer : public antlr::InputBuffer { public: MemoryMappedInputBuffer(const std::string& filename) { - errno = 0; struct stat st; if( stat(filename.c_str(), &st) == -1 ) { - throw Exception("unable to stat() file"); -// throw Exception( "unable to stat() file " << filename << " errno " << errno ); + char buf[80]; + const char* errMsg = strerror_r(errno, buf, sizeof(buf)); + throw Exception("unable to stat() file `" + filename + "': " + errMsg); } d_size = st.st_size; int fd = open(filename.c_str(), O_RDONLY); if( fd == -1 ) { - throw Exception("unable to fopen() file"); + char buf[80]; + const char* errMsg = strerror_r(errno, buf, sizeof(buf)); + throw Exception("unable to fopen() file `" + filename + "': " + errMsg); } d_start = static_cast< const char * >( mmap( 0, d_size, PROT_READ, MAP_FILE | MAP_PRIVATE, fd, 0 ) ); - errno = 0; if( intptr_t( d_start ) == -1 ) { - throw Exception("unable to mmap() file"); -// throw Exception( "unable to mmap() file " << filename << " errno " << errno ); + char buf[80]; + const char* errMsg = strerror_r(errno, buf, sizeof(buf)); + throw Exception("unable to mmap() file `" + filename + "': " + errMsg); } d_cur = d_start; d_end = d_start + d_size; } ~MemoryMappedInputBuffer() { - munmap((void*)d_start,d_size); + munmap((void*) d_start, d_size); } inline int getChar() { @@ -71,8 +76,7 @@ private: const char *d_start, *d_end, *d_cur; }; -} -} - +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* MEMORY_MAPPED_INPUT_BUFFER_H_ */ +#endif /* __CVC4__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 852eda595..a129d97ee 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -18,12 +18,12 @@ #include #include -#include "parser.h" -#include "memory_mapped_input_buffer.h" +#include "parser/parser.h" +#include "parser/memory_mapped_input_buffer.h" #include "expr/command.h" #include "util/output.h" #include "util/Assert.h" -#include "parser_exception.h" +#include "parser/parser_exception.h" #include "parser/antlr_parser.h" #include "parser/smt/generated/AntlrSmtParser.hpp" #include "parser/smt/generated/AntlrSmtLexer.hpp" @@ -125,7 +125,7 @@ Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, Parser* Parser::getMemoryMappedParser(ExprManager* em, InputLanguage lang, string filename) { MemoryMappedInputBuffer* inputBuffer = new MemoryMappedInputBuffer(filename); - return getNewParser(em,lang,inputBuffer,filename); + return getNewParser(em, lang, inputBuffer, filename); } Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang, diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index e30398824..f0ddc6a7f 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -24,14 +24,14 @@ namespace CVC4 { namespace parser { -class CVC4_PUBLIC ParserException: public Exception { +class CVC4_PUBLIC ParserException : public Exception { public: // Constructors ParserException() { } ParserException(const std::string& msg): Exception(msg) { } ParserException(const char* msg): Exception(msg) { } // Destructor - virtual ~ParserException() { } + virtual ~ParserException() throw() {} virtual std::string toString() const { return "Parse Error: " + d_msg; } diff --git a/src/parser/symbol_table.h b/src/parser/symbol_table.h index 5838790a8..4ab2fb521 100644 --- a/src/parser/symbol_table.h +++ b/src/parser/symbol_table.h @@ -35,7 +35,7 @@ struct StringHashFcn { /** * Generic symbol table for looking up variables by name. */ -template +template class SymbolTable { private: @@ -85,7 +85,7 @@ public: ObjectType getObject(const std::string& name) throw () { table_iterator find = d_nameBindings.find(name); Assert(find != d_nameBindings.end()); - return find->second /*.top()*/ ; + return find->second; /*.top()*/ } /** diff --git a/src/prop/cnf_conversion.h b/src/prop/cnf_conversion.h deleted file mode 100644 index d66e721db..000000000 --- a/src/prop/cnf_conversion.h +++ /dev/null @@ -1,51 +0,0 @@ -/********************* */ -/** cnf_conversion.h - ** Original author: taking - ** Major contributors: none - ** Minor contributors (to current version): dejan, mdeters - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 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. - ** - ** A type for describing possible CNF conversions. - **/ - -#include "cvc4_private.h" - -#ifndef __CVC4__CNF_CONVERSION_H -#define __CVC4__CNF_CONVERSION_H - -namespace CVC4 { - -enum CnfConversion { - /** TODO: explanation of DIRECT_EXPONENTIAL (is this implemented?) */ - CNF_DIRECT_EXPONENTIAL = 0, - /** Explanation of CNF_VAR_INTRODUCTION */ - CNF_VAR_INTRODUCTION = 1 -}; - -inline std::ostream& operator<<(std::ostream&, CVC4::CnfConversion) CVC4_PUBLIC; - -inline std::ostream& operator<<(std::ostream& out, CVC4::CnfConversion c) { - using namespace CVC4; - - switch(c) { - case CNF_DIRECT_EXPONENTIAL: - out << "CNF_DIRECT_EXPONENTIAL"; - break; - case CNF_VAR_INTRODUCTION: - out << "CNF_VAR_INTRODUCTION"; - break; - default: - out << "UNKNOWN-CONVERTER!" << int(c); - } - - return out; -} - -}/* CVC4 namespace */ - -#endif /* __CVC4__CNF_CONVERSION_H */ diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 6e3b6ae2f..612b00bcf 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -320,21 +320,21 @@ SatLiteral TseitinCnfStream::toCNF(const TNode& node) { void TseitinCnfStream::convertAndAssert(const TNode& node) { Debug("cnf") << "convertAndAssert(" << node << ")" << endl; // If the node is a conjuntion, we handle each conjunct separatelu - if (node.getKind() == AND) { + if(node.getKind() == AND) { TNode::const_iterator conjunct = node.begin(); TNode::const_iterator node_end = node.end(); - while (conjunct != node_end) { + while(conjunct != node_end) { convertAndAssert(*conjunct); ++ conjunct; } return; } // If the node is a disjunction, we construct a clause and assert it - if (node.getKind() == OR) { + if(node.getKind() == OR) { int nChildren = node.getNumChildren(); SatClause clause(nChildren); TNode::const_iterator disjunct = node.begin(); - for (int i = 0; i < nChildren; ++ disjunct, ++ i) { + for(int i = 0; i < nChildren; ++ disjunct, ++ i) { clause[i] = toCNF(*disjunct); } assertClause(clause); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c45314a55..8def3e279 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -25,8 +25,45 @@ using CVC4::context::Context; namespace CVC4 { +namespace smt { + +/** + * This is an inelegant solution, but for the present, it will work. + * The point of this is to separate the public and private portions of + * the SmtEngine class, so that smt_engine.h doesn't + * #include "expr/node.h", which is a private CVC4 header (and can lead + * to linking errors due to the improper inlining of non-visible symbols + * into user code!). + * + * The "real" solution (that which is usually implemented) is to move + * ALL the implementation to SmtEnginePrivate and maintain a + * heap-allocated instance of it in SmtEngine. SmtEngine (the public + * one) becomes an "interface shell" which simply acts as a forwarder + * of method calls. + */ +class SmtEnginePrivate { +public: + + /** + * Pre-process an Node. This is expected to be highly-variable, + * with a lot of "source-level configurability" to add multiple + * passes over the Node. TODO: may need to specify a LEVEL of + * preprocessing (certain contexts need more/less ?). + */ + static Node preprocess(SmtEngine& smt, TNode node); + + /** + * Adds a formula to the current context. + */ + static void addFormula(SmtEngine& smt, TNode node); +};/* class SmtEnginePrivate */ + +}/* namespace CVC4::smt */ + +using ::CVC4::smt::SmtEnginePrivate; + SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : - d_ctxt(new Context), + d_ctxt(em->getContext()), d_exprManager(em), d_nodeManager(em->getNodeManager()), d_options(opts) { @@ -37,10 +74,10 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : } SmtEngine::~SmtEngine() { + NodeManagerScope nms(d_nodeManager); delete d_propEngine; delete d_theoryEngine; delete d_decisionEngine; - delete d_ctxt; } void SmtEngine::doCommand(Command* c) { @@ -48,7 +85,7 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } -Node SmtEngine::preprocess(TNode e) { +Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) { return e; } @@ -62,15 +99,15 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEngine::addFormula(TNode e) { +void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode e) { Debug("smt") << "push_back assertion " << e << std::endl; - d_propEngine->assertFormula(preprocess(e)); + smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, e)); } Result SmtEngine::checkSat(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT checkSat(" << e << ")" << std::endl; - addFormula(e.getNode()); + SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << std::endl; return r; @@ -79,7 +116,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { Result SmtEngine::query(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT query(" << e << ")" << std::endl; - addFormula(e.getNode().notNode()); + SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); Debug("smt") << "SMT query(" << e << ") ==> " << r << std::endl; return r; @@ -88,7 +125,7 @@ Result SmtEngine::query(const BoolExpr& e) { Result SmtEngine::assertFormula(const BoolExpr& e) { NodeManagerScope nms(d_nodeManager); Debug("smt") << "SMT assertFormula(" << e << ")" << std::endl; - addFormula(e.getNode()); + SmtEnginePrivate::addFormula(*this, e.getNode()); return quickCheck().asValidityResult(); } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 7495e4100..36cb8746c 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -24,9 +24,6 @@ #include "util/result.h" #include "util/model.h" -// FIXME private header in public code -#include "expr/node.h" - // In terms of abstraction, this is below (and provides services to) // ValidityChecker and above (and requires the services of) // PropEngine. @@ -35,7 +32,7 @@ namespace CVC4 { namespace context { class Context; -} +}/* CVC4::context namespace */ class Command; class Options; @@ -44,7 +41,11 @@ class DecisionEngine; namespace prop { class PropEngine; -} +}/* CVC4::prop namespace */ + +namespace smt { + class SmtEnginePrivate; +}/* CVC4::smt namespace */ // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass @@ -140,18 +141,9 @@ private: /** The propositional engine */ prop::PropEngine* d_propEngine; - /** - * Pre-process an Node. This is expected to be highly-variable, - * with a lot of "source-level configurability" to add multiple - * passes over the Node. TODO: may need to specify a LEVEL of - * preprocessing (certain contexts need more/less ?). - */ - Node preprocess(TNode node); - - /** - * Adds a formula to the current context. - */ - void addFormula(TNode node); + // preprocess() and addFormula() used to be housed here; they are + // now in an SmtEnginePrivate class. See the comment in + // smt_engine.cpp. /** * Full check of consistency in current context. Returns true iff @@ -166,6 +158,8 @@ private: */ Result quickCheck(); + friend class ::CVC4::smt::SmtEnginePrivate; + };/* class SmtEngine */ }/* CVC4 namespace */ diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 735712cdc..199b09164 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -21,6 +21,7 @@ #include "expr/node.h" #include "context/context.h" +#include "context/cdo.h" #include "context/context_mm.h" namespace CVC4 { @@ -105,7 +106,6 @@ private: */ ECData* d_find; - /** * This is pointer back to the node that represents this equivalence class. * diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index d432d733f..3753bd78a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -30,6 +30,7 @@ #include "theory/theory.h" #include "context/context.h" +#include "context/cdlist.h" #include "theory/uf/ecdata.h" namespace CVC4 { diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 8e2dd9220..f992032ee 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -25,6 +25,10 @@ using namespace std; namespace CVC4 { +#ifdef CVC4_DEBUG +__thread CVC4_PUBLIC const char* s_debugAssertionFailure = NULL; +#endif /* CVC4_DEBUG */ + void AssertionException::construct(const char* header, const char* extra, const char* function, const char* file, unsigned line, const char* fmt, @@ -65,7 +69,13 @@ void AssertionException::construct(const char* header, const char* extra, } setMessage(string(buf)); + +#ifdef CVC4_DEBUG + // we leak buf[] but only in debug mode with assertions failing + s_debugAssertionFailure = buf; +#else /* CVC4_DEBUG */ delete [] buf; +#endif /* CVC4_DEBUG */ } void AssertionException::construct(const char* header, const char* extra, @@ -98,7 +108,13 @@ void AssertionException::construct(const char* header, const char* extra, } setMessage(string(buf)); + +#ifdef CVC4_DEBUG + // we leak buf[] but only in debug mode with assertions failing + s_debugAssertionFailure = buf; +#else /* CVC4_DEBUG */ delete [] buf; +#endif /* CVC4_DEBUG */ } }/* CVC4 namespace */ diff --git a/src/util/Assert.h b/src/util/Assert.h index 3b42f2887..8c230218c 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -19,12 +19,13 @@ #include #include #include +#include #include -#include "util/exception.h" -#include "cvc4_config.h" -#include "config.h" -#include +#include "config.h" +#include "cvc4_config.h" +#include "util/exception.h" +#include "util/output.h" namespace CVC4 { @@ -192,14 +193,42 @@ public: } };/* class IllegalArgumentException */ -#define AlwaysAssert(cond, msg...) \ - do { \ - if(EXPECT_FALSE( ! (cond) )) { \ - throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ - } \ +#ifdef CVC4_DEBUG + +extern __thread CVC4_PUBLIC const char* s_debugAssertionFailure; + +// If we're currently handling an exception, print a warning instead; +// otherwise std::terminate() is called by the runtime and we lose +// details of the exception +#define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + if(EXPECT_FALSE( std::uncaught_exception() )) { \ + Warning() << "===========================================" << std::endl \ + << "An assertion failed during stack unwinding:" << std::endl \ + << AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) << std::endl \ + << "===========================================" << std::endl; \ + if(s_debugAssertionFailure != NULL) { \ + Warning() << "The propagating exception is:" << std::endl \ + << s_debugAssertionFailure << std::endl \ + << "===========================================" << std::endl; \ + } \ + } else { \ + throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } \ } while(0) -#define DtorAlwaysAssert(cond, msg...) \ - assert(EXPECT_TRUE( cond )) +#else /* CVC4_DEBUG */ +// These simpler (but less useful) versions for non-debug builds fails +// with terminate() if thrown during stack unwinding. +# define AlwaysAssert(cond, msg...) \ + do { \ + if(EXPECT_FALSE( ! (cond) )) { \ + throw AssertionException(#cond, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \ + } \ + } while(0) +#endif /* CVC4_DEBUG */ + #define Unreachable(msg...) \ throw UnreachableCodeException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg) #define Unhandled(msg...) \ @@ -219,11 +248,9 @@ public: #ifdef CVC4_ASSERTIONS # define Assert(cond, msg...) AlwaysAssert(cond, ## msg) -# define DtorAssert(cond, msg...) assert(EXPECT_TRUE( cond )) # define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg) #else /* ! CVC4_ASSERTIONS */ # define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ -# define DtorAssert(cond, msg...) /*EXPECT_TRUE( cond )*/ # define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/ #endif /* CVC4_ASSERTIONS */ diff --git a/src/util/exception.h b/src/util/exception.h index b77e7c860..5449d67f7 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -31,7 +31,7 @@ public: Exception(const std::string& msg) : d_msg(msg) {} Exception(const char* msg) : d_msg(msg) {} // Destructor - virtual ~Exception() {} + virtual ~Exception() throw() {} // NON-VIRTUAL METHOD for setting and printing the error message void setMessage(const std::string& msg) { d_msg = msg; } // Printing: feel free to redefine toString(). When inherited, diff --git a/src/util/options.h b/src/util/options.h index 676dc0059..b71acd982 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -18,7 +18,6 @@ #include #include "parser/parser.h" -#include "prop/cnf_conversion.h" namespace CVC4 { @@ -42,9 +41,6 @@ struct CVC4_PUBLIC Options { /** The input language */ parser::Parser::InputLanguage lang; - /** The CNF conversion */ - CVC4::CnfConversion d_cnfConversion; - /** Should we exit after parsing? */ bool parseOnly; @@ -61,7 +57,6 @@ struct CVC4_PUBLIC Options { err(0), verbosity(0), lang(parser::Parser::LANG_AUTO), - d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION), parseOnly(false), semanticChecks(true), memoryMap(false) diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 8caec4f40..967d6a8c8 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -7,6 +7,7 @@ UNIT_TESTS = \ parser/parser_black \ context/context_black \ context/context_mm_black \ + context/cdlist_black \ theory/theory_black \ theory/theory_uf_white \ util/assert_white \ diff --git a/test/unit/context/cdlist_black.h b/test/unit/context/cdlist_black.h new file mode 100644 index 000000000..560c70722 --- /dev/null +++ b/test/unit/context/cdlist_black.h @@ -0,0 +1,72 @@ +/********************* */ +/** cdlist_black.h + ** Original author: dejan + ** Major contributors: none + ** Minor contributors (to current version): mdeters + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 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. + ** + ** Black box testing of CVC4::context::CDList<>. + **/ + +#include + +#include +#include +#include "context/context.h" +#include "context/cdlist.h" + +using namespace std; +using namespace CVC4::context; + +class CDListBlack : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context(); + } + + // test at different sizes. this triggers grow() behavior differently. + // grow() is completely broken in revision 256; fix forthcoming by Tim + void testCDList10() { listTest(10); } + void testCDList15() { listTest(15); } + void testCDList20() { listTest(20); } + void testCDList35() { listTest(35); } + void testCDList50() { listTest(50); } + void testCDList99() { listTest(99); } + + void listTest(int N) { + CDList list(d_context); + + TS_ASSERT(list.empty()); + for(int i = 0; i < N; ++i) { + TS_ASSERT(list.size() == i); + list.push_back(i); + TS_ASSERT(!list.empty()); + TS_ASSERT(list.back() == i); + int i2 = 0; + for(CDList::const_iterator j = list.begin(); + j != list.end(); + ++j) { + TS_ASSERT(*j == i2++); + } + } + TS_ASSERT(list.size() == N); + + for(int i = 0; i < N; ++i) { + TS_ASSERT(list[i] == i); + } + } + + void tearDown() { + delete d_context; + } +}; diff --git a/test/unit/context/context_black.h b/test/unit/context/context_black.h index 64ad2d7f7..f06ed9f42 100644 --- a/test/unit/context/context_black.h +++ b/test/unit/context/context_black.h @@ -10,17 +10,20 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Black box testing of CVC4::Node. + ** Black box testing of CVC4::context::Context. **/ #include -//Used in some of the tests #include #include #include "context/context.h" +#include "context/cdlist.h" +#include "context/cdo.h" +#include "util/Assert.h" using namespace std; +using namespace CVC4; using namespace CVC4::context; class ContextBlack : public CxxTest::TestSuite { @@ -31,7 +34,7 @@ private: public: void setUp() { - d_context = new Context(); + d_context = new Context; } void testIntCDO() { @@ -53,40 +56,8 @@ public: // the interface doesn't declare any exceptions d_context->push(); d_context->pop(); -// d_context->pop(); -// d_context->pop(); - } - - // test at different sizes. this triggers grow() behavior differently. - // grow() is completely broken in revision 256; fix forthcoming by Tim - void testCDList10() { listTest(10); } - void testCDList15() { listTest(15); } - void testCDList20() { listTest(20); } - void testCDList35() { listTest(35); } - void testCDList50() { listTest(50); } - void testCDList99() { listTest(99); } - - void listTest(int N) { - CDList list(d_context); - - TS_ASSERT(list.empty()); - for(int i = 0; i < N; ++i) { - TS_ASSERT(list.size() == i); - list.push_back(i); - TS_ASSERT(!list.empty()); - TS_ASSERT(list.back() == i); - int i2 = 0; - for(CDList::const_iterator j = list.begin(); - j != list.end(); - ++j) { - TS_ASSERT(*j == i2++); - } - } - TS_ASSERT(list.size() == N); - - for(int i = 0; i < N; ++i) { - TS_ASSERT(list[i] == i); - } + TS_ASSERT_THROWS( d_context->pop(), AssertionException ); + TS_ASSERT_THROWS( d_context->pop(), AssertionException ); } void tearDown() { diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c11d5cf86..96f02c489 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -27,24 +27,28 @@ using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::context; using namespace std; class NodeBlack : public CxxTest::TestSuite { private: - NodeManager *d_nodeManager; - NodeManagerScope *d_scope; + Context* d_ctxt; + NodeManager* d_nodeManager; + NodeManagerScope* d_scope; public: void setUp() { - d_nodeManager = new NodeManager(); + d_ctxt = new Context; + d_nodeManager = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nodeManager); } void tearDown() { delete d_scope; delete d_nodeManager; + delete d_ctxt; } bool imp(bool a, bool b) const { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 871e93dca..ab3c1c842 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -23,29 +23,34 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/kind.h" +#include "context/context.h" #include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::context; using namespace std; class NodeBuilderBlack : public CxxTest::TestSuite { private: - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; public: void setUp() { - d_nm = new NodeManager(); + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); specKind = PLUS; } void tearDown() { - delete d_nm; delete d_scope; + delete d_nm; + delete d_ctxt; } @@ -609,20 +614,37 @@ public: f, d_nm->mkNode(AND, q, a))); - Node assoc1 = (a && b) && c; - Node assoc2 = a && (b && c); - - TS_ASSERT_EQUALS(assoc1, d_nm->mkNode(AND, a, b, c)); - TS_ASSERT_EQUALS(assoc2, d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); - - Node prec1 = (a && b) || c; - Node prec2 = a || (b && c); - Node prec3 = a && (b || c); - Node prec4 = (a || b) && c; - - TS_ASSERT_EQUALS(prec1, d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); - TS_ASSERT_EQUALS(prec2, d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); - TS_ASSERT_EQUALS(prec3, d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); - TS_ASSERT_EQUALS(prec4, d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); + TS_ASSERT_EQUALS(Node((a && b) && c), d_nm->mkNode(AND, a, b, c)); + TS_ASSERT_EQUALS(Node(a && (b && c)), d_nm->mkNode(AND, a, d_nm->mkNode(AND, b, c))); + TS_ASSERT_EQUALS(Node((a || b) || c), d_nm->mkNode(OR, a, b, c)); + TS_ASSERT_EQUALS(Node(a || (b || c)), d_nm->mkNode(OR, a, d_nm->mkNode(OR, b, c))); + TS_ASSERT_EQUALS(Node((a && b) || c), d_nm->mkNode(OR, d_nm->mkNode(AND, a, b), c)); + TS_ASSERT_EQUALS(Node(a && (b || c)), d_nm->mkNode(AND, a, d_nm->mkNode(OR, b, c))); + TS_ASSERT_EQUALS(Node((a || b) && c), d_nm->mkNode(AND, d_nm->mkNode(OR, a, b), c)); + TS_ASSERT_EQUALS(Node(a || (b && c)), d_nm->mkNode(OR, a, d_nm->mkNode(AND, b, c))); + + TS_ASSERT_EQUALS(Node((a + b) + c), d_nm->mkNode(PLUS, a, b, c)); + TS_ASSERT_EQUALS(Node(a + (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, c))); + TS_ASSERT_EQUALS(Node((a - b) - c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), d_nm->mkNode(UMINUS, c))); + TS_ASSERT_EQUALS(Node(a - (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c))))); + TS_ASSERT_EQUALS(Node((a * b) * c), d_nm->mkNode(MULT, a, b, c)); + TS_ASSERT_EQUALS(Node(a * (b * c)), d_nm->mkNode(MULT, a, d_nm->mkNode(MULT, b, c))); + TS_ASSERT_EQUALS(Node((a + b) - c), d_nm->mkNode(PLUS, a, b, d_nm->mkNode(UMINUS, c))); + TS_ASSERT_EQUALS(Node(a + (b - c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))); + TS_ASSERT_EQUALS(Node((a - b) + c), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b), c)); + TS_ASSERT_EQUALS(Node(a - (b + c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(PLUS, b, c)))); + TS_ASSERT_EQUALS(Node((a + b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, b), c)); + TS_ASSERT_EQUALS(Node(a + (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(MULT, b, c))); + TS_ASSERT_EQUALS(Node((a - b) * c), d_nm->mkNode(MULT, d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, b)), c)); + TS_ASSERT_EQUALS(Node(a - (b * c)), d_nm->mkNode(PLUS, a, d_nm->mkNode(UMINUS, d_nm->mkNode(MULT, b, c)))); + TS_ASSERT_EQUALS(Node((a * b) + c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), c)); + TS_ASSERT_EQUALS(Node(a * (b + c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, c))); + TS_ASSERT_EQUALS(Node((a * b) - c), d_nm->mkNode(PLUS, d_nm->mkNode(MULT, a, b), d_nm->mkNode(UMINUS, c))); + TS_ASSERT_EQUALS(Node(a * (b - c)), d_nm->mkNode(MULT, a, d_nm->mkNode(PLUS, b, d_nm->mkNode(UMINUS, c)))); + + TS_ASSERT_EQUALS(Node(-a), d_nm->mkNode(UMINUS, a)); + TS_ASSERT_EQUALS(Node(- a - b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), d_nm->mkNode(UMINUS, b))); + TS_ASSERT_EQUALS(Node(- a + b), d_nm->mkNode(PLUS, d_nm->mkNode(UMINUS, a), b)); + TS_ASSERT_EQUALS(Node(- a * b), d_nm->mkNode(MULT, d_nm->mkNode(UMINUS, a), b)); } }; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 871abe232..88ae5253f 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -22,9 +22,12 @@ #include "expr/node_manager.h" #include "expr/node.h" #include "expr/attribute.h" +#include "context/context.h" +#include "util/Assert.h" using namespace CVC4; using namespace CVC4::kind; +using namespace CVC4::context; using namespace CVC4::expr; using namespace CVC4::expr::attr; using namespace std; @@ -41,39 +44,33 @@ typedef Attribute TestStringAttr2; // it would be nice to have CDAttribute<> for context-dependence typedef CDAttribute TestCDFlag; -struct ecdata; -struct cleanupfcn { - static void cleanup(ecdata* ec) { /* clean up */ } -}; - -// ManagedAttribute<> has a cleanup function deleting the value -typedef ManagedAttribute TestECDataAttr; - typedef Attribute TestFlag1; typedef Attribute TestFlag2; typedef Attribute TestFlag3; typedef Attribute TestFlag4; typedef Attribute TestFlag5; -struct FooBar {}; -struct Test6; -typedef Attribute TestFlag6; +typedef CDAttribute TestFlag1cd; +typedef CDAttribute TestFlag2cd; class NodeWhite : public CxxTest::TestSuite { - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; public: void setUp() { - d_nm = new NodeManager(); + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); } void tearDown() { delete d_scope; delete d_nm; + delete d_ctxt; } void testNull() { @@ -96,16 +93,149 @@ public: TS_ASSERT(VarNameAttr::s_id == 0); TS_ASSERT(TestStringAttr1::s_id == 1); TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT(attr::LastAttributeId::s_id == 3); + TS_ASSERT((attr::LastAttributeId::s_id == 3)); TS_ASSERT(TypeAttr::s_id == 0); - TS_ASSERT(attr::LastAttributeId::s_id == 1); + TS_ASSERT((attr::LastAttributeId::s_id == 1)); TS_ASSERT(TestFlag1::s_id == 0); TS_ASSERT(TestFlag2::s_id == 1); TS_ASSERT(TestFlag3::s_id == 2); TS_ASSERT(TestFlag4::s_id == 3); TS_ASSERT(TestFlag5::s_id == 4); + TS_ASSERT((attr::LastAttributeId::s_id == 5)); + + TS_ASSERT(TestFlag1cd::s_id == 0); + TS_ASSERT(TestFlag2cd::s_id == 1); + TS_ASSERT((attr::LastAttributeId::s_id == 2)); + } + + void testCDAttributes() { + AttributeManager& am = d_nm->d_attrManager; + + //Debug.on("boolattr"); + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 1 + + // test that all boolean flags are FALSE to start + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + // test that they all HAVE the boolean attributes + TS_ASSERT(a.hasAttribute(TestFlag1cd())); + TS_ASSERT(b.hasAttribute(TestFlag1cd())); + TS_ASSERT(c.hasAttribute(TestFlag1cd())); + + // test two-arg version of hasAttribute() + bool bb; + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + + // setting boolean flags + Debug("boolattr", "set flag 1 on a to T\n"); + a.setAttribute(TestFlag1cd(), true); + Debug("boolattr", "set flag 1 on b to F\n"); + b.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on c to F\n"); + c.setAttribute(TestFlag1cd(), false); + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on a to F\n"); + a.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on b to T\n"); + b.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 3 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on c to T\n"); + c.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 1 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 0 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); } void testAttributes() { @@ -169,49 +299,29 @@ public: TS_ASSERT(! unnamed.getAttribute(TestFlag5())); // test that they all HAVE the boolean attributes - Debug("boolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag1())); - Debug("boolattr", "get flag 2 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag2())); - Debug("boolattr", "get flag 3 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag3())); - Debug("boolattr", "get flag 4 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag4())); - Debug("boolattr", "get flag 5 on a (should be F)\n"); TS_ASSERT(a.hasAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on b (should be F)\n"); TS_ASSERT(b.hasAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on c (should be F)\n"); TS_ASSERT(c.hasAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); TS_ASSERT(unnamed.hasAttribute(TestFlag5())); // test two-arg version of hasAttribute() @@ -465,6 +575,5 @@ public: TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - } }; diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 17fefd07b..908ab81fc 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -87,8 +87,9 @@ public: set d_registered; vector d_getSequence; - DummyTheory(context::Context* ctxt, OutputChannel& out) : - TheoryImpl(ctxt, out) {} + DummyTheory(Context* ctxt, OutputChannel& out) : + TheoryImpl(ctxt, out) { + } void registerTerm(TNode n) { // check that we registerTerm() a term only once @@ -125,13 +126,12 @@ public: class TheoryBlack : public CxxTest::TestSuite { - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; TestOutputChannel d_outputChannel; - Context* d_context; - DummyTheory* d_dummy; Node atom0; @@ -139,28 +139,23 @@ class TheoryBlack : public CxxTest::TestSuite { public: - TheoryBlack() {} - void setUp() { - d_nm = new NodeManager(); - + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - - d_context = new Context(); - - d_dummy = new DummyTheory(d_context, d_outputChannel); - + d_dummy = new DummyTheory(d_ctxt, d_outputChannel); d_outputChannel.clear(); - atom0 = d_nm->mkNode(kind::TRUE); atom1 = d_nm->mkNode(kind::FALSE); } void tearDown() { + atom1 = Node::null(); + atom0 = Node::null(); delete d_dummy; - delete d_context; delete d_scope; delete d_nm; + delete d_ctxt; } void testEffort(){ diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index fe2c8d821..86266e923 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -36,10 +36,10 @@ using namespace std; * Very basic OutputChannel for testing simple Theory Behaviour. * Stores a call sequence for the output channel */ -enum OutputChannelCallType{CONFLICT, PROPOGATE, LEMMA, EXPLANATION}; +enum OutputChannelCallType { CONFLICT, PROPOGATE, LEMMA, EXPLANATION }; class TestOutputChannel : public OutputChannel { private: - void push(OutputChannelCallType call, TNode n){ + void push(OutputChannelCallType call, TNode n) { d_callHistory.push_back(make_pair(call,n)); } public: @@ -51,71 +51,71 @@ public: void safePoint() throw(Interrupted) {} - void conflict(TNode n, bool safe = false) throw(Interrupted){ + void conflict(TNode n, bool safe = false) throw(Interrupted) { push(CONFLICT, n); } - void propagate(TNode n, bool safe = false) throw(Interrupted){ + void propagate(TNode n, bool safe = false) throw(Interrupted) { push(PROPOGATE, n); } - void lemma(TNode n, bool safe = false) throw(Interrupted){ + void lemma(TNode n, bool safe = false) throw(Interrupted) { push(LEMMA, n); } - void explanation(TNode n, bool safe = false) throw(Interrupted){ + void explanation(TNode n, bool safe = false) throw(Interrupted) { push(EXPLANATION, n); } - void clear(){ + void clear() { d_callHistory.clear(); } - Node getIthNode(int i){ + + Node getIthNode(int i) { Node tmp = (d_callHistory[i]).second; return tmp; } - OutputChannelCallType getIthCallType(int i){ + OutputChannelCallType getIthCallType(int i) { return (d_callHistory[i]).first; } - unsigned getNumCalls(){ + unsigned getNumCalls() { return d_callHistory.size(); } }; class TheoryUFWhite : public CxxTest::TestSuite { - NodeManagerScope *d_scope; - NodeManager *d_nm; + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; TestOutputChannel d_outputChannel; - Theory::Effort level; + Theory::Effort d_level; - Context* d_context; TheoryUF* d_euf; public: - TheoryUFWhite(): level(Theory::FULL_EFFORT) { } + TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {} void setUp() { - d_nm = new NodeManager(); + d_ctxt = new Context; + d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - - d_context = new Context(); - d_outputChannel.clear(); - d_euf = new TheoryUF(d_context, d_outputChannel); + d_euf = new TheoryUF(d_ctxt, d_outputChannel); } void tearDown() { delete d_euf; - delete d_context; + d_outputChannel.clear(); delete d_scope; delete d_nm; + delete d_ctxt; } - void testPushPopChain(){ + void testPushPopChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); @@ -140,26 +140,26 @@ public: d_euf->assertFact( f3_x_eq_x ); d_euf->assertFact( f1_x_neq_x ); - d_euf->check(level); - d_context->push(); + d_euf->check(d_level); + d_ctxt->push(); d_euf->assertFact( f5_x_eq_x ); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); Node realConflict = d_outputChannel.getIthNode(0); TS_ASSERT_EQUALS(expectedConflict, realConflict); - d_context->pop(); - d_euf->check(level); + d_ctxt->pop(); + d_euf->check(d_level); //Test that no additional calls to the output channel occurred. TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); d_euf->assertFact( f5_x_eq_x ); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); @@ -174,7 +174,7 @@ public: /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */ - void testSimpleChain(){ + void testSimpleChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); @@ -188,7 +188,7 @@ public: d_euf->assertFact(f_f_x_eq_x); d_euf->assertFact(f_f_f_x_neq_f_x); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); @@ -199,13 +199,13 @@ public: } /* test that !(x == x) is inconsistent */ - void testSelfInconsistent(){ + void testSelfInconsistent() { Node x = d_nm->mkVar(); Node x_neq_x = (x.eqNode(x)).notNode(); Node and_x_neq_x = d_nm->mkNode(kind::AND, x_neq_x); d_euf->assertFact(x_neq_x); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(and_x_neq_x, d_outputChannel.getIthNode(0)); @@ -213,12 +213,12 @@ public: } /* test that (x == x) is consistent */ - void testSelfConsistent(){ + void testSelfConsistent() { Node x = d_nm->mkVar(); Node x_eq_x = x.eqNode(x); d_euf->assertFact(x_eq_x); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(0, d_outputChannel.getNumCalls()); } @@ -229,7 +229,7 @@ public: f(f(f(f(f(x))))) = x, f(x) != x } is inconsistent */ - void testChain(){ + void testChain() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); @@ -251,7 +251,7 @@ public: d_euf->assertFact( f3_x_eq_x ); d_euf->assertFact( f5_x_eq_x ); d_euf->assertFact( f1_x_neq_x ); - d_euf->check(level); + d_euf->check(d_level); TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); @@ -260,28 +260,28 @@ public: } - void testPushPopA(){ + void testPushPopA() { Node x = d_nm->mkVar(); Node x_eq_x = x.eqNode(x); - d_context->push(); + d_ctxt->push(); d_euf->assertFact( x_eq_x ); - d_euf->check(level); - d_context->pop(); - d_euf->check(level); + d_euf->check(d_level); + d_ctxt->pop(); + d_euf->check(d_level); } - void testPushPopB(){ + void testPushPopB() { Node x = d_nm->mkVar(); Node f = d_nm->mkVar(); Node f_x = d_nm->mkNode(kind::APPLY, f, x); Node f_x_eq_x = f_x.eqNode(x); d_euf->assertFact( f_x_eq_x ); - d_context->push(); - d_euf->check(level); - d_context->pop(); - d_euf->check(level); + d_ctxt->push(); + d_euf->check(d_level); + d_ctxt->pop(); + d_euf->check(d_level); } -- 2.30.2