diff options
113 files changed, 766 insertions, 350 deletions
diff --git a/config/antlr.m4 b/config/antlr.m4 index 64b554378..604d2f6bc 100644 --- a/config/antlr.m4 +++ b/config/antlr.m4 @@ -26,10 +26,11 @@ AC_DEFUN([AC_PROG_ANTLR], [ ## # Check the existence of the ANTLR3 C runtime library and headers -# Will set ANTLR_INCLUDES and ANTLR_LIBS to the location of the ANTLR headers -# and library respectively +# Will set ANTLR_INCLUDES and ANTLR_LIBS to the location of the ANTLR +# headers and library respectively ## AC_DEFUN([AC_LIB_ANTLR],[ + AC_ARG_VAR(ANTLR_HOME, [path to libantlr3c installation]) # Get the location of the ANTLR3 C includes and libraries AC_ARG_WITH( diff --git a/configure.ac b/configure.ac index a80d1fee9..7007ba47f 100644 --- a/configure.ac +++ b/configure.ac @@ -480,6 +480,9 @@ CXXFLAGS="${CXXFLAGS:+$CXXFLAGS }$CVC4CXXFLAGS -Wno-deprecated" CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated" LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS" +FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden' +AC_SUBST(FLAG_VISIBILITY_HIDDEN) + # mk_include # # When automake scans Makefiles, it complains about non-standard make diff --git a/src/Makefile.am b/src/Makefile.am index 17c867163..593499c9b 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@ AM_CPPFLAGS = -D__BUILDING_CVC4LIB \ -I@srcdir@/include -I@srcdir@ -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = expr util context theory prop smt . parser main diff --git a/src/context/Makefile.am b/src/context/Makefile.am index 54accdd6e..85847e096 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libcontext.la diff --git a/src/context/cdmap.h b/src/context/cdmap.h index e9ae8337e..d4de88daf 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -191,7 +191,8 @@ class CDMap : public ContextObj { for(typename std::vector<Element*>::iterator i = d_trash.begin(); i != d_trash.end(); ++i) { - (*i)->deleteSelf(); + Debug("gc") << "emptyTrash(): " << *i << std::endl; + //(*i)->deleteSelf(); } d_trash.clear(); } diff --git a/src/context/context.h b/src/context/context.h index 455169a62..0e2a9107f 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -208,12 +208,12 @@ public: /** * Get the level of the current Scope */ - int getLevel(void) const { return d_level; } + int getLevel() const { return d_level; } /** * Return true iff this Scope is the current top Scope */ - bool isCurrent(void) const { return this == d_pContext->getTopScope(); } + bool isCurrent() const { return this == d_pContext->getTopScope(); } /** * When a ContextObj object is modified for the first time in this Scope, it @@ -240,7 +240,7 @@ public: static void operator delete(void* pMem) {} //FIXME: //! Check for memory leaks - // void check(void); + // void check(); };/* class Scope */ diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 76f6ef1a4..1f5e403cc 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libexpr.la diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 052458cbe..96152d075 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -113,6 +113,9 @@ enum MetaKind_t { // individual MetaKind constants under kind::metakind:: typedef ::CVC4::kind::metakind::MetaKind_t MetaKind; +/** + * Get the metakind for a particular kind. + */ static inline MetaKind metaKindOf(Kind k) { static const MetaKind metaKinds[] = { metakind::INVALID, /* NULL_EXPR */ @@ -123,15 +126,20 @@ ${metakind_kinds} return metaKinds[k]; }/* metaKindOf(k) */ -static inline bool kindIsAtomic(Kind k) { - static const bool isAtomic[] = { +/** + * Determine if a particular kind can be atomic or not. Some kinds + * are never atomic (OR, NOT, ITE...), some can be atomic depending on + * their children (PLUS might have an ITE under it, for instance). + */ +static inline bool kindCanBeAtomic(Kind k) { + static const bool canBeAtomic[] = { false, /* NULL_EXPR */ -${metakind_isatomic} +${metakind_canbeatomic} false /* LAST_KIND */ - };/* isAtomic[] */ + };/* canBeAtomic[] */ - return isAtomic[k]; -}/* kindIsAtomic(k) */ + return canBeAtomic[k]; +}/* kindCanBeAtomic(k) */ }/* CVC4::kind namespace */ diff --git a/src/expr/mkexpr b/src/expr/mkexpr index 6508f8121..f59388def 100755 --- a/src/expr/mkexpr +++ b/src/expr/mkexpr @@ -32,6 +32,23 @@ cat <<EOF ** for the CVC4 project. **/ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ +/* THIS FILE IS AUTOMATICALLY GENERATED, DO NOT EDIT ! */ + +/* Edit the template file instead: */ +/* $1 */ + EOF me=$(basename "$0") diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index 3884f636a..b8dbc2dd6 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -200,11 +200,11 @@ function register_metakind { nc=$3 if [ $mk = NONATOMIC_OPERATOR ]; then - metakind_isatomic="${metakind_isatomic} false, /* $k */ + metakind_canbeatomic="${metakind_canbeatomic} false, /* $k */ "; mk=OPERATOR else - metakind_isatomic="${metakind_isatomic} true, /* $k */ + metakind_canbeatomic="${metakind_canbeatomic} true, /* $k */ "; fi @@ -278,7 +278,7 @@ while [ $# -gt 0 ]; do metakind_kinds="${metakind_kinds} /* from $b */ " - metakind_isatomic="${metakind_isatomic} + metakind_canbeatomic="${metakind_canbeatomic} /* from $b */ " source "$kf" @@ -293,7 +293,7 @@ text=$(cat "$template") for var in \ metakind_includes \ metakind_kinds \ - metakind_isatomic \ + metakind_canbeatomic \ metakind_constantMaps \ metakind_compares \ metakind_constHashes \ diff --git a/src/expr/node.h b/src/expr/node.h index 6f6fdfb4d..3a2aca571 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -587,8 +587,8 @@ template <bool ref_count> NodeTemplate<ref_count> NodeTemplate<ref_count>::s_null(&expr::NodeValue::s_null); template <bool ref_count> -bool NodeTemplate<ref_count>::isAtomic() const { - return kind::kindIsAtomic(getKind()); +inline bool NodeTemplate<ref_count>::isAtomic() const { + return NodeManager::currentNM()->isAtomic(*this); } // FIXME: escape from type system convenient but is there a better diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 99b1471f9..71242f2e1 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -35,18 +35,15 @@ namespace CVC4 { -class Type; - namespace expr { -namespace attr { - -struct VarName {}; -struct Type {}; +// Definition of an attribute for the variable name. +// TODO: hide this attribute behind a NodeManager interface. +namespace attr { + struct VarNameTag {}; }/* CVC4::expr::attr namespace */ -typedef Attribute<attr::VarName, std::string> VarNameAttr; -typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupStrategy> TypeAttr; +typedef expr::Attribute<attr::VarNameTag, std::string> VarNameAttr; }/* CVC4::expr namespace */ @@ -125,6 +122,44 @@ class NodeManager { expr::NodeValue* child[N]; };/* struct NodeManager::NVStorage<N> */ + // attribute tags + struct TypeTag {}; + struct AtomicTag {}; + + // NodeManager's attributes. These aren't exposed outside of this + // class; use the getters. + typedef expr::ManagedAttribute<TypeTag, + CVC4::Type*, + expr::attr::TypeCleanupStrategy> TypeAttr; + typedef expr::Attribute<AtomicTag, bool> AtomicAttr; + + /** + * Returns true if this node is atomic (has no more Boolean + * structure). This is the NodeValue version for NodeManager's + * internal use. There's a public version of this function below + * that takes a TNode. + * @param nv the node to check for atomicity + * @return true if atomic + */ + inline bool isAtomic(expr::NodeValue* nv) const { + // The kindCanBeAtomic() and metakind checking are just optimizations + // (to avoid the hashtable lookup). We assume that all nodes have + // the atomic attribute pre-computed and set at their time of + // creation. This is because: + // (1) it's super cheap to do it bottom-up. + // (2) if we computed it lazily, we'd need a second attribute to + // tell us whether we had computed it yet or not. + // The pre-computation and registration occurs in poolInsert(). + AssertArgument(nv->getMetaKind() != kind::metakind::INVALID, *nv, + "NodeManager::isAtomic() called on INVALID node (%s)", + kind::kindToString(nv->getKind()).c_str()); + return + nv->getMetaKind() == kind::metakind::VARIABLE || + nv->getMetaKind() == kind::metakind::CONSTANT || + ( kind::kindCanBeAtomic(nv->getKind()) && + getAttribute(nv, AtomicAttr()) ); + } + public: NodeManager(context::Context* ctxt); @@ -324,6 +359,15 @@ public: * TODO: Does this call compute the type if it's not already available? */ inline Type* getType(TNode n) const; + + /** + * Returns true if this node is atomic (has no more Boolean structure) + * @param n the node to check for atomicity + * @return true if atomic + */ + inline bool isAtomic(TNode n) const { + return isAtomic(n.d_nv); + } }; /** @@ -476,7 +520,7 @@ inline Type* NodeManager::mkSort(const std::string& name) const { } inline Type* NodeManager::getType(TNode n) const { - return getAttribute(n, CVC4::expr::TypeAttr()); + return getAttribute(n, TypeAttr()); } inline expr::NodeValue* NodeManager::poolLookup(expr::NodeValue* nv) const { @@ -492,6 +536,39 @@ inline void NodeManager::poolInsert(expr::NodeValue* nv) { Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), "NodeValue already in the pool!"); d_nodeValuePool.insert(nv);// FIXME multithreading + + switch(nv->getMetaKind()) { + case kind::metakind::INVALID: + case kind::metakind::VARIABLE: + case kind::metakind::CONSTANT: + // nothing to do (don't bother setting the attribute, isAtomic() + // on VARIABLEs and CONSTANTs is always true) + break; + + case kind::metakind::OPERATOR: + case kind::metakind::PARAMETERIZED: + { + // register this NodeValue as atomic or not; use nv_begin/end + // because we need to consider the operator too in the case of + // PARAMETERIZED-metakinded nodes (i.e. APPLYs); they could have a + // buried ITE. + + // assume it's atomic if its kind can be atomic, check children + // to see if that is actually true + bool atomic = kind::kindCanBeAtomic(nv->getKind()); + if(atomic) { + for(expr::NodeValue::nv_iterator i = nv->nv_begin(); + i != nv->nv_end(); + ++i) { + if(!(atomic = isAtomic(*i))) { + break; + } + } + } + + setAttribute(nv, AtomicAttr(), atomic); + } + } } inline void NodeManager::poolRemove(expr::NodeValue* nv) { @@ -569,7 +646,7 @@ inline Node NodeManager::mkVar(Type* type, const std::string& name) { inline Node NodeManager::mkVar(Type* type) { Node n = mkVar(); type->inc();// reference-count the type - n.setAttribute(expr::TypeAttr(), type); + n.setAttribute(TypeAttr(), type); return n; } diff --git a/src/main/main.cpp b/src/main/main.cpp index b10103635..819f7695e 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -58,25 +58,25 @@ int main(int argc, char* argv[]) { } cerr << "CVC4 Error:" << endl << e << endl; printf(usage, options.binary_name.c_str()); - abort(); + exit(1); } catch(Exception& e) { if(options.smtcomp_mode) { cout << "unknown" << endl; } cerr << "CVC4 Error:" << endl << e << endl; - abort(); + exit(1); } catch(bad_alloc) { if(options.smtcomp_mode) { cout << "unknown" << endl; } cerr << "CVC4 ran out of memory." << endl; - abort(); + exit(1); } catch(...) { if(options.smtcomp_mode) { cout << "unknown" << endl; } cerr << "CVC4 threw an exception of unknown type." << endl; - abort(); + exit(1); } } diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 1aaf7ab69..dad8059f5 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -15,7 +15,7 @@ LIBCVC4PARSER_VERSION = @CVC4_PARSER_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../include -I@srcdir@/.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) SUBDIRS = smt cvc diff --git a/src/parser/bounded_token_buffer.cpp b/src/parser/bounded_token_buffer.cpp index 1418e8f3c..29006b343 100644 --- a/src/parser/bounded_token_buffer.cpp +++ b/src/parser/bounded_token_buffer.cpp @@ -281,13 +281,13 @@ dbgTokLT (pANTLR3_TOKEN_STREAM ts, ANTLR3_INT32 k) static pANTLR3_COMMON_TOKEN LB(pANTLR3_COMMON_TOKEN_STREAM cts, ANTLR3_INT32 k) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_COMMON_TOKEN get (pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 i) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_TOKEN_SOURCE @@ -306,19 +306,19 @@ setTokenSource ( pANTLR3_TOKEN_STREAM ts, static pANTLR3_STRING toString (pANTLR3_TOKEN_STREAM ts) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_STRING toStringSS(pANTLR3_TOKEN_STREAM ts, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_STRING toStringTT (pANTLR3_TOKEN_STREAM ts, pANTLR3_COMMON_TOKEN start, pANTLR3_COMMON_TOKEN stop) { - AlwaysAssert(false); + Unreachable(); } /** Move the input pointer to the next incoming token. The stream @@ -395,13 +395,13 @@ discardOffChannel (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_BOOLEAN dis static pANTLR3_VECTOR getTokens (pANTLR3_COMMON_TOKEN_STREAM tokenStream) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_LIST getTokenRange (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop) { - AlwaysAssert(false); + Unreachable(); } /** Given a start and stop index, return a List of all tokens in * the token type BitSet. Return null if no tokens were found. This @@ -410,19 +410,19 @@ getTokenRange (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANT static pANTLR3_LIST getTokensSet (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, pANTLR3_BITSET types) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_LIST getTokensList (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, pANTLR3_LIST list) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_LIST getTokensType (pANTLR3_COMMON_TOKEN_STREAM tokenStream, ANTLR3_UINT32 start, ANTLR3_UINT32 stop, ANTLR3_UINT32 type) { - AlwaysAssert(false); + Unreachable(); } static ANTLR3_UINT32 @@ -450,13 +450,13 @@ _LA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) static ANTLR3_UINT32 dbgLA (pANTLR3_INT_STREAM is, ANTLR3_INT32 i) { - AlwaysAssert(false); + Unreachable(); } static ANTLR3_MARKER mark (pANTLR3_INT_STREAM is) { - AlwaysAssert(false); + Unreachable(); } /// As per mark() but with a call to tell the debugger we are doing this @@ -464,7 +464,7 @@ mark (pANTLR3_INT_STREAM is) static ANTLR3_MARKER dbgMark (pANTLR3_INT_STREAM is) { - AlwaysAssert(false); + Unreachable(); } static void @@ -476,7 +476,7 @@ release (pANTLR3_INT_STREAM is, ANTLR3_MARKER mark) static ANTLR3_UINT32 size (pANTLR3_INT_STREAM is) { - AlwaysAssert(false); + Unreachable(); } static ANTLR3_MARKER @@ -496,33 +496,33 @@ tindex (pANTLR3_INT_STREAM is) static void dbgRewindLast (pANTLR3_INT_STREAM is) { - AlwaysAssert(false); + Unreachable(); } static void rewindLast (pANTLR3_INT_STREAM is) { - AlwaysAssert(false); + Unreachable(); } static void rewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { - AlwaysAssert(false); + Unreachable(); } static void dbgRewindStream (pANTLR3_INT_STREAM is, ANTLR3_MARKER marker) { - AlwaysAssert(false); + Unreachable(); } static void seek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) { - AlwaysAssert(false); + Unreachable(); } static void dbgSeek (pANTLR3_INT_STREAM is, ANTLR3_MARKER index) { - AlwaysAssert(false); + Unreachable(); } static pANTLR3_COMMON_TOKEN nextToken(pBOUNDED_TOKEN_BUFFER buffer) { diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am index ade8d83e7..08e6c4d52 100644 --- a/src/parser/cvc/Makefile.am +++ b/src/parser/cvc/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) # Compile generated C files using C++ compiler CC=$(CXX) diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am index f081f493f..3ffe61b05 100644 --- a/src/parser/smt/Makefile.am +++ b/src/parser/smt/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4PARSERLIB \ -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES) -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) # Compile generated C files using C++ compiler AM_CFLAGS = $(AM_CXXFLAGS) diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index fc0697eda..357818b32 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libprop.la diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index 366cc34c8..d68237d9b 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../.. -I@srcdir@/../../include -AM_CXXFLAGS = -Wall -fvisibility=hidden -DNDEBUG +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index a2da2c949..889385d77 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libsmt.la diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 2891e64cf..6b1854bfc 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libtheory.la diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am index 226d5af12..cb838f497 100644 --- a/src/theory/arith/Makefile.am +++ b/src/theory/arith/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarith.la libarith_la_SOURCES = \ - theory_def.h \ theory_arith.h EXTRA_DIST = kinds diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 973651f7a..d211cd37d 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace arith { -class TheoryArith : public TheoryImpl<TheoryArith> { +class TheoryArith : public Theory { public: TheoryArith(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryArith>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/arrays/Makefile.am b/src/theory/arrays/Makefile.am index af3a28b3b..5d3514dda 100644 --- a/src/theory/arrays/Makefile.am +++ b/src/theory/arrays/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libarrays.la libarrays_la_SOURCES = \ - theory_def.h \ theory_arrays.h EXTRA_DIST = kinds diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index ec3b88ccd..2f62aacd7 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace arrays { -class TheoryArrays : public TheoryImpl<TheoryArrays> { +class TheoryArrays : public Theory { public: TheoryArrays(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryArrays>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/booleans/Makefile.am b/src/theory/booleans/Makefile.am index cbdf13add..690299630 100644 --- a/src/theory/booleans/Makefile.am +++ b/src/theory/booleans/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbooleans.la libbooleans_la_SOURCES = \ - theory_def.h \ theory_bool.h EXTRA_DIST = kinds diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 5196bb018..eb6e84c39 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace booleans { -class TheoryBool : public TheoryImpl<TheoryBool> { +class TheoryBool : public Theory { public: TheoryBool(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryBool>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am index 54622bf9a..d90472fd3 100644 --- a/src/theory/bv/Makefile.am +++ b/src/theory/bv/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libbv.la libbv_la_SOURCES = \ - theory_def.h \ theory_bv.h EXTRA_DIST = kinds diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index fbb62545d..a859291a7 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -25,10 +25,10 @@ namespace CVC4 { namespace theory { namespace bv { -class TheoryBV : public TheoryImpl<TheoryBV> { +class TheoryBV : public Theory { public: TheoryBV(context::Context* c, OutputChannel& out) : - TheoryImpl<TheoryBV>(c, out) { + Theory(c, out) { } void preRegisterTerm(TNode n) { Unimplemented(); } diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 17a35f2ed..d4bd717be 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -23,5 +23,82 @@ using namespace std; namespace CVC4 { namespace theory { +Node Theory::get() { + Assert( !d_facts.empty(), + "Theory::get() called with assertion queue empty!" ); + + Node fact = d_facts.front(); + d_facts.pop_front(); + + Debug("theory") << "Theory::get() => " << fact + << "(" << d_facts.size() << " left)" << std::endl; + + if(! fact.getAttribute(RegisteredAttr())) { + std::list<TNode> toReg; + toReg.push_back(fact); + + Debug("theory") << "Theory::get(): registering new atom" << std::endl; + + /* Essentially this is doing a breadth-first numbering of + * non-registered subterms with children. Any non-registered + * leaves are immediately registered. */ + for(std::list<TNode>::iterator workp = toReg.begin(); + workp != toReg.end(); + ++workp) { + + TNode n = *workp; + + if(n.hasOperator()) { + TNode c = n.getOperator(); + + if(! c.getAttribute(RegisteredAttr())) { + if(c.getNumChildren() == 0) { + c.setAttribute(RegisteredAttr(), true); + registerTerm(c); + } else { + toReg.push_back(c); + } + } + } + + for(TNode::iterator i = n.begin(); i != n.end(); ++i) { + TNode c = *i; + + if(! c.getAttribute(RegisteredAttr())) { + if(c.getNumChildren() == 0) { + c.setAttribute(RegisteredAttr(), true); + registerTerm(c); + } else { + toReg.push_back(c); + } + } + } + } + + /* Now register the list of terms in reverse order. Between this + * and the above registration of leaves, this should ensure that + * all subterms in the entire tree were registered in + * reverse-topological order. */ + for(std::list<TNode>::reverse_iterator i = toReg.rbegin(); + i != toReg.rend(); + ++i) { + + TNode n = *i; + + /* Note that a shared TNode in the DAG rooted at "fact" could + * appear twice on the list, so we have to avoid hitting it + * twice. */ + // FIXME when ExprSets are online, use one of those to avoid + // duplicates in the above? + if(! n.getAttribute(RegisteredAttr())) { + n.setAttribute(RegisteredAttr(), true); + registerTerm(n); + } + } + } + + return fact; +} + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 4c3a43061..2fcac86b0 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -38,36 +38,22 @@ namespace theory { struct RewriteCacheTag {}; typedef expr::Attribute<RewriteCacheTag, TNode> RewriteCache; -template <class T> -class TheoryImpl; - /** * Base class for T-solvers. Abstract DPLL(T). * * This is essentially an interface class. The TheoryEngine has - * pointers to Theory. But each individual theory implementation T - * should inherit from TheoryImpl<T>, which specializes a few things - * for that theory. + * pointers to Theory. Note that only one specific Theory type (e.g., + * TheoryUF) can exist per NodeManager, because of how the + * RegisteredAttr works. (If you need multiple instances of the same + * theory, you'll have to write a multiplexed theory that dispatches + * all calls to them.) */ class Theory { private: - template <class T> - friend class ::CVC4::theory::TheoryImpl; - friend class ::CVC4::TheoryEngine; /** - * Construct a Theory. - */ - Theory(context::Context* ctxt, OutputChannel& out) throw() : - d_context(ctxt), - d_facts(), - d_factsResetter(*this), - d_out(&out) { - } - - /** * Disallow default construction. */ Theory(); @@ -110,13 +96,23 @@ private: protected: /** + * Construct a Theory. + */ + Theory(context::Context* ctxt, OutputChannel& out) throw() : + d_context(ctxt), + d_facts(), + d_factsResetter(*this), + d_out(&out) { + } + + /** * This is called at shutdown time by the TheoryEngine, just before * destruction. It is important because there are destruction * ordering issues between PropEngine and Theory (based on what * hard-links to Nodes are outstanding). As the fact queue might be * nonempty, we ensure here that it's clear. If you overload this, - * you must make an explicit call here to the Theory implementation - * of this function too. + * you must make an explicit call here to this->Theory::shutdown() + * too. */ virtual void shutdown() { d_facts.clear(); @@ -158,6 +154,24 @@ protected: return n.getAttribute(RewriteCache()); } + /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ + struct Registered {}; + /** The "registerTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; + + /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ + struct PreRegistered {}; + /** The "preRegisterTerm()-has-been-called" flag on Nodes */ + typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; + + /** + * Returns the next atom in the assertFact() queue. Guarantees that + * registerTerm() has been called on the theory specific subterms. + * + * @return the next atom in the assertFact() queue. + */ + Node get(); + public: /** @@ -308,133 +322,6 @@ protected: };/* class Theory */ - -/** - * Base class for T-solver implementations. Each individual - * implementation T of the Theory interface should inherit from - * TheoryImpl<T>. This class specializes some things for a particular - * theory implementation. - * - * The problem with this is that Theory implementations cannot be - * further subclassed without designing all non-children in the type - * DAG to play the same trick as here (be template-polymorphic in their - * most-derived child), linearizing the inheritance hierarchy (viewing - * each instantiation separately). - */ -template <class T> -class TheoryImpl : public Theory { - -protected: - - /** - * Construct a Theory. - */ - TheoryImpl(context::Context* ctxt, OutputChannel& out) : - Theory(ctxt, out) { - /* FIXME: assert here that a TheoryImpl<T> doesn't already exist - * for this NodeManager?? If it does, we're hosed because they'll - * share per-theory node attributes. */ - } - - /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ - struct Registered {}; - /** The "registerTerm()-has-been-called" flag on Nodes */ - typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; - - /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ - struct PreRegistered {}; - /** The "preRegisterTerm()-has-been-called" flag on Nodes */ - typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; - - /** - * Returns the next atom in the assertFact() queue. Guarantees that - * registerTerm() has been called on the theory specific subterms. - * - * @return the next atom in the assertFact() queue. - */ - Node get(); -};/* class TheoryImpl<T> */ - -template <class T> -Node TheoryImpl<T>::get() { - Assert(typeid(*this) == typeid(T), - "Improper Theory inheritance chain detected."); - - Assert( !d_facts.empty(), - "Theory::get() called with assertion queue empty!" ); - - Node fact = d_facts.front(); - d_facts.pop_front(); - - Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl; - - if(! fact.getAttribute(RegisteredAttr())) { - std::list<TNode> toReg; - toReg.push_back(fact); - - Debug("theory") << "Theory::get(): registering new atom" << std::endl; - - /* Essentially this is doing a breadth-first numbering of - * non-registered subterms with children. Any non-registered - * leaves are immediately registered. */ - for(std::list<TNode>::iterator workp = toReg.begin(); - workp != toReg.end(); - ++workp) { - - TNode n = *workp; - - if(n.hasOperator()) { - TNode c = n.getOperator(); - - if(! c.getAttribute(RegisteredAttr())) { - if(c.getNumChildren() == 0) { - c.setAttribute(RegisteredAttr(), true); - registerTerm(c); - } else { - toReg.push_back(c); - } - } - } - - for(TNode::iterator i = n.begin(); i != n.end(); ++i) { - TNode c = *i; - - if(! c.getAttribute(RegisteredAttr())) { - if(c.getNumChildren() == 0) { - c.setAttribute(RegisteredAttr(), true); - registerTerm(c); - } else { - toReg.push_back(c); - } - } - } - } - - /* Now register the list of terms in reverse order. Between this - * and the above registration of leaves, this should ensure that - * all subterms in the entire tree were registered in - * reverse-topological order. */ - for(std::list<TNode>::reverse_iterator i = toReg.rbegin(); - i != toReg.rend(); - ++i) { - - TNode n = *i; - - /* Note that a shared TNode in the DAG rooted at "fact" could - * appear twice on the list, so we have to avoid hitting it - * twice. */ - // FIXME when ExprSets are online, use one of those to avoid - // duplicates in the above? - if(! n.getAttribute(RegisteredAttr())) { - n.setAttribute(RegisteredAttr(), true); - registerTerm(n); - } - } - } - - return fact; -} - }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 156733c5b..e0aa3a1df 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -1,12 +1,11 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../../include -I@srcdir@/../.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libuf.la libuf_la_SOURCES = \ - theory_def.h \ ecdata.h \ ecdata.cpp \ theory_uf.h \ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 3fe82b16c..f0d8b47e0 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -10,10 +10,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** + ** Implementation of the theory of uninterpreted functions. **/ - #include "theory/uf/theory_uf.h" #include "theory/uf/ecdata.h" #include "expr/kind.h" @@ -24,37 +23,32 @@ using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; - - TheoryUF::TheoryUF(Context* c, OutputChannel& out) : - TheoryImpl<TheoryUF>(c, out), + Theory(c, out), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), d_disequality(c), - d_registered(c) -{} + d_registered(c) { +} -TheoryUF::~TheoryUF(){} +TheoryUF::~TheoryUF() { +} -void TheoryUF::preRegisterTerm(TNode n){ +void TheoryUF::preRegisterTerm(TNode n) { Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; } -void TheoryUF::registerTerm(TNode n){ +void TheoryUF::registerTerm(TNode n) { Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; - d_registered.push_back(n); - - - ECData* ecN; - if(n.getAttribute(ECAttr(), ecN)){ + if(n.getAttribute(ECAttr(), ecN)) { /* registerTerm(n) is only called when a node has not been seen in the * current context. ECAttr() is not a context-dependent attribute. * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call, @@ -101,7 +95,7 @@ void TheoryUF::registerTerm(TNode n){ "Expected getWatchListSize() == 0. " "This data is either already in use or was not properly maintained " "during backtracking"); - }else{ + } else { //The attribute does not exist, so it is created and set ecN = new (true) ECData(getContext(), n); n.setAttribute(ECAttr(), ecN); @@ -110,10 +104,10 @@ void TheoryUF::registerTerm(TNode n){ /* If the node is an APPLY_UF, we need to add it to the predecessor list * of its children. */ - if(n.getKind() == APPLY_UF){ + if(n.getKind() == APPLY_UF) { TNode::iterator cIter = n.begin(); - for(; cIter != n.end(); ++cIter){ + for(; cIter != n.end(); ++cIter) { TNode child = *cIter; /* Because this can be called after nodes have been merged, we need @@ -124,8 +118,8 @@ void TheoryUF::registerTerm(TNode n){ /* Because this can be called after nodes have been merged we may need * to be merged with other predecessors of the equivalence class. */ - for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ){ - if(equiv(n, Px->d_data)){ + for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ) { + if(equiv(n, Px->d_data)) { Node pend = n.eqNode(Px->d_data); d_pending.push_back(pend); } @@ -138,30 +132,32 @@ void TheoryUF::registerTerm(TNode n){ } -bool TheoryUF::sameCongruenceClass(TNode x, TNode y){ +bool TheoryUF::sameCongruenceClass(TNode x, TNode y) { return ccFind(x.getAttribute(ECAttr())) == ccFind(y.getAttribute(ECAttr())); } -bool TheoryUF::equiv(TNode x, TNode y){ +bool TheoryUF::equiv(TNode x, TNode y) { Assert(x.getKind() == kind::APPLY_UF); Assert(y.getKind() == kind::APPLY_UF); - if(x.getNumChildren() != y.getNumChildren()) + if(x.getNumChildren() != y.getNumChildren()) { return false; + } - if(x.getOperator() != y.getOperator()) + if(x.getOperator() != y.getOperator()) { return false; + } // intentionally don't look at operator TNode::iterator xIter = x.begin(); TNode::iterator yIter = y.begin(); - while(xIter != x.end()){ + while(xIter != x.end()) { - if(!sameCongruenceClass(*xIter, *yIter)){ + if(!sameCongruenceClass(*xIter, *yIter)) { return false; } @@ -178,10 +174,10 @@ bool TheoryUF::equiv(TNode x, TNode y){ * many better algorithms use eager path compression. * 2) Elminate recursion. */ -ECData* TheoryUF::ccFind(ECData * x){ - if( x->getFind() == x) +ECData* TheoryUF::ccFind(ECData * x) { + if(x->getFind() == x) { return x; - else{ + } else { return ccFind(x->getFind()); } /* Slightly better Find w/ path compression and no recursion*/ @@ -189,7 +185,7 @@ ECData* TheoryUF::ccFind(ECData * x){ ECData* start; ECData* next = x; while(x != x->getFind()) x=x->getRep(); - while( (start = next) != x){ + while( (start = next) != x) { next = start->getFind(); start->setFind(x); } @@ -197,23 +193,23 @@ ECData* TheoryUF::ccFind(ECData * x){ */ } -void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ +void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) { ECData* nslave; ECData* nmaster; - if(ecX->getWatchListSize() <= ecY->getWatchListSize()){ + if(ecX->getWatchListSize() <= ecY->getWatchListSize()) { nslave = ecX; nmaster = ecY; - }else{ + } else { nslave = ecY; nmaster = ecX; } nslave->setFind(nmaster); - for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ){ - for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ){ - if(equiv(Px->d_data,Py->d_data)){ + for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ) { + for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ) { + if(equiv(Px->d_data,Py->d_data)) { Node pendingEq = (Px->d_data).eqNode(Py->d_data); d_pending.push_back(pendingEq); } @@ -223,7 +219,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ ECData::takeOverDescendantWatchList(nslave, nmaster); } -void TheoryUF::merge(){ +void TheoryUF::merge() { while(d_currentPendingIdx < d_pending.size() ) { Node assertion = d_pending[d_currentPendingIdx]; d_currentPendingIdx = d_currentPendingIdx + 1; @@ -248,7 +244,7 @@ void TheoryUF::merge(){ } } -Node TheoryUF::constructConflict(TNode diseq){ +Node TheoryUF::constructConflict(TNode diseq) { Debug("uf") << "uf: begin constructConflict()" << std::endl; NodeBuilder<> nb(kind::AND); @@ -267,15 +263,15 @@ Node TheoryUF::constructConflict(TNode diseq){ return conflict; } -void TheoryUF::check(Effort level){ +void TheoryUF::check(Effort level) { Debug("uf") << "uf: begin check(" << level << ")" << std::endl; - while(!done()){ + while(!done()) { Node assertion = get(); Debug("uf") << "TheoryUF::check(): " << assertion << std::endl; - switch(assertion.getKind()){ + switch(assertion.getKind()) { case EQUAL: d_assertions.push_back(assertion); d_pending.push_back(assertion); @@ -292,18 +288,18 @@ void TheoryUF::check(Effort level){ } //Make sure all outstanding merges are completed. - if(d_currentPendingIdx < d_pending.size()){ + if(d_currentPendingIdx < d_pending.size()) { merge(); } - if(fullEffort(level)){ + if(fullEffort(level)) { for(CDList<Node>::const_iterator diseqIter = d_disequality.begin(); diseqIter != d_disequality.end(); - ++diseqIter){ + ++diseqIter) { TNode left = (*diseqIter)[0]; TNode right = (*diseqIter)[1]; - if(sameCongruenceClass(left, right)){ + if(sameCongruenceClass(left, right)) { Node remakeNeq = (*diseqIter).notNode(); Node conflict = constructConflict(remakeNeq); d_out->conflict(conflict, false); @@ -313,5 +309,4 @@ void TheoryUF::check(Effort level){ } Debug("uf") << "uf: end check(" << level << ")" << std::endl; - } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 8495e6c9c..5863a31fc 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -38,7 +38,7 @@ namespace CVC4 { namespace theory { namespace uf { -class TheoryUF : public TheoryImpl<TheoryUF> { +class TheoryUF : public Theory { private: @@ -176,31 +176,30 @@ private: /** Constructs a conflict from an inconsistent disequality. */ Node constructConflict(TNode diseq); -}; +};/* class TheoryUF */ /** * Cleanup function for ECData. This will be used for called whenever * a ECAttr is being destructed. */ -struct ECCleanupStrategy{ - static void cleanup(ECData* ec){ +struct ECCleanupStrategy { + static void cleanup(ECData* ec) { Debug("ufgc") << "cleaning up ECData " << ec << "\n"; ec->deleteSelf(); } -}; +};/* struct ECCleanupStrategy */ /** Unique name to use for constructing ECAttr. */ -struct EquivClass; +struct ECAttrTag {}; /** * ECAttr is the attribute that maps a node to an equivalence class. */ -typedef expr::Attribute<EquivClass, ECData*, ECCleanupStrategy > ECAttr; - -} /* CVC4::theory::uf namespace */ -} /* CVC4::theory namespace */ -} /* CVC4 namespace */ +typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr; +}/* CVC4::theory::uf namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__UF__THEORY_UF_H */ diff --git a/src/util/Assert.cpp b/src/util/Assert.cpp index 06be4ab7c..1611f28d3 100644 --- a/src/util/Assert.cpp +++ b/src/util/Assert.cpp @@ -70,8 +70,10 @@ 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; + if(s_debugAssertionFailure == NULL) { + // we leak buf[] but only in debug mode with assertions failing + s_debugAssertionFailure = buf; + } #else /* CVC4_DEBUG */ delete [] buf; #endif /* CVC4_DEBUG */ @@ -110,7 +112,9 @@ void AssertionException::construct(const char* header, const char* extra, #ifdef CVC4_DEBUG // we leak buf[] but only in debug mode with assertions failing - s_debugAssertionFailure = buf; + if(s_debugAssertionFailure == NULL) { + s_debugAssertionFailure = buf; + } #else /* CVC4_DEBUG */ delete [] buf; #endif /* CVC4_DEBUG */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 5e8dfd2a4..6597c8b48 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -1,7 +1,7 @@ AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall -fvisibility=hidden +AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libutil.la diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index f4ce30968..5ed13a139 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -94,7 +94,7 @@ string Configuration::about() { This is a pre-release of CVC4.\n\ Copyright (C) 2009, 2010\n\ The ACSys Group\n\ - Courant Institute of Mathematical Sciences,\n\ + Courant Institute of Mathematical Sciences\n\ New York University\n\ New York, NY 10012 USA\n"); } diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index eb07b22fb..fe95ed7aa 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,7 +1,9 @@ SUBDIRS = precedence uf -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = \ + error.cvc \ + boolean-prec.cvc \ distinct.smt \ flet.smt \ flet2.smt \ @@ -43,7 +45,7 @@ TESTS = \ wiki.19.cvc \ wiki.20.cvc \ wiki.21.cvc - + # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/boolean-prec.cvc b/test/regress/regress0/boolean-prec.cvc index 4f84de94d..d0205116c 100644 --- a/test/regress/regress0/boolean-prec.cvc +++ b/test/regress/regress0/boolean-prec.cvc @@ -1,6 +1,7 @@ -% Expect: VALID +% EXPECT: VALID % Simple test for right precedence of AND, <=>, NOT. A, B, C: BOOLEAN; QUERY (NOT A AND NOT B <=> C) <=> (((NOT A) AND (NOT B)) <=> C); +% EXIT: 20 diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index 89afbe325..eeac40c9f 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -804,3 +804,4 @@ a288 : BOOLEAN = ELSE FALSE ENDIF; QUERY a288; +% EXIT: 20 diff --git a/test/regress/regress0/bug1.cvc b/test/regress/regress0/bug1.cvc index d3d936381..2b59638d1 100644 --- a/test/regress/regress0/bug1.cvc +++ b/test/regress/regress0/bug1.cvc @@ -6,3 +6,4 @@ ASSERT ((x > y) => f(x) > f (y)); ASSERT (x = 3); ASSERT (y = 2); QUERY(f(x) > f (y)); +% EXIT: 20 diff --git a/test/regress/regress0/bug32.cvc b/test/regress/regress0/bug32.cvc index 8d113d785..c6d79a4ab 100644 --- a/test/regress/regress0/bug32.cvc +++ b/test/regress/regress0/bug32.cvc @@ -4,3 +4,4 @@ b:BOOLEAN; ASSERT(a); QUERY(a OR b); +% EXIT: 20 diff --git a/test/regress/regress0/error.cvc b/test/regress/regress0/error.cvc new file mode 100644 index 000000000..09a69e212 --- /dev/null +++ b/test/regress/regress0/error.cvc @@ -0,0 +1,4 @@ +% EXPECT-ERROR: CVC4 Error: +% EXPECT-ERROR: Parse Error: Parser Error: error.cvc:3.9: Symbol BOOL not declared +p : BOOL; +% EXIT: 1 diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index bdd45b6d0..07bfa392c 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -177,3 +177,4 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/logops.01.cvc b/test/regress/regress0/logops.01.cvc index d947d1a27..5348cf7e4 100644 --- a/test/regress/regress0/logops.01.cvc +++ b/test/regress/regress0/logops.01.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY (a XOR b) <=> (NOT a AND b) OR (NOT b AND a); +% EXIT: 20 diff --git a/test/regress/regress0/logops.02.cvc b/test/regress/regress0/logops.02.cvc index ba2d55b4f..4a8539fae 100644 --- a/test/regress/regress0/logops.02.cvc +++ b/test/regress/regress0/logops.02.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: INVALID QUERY NOT c AND b; +% EXIT: 10 diff --git a/test/regress/regress0/logops.03.cvc b/test/regress/regress0/logops.03.cvc index 85b23d2b0..6b5f34613 100644 --- a/test/regress/regress0/logops.03.cvc +++ b/test/regress/regress0/logops.03.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY (IF c THEN a ELSE b ENDIF) <=> ((c AND a) OR (NOT c AND b)); +% EXIT: 20 diff --git a/test/regress/regress0/logops.04.cvc b/test/regress/regress0/logops.04.cvc index a71096542..6e7aa1f5e 100644 --- a/test/regress/regress0/logops.04.cvc +++ b/test/regress/regress0/logops.04.cvc @@ -1,3 +1,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY (a => b) <=> (NOT a OR b); +% EXIT: 20 diff --git a/test/regress/regress0/logops.05.cvc b/test/regress/regress0/logops.05.cvc index 19bbae5b4..14e2c887a 100644 --- a/test/regress/regress0/logops.05.cvc +++ b/test/regress/regress0/logops.05.cvc @@ -2,3 +2,4 @@ a, b, c: BOOLEAN; % EXPECT: VALID QUERY TRUE XOR FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 0b4fcd4a6..362ec70b6 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 TESTS = \ iff-implies.cvc \ implies-iff.cvc \ diff --git a/test/regress/regress0/precedence/and-not.cvc b/test/regress/regress0/precedence/and-not.cvc index d283ca881..0de37db83 100644 --- a/test/regress/regress0/precedence/and-not.cvc +++ b/test/regress/regress0/precedence/and-not.cvc @@ -4,3 +4,4 @@ A, B: BOOLEAN; QUERY (A AND NOT B) <=> (A AND (NOT B)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/and-xor.cvc b/test/regress/regress0/precedence/and-xor.cvc index c7268727a..7b29bb95e 100644 --- a/test/regress/regress0/precedence/and-xor.cvc +++ b/test/regress/regress0/precedence/and-xor.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A AND B XOR C) <=> ((A AND B) XOR C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/eq-fun.cvc b/test/regress/regress0/precedence/eq-fun.cvc index 43feeb1f8..e85b4a3e6 100644 --- a/test/regress/regress0/precedence/eq-fun.cvc +++ b/test/regress/regress0/precedence/eq-fun.cvc @@ -6,3 +6,4 @@ x , y: T; f : T -> T; QUERY (f(x) = f(y)) <=> ((f(x)) = (f(y))); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/iff-assoc.cvc b/test/regress/regress0/precedence/iff-assoc.cvc index 82e0cbc72..b92354753 100644 --- a/test/regress/regress0/precedence/iff-assoc.cvc +++ b/test/regress/regress0/precedence/iff-assoc.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A <=> B <=> C) <=> (A <=> (B <=> C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/iff-implies.cvc b/test/regress/regress0/precedence/iff-implies.cvc index bebafce14..0115fc319 100644 --- a/test/regress/regress0/precedence/iff-implies.cvc +++ b/test/regress/regress0/precedence/iff-implies.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A <=> B => C) <=> ((A <=> (B => C))); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/implies-assoc.cvc b/test/regress/regress0/precedence/implies-assoc.cvc index c73616caf..d465df313 100644 --- a/test/regress/regress0/precedence/implies-assoc.cvc +++ b/test/regress/regress0/precedence/implies-assoc.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A => B => C) <=> (A => (B => C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/implies-iff.cvc b/test/regress/regress0/precedence/implies-iff.cvc index f44c4bc75..f8c813ceb 100644 --- a/test/regress/regress0/precedence/implies-iff.cvc +++ b/test/regress/regress0/precedence/implies-iff.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A => B <=> C) <=> ((A => B) <=> C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/implies-or.cvc b/test/regress/regress0/precedence/implies-or.cvc index 835da8570..24edb4ecd 100644 --- a/test/regress/regress0/precedence/implies-or.cvc +++ b/test/regress/regress0/precedence/implies-or.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A => B OR C) <=> (A => (B OR C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/not-and.cvc b/test/regress/regress0/precedence/not-and.cvc index 44c27af53..8c849a0d9 100644 --- a/test/regress/regress0/precedence/not-and.cvc +++ b/test/regress/regress0/precedence/not-and.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (NOT A AND B) <=> ((NOT A) AND B); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/not-eq.cvc b/test/regress/regress0/precedence/not-eq.cvc index 1126926b8..16c812086 100644 --- a/test/regress/regress0/precedence/not-eq.cvc +++ b/test/regress/regress0/precedence/not-eq.cvc @@ -4,3 +4,4 @@ A, B: BOOLEAN; QUERY (NOT A = B) <=> (NOT (A = B)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/or-implies.cvc b/test/regress/regress0/precedence/or-implies.cvc index 3b336db5a..d91f79dc8 100644 --- a/test/regress/regress0/precedence/or-implies.cvc +++ b/test/regress/regress0/precedence/or-implies.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A OR B => C) <=> ((A OR B) => C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/or-xor.cvc b/test/regress/regress0/precedence/or-xor.cvc index 2198962c8..47cc87c76 100644 --- a/test/regress/regress0/precedence/or-xor.cvc +++ b/test/regress/regress0/precedence/or-xor.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A OR B XOR C) <=> (A OR (B XOR C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/xor-and.cvc b/test/regress/regress0/precedence/xor-and.cvc index ccdaeebad..ba3f48a7f 100644 --- a/test/regress/regress0/precedence/xor-and.cvc +++ b/test/regress/regress0/precedence/xor-and.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A XOR B AND C) <=> (A XOR (B AND C)); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/xor-assoc.cvc b/test/regress/regress0/precedence/xor-assoc.cvc index ffdb2c8c9..27911332c 100644 --- a/test/regress/regress0/precedence/xor-assoc.cvc +++ b/test/regress/regress0/precedence/xor-assoc.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A XOR B XOR C) <=> ((A XOR B) XOR C); +% EXIT: 20 diff --git a/test/regress/regress0/precedence/xor-or.cvc b/test/regress/regress0/precedence/xor-or.cvc index 959dec14e..2b4436937 100644 --- a/test/regress/regress0/precedence/xor-or.cvc +++ b/test/regress/regress0/precedence/xor-or.cvc @@ -4,3 +4,4 @@ A, B, C: BOOLEAN; QUERY (A XOR B OR C) <=> ((A XOR B) OR C); +% EXIT: 20 diff --git a/test/regress/regress0/queries0.cvc b/test/regress/regress0/queries0.cvc index 36107e784..fe6235981 100644 --- a/test/regress/regress0/queries0.cvc +++ b/test/regress/regress0/queries0.cvc @@ -8,3 +8,4 @@ QUERY (a AND b) OR NOT (a AND b); % EXPECT: INVALID QUERY (a OR b); +% EXIT: 10 diff --git a/test/regress/regress0/simple.cvc b/test/regress/regress0/simple.cvc index 21145b6e0..a0bff6c5a 100644 --- a/test/regress/regress0/simple.cvc +++ b/test/regress/regress0/simple.cvc @@ -5,3 +5,4 @@ ASSERT x3 OR x2; ASSERT x1 AND NOT x1; % EXPECT: VALID QUERY x2; +% EXIT: 20 diff --git a/test/regress/regress0/smallcnf.cvc b/test/regress/regress0/smallcnf.cvc index 3a36b8c1e..fe17e0b53 100644 --- a/test/regress/regress0/smallcnf.cvc +++ b/test/regress/regress0/smallcnf.cvc @@ -7,3 +7,4 @@ ASSERT a OR NOT b OR c; % EXPECT: INVALID QUERY FALSE; +% EXIT: 10 diff --git a/test/regress/regress0/test11.cvc b/test/regress/regress0/test11.cvc index 6f0cac8fa..2fa1e23ba 100644 --- a/test/regress/regress0/test11.cvc +++ b/test/regress/regress0/test11.cvc @@ -5,3 +5,4 @@ ASSERT NOT (x OR y); % EXPECT: VALID QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/test12.cvc b/test/regress/regress0/test12.cvc index 48966f53b..a3d63b497 100644 --- a/test/regress/regress0/test12.cvc +++ b/test/regress/regress0/test12.cvc @@ -175,3 +175,4 @@ QUERY NOT P_10; POP; PUSH; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/test9.cvc b/test/regress/regress0/test9.cvc index de6be2f54..64c2011a4 100644 --- a/test/regress/regress0/test9.cvc +++ b/test/regress/regress0/test9.cvc @@ -2,3 +2,4 @@ P,Q:BOOLEAN; ASSERT (P OR Q); QUERY (P OR Q); +% EXIT: 20 diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index ec99fd45c..802189f2b 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../../run_regression @top_builddir@/src/main/cvc4 TESTS = \ euf_simp01.smt \ euf_simp02.smt \ diff --git a/test/regress/regress0/uf/simple.01.cvc b/test/regress/regress0/uf/simple.01.cvc index f5d8c1033..84b8b8a8d 100644 --- a/test/regress/regress0/uf/simple.01.cvc +++ b/test/regress/regress0/uf/simple.01.cvc @@ -5,3 +5,4 @@ x, y: A; f: A -> B; QUERY (x = y => f(x) = f(y)); +% EXIT: 20 diff --git a/test/regress/regress0/uf/simple.02.cvc b/test/regress/regress0/uf/simple.02.cvc index 0ebc319ba..21d3e3cee 100644 --- a/test/regress/regress0/uf/simple.02.cvc +++ b/test/regress/regress0/uf/simple.02.cvc @@ -5,3 +5,4 @@ x, y: A; f: A -> B; QUERY (f(x) = f(y)); +% EXIT: 10 diff --git a/test/regress/regress0/uf/simple.03.cvc b/test/regress/regress0/uf/simple.03.cvc index 54948edb8..476c6cd4a 100644 --- a/test/regress/regress0/uf/simple.03.cvc +++ b/test/regress/regress0/uf/simple.03.cvc @@ -9,3 +9,4 @@ f: A -> B; ASSERT (x = a AND y = a) OR (x = b AND y = b); QUERY (f(x) = f(y)); +% EXIT: 20 diff --git a/test/regress/regress0/uf/simple.04.cvc b/test/regress/regress0/uf/simple.04.cvc index 58bb6fef1..c9675588d 100644 --- a/test/regress/regress0/uf/simple.04.cvc +++ b/test/regress/regress0/uf/simple.04.cvc @@ -9,3 +9,4 @@ f: A -> B; ASSERT (x = a OR x = b) AND (y = b OR y = a); QUERY (f(x) = f(y)); +% EXIT: 10 diff --git a/test/regress/regress0/uf20-03.cvc b/test/regress/regress0/uf20-03.cvc index 74fdb1116..a44b028a2 100644 --- a/test/regress/regress0/uf20-03.cvc +++ b/test/regress/regress0/uf20-03.cvc @@ -113,3 +113,4 @@ ASSERT x_10 OR NOT x_11 OR x_16; QUERY FALSE; +% EXIT: 10 diff --git a/test/regress/regress0/wiki.01.cvc b/test/regress/regress0/wiki.01.cvc index 57660b5a1..7b6835469 100644 --- a/test/regress/regress0/wiki.01.cvc +++ b/test/regress/regress0/wiki.01.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR (b OR c) <=> (a OR b) OR c; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.02.cvc b/test/regress/regress0/wiki.02.cvc index baba45927..9fd4f8fb7 100644 --- a/test/regress/regress0/wiki.02.cvc +++ b/test/regress/regress0/wiki.02.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND (b AND c) <=> (a AND b) AND c; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.03.cvc b/test/regress/regress0/wiki.03.cvc index 791cc45c8..63c1029b4 100644 --- a/test/regress/regress0/wiki.03.cvc +++ b/test/regress/regress0/wiki.03.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR b <=> b OR a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.04.cvc b/test/regress/regress0/wiki.04.cvc index f0f73ce1f..77fa0059b 100644 --- a/test/regress/regress0/wiki.04.cvc +++ b/test/regress/regress0/wiki.04.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND b <=> b AND a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index afb094dae..cb7140bcc 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR (a AND b) <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.06.cvc b/test/regress/regress0/wiki.06.cvc index 421bfbdfd..6c69ca4bc 100644 --- a/test/regress/regress0/wiki.06.cvc +++ b/test/regress/regress0/wiki.06.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND (a OR b) <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.07.cvc b/test/regress/regress0/wiki.07.cvc index a28cbf553..a0281d04b 100644 --- a/test/regress/regress0/wiki.07.cvc +++ b/test/regress/regress0/wiki.07.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR (b AND c) <=> (a OR b) AND (a OR c); +% EXIT: 20 diff --git a/test/regress/regress0/wiki.08.cvc b/test/regress/regress0/wiki.08.cvc index 70fc5f430..ddf0f328c 100644 --- a/test/regress/regress0/wiki.08.cvc +++ b/test/regress/regress0/wiki.08.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND (b OR c) <=> (a AND b) OR (a AND c); +% EXIT: 20 diff --git a/test/regress/regress0/wiki.09.cvc b/test/regress/regress0/wiki.09.cvc index d3118536d..f97021910 100644 --- a/test/regress/regress0/wiki.09.cvc +++ b/test/regress/regress0/wiki.09.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR NOT a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.10.cvc b/test/regress/regress0/wiki.10.cvc index 41a9bcd3f..da8a1a9c3 100644 --- a/test/regress/regress0/wiki.10.cvc +++ b/test/regress/regress0/wiki.10.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND NOT a <=> FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.11.cvc b/test/regress/regress0/wiki.11.cvc index e9c0b9cce..4d7c3c130 100644 --- a/test/regress/regress0/wiki.11.cvc +++ b/test/regress/regress0/wiki.11.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR a <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.12.cvc b/test/regress/regress0/wiki.12.cvc index d5e7bd776..c932892c8 100644 --- a/test/regress/regress0/wiki.12.cvc +++ b/test/regress/regress0/wiki.12.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND a <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.13.cvc b/test/regress/regress0/wiki.13.cvc index 2674ba47b..3ad4fd4ab 100644 --- a/test/regress/regress0/wiki.13.cvc +++ b/test/regress/regress0/wiki.13.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR FALSE <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.14.cvc b/test/regress/regress0/wiki.14.cvc index 378b84dcd..454cf442c 100644 --- a/test/regress/regress0/wiki.14.cvc +++ b/test/regress/regress0/wiki.14.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND TRUE <=> a; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.15.cvc b/test/regress/regress0/wiki.15.cvc index ca51c4632..81a13f798 100644 --- a/test/regress/regress0/wiki.15.cvc +++ b/test/regress/regress0/wiki.15.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a OR TRUE <=> TRUE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.16.cvc b/test/regress/regress0/wiki.16.cvc index af47433f8..bd13faf11 100644 --- a/test/regress/regress0/wiki.16.cvc +++ b/test/regress/regress0/wiki.16.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY a AND FALSE <=> FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.17.cvc b/test/regress/regress0/wiki.17.cvc index dc7e7a1c3..48949f89f 100644 --- a/test/regress/regress0/wiki.17.cvc +++ b/test/regress/regress0/wiki.17.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT FALSE <=> TRUE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.18.cvc b/test/regress/regress0/wiki.18.cvc index 21a87f4b5..8959d34a6 100644 --- a/test/regress/regress0/wiki.18.cvc +++ b/test/regress/regress0/wiki.18.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT TRUE <=> FALSE; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.19.cvc b/test/regress/regress0/wiki.19.cvc index c6081c200..11366526b 100644 --- a/test/regress/regress0/wiki.19.cvc +++ b/test/regress/regress0/wiki.19.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT (a OR b) <=> NOT a AND NOT b; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.20.cvc b/test/regress/regress0/wiki.20.cvc index 3bec9348b..5ef534bb0 100644 --- a/test/regress/regress0/wiki.20.cvc +++ b/test/regress/regress0/wiki.20.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT (a AND b) <=> NOT a OR NOT b; +% EXIT: 20 diff --git a/test/regress/regress0/wiki.21.cvc b/test/regress/regress0/wiki.21.cvc index e99ba2d68..bcd7146fb 100644 --- a/test/regress/regress0/wiki.21.cvc +++ b/test/regress/regress0/wiki.21.cvc @@ -2,3 +2,4 @@ a, b, c : BOOLEAN; % EXPECT: VALID QUERY NOT NOT a <=> a; +% EXIT: 20 diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 8a41e99a3..9307a33a2 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = friedman_n4_i5.smt \ hole7.cvc \ hole8.cvc \ diff --git a/test/regress/regress1/hole7.cvc b/test/regress/regress1/hole7.cvc index 1bebf8049..5ff290f62 100644 --- a/test/regress/regress1/hole7.cvc +++ b/test/regress/regress1/hole7.cvc @@ -262,3 +262,4 @@ ASSERT x_56 OR x_55 OR x_54 OR x_53 OR x_52 OR x_51 OR x_50; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress1/hole8.cvc b/test/regress/regress1/hole8.cvc index 65942a27f..d0f974619 100644 --- a/test/regress/regress1/hole8.cvc +++ b/test/regress/regress1/hole8.cvc @@ -371,3 +371,4 @@ ASSERT x_72 OR x_71 OR x_70 OR x_69 OR x_68 OR x_67 OR x_66 OR x_65; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 2f72dd5e2..710ee6b8e 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = bmc-galileo-8.smt \ bmc-galileo-9.smt \ bmc-ibm-10.smt \ diff --git a/test/regress/regress2/hole9.cvc b/test/regress/regress2/hole9.cvc index 93377ca0b..e631444d3 100644 --- a/test/regress/regress2/hole9.cvc +++ b/test/regress/regress2/hole9.cvc @@ -507,3 +507,4 @@ ASSERT x_90 OR x_89 OR x_88 OR x_87 OR x_86 OR x_85 OR x_84 OR x_83 OR x_82; QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index f0f46171c..156fffb54 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -1,4 +1,4 @@ -TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/../../bin/cvc4 +TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4 TESTS = C880mul.miter.shuffled-as.sat03-348.smt \ comb2.shuffled-as.sat03-420.smt \ hole10.cvc \ diff --git a/test/regress/regress3/hole10.cvc b/test/regress/regress3/hole10.cvc index 39c978b18..661e3ef4b 100644 --- a/test/regress/regress3/hole10.cvc +++ b/test/regress/regress3/hole10.cvc @@ -673,3 +673,4 @@ ASSERT x_110 OR x_109 OR x_108 OR x_107 OR x_106 OR x_105 OR x_104 OR x_103 OR x QUERY FALSE; +% EXIT: 20 diff --git a/test/regress/run_regression b/test/regress/run_regression index 2be776b3f..65ab6c31a 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -44,35 +44,68 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` - if [ -z "$expected_output" ]; then - error "cannot determine status of \`$benchmark'" + expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` + if [ -z "$expected_output" -a -z "$expected_error" ]; then + error "cannot determine expected output of \`$benchmark': " \ + "please use \`% EXPECT:' and/or \`% EXPECT-ERROR:' gestures" fi expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | sed 's,^% EXIT: ,,'` + if [ -z "$expected_exit_status" ]; then + error "cannot determine expected exit status of \`$benchmark': please use \`% EXIT:' gesture" + fi else error "benchmark \`$benchmark' must be *.cvc or *.smt" fi -expfile=`mktemp -t cvc4_expected.XXXXXXXXXX` -outfile=`mktemp -t cvc4_output.XXXXXXXXXX` -echo "$expected_output" >"$expfile" +expoutfile=`mktemp -t cvc4_expect_stdout.XXXXXXXXXX` +experrfile=`mktemp -t cvc4_expect_stderr.XXXXXXXXXX` +outfile=`mktemp -t cvc4_stdout.XXXXXXXXXX` +errfile=`mktemp -t cvc4_stderr.XXXXXXXXXX` +exitstatusfile=`mktemp -t cvc4_exitstatus.XXXXXXXXXX` +if [ -z "$expected_output" ]; then + # in case expected stdout output is empty, make sure we don't differ + # by a newline, which we would if we echo "" >"$expoutfile" + touch "$expoutfile" +else + echo "$expected_output" >"$expoutfile" +fi +if [ -z "$expected_error" ]; then + # in case expected stderr output is empty, make sure we don't differ + # by a newline, which we would if we echo "" >"$experrfile" + touch "$experrfile" +else + echo "$expected_error" >"$experrfile" +fi -# echo "$cvc4" --segv-nospin "$benchmark" -"$cvc4" --segv-nospin "$benchmark" > "$outfile" +("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile" -diffs=`diff -u "$expfile" "$outfile"` +diffs=`diff -u "$expoutfile" "$outfile"` diffexit=$? -rm -f "$expfile" +diffserr=`diff -u "$experrfile" "$errfile"` +diffexiterr=$? +exit_status=`cat "$exitstatusfile"` + +rm -f "$expoutfile" +rm -f "$experrfile" rm -f "$outfile" +rm -f "$errfile" +rm -f "$exitstatusfile" + +exitcode=0 if [ $diffexit -ne 0 ]; then - echo "$prog: error: differences between expected and actual output" + echo "$prog: error: differences between expected and actual output on stdout" echo "$diffs" - exit 1 + exitcode=1 +fi +if [ $diffexiterr -ne 0 ]; then + echo "$prog: error: differences between expected and actual output on stderr" + echo "$diffserr" + exitcode=1 fi -if [ -n "$expected_exit_status" ]; then - : - #if [ $exit_status != "$expected_exit_status" ]; then - # error "expected exit status \`$expected_exit_status' but got \`$exit_status'" - #fi +if [ "$exit_status" != "$expected_exit_status" ]; then + echo "$prog: error: expected exit status \`$expected_exit_status' but got \`$exit_status'" + exitcode=1 fi +exit $exitcode diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 768a56a9b..451100b59 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -10,6 +10,7 @@ UNIT_TESTS = \ expr/attribute_black \ parser/parser_white \ context/context_black \ + context/context_white \ context/context_mm_black \ context/cdo_black \ context/cdlist_black \ diff --git a/test/unit/context/cdmap_black.h b/test/unit/context/cdmap_black.h index 7040e4cc1..262c66fe5 100644 --- a/test/unit/context/cdmap_black.h +++ b/test/unit/context/cdmap_black.h @@ -30,6 +30,8 @@ public: void setUp() { d_context = new Context; //Debug.on("cdmap"); + //Debug.on("gc"); + //Debug.on("pushpop"); } void tearDown() { diff --git a/test/unit/context/context_white.h b/test/unit/context/context_white.h new file mode 100644 index 000000000..3e0928baf --- /dev/null +++ b/test/unit/context/context_white.h @@ -0,0 +1,186 @@ +/********************* */ +/** context_white.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. + ** + ** White box testing of CVC4::context::Context. + **/ + +#include <cxxtest/TestSuite.h> + +#include "context/context.h" +#include "context/cdo.h" +#include "util/Assert.h" + +using namespace std; +using namespace CVC4; +using namespace CVC4::context; + +class ContextWhite : public CxxTest::TestSuite { +private: + + Context* d_context; + +public: + + void setUp() { + d_context = new Context; + } + + void tearDown() { + delete d_context; + } + + void testContextSimple() { + Scope *s = d_context->getTopScope(); + + TS_ASSERT(s == d_context->getBottomScope()); + TS_ASSERT(d_context->getLevel() == 0); + TS_ASSERT(d_context->d_scopeList.size() == 1); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == NULL); + + CDO<int> a(d_context); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &a); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &s->d_pContextObjList); + + CDO<int> b(d_context); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + + d_context->push(); + Scope* t = d_context->getTopScope(); + TS_ASSERT(s != t); + + TS_ASSERT(s == d_context->getBottomScope()); + TS_ASSERT(d_context->getLevel() == 1); + TS_ASSERT(d_context->d_scopeList.size() == 2); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + TS_ASSERT(s->d_pContextObjList == &b); + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == NULL); + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + + a = 5; + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &a); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &t->d_pContextObjList); + + b = 3; + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == t); + TS_ASSERT(b.d_pContextObjRestore != NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList); + + d_context->push(); + Scope* u = d_context->getTopScope(); + TS_ASSERT(u != t); + TS_ASSERT(u != s); + + CDO<int> c(d_context); + c = 4; + + TS_ASSERT(c.d_pScope == u); + TS_ASSERT(c.d_pContextObjRestore != NULL); + TS_ASSERT(c.d_pContextObjNext == NULL); + TS_ASSERT(c.d_ppContextObjPrev == &u->d_pContextObjList); + + d_context->pop(); + + TS_ASSERT(t->d_pContext == d_context); + TS_ASSERT(t->d_pCMM == d_context->d_pCMM); + TS_ASSERT(t->d_level == 1); + TS_ASSERT(t->d_pContextObjList == &b); + + TS_ASSERT(a.d_pScope == t); + TS_ASSERT(a.d_pContextObjRestore != NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == t); + TS_ASSERT(b.d_pContextObjRestore != NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + //TS_ASSERT(b.d_ppContextObjPrev == &t->d_pContextObjList);// THIS ONE FAILS + + d_context->pop(); + + TS_ASSERT(s->d_pContext == d_context); + TS_ASSERT(s->d_pCMM == d_context->d_pCMM); + TS_ASSERT(s->d_level == 0); + //TS_ASSERT(s->d_pContextObjList == &b);// THIS ONE FAILS + + TS_ASSERT(a.d_pScope == s); + TS_ASSERT(a.d_pContextObjRestore == NULL); + TS_ASSERT(a.d_pContextObjNext == NULL); + TS_ASSERT(a.d_ppContextObjPrev == &b.d_pContextObjNext); + + TS_ASSERT(b.d_pScope == s); + TS_ASSERT(b.d_pContextObjRestore == NULL); + TS_ASSERT(b.d_pContextObjNext == &a); + TS_ASSERT(b.d_ppContextObjPrev == &s->d_pContextObjList); + } +}; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index fb18601a3..64c768a13 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -17,12 +17,14 @@ #include <string> +#include "context/context.h" #include "expr/node_value.h" #include "expr/node_builder.h" #include "expr/node_manager.h" -#include "expr/node.h" #include "expr/attribute.h" -#include "context/context.h" +#include "expr/node.h" +#include "theory/theory.h" +#include "theory/uf/theory_uf.h" #include "util/Assert.h" using namespace CVC4; @@ -74,24 +76,73 @@ public: } void testAttributeIds() { - TS_ASSERT(VarNameAttr::s_id == 0); - TS_ASSERT(TestStringAttr1::s_id == 1); - TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT((attr::LastAttributeId<string, false>::s_id == 3)); - - TS_ASSERT(TypeAttr::s_id == 0); - 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)); + // Test that IDs for (a subset of) attributes in the system are + // unique and that the LastAttributeId (which would be the next ID + // to assign) is greater than all attribute IDs. + + // We used to check ID assignments explicitly. However, between + // compilation modules, you don't get a strong guarantee + // (initialization order is somewhat implementation-specific, and + // anyway you'd have to change the tests anytime you add an + // attribute). So we back off, and just test that they're unique + // and that the next ID to be assigned is strictly greater than + // those that have already been assigned. + + unsigned lastId = attr::LastAttributeId<string, false>::s_id; + TS_ASSERT_LESS_THAN(VarNameAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestStringAttr1::s_id, lastId); + TS_ASSERT_LESS_THAN(TestStringAttr2::s_id, lastId); + + TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr1::s_id); + TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id); + TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id); + + lastId = attr::LastAttributeId<void*, false>::s_id; + TS_ASSERT_LESS_THAN(NodeManager::TypeAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); + TS_ASSERT_DIFFERS(NodeManager::TypeAttr::s_id, theory::uf::ECAttr::s_id); + + lastId = attr::LastAttributeId<bool, false>::s_id; + TS_ASSERT_LESS_THAN(NodeManager::AtomicAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, + theory::Theory::PreRegisteredAttr::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag1::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(NodeManager::AtomicAttr::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag3::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag2::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag4::s_id); + TS_ASSERT_DIFFERS(TestFlag3::s_id, TestFlag5::s_id); + TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); + + lastId = attr::LastAttributeId<bool, true>::s_id; + TS_ASSERT_LESS_THAN(theory::Theory::RegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); + TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); + TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag1cd::s_id); + TS_ASSERT_DIFFERS(theory::Theory::RegisteredAttr::s_id, TestFlag2cd::s_id); + TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); + + lastId = attr::LastAttributeId<TNode, false>::s_id; + TS_ASSERT_LESS_THAN(theory::RewriteCache::s_id, lastId); } void testCDAttributes() { diff --git a/test/unit/expr/expr_black.h b/test/unit/expr/expr_black.h index e253b4a24..03d4ba31c 100644 --- a/test/unit/expr/expr_black.h +++ b/test/unit/expr/expr_black.h @@ -354,7 +354,9 @@ public: TS_ASSERT(mult->isAtomic()); TS_ASSERT(plus->isAtomic()); TS_ASSERT(d->isAtomic()); - TS_ASSERT(!null->isAtomic()); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(null->isAtomic(), IllegalArgumentException); +#endif /* CVC4_ASSERTIONS */ TS_ASSERT(i1->isAtomic()); TS_ASSERT(i2->isAtomic()); @@ -368,6 +370,12 @@ public: TS_ASSERT(!x.isAtomic()); TS_ASSERT(!y.isAtomic()); TS_ASSERT(!z.isAtomic()); + + Expr w1 = d_em->mkExpr(PLUS, d_em->mkExpr(ITE, z, *i1, *i2), *i2); + Expr w2 = d_em->mkExpr(PLUS, d_em->mkExpr(MULT, *i1, *i2), *i2); + + TS_ASSERT(!w1.isAtomic()); + TS_ASSERT(w2.isAtomic()); } void testGetConst() { diff --git a/test/unit/expr/node_builder_black.h b/test/unit/expr/node_builder_black.h index 81aa424f8..2a7b3623e 100644 --- a/test/unit/expr/node_builder_black.h +++ b/test/unit/expr/node_builder_black.h @@ -244,9 +244,9 @@ public: Node n = noKind; -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(noKind.getKind();); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(noKind.getKind(), AssertionException); +#endif /* CVC4_ASSERTIONS */ NodeBuilder<> spec(specKind); TS_ASSERT_EQUALS(spec.getKind(), specKind); @@ -277,11 +277,11 @@ public: push_back(noKind, K); TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS noKind << specKind; n = noKind; - TS_ASSERT_THROWS_ANYTHING( noKind.getNumChildren() ); -#endif + TS_ASSERT_THROWS( noKind.getNumChildren(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ } void testOperatorSquare() { @@ -297,10 +297,10 @@ public: Node i_2 = d_nm->mkConst(true); Node i_K = d_nm->mkNode(NOT, i_0); -#ifdef CVC4_DEBUG - TS_ASSERT_THROWS_ANYTHING(arr[-1];); - TS_ASSERT_THROWS_ANYTHING(arr[0];); -#endif +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(arr[-1], AssertionException); + TS_ASSERT_THROWS(arr[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ arr << i_0; @@ -330,10 +330,10 @@ public: } TS_ASSERT_EQUALS(arr[K], i_K); -#ifdef CVC4_DEBUG +#ifdef CVC4_ASSERTIONS Node n = arr; - TS_ASSERT_THROWS_ANYTHING(arr[0]); -#endif + TS_ASSERT_THROWS(arr[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ } void testClear() { @@ -469,6 +469,10 @@ public: Node p = d_nm->mkNode(PLUS, z, d_nm->mkNode(UMINUS, x), z); Node q = d_nm->mkNode(AND, x, z, d_nm->mkNode(NOT, y)); +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS(d_nm->mkNode(XOR, y, x, x), AssertionException); +#endif /* CVC4_ASSERTIONS */ + NodeBuilder<> b; // test append(TNode) diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 427a22c9d..c6da48291 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -82,13 +82,13 @@ public: } }; -class DummyTheory : public TheoryImpl<DummyTheory> { +class DummyTheory : public Theory { public: set<Node> d_registered; vector<Node> d_getSequence; DummyTheory(Context* ctxt, OutputChannel& out) : - TheoryImpl<DummyTheory>(ctxt, out) { + Theory(ctxt, out) { } void registerTerm(TNode n) { |