-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 <mdeters@cs.nyu.edu> 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 <mdeters@cs.nyu.edu> 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
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.
+
+++ /dev/null
-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
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
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=
AC_MSG_RESULT([$enable_coverage])
if test "$enable_coverage" = yes; then
+ CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE"
CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
fi
AC_MSG_RESULT([$enable_profiling])
if test "$enable_profiling" = yes; then
+ CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING"
CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
CVC4LDFLAGS="$CVC4LDFLAGS -pg"
fi
--- /dev/null
+#!/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 = <FP>;
+ 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 = <FP>;
+ 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</;
+ print "need space between tokens } and 'else'\n" if $buf =~ /\}else\b/;
+ print "need space between tokens 'else' and {\n" if $buf =~ /\belse\{/;
+ print "need space between tokens 'do' and {\n" if $buf =~ /\bdo\{/;
+ print "need space between tokens } and 'while'\n" if $buf =~ /\}while\b/;
+
+ print "no space permitted before ;\n" if $buf =~ /\s+;/;
+ print "no space permitted between tokens 'if' and (\n" if $buf =~ /\bif\s\(/;
+ print "no space permitted between tokens 'while' and (\n" if $buf =~ /\bwhile\s\(/;
+ print "no space permitted between tokens 'for' and (\n" if $buf =~ /\bfor\s\(/;
+
+ my $code = $buf;
+ $code =~ s,\\.,.,g;
+ $code =~ s,"[^"]*","",g;
+
+ #print "'if' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bif\b.*[^{]\s*$/m;
+ #print "'while' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bwhile\b.*[^{]\s*$/m;
+ #print "'for' blocks must be braced, '{' should be last character on block opening line\n" if $code =~ /\bfor\b.*[^{]\s*$/m;
+ print "'else' cannot start a line (should follow preceding '}')\n" if $code =~ /^\s+else\b/m;
+}
+
+sub check_as_header_cpp {
+ my($buf) = @_;
+ check_as_any_cpp($buf);
+}
+
+sub check_as_source_cpp {
+ my($buf) = @_;
+ check_as_any_cpp($buf);
+}
+
+## Local Variables:
+## perl-indent-level: 2
+## perl-brace-offset: 0
+## End:
--- /dev/null
+indent -l 80 -lc 80 -lps -bli 2 -bbo -nbbb -bap -bad -br -brf -brs -cbi 1 -ce -cdw -cli 0 -hnl -i 2 -il 0 -lp -ci 0 -nut -ss -npro -npcs -nprs -npsl -nsaf -nsai -nsaw -sc -cd0 -dj0
context.cpp \
context.h \
context_mm.cpp \
- context_mm.h
-
+ context_mm.h \
+ cdo.h \
+ cdlist.h \
+ cdmap.h \
+ cdset.h
--- /dev/null
+/********************* */
+/** cdlist.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 list class.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__CONTEXT__CDLIST_H
+#define __CVC4__CONTEXT__CDLIST_H
+
+#include "context/context.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+namespace context {
+
+/**
+ * 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 T>
+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<T>(*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<T>*)data)->d_size;
+ while(d_size != size) {
+ --d_size;
+ d_list[d_size].~T();
+ }
+ } else {
+ d_size = ((CDList<T>*)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<T>& 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>;
+ 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 */
--- /dev/null
+/********************* */
+/** 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 <iterator>
+#include <ext/hash_map>
+
+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 Key, class Data, class HashFcn = __gnu_cxx::hash<Key> > class CDMap;
+
+template <class Key, class Data, class HashFcn = __gnu_cxx::hash<Key> >
+class CDOmap : public ContextObj {
+ Key d_key;
+ Data d_data;
+ bool d_inMap; // whether the data must be in the map
+ CDMap<Key, Data, HashFcn>* d_cdmap;
+
+ // Doubly-linked list for keeping track of elements in order of insertion
+ CDOmap<Key, Data, HashFcn>* d_prev;
+ CDOmap<Key, Data, HashFcn>* d_next;
+
+ virtual ContextObj* save(ContextMemoryManager* pCMM) {
+ return new(pCMM) CDOmap<Key, Data, HashFcn>(*this);
+ }
+
+ virtual void restore(ContextObj* data) {
+ CDOmap<Key, Data, HashFcn>* p((CDOmap<Key, Data, HashFcn>*) 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<Key, Data, HashFcn>* cdmap,
+ const Key& key,
+ const Data& data) :
+ ContextObj(context),
+ d_key(key),
+ d_inMap(false),
+ d_cdmap(cdmap) {
+
+ set(data);
+
+ CDOmap<Key, Data, HashFcn>*& 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<Key, Data, HashFcn>& operator=(const Data& data) {
+ set(data);
+ return *this;
+ }
+
+ CDOmap<Key, Data, HashFcn>* 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 <class Key, class Data, class HashFcn>
+ 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 Key, class Data, class HashFcn>
+class CDMap : public ContextObj {
+
+ friend class CDOmap<Key, Data, HashFcn>;
+
+ __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn> d_map;
+
+ // The vector of CDOmap objects to be destroyed
+ std::vector<CDOmap<Key, Data, HashFcn>*> d_trash;
+ CDOmap<Key, Data, HashFcn>* 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<CDOmap<Key, Data, HashFcn>*>::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<Key, CDOmap<Key, Data, HashFcn>*, 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<Key, Data, HashFcn>& ElementReference;
+
+ // If a key is not present, a new object is created and inserted
+ CDOmap<Key, Data, HashFcn>& operator[](const Key& k) {
+ emptyTrash();
+
+ typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+ i(d_map.find(k));
+
+ CDOmap<Key, Data, HashFcn>* obj;
+ if(i == d_map.end()) { // Create new object
+ obj = new(true) CDOmap<Key, Data, HashFcn>(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<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::iterator
+ i(d_map.find(k));
+
+ if(i == d_map.end()) { // Create new object
+ CDOmap<Key, Data, HashFcn>*
+ obj(new(true) CDOmap<Key, Data, HashFcn>(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<const Key, CDOMap<Key, Data, HashFcn>&>;
+ // in most cases, this will be functionally similar to pair<const Key, Data>.
+ class iterator : public std::iterator<std::input_iterator_tag, std::pair<const Key, Data>, std::ptrdiff_t> {
+
+ // Private members
+ typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, HashFcn>::const_iterator d_it;
+
+ public:
+
+ // Constructor from __gnu_cxx::hash_map
+ iterator(const typename __gnu_cxx::hash_map<Key, CDOmap<Key, Data, HashFcn>*, 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<const Key, Data> operator*() const {
+ const std::pair<const Key, CDOmap<Key, Data, HashFcn>*>& p(*d_it);
+ return std::pair<const Key, Data>(p.first, *p.second);
+ }
+
+ // Who needs an operator->() for maps anyway?...
+ // It'd be nice, but not possible by design.
+ //std::pair<const Key, Data>* 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<const Key, Data>* d_pair;
+ public:
+ Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
+ std::pair<const Key, Data>& 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<Key, Data, HashFcn>* d_it;
+
+ public:
+
+ orderedIterator(const CDOmap<Key, Data, HashFcn>* 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<const Key, Data> operator*() const {
+ return std::pair<const Key, Data>(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<const Key, Data>* d_pair;
+
+ public:
+
+ Proxy(const std::pair<const Key, Data>& p): d_pair(&p) {}
+
+ std::pair<const Key, Data>& 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 */
--- /dev/null
+/********************* */
+/** 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 T>
+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<T>(*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<T>*) 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<T>& cdo) : ContextObj(cdo), d_data(cdo.d_data) {}
+
+ /**
+ * operator= for CDO is private to ensure CDO object is not copied.
+ */
+ CDO<T>& operator=(const CDO<T>& 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<T>& operator=(const T& data) {
+ set(data);
+ return *this;
+ }
+
+};/* class CDO */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDO_H */
--- /dev/null
+/********************* */
+/** 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 K, class HashFcn>
+class CDSet;
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__CONTEXT__CDSET_H */
}
-Context::~Context() {
+Context::~Context() throw(AssertionException) {
// Delete all Scopes
popto(0);
// 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;
// Notify the (pre-pop) ContextNotifyObj objects
ContextNotifyObj* pCNO = d_pCNOpre;
- while (pCNO != NULL) {
+ while(pCNO != NULL) {
pCNO->notify();
pCNO = pCNO->d_pCNOnext;
}
// Notify the (post-pop) ContextNotifyObj objects
pCNO = d_pCNOpost;
- while (pCNO != NULL) {
+ while(pCNO != NULL) {
pCNO->notify();
pCNO = pCNO->d_pCNOnext;
}
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();
}
}
-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);
}
-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 */
#include "context/context_mm.h"
#include "util/Assert.h"
+
#include <cstdlib>
#include <cstring>
#include <new>
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 {
/**
/**
* Destructor: pop all scopes, delete ContextMemoryManager
*/
- ~Context();
+ ~Context() throw(AssertionException);
/**
* Return the current (top) scope
/**
* 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
* 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
* 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
* 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.
ContextObj* restoreAndContinue();
protected:
+
/**
* This is a method that must be implemented by all classes inheriting from
* ContextObj. See the comment before the class declaration.
* 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
* 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
* 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;
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
// 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();
}
}
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 T>
-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<T>(*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<T>*)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<T>& cdo): ContextObj(cdo), d_data(cdo.d_data) { }
-
- /**
- * operator= for CDO is private to ensure CDO object is not copied.
- */
- CDO<T>& operator=(const CDO<T>& 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<T>& 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 T>
-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<T>(*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<T>*)data)->d_size;
- while (d_size != size) {
- --d_size;
- d_list[d_size].~T();
- }
- }
- else {
- d_size = ((CDList<T>*)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<T>& 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>;
- 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 T>
-class CDMap;
-
-template <class T>
-class CDSet;
-
-} /* CVC4::context namespace */
-
-} /* CVC4 namespace */
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
#endif /* __CVC4__CONTEXT__CONTEXT_H */
-
"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();
}
}
// 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;
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;
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();
}
} /* CVC4::context namespace */
-
-
} /* CVC4 namespace */
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 {
/**
void newChunk();
public:
+
/**
* Constructor - creates an initial region and an empty stack
*/
/**
* Destructor - deletes all memory in all regions
*/
- ~ContextMemoryManager();
+ ~ContextMemoryManager() throw();
/**
* Allocate size bytes from the current region
*/
void pop();
-}; /* class ContextMemoryManager */
+};/* class ContextMemoryManager */
}/* CVC4::context namespace */
}/* CVC4 namespace */
#include <ext/hash_map>
#include "config.h"
-#include "context/context.h"
+#include "context/cdmap.h"
#include "expr/node.h"
#include "expr/type.h"
}
};/* class AttrHash<bool> */
+/**
+ * A "CDAttrHash<value_type>"---the hash table underlying
+ * attributes---is simply a context-dependent mapping of
+ * pair<unique-attribute-id, Node> to value_type using our specialized
+ * hash function for these pairs.
+ */
+template <class value_type>
+class CDAttrHash :
+ public CVC4::context::CDMap<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashFcn> {
+public:
+ CDAttrHash(context::Context* ctxt) :
+ context::CDMap<std::pair<uint64_t, NodeValue*>,
+ value_type,
+ AttrHashFcn>(ctxt) {
+ }
+};
+
}/* CVC4::expr::attr namespace */
// ATTRIBUTE CLEANUP FUNCTIONS =================================================
/** Default cleanup for unmanaged Attribute<> */
template <class T>
struct AttributeCleanupFcn {
- inline void cleanup(const T&) {}
+ static inline void cleanup(const T&) {}
};
/** Default cleanup for ManagedAttribute<> */
/** Specialization for T* */
template <class T>
struct ManagedAttributeCleanupFcn<T*> {
- inline void cleanup(T* p) { delete p; }
+ static inline void cleanup(T* p) { delete p; }
};
/** Specialization for const T* */
template <class T>
struct ManagedAttributeCleanupFcn<const T*> {
- inline void cleanup(const T* p) { delete p; }
+ static inline void cleanup(const T* p) { delete p; }
};
}/* CVC4::expr::attr namespace */
* 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 <class T,
class value_t,
class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
- bool context_dependent = false>
+ bool context_dep = false>
struct Attribute {
/** The value type for this 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:
/**
/**
* An "attribute type" structure for boolean flags (special).
*/
-template <class T, class CleanupFcn, bool context_dependent>
-struct Attribute<T, bool, CleanupFcn, context_dependent> {
+template <class T, class CleanupFcn, bool context_dep>
+struct Attribute<T, bool, CleanupFcn, context_dep> {
/** The value type for this attribute; here, bool. */
typedef bool value_type;
*/
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.
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 <class T,
class value_type>
struct CDAttribute :
public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, 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 <class T,
class value_type,
class CleanupFcn = attr::ManagedAttributeCleanupFcn<value_type> >
* This is the last-attribute-assigner. IDs are not globally
* unique; rather, they are unique for each table_value_type.
*/
-template <class T>
+template <class T, bool context_dep>
struct LastAttributeId {
static uint64_t s_id;
};
/** Initially zero. */
-template <class T>
-uint64_t LastAttributeId<T>::s_id = 0;
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::s_id = 0;
}/* CVC4::expr::attr namespace */
/** Assign unique IDs to attributes at load time. */
-template <class T, class value_t, class CleanupFcn, bool context_dependent>
-const uint64_t Attribute<T, value_t, CleanupFcn, context_dependent>::s_id =
- attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
+template <class T, class value_t, class CleanupFcn, bool context_dep>
+const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
+ attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::s_id++;
/**
* Assign unique IDs to bool-valued attributes at load time, checking
* that they are in range.
*/
-template <class T, class CleanupFcn, bool context_dependent>
-const uint64_t Attribute<T, bool, CleanupFcn, context_dependent>::s_id =
- Attribute<T, bool, CleanupFcn, context_dependent>::checkID(attr::LastAttributeId<bool>::s_id++);
+template <class T, class CleanupFcn, bool context_dep>
+const uint64_t Attribute<T, bool, CleanupFcn, context_dep>::s_id =
+ Attribute<T, bool, CleanupFcn, context_dep>::checkID(attr::LastAttributeId<bool, context_dep>::s_id++);
// ATTRIBUTE MANAGER ===========================================================
class AttributeManager {
/** Underlying hash table for boolean-valued attributes */
- AttrHash<bool> d_bools;
+ AttrHash<bool> d_bools;
/** Underlying hash table for integral-valued attributes */
- AttrHash<uint64_t> d_ints;
+ AttrHash<uint64_t> d_ints;
/** Underlying hash table for node-valued attributes */
- AttrHash<TNode> d_exprs;
+ AttrHash<TNode> d_exprs;
/** Underlying hash table for string-valued attributes */
AttrHash<std::string> d_strings;
/** Underlying hash table for pointer-valued attributes */
- AttrHash<void*> d_ptrs;
+ AttrHash<void*> d_ptrs;
+
+ /** Underlying hash table for context-dependent boolean-valued attributes */
+ CDAttrHash<bool> d_cdbools;
+ /** Underlying hash table for context-dependent integral-valued attributes */
+ CDAttrHash<uint64_t> d_cdints;
+ /** Underlying hash table for context-dependent node-valued attributes */
+ CDAttrHash<TNode> d_cdexprs;
+ /** Underlying hash table for context-dependent string-valued attributes */
+ CDAttrHash<std::string> d_cdstrings;
+ /** Underlying hash table for context-dependent pointer-valued attributes */
+ CDAttrHash<void*> d_cdptrs;
/**
* getTable<> is a helper template that gets the right table from an
* AttributeManager given its type.
*/
- template <class T>
+ template <class T, bool context_dep>
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.
* The getTable<> template provides (static) access to the
* AttributeManager field holding the table.
*/
-template <class T>
+template <class T, bool context_dep>
struct getTable;
/** Access the "d_bools" member of AttributeManager. */
template <>
-struct getTable<bool> {
+struct getTable<bool, false> {
typedef AttrHash<bool> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_bools;
/** Access the "d_ints" member of AttributeManager. */
template <>
-struct getTable<uint64_t> {
+struct getTable<uint64_t, false> {
typedef AttrHash<uint64_t> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ints;
/** Access the "d_exprs" member of AttributeManager. */
template <>
-struct getTable<Node> {
+struct getTable<Node, false> {
typedef AttrHash<TNode> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_exprs;
/** Access the "d_strings" member of AttributeManager. */
template <>
-struct getTable<std::string> {
+struct getTable<std::string, false> {
typedef AttrHash<std::string> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_strings;
/** Access the "d_ptrs" member of AttributeManager. */
template <class T>
-struct getTable<T*> {
+struct getTable<T*, false> {
typedef AttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ptrs;
/** Access the "d_ptrs" member of AttributeManager. */
template <class T>
-struct getTable<const T*> {
+struct getTable<const T*, false> {
typedef AttrHash<void*> table_type;
static inline table_type& get(AttributeManager& am) {
return am.d_ptrs;
}
};
+/** Access the "d_cdbools" member of AttributeManager. */
+template <>
+struct getTable<bool, true> {
+ typedef CDAttrHash<bool> 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<uint64_t, true> {
+ typedef CDAttrHash<uint64_t> 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<Node, true> {
+ typedef CDAttrHash<TNode> 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<std::string, true> {
+ typedef CDAttrHash<std::string> 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 <class T>
+struct getTable<T*, true> {
+ typedef CDAttrHash<void*> 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 <class T>
+struct getTable<const T*, true> {
+ typedef CDAttrHash<void*> 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 ===========================================
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
- const table_type& ah = getTable<value_type>::get(*this);
+ const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), n.d_nv));
if(i == ah.end()) {
typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
- const table_type& ah = getTable<value_type>::get(*am);
+ const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
NodeValue* nv) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
- const table_type& ah = getTable<value_type>::get(*am);
+ const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
typename AttrKind::value_type& ret) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
- const table_type& ah = getTable<value_type>::get(*am);
+ const table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*am);
typename table_type::const_iterator i = ah.find(std::make_pair(AttrKind::getId(), nv));
if(i == ah.end()) {
typedef typename AttrKind::value_type value_type;
typedef KindValueToTableValueMapping<value_type> mapping;
- typedef typename getTable<value_type>::table_type table_type;
+ typedef typename getTable<value_type, AttrKind::context_dependent>::table_type table_type;
- table_type& ah = getTable<value_type>::get(*this);
+ table_type& ah = getTable<value_type, AttrKind::context_dependent>::get(*this);
ah[std::make_pair(AttrKind::getId(), n.d_nv)] = mapping::convert(value);
}
namespace CVC4 {
ostream& operator<<(ostream& out, const Command* command) {
- if (command == NULL) {
+ if(command == NULL) {
out << "null";
} else {
command->toStream(out);
}
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!");
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;
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();
#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 {
return d_nodeManager;
}
-} // End namespace CVC4
+Context* ExprManager::getContext() const {
+ return d_ctxt;
+}
+
+}/* CVC4 namespace */
class SmtEngine;
class NodeManager;
+namespace context {
+ class Context;
+}/* CVC4::context namespace */
+
class CVC4_PUBLIC ExprManager {
public:
/** Make a function type with input types from argTypes. */
const FunctionType*
- mkFunctionType(const std::vector<const Type*>& argTypes,
+ mkFunctionType(const std::vector<const Type*>& argTypes,
const Type* range);
/** Make a new sort with the given name. */
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 */
class Type;
class NodeManager;
-template<bool ref_count> class NodeTemplate;
+template <bool ref_count>
+class NodeTemplate;
/**
* The Node class encapsulates the NodeValue with reference counting.
* maintained in the NodeValue if ref_count is true.
* @param ref_count if true reference are counted in the NodeValue
*/
-template<bool ref_count>
+template <bool ref_count>
class NodeTemplate {
/**
*/
explicit NodeTemplate(const expr::NodeValue*);
- friend class NodeTemplate<true> ;
- friend class NodeTemplate<false> ;
+ friend class NodeTemplate<true>;
+ friend class NodeTemplate<false>;
friend class NodeManager;
- template<unsigned>
+ template <unsigned>
friend class NodeBuilder;
friend class ::CVC4::expr::attr::AttributeManager;
* 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.
* @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 */
}
};
-template<bool ref_count>
+template <bool ref_count>
inline size_t NodeTemplate<ref_count>::getNumChildren() const {
return d_nv->d_nchildren;
}
-template<bool ref_count>
-template<class AttrKind>
+template <bool ref_count>
+template <class AttrKind>
inline typename AttrKind::value_type NodeTemplate<ref_count>::
getAttribute(const AttrKind&) const {
Assert( NodeManager::currentNM() != NULL,
return NodeManager::currentNM()->getAttribute(*this, AttrKind());
}
-template<bool ref_count>
-template<class AttrKind>
+template <bool ref_count>
+template <class AttrKind>
inline bool NodeTemplate<ref_count>::
hasAttribute(const AttrKind&) const {
Assert( NodeManager::currentNM() != NULL,
return NodeManager::currentNM()->hasAttribute(*this, AttrKind());
}
-template<bool ref_count>
-template<class AttrKind>
-inline bool NodeTemplate<ref_count>::
-hasAttribute(const AttrKind&, typename AttrKind::value_type& ret) const {
+template <bool ref_count>
+template <class AttrKind>
+inline bool NodeTemplate<ref_count>::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<bool ref_count>
-template<class AttrKind>
+template <bool ref_count>
+template <class AttrKind>
inline void NodeTemplate<ref_count>::
setAttribute(const AttrKind&, const typename AttrKind::value_type& value) {
Assert( NodeManager::currentNM() != NULL,
NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
}
-template<bool ref_count>
+template <bool ref_count>
NodeTemplate<ref_count> NodeTemplate<ref_count>::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<bool ref_count>
+template <bool ref_count>
bool NodeTemplate<ref_count>::isAtomic() const {
using namespace kind;
switch(getKind()) {
// 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<bool ref_count>
+template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const expr::NodeValue* ev) :
d_nv(const_cast<expr::NodeValue*> (ev)) {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
// the code for these two "conversion/copy constructors" is identical, but
// apparently we need both. see comment in the class.
-template<bool ref_count>
+template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate<!ref_count>& e) {
Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
d_nv = e.d_nv;
}
}
-template<bool ref_count>
+template <bool ref_count>
NodeTemplate<ref_count>::NodeTemplate(const NodeTemplate& e) {
Assert(e.d_nv != NULL, "Expecting a non-NULL expression value!");
d_nv = e.d_nv;
}
}
-template<bool ref_count>
-NodeTemplate<ref_count>::~NodeTemplate() throw() {
- DtorAssert(d_nv != NULL, "Expecting a non-NULL expression value!");
+template <bool ref_count>
+NodeTemplate<ref_count>::~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<bool ref_count>
+template <bool ref_count>
void NodeTemplate<ref_count>::assignNodeValue(expr::NodeValue* ev) {
d_nv = ev;
if(ref_count) {
}
}
-template<bool ref_count>
+template <bool ref_count>
NodeTemplate<ref_count>& NodeTemplate<ref_count>::
operator=(const NodeTemplate& e) {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
return *this;
}
-template<bool ref_count>
+template <bool ref_count>
NodeTemplate<ref_count>& NodeTemplate<ref_count>::
operator=(const NodeTemplate<!ref_count>& e) {
Assert(d_nv != NULL, "Expecting a non-NULL expression value!");
return *this;
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::eqNode(const NodeTemplate<
- ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::eqNode(const NodeTemplate<ref_count>& right) const {
return NodeManager::currentNM()->mkNode(kind::EQUAL, *this, right);
}
-template<bool ref_count>
+template <bool ref_count>
NodeTemplate<true> NodeTemplate<ref_count>::notNode() const {
return NodeManager::currentNM()->mkNode(kind::NOT, *this);
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::andNode(const NodeTemplate<
- ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::andNode(const NodeTemplate<ref_count>& right) const {
return NodeManager::currentNM()->mkNode(kind::AND, *this, right);
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::orNode(const NodeTemplate<
- ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::orNode(const NodeTemplate<ref_count>& right) const {
return NodeManager::currentNM()->mkNode(kind::OR, *this, right);
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::iteNode(const NodeTemplate<
- ref_count>& thenpart, const NodeTemplate<ref_count>& elsepart) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count>& thenpart,
+ const NodeTemplate<ref_count>& elsepart) const {
return NodeManager::currentNM()->mkNode(kind::ITE, *this, thenpart, elsepart);
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::iffNode(const NodeTemplate<
- ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count>& right) const {
return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::impNode(const NodeTemplate<
- ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count>& right) const {
return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
}
-template<bool ref_count>
-NodeTemplate<true> NodeTemplate<ref_count>::xorNode(const NodeTemplate<
- ref_count>& right) const {
+template <bool ref_count>
+NodeTemplate<true>
+NodeTemplate<ref_count>::xorNode(const NodeTemplate<ref_count>& right) const {
return NodeManager::currentNM()->mkNode(kind::XOR, *this, right);
}
-template<bool ref_count>
+template <bool ref_count>
void NodeTemplate<ref_count>::printAst(std::ostream& out, int ind) const {
indent(out, ind);
out << '(';
}
/**
- * 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 ref_count>
bool NodeTemplate<ref_count>::hasOperator() const {
}
}
-template<bool ref_count>
+template <bool ref_count>
const Type* NodeTemplate<ref_count>::getType() const {
Assert( NodeManager::currentNM() != NULL,
"There is no current CVC4::NodeManager associated to this thread.\n"
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
*
* 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
n.printAst(Warning(), 0);
Warning().flush();
}
+#endif /* CVC4_DEBUG */
}/* CVC4 namespace */
class AndNodeBuilder;
class OrNodeBuilder;
class PlusNodeBuilder;
-class MinusNodeBuilder;
class MultNodeBuilder;
template <unsigned nchild_thresh>
// extract another
bool d_used;
- expr::NodeValue *d_nv;
+ expr::NodeValue* d_nv;
expr::NodeValue d_inlineNv;
expr::NodeValue *d_childrenStorage[nchild_thresh];
}
// 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");
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();
+ }
}
}
template <unsigned N> inline NodeBuilder(const NodeBuilder<N>& nb);
inline NodeBuilder(NodeManager* nm);
inline NodeBuilder(NodeManager* nm, Kind k);
- inline ~NodeBuilder() throw();
+ inline ~NodeBuilder();
typedef expr::NodeValue::iterator<true> iterator;
typedef expr::NodeValue::iterator<true> const_iterator;
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 <unsigned N> 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 <unsigned N>
+ friend class NodeBuilder;
};/* class NodeBuilder */
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 <bool rc>
inline PlusNodeBuilder MultNodeBuilder::operator+(const NodeTemplate<rc>& n) {
template <bool rc>
inline PlusNodeBuilder MultNodeBuilder::operator-(const NodeTemplate<rc>& n) {
- return PlusNodeBuilder(Node(d_eb), n);
+ return PlusNodeBuilder(Node(d_eb), NodeManager::currentNM()->mkNode(kind::UMINUS, n));
}
template <bool rc>
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 <bool rc1, bool rc2>
inline AndNodeBuilder operator&&(const NodeTemplate<rc1>& a, const NodeTemplate<rc2>& b) {
return a || Node(b.d_eb);
}
+template <bool rc>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+ return a + Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator+(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+ return a + Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+ return a - Node(b.d_eb);
+}
+
+template <bool rc>
+inline PlusNodeBuilder operator-(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+ return a - Node(b.d_eb);
+}
+
+template <bool rc>
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const PlusNodeBuilder& b) {
+ return a * Node(b.d_eb);
+}
+
+template <bool rc>
+inline MultNodeBuilder operator*(const NodeTemplate<rc>& a, const MultNodeBuilder& b) {
+ return a * Node(b.d_eb);
+}
+
+template <bool rc>
+inline NodeTemplate<true> operator-(const NodeTemplate<rc>& a) {
+ return NodeManager::currentNM()->mkNode(kind::UMINUS, a);
+}
+
}/* CVC4 namespace */
#include "expr/node.h"
}
template <unsigned nchild_thresh>
-inline NodeBuilder<nchild_thresh>::~NodeBuilder() throw() {
+inline NodeBuilder<nchild_thresh>::~NodeBuilder() {
if(!d_used) {
// Warning("NodeBuilder unused at destruction\n");
// Commented above, as it happens a lot, for example with exceptions
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;
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;
}
template <unsigned nchild_thresh>
-inline void NodeBuilder<nchild_thresh>::dealloc() throw() {
+inline void NodeBuilder<nchild_thresh>::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();
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
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;
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
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
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
template <unsigned nchild_thresh>
inline std::ostream& operator<<(std::ostream& out,
const NodeBuilder<nchild_thresh>& b) {
-
b.toStream(out);
return out;
}
#include "expr/kind.h"
#include "expr/expr.h"
+#include "context/context.h"
namespace CVC4 {
template <unsigned> friend class CVC4::NodeBuilder;
- typedef __gnu_cxx::hash_set<expr::NodeValue*, expr::NodeValueHashFcn,
+ typedef __gnu_cxx::hash_set<expr::NodeValue*,
+ expr::NodeValueInternalHashFcn,
expr::NodeValue::NodeValueEq> NodeValueSet;
NodeValueSet d_nodeValueSet;
void poolInsert(expr::NodeValue* nv);
friend class NodeManagerScope;
+ friend class expr::NodeValue;
+
+ std::vector<expr::NodeValue*> 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 );
}
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;
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()) {
}
};
#include "cvc4_config.h"
#include <stdint.h>
-#include "kind.h"
+#include "expr/kind.h"
#include <string>
#include <iterator>
NodeValue(int);
/** Destructor decrements the ref counts of its children */
- ~NodeValue() throw();
+ ~NodeValue();
typedef NodeValue** nv_iterator;
typedef NodeValue const* const* const_nv_iterator;
}
/**
- * 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;
}
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),
d_nchildren(0) {
}
-inline NodeValue::~NodeValue() throw() {
+inline NodeValue::~NodeValue() {
for(nv_iterator i = nv_begin(); i != nv_end(); ++i) {
(*i)->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);
}
}
}
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 */
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
* any collision.
*/
enum OptionValue {
- CNF = 256, /* no clash with char options */
- SMTCOMP,
+ SMTCOMP = 256, /* no clash with char options */
STATS,
SEGV_NOSPIN,
PARSE_ONLY,
{ "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 },
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 */
} 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);
#include <cstdio>
#include <cstdlib>
#include <cerrno>
+#include <exception>
#include <string.h>
#include <signal.h>
#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;
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 */
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;
}
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;
}
** 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 <cstdio>
+#include <cerrno>
#include <fcntl.h>
-#include <stdio.h>
#include <stdint.h>
+#include <string.h>
-#include <sys/errno.h>
#include <sys/mman.h>
#include <sys/stat.h>
+
#include <antlr/InputBuffer.hpp>
#include "util/Assert.h"
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() {
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 */
#include <antlr/CharScanner.hpp>
#include <antlr/CharBuffer.hpp>
-#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"
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,
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;
}
/**
* Generic symbol table for looking up variables by name.
*/
-template<typename ObjectType>
+template <class ObjectType>
class SymbolTable {
private:
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()*/
}
/**
+++ /dev/null
-/********************* */
-/** 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 */
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);
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) {
}
SmtEngine::~SmtEngine() {
+ NodeManagerScope nms(d_nodeManager);
delete d_propEngine;
delete d_theoryEngine;
delete d_decisionEngine;
- delete d_ctxt;
}
void SmtEngine::doCommand(Command* c) {
c->invoke(this);
}
-Node SmtEngine::preprocess(TNode e) {
+Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) {
return e;
}
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;
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;
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();
}
#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.
namespace context {
class Context;
-}
+}/* CVC4::context namespace */
class Command;
class Options;
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
/** 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
*/
Result quickCheck();
+ friend class ::CVC4::smt::SmtEnginePrivate;
+
};/* class SmtEngine */
}/* CVC4 namespace */
#include "expr/node.h"
#include "context/context.h"
+#include "context/cdo.h"
#include "context/context_mm.h"
namespace CVC4 {
*/
ECData* d_find;
-
/**
* This is pointer back to the node that represents this equivalence class.
*
#include "theory/theory.h"
#include "context/context.h"
+#include "context/cdlist.h"
#include "theory/uf/ecdata.h"
namespace CVC4 {
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,
}
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,
}
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 */
#include <string>
#include <sstream>
#include <cstdio>
+#include <cstdlib>
#include <cstdarg>
-#include "util/exception.h"
-#include "cvc4_config.h"
-#include "config.h"
-#include <cassert>
+#include "config.h"
+#include "cvc4_config.h"
+#include "util/exception.h"
+#include "util/output.h"
namespace CVC4 {
}
};/* 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...) \
#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 */
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,
#include <iostream>
#include "parser/parser.h"
-#include "prop/cnf_conversion.h"
namespace CVC4 {
/** The input language */
parser::Parser::InputLanguage lang;
- /** The CNF conversion */
- CVC4::CnfConversion d_cnfConversion;
-
/** Should we exit after parsing? */
bool parseOnly;
err(0),
verbosity(0),
lang(parser::Parser::LANG_AUTO),
- d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION),
parseOnly(false),
semanticChecks(true),
memoryMap(false)
parser/parser_black \
context/context_black \
context/context_mm_black \
+ context/cdlist_black \
theory/theory_black \
theory/theory_uf_white \
util/assert_white \
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+#include <vector>
+#include <iostream>
+#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<int> 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<int>::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;
+ }
+};
** 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 <cxxtest/TestSuite.h>
-//Used in some of the tests
#include <vector>
#include <iostream>
#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 {
public:
void setUp() {
- d_context = new Context();
+ d_context = new Context;
}
void testIntCDO() {
// 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<int> 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<int>::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() {
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 {
#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;
}
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));
}
};
#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;
// it would be nice to have CDAttribute<> for context-dependence
typedef CDAttribute<Test1, bool> TestCDFlag;
-struct ecdata;
-struct cleanupfcn {
- static void cleanup(ecdata* ec) { /* clean up */ }
-};
-
-// ManagedAttribute<> has a cleanup function deleting the value
-typedef ManagedAttribute<Test1, ecdata*, cleanupfcn> TestECDataAttr;
-
typedef Attribute<Test1, bool> TestFlag1;
typedef Attribute<Test2, bool> TestFlag2;
typedef Attribute<Test3, bool> TestFlag3;
typedef Attribute<Test4, bool> TestFlag4;
typedef Attribute<Test5, bool> TestFlag5;
-struct FooBar {};
-struct Test6;
-typedef Attribute<Test6, FooBar> TestFlag6;
+typedef CDAttribute<Test1, bool> TestFlag1cd;
+typedef CDAttribute<Test2, bool> 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() {
TS_ASSERT(VarNameAttr::s_id == 0);
TS_ASSERT(TestStringAttr1::s_id == 1);
TS_ASSERT(TestStringAttr2::s_id == 2);
- TS_ASSERT(attr::LastAttributeId<string>::s_id == 3);
+ TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3));
TS_ASSERT(TypeAttr::s_id == 0);
- TS_ASSERT(attr::LastAttributeId<void*>::s_id == 1);
+ TS_ASSERT((attr::LastAttributeId<void*, false>::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<bool, false>::s_id == 5));
+
+ TS_ASSERT(TestFlag1cd::s_id == 0);
+ TS_ASSERT(TestFlag2cd::s_id == 1);
+ TS_ASSERT((attr::LastAttributeId<bool, true>::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() {
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()
TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == "");
TS_ASSERT(! unnamed.hasAttribute(VarNameAttr()));
-
}
};
set<Node> d_registered;
vector<Node> d_getSequence;
- DummyTheory(context::Context* ctxt, OutputChannel& out) :
- TheoryImpl<DummyTheory>(ctxt, out) {}
+ DummyTheory(Context* ctxt, OutputChannel& out) :
+ TheoryImpl<DummyTheory>(ctxt, out) {
+ }
void registerTerm(TNode n) {
// check that we registerTerm() a term only once
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;
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(){
* 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:
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);
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));
/* 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);
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));
}
/* 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));
}
/* 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());
}
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);
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));
}
- 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);
}
projects / cvc5.git / commitdiff