From 9576517676138a8ca2887a967f1b056662ef6754 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 16 Mar 2010 20:24:37 +0000 Subject: * test/unit/Makefile.am, test/unit/expr/attribute_white.h, test/unit/expr/node_white.h: add whitebox attribute test (pulled out attribute stuff from node_white) * test/unit/parser/parser_black.h: fix memory leaks uncovered by valgrind * src/theory/interrupted.h: actually make this "lightweight" (not derived from CVC4::Exception), as promised in my last commit * src/theory/uf/theory_uf.h, test/unit/expr/attribute_black.h: match the new-style cleanup function definition * src/expr/attribute.cpp, src/expr/attribute.h: support for attribute deletion, custom cleanup functions, clearer cleanup function definition. * src/expr/node_manager.h, src/expr/node_manager.cpp: reclaim remaining zombies in dtor, rename NodeValueSet ==> "NodeValuePool", and enable freeing of NodeValues * src/expr/type.h, src/expr/type.cpp: reference-counting for types, customized cleanup function for types, also code cleanup * (various): changed "const Type*" to "Type*" (to enable reference-counting etc. Types are still immutable.) * src/util/output.h: add ::isOn()-- which queries whether a Debug/Trace flag is currently on or not. * src/smt/smt_engine.cpp, src/parser/antlr_parser.cpp, src/expr/type.cpp, src/expr/expr_manager.cpp, various others: minor code cleanup --- src/expr/attribute.cpp | 43 ++- src/expr/attribute.h | 227 ++++++++++++---- src/expr/expr.cpp | 2 +- src/expr/expr.h | 2 +- src/expr/expr_manager.cpp | 24 +- src/expr/expr_manager.h | 22 +- src/expr/node.h | 4 +- src/expr/node_manager.cpp | 18 +- src/expr/node_manager.h | 59 ++-- src/expr/type.cpp | 33 ++- src/expr/type.h | 76 +++++- src/parser/antlr_parser.cpp | 93 +++---- src/parser/antlr_parser.h | 28 +- src/parser/cvc/cvc_parser.g | 50 ++-- src/parser/smt/smt_lexer.g | 4 +- src/parser/smt/smt_parser.g | 76 +++--- src/smt/smt_engine.cpp | 14 +- src/theory/interrupted.h | 11 +- src/theory/uf/theory_uf.h | 3 +- src/util/output.h | 9 + test/unit/Makefile.am | 1 + test/unit/expr/attribute_black.h | 2 +- test/unit/expr/attribute_white.h | 565 +++++++++++++++++++++++++++++++++++++++ test/unit/expr/node_black.h | 131 ++++----- test/unit/expr/node_white.h | 513 ----------------------------------- test/unit/parser/parser_black.h | 7 +- 26 files changed, 1144 insertions(+), 873 deletions(-) create mode 100644 test/unit/expr/attribute_white.h diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index e8e93f6ff..be54a973e 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -17,24 +17,43 @@ #include "expr/node_value.h" #include "util/output.h" +#include + +using namespace std; + namespace CVC4 { namespace expr { namespace attr { +/** + * Search for the NodeValue in all attribute tables and remove it, + * calling the cleanup function if one is defined. + */ +template +inline void AttributeManager::deleteFromTable(AttrHash& table, + NodeValue* nv) { + for(uint64_t id = 0; id < attr::LastAttributeId::s_id; ++id) { + typedef AttributeTraits traits_t; + typedef AttrHash hash_t; + pair pr = std::make_pair(id, nv); + if(traits_t::cleanup[id] != NULL) { + typename hash_t::iterator i = table.find(pr); + if(i != table.end()) { + traits_t::cleanup[id]((*i).second); + table.erase(pr); + } + } else { + table.erase(pr); + } + } +} + void AttributeManager::deleteAllAttributes(NodeValue* nv) { d_bools.erase(nv); - for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_ints.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_exprs.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_strings.erase(std::make_pair(id, nv)); - } - for(unsigned id = 0; id < attr::LastAttributeId::s_id; ++id) { - d_ptrs.erase(std::make_pair(id, nv)); - } + deleteFromTable(d_ints, nv); + deleteFromTable(d_exprs, nv); + deleteFromTable(d_strings, nv); + deleteFromTable(d_ptrs, nv); // FIXME CD-bools in optimized table /* diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 4dc050648..62619e2b6 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -389,28 +389,139 @@ public: namespace attr { /** Default cleanup for unmanaged Attribute<> */ -template -struct AttributeCleanupFcn { - static inline void cleanup(const T&) {} -}; +struct NullCleanupFcn { +};/* struct NullCleanupFcn */ /** Default cleanup for ManagedAttribute<> */ template struct ManagedAttributeCleanupFcn { -}; +};/* struct ManagedAttributeCleanupFcn<> */ /** Specialization for T* */ template struct ManagedAttributeCleanupFcn { static inline void cleanup(T* p) { delete p; } -}; +};/* struct ManagedAttributeCleanupFcn */ /** Specialization for const T* */ template struct ManagedAttributeCleanupFcn { static inline void cleanup(const T* p) { delete p; } +};/* struct ManagedAttributeCleanupFcn */ + +/** + * Helper for Attribute<> class below to determine whether a cleanup + * is defined or not. + */ +template +struct getCleanupFcn { + typedef T value_type; + typedef KindValueToTableValueMapping mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupFcn<> */ + +/** + * Specialization for NullCleanupFcn. + */ +template +struct getCleanupFcn { + typedef T value_type; + typedef KindValueToTableValueMapping mapping; + static void (*const fn)(typename mapping::table_value_type); +};/* struct getCleanupFcn */ + +// out-of-class initialization required (because it's a non-integral type) +template +void (*const getCleanupFcn::fn)(typename getCleanupFcn::mapping::table_value_type) = NULL; + +/** + * Specialization for ManagedAttributeCleanupFcn. + */ +template +struct getCleanupFcn > { + typedef T value_type; + typedef KindValueToTableValueMapping mapping; + static void (*const fn)(typename mapping::table_value_type); +};/* struct getCleanupFcn > */ + +// out-of-class initialization required (because it's a non-integral type) +template +void (*const getCleanupFcn >::fn)(typename getCleanupFcn >::mapping::table_value_type) = NULL; + +/** + * Specialization for ManagedAttributeCleanupFcn. + */ +template +struct getCleanupFcn > { + typedef T* value_type; + typedef ManagedAttributeCleanupFcn C; + typedef KindValueToTableValueMapping mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupFcn > */ + +/** + * Specialization for ManagedAttributeCleanupFcn. + */ +template +struct getCleanupFcn > { + typedef const T* value_type; + typedef ManagedAttributeCleanupFcn C; + typedef KindValueToTableValueMapping mapping; + static void fn(typename mapping::table_value_type t) { + C::cleanup(mapping::convertBack(t)); + } +};/* struct getCleanupFcn > */ + +/** + * Cause compile-time error for improperly-instantiated + * getCleanupFcn<>. + */ +template +struct getCleanupFcn >; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE IDENTIFIER ASSIGNMENT TEMPLATE ==================================== + +namespace attr { + +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ +template +struct LastAttributeId { + static uint64_t s_id; +}; + +/** Initially zero. */ +template +uint64_t LastAttributeId::s_id = 0; + +}/* CVC4::expr::attr namespace */ + +// ATTRIBUTE TRAITS ============================================================ + +namespace attr { + +/** + * This is the last-attribute-assigner. IDs are not globally + * unique; rather, they are unique for each table_value_type. + */ +template +struct AttributeTraits { + typedef void (*cleanup_t)(T); + static std::vector cleanup; }; +template +std::vector::cleanup_t> + AttributeTraits::cleanup; + }/* CVC4::expr::attr namespace */ // ATTRIBUTE DEFINITION ======================================================== @@ -431,9 +542,16 @@ struct ManagedAttributeCleanupFcn { */ template , + class CleanupFcn = attr::NullCleanupFcn, bool context_dep = false> -struct Attribute { +class Attribute { + /** + * The unique ID associated to this attribute. Assigned statically, + * at load time. + */ + static const uint64_t s_id; + +public: /** The value type for this attribute. */ typedef value_t value_type; @@ -454,20 +572,43 @@ struct Attribute { */ static const bool context_dependent = context_dep; -private: - /** - * The unique ID associated to this attribute. Assigned statically, - * at load time. + * Register this attribute kind and 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; + static inline uint64_t registerAttribute() { + typedef typename attr::KindValueToTableValueMapping::table_value_type table_value_type; + typedef attr::AttributeTraits traits; + uint64_t id = attr::LastAttributeId::s_id++; + Assert(traits::cleanup.size() == id);// sanity check + traits::cleanup.push_back(attr::getCleanupFcn::fn); + return id; + } +};/* class Attribute<> */ + +/** + * An "attribute type" structure for boolean flags (special). The + * full one is below; the existence of this one disallows for boolean + * flag attributes with a specialized cleanup function. + */ +/* -- doesn't work; other specialization is "more specific" ?? +template +class Attribute { + template struct ERROR_bool_attributes_cannot_have_cleanup_functions; + ERROR_bool_attributes_cannot_have_cleanup_functions blah; }; +*/ /** * An "attribute type" structure for boolean flags (special). */ -template -struct Attribute { +template +class Attribute { + /** IDs for bool-valued attributes are actually bit assignments. */ + static const uint64_t s_id; + +public: /** The value type for this attribute; here, bool. */ typedef bool value_type; @@ -495,21 +636,18 @@ struct Attribute { 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. + * Register this attribute kind and check that the ID is a valid ID + * for bool-valued attributes. Fail an assert if not. Otherwise + * return the id. */ - static inline uint64_t checkID(uint64_t id) { + static inline uint64_t registerAttribute() { + uint64_t id = attr::LastAttributeId::s_id++; AlwaysAssert( id <= 63, "Too many boolean node attributes registered " "during initialization !" ); return id; } - -private: - - /** IDs for bool-valued attributes are actually bit assignments. */ - static const uint64_t s_id; -}; +};/* class Attribute<..., bool, ...> */ /** * This is a context-dependent attribute kind (the only difference @@ -520,7 +658,7 @@ private: template struct CDAttribute : - public Attribute, true> {}; + public Attribute {}; /** * This is a managed attribute kind (the only difference between @@ -541,35 +679,21 @@ struct ManagedAttribute : // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= -namespace attr { - -/** - * This is the last-attribute-assigner. IDs are not globally - * unique; rather, they are unique for each table_value_type. - */ -template -struct LastAttributeId { - static uint64_t s_id; -}; - -/** Initially zero. */ -template -uint64_t LastAttributeId::s_id = 0; - -}/* CVC4::expr::attr namespace */ - /** Assign unique IDs to attributes at load time. */ +// Use of the comma-operator here forces instantiation (and +// initialization) of the AttributeTraits<> structure and its +// "cleanup" vector before registerAttribute() is called. This is +// important because otherwise the vector is initialized later, +// clearing the first-pushed cleanup function. template const uint64_t Attribute::s_id = - attr::LastAttributeId::table_value_type, context_dep>::s_id++; + ( attr::AttributeTraits::table_value_type, context_dep>::cleanup.size(), + Attribute::registerAttribute() ); -/** - * Assign unique IDs to bool-valued attributes at load time, checking - * that they are in range. - */ -template -const uint64_t Attribute::s_id = - Attribute::checkID(attr::LastAttributeId::s_id++); +/** Assign unique IDs to attributes at load time. */ +template +const uint64_t Attribute::s_id = + Attribute::registerAttribute(); // ATTRIBUTE MANAGER =========================================================== @@ -609,6 +733,9 @@ class AttributeManager { /** Underlying hash table for context-dependent pointer-valued attributes */ CDAttrHash d_cdptrs; + template + void deleteFromTable(AttrHash& table, NodeValue* nv); + /** * getTable<> is a helper template that gets the right table from an * AttributeManager given its type. diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index 2f84f018b..6f611cf95 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -91,7 +91,7 @@ size_t Expr::getNumChildren() const { return d_node->getNumChildren(); } -const Type* Expr::getType() const { +Type* Expr::getType() const { ExprManagerScope ems(*this); return d_node->getType(); } diff --git a/src/expr/expr.h b/src/expr/expr.h index b297be6fb..c5478b1da 100644 --- a/src/expr/expr.h +++ b/src/expr/expr.h @@ -106,7 +106,7 @@ public: /** Returns the type of the expression, if it has been computed. * Returns NULL if the type of the expression is not known. */ - const Type* getType() const; + Type* getType() const; /** * Returns the string representation of the expression. diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index f0a35e5f1..0b0139118 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -42,12 +42,12 @@ ExprManager::~ExprManager() { delete d_ctxt; } -const BooleanType* ExprManager::booleanType() const { +BooleanType* ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); return d_nodeManager->booleanType(); } -const KindType* ExprManager::kindType() const { +KindType* ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); return d_nodeManager->kindType(); } @@ -106,32 +106,30 @@ Expr ExprManager::mkExpr(Kind kind, const vector& children) { } /** Make a function type from domain to range. */ -const FunctionType* -ExprManager::mkFunctionType(const Type* domain, - const Type* range) { +FunctionType* ExprManager::mkFunctionType(Type* domain, + Type* range) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(domain,range); + return d_nodeManager->mkFunctionType(domain, range); } /** Make a function type with input types from argTypes. */ -const FunctionType* -ExprManager::mkFunctionType(const std::vector& argTypes, - const Type* range) { +FunctionType* ExprManager::mkFunctionType(const std::vector& argTypes, + Type* range) { NodeManagerScope nms(d_nodeManager); - return d_nodeManager->mkFunctionType(argTypes,range); + return d_nodeManager->mkFunctionType(argTypes, range); } -const Type* ExprManager::mkSort(const std::string& name) { +Type* ExprManager::mkSort(const std::string& name) { NodeManagerScope nms(d_nodeManager); return d_nodeManager->mkSort(name); } -Expr ExprManager::mkVar(const Type* type, const std::string& name) { +Expr ExprManager::mkVar(Type* type, const std::string& name) { NodeManagerScope nms(d_nodeManager); return Expr(this, new Node(d_nodeManager->mkVar(type, name))); } -Expr ExprManager::mkVar(const Type* type) { +Expr ExprManager::mkVar(Type* type) { NodeManagerScope nms(d_nodeManager); return Expr(this, new Node(d_nodeManager->mkVar(type))); } diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index ff4e0db6b..3c73e1ced 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -51,10 +51,10 @@ public: ~ExprManager(); /** Get the type for booleans */ - const BooleanType* booleanType() const; + BooleanType* booleanType() const; /** Get the type for sorts. */ - const KindType* kindType() const; + KindType* kindType() const; /** * Make a unary expression of a given kind (TRUE, FALSE,...). @@ -95,21 +95,21 @@ public: Expr mkExpr(Kind kind, const std::vector& children); /** Make a function type from domain to range. */ - const FunctionType* - mkFunctionType(const Type* domain, - const Type* range); + FunctionType* + mkFunctionType(Type* domain, + Type* range); /** Make a function type with input types from argTypes. */ - const FunctionType* - mkFunctionType(const std::vector& argTypes, - const Type* range); + FunctionType* + mkFunctionType(const std::vector& argTypes, + Type* range); /** Make a new sort with the given name. */ - const Type* mkSort(const std::string& name); + Type* mkSort(const std::string& name); // variables are special, because duplicates are permitted - Expr mkVar(const Type* type, const std::string& name); - Expr mkVar(const Type* type); + Expr mkVar(Type* type, const std::string& name); + Expr mkVar(Type* type); private: /** The context */ diff --git a/src/expr/node.h b/src/expr/node.h index d1bb8f3b3..25990cedf 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -240,7 +240,7 @@ public: * Returns the type of this node. * @return the type */ - const Type* getType() const; + Type* getType() const; /** * Returns the kind of this node. @@ -707,7 +707,7 @@ bool NodeTemplate::hasOperator() const { } template -const Type* NodeTemplate::getType() const { +Type* NodeTemplate::getType() 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 ?" ); diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7be593575..7b171a48b 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -25,9 +25,18 @@ namespace CVC4 { __thread NodeManager* NodeManager::s_current = 0; +NodeManager::~NodeManager() { + NodeManagerScope nms(this); + while(!d_zombies.empty()) { + reclaimZombies(); + } + + poolRemove( &expr::NodeValue::s_null ); +} + NodeValue* NodeManager::poolLookup(NodeValue* nv) const { - NodeValueSet::const_iterator find = d_nodeValueSet.find(nv); - if(find == d_nodeValueSet.end()) { + NodeValuePool::const_iterator find = d_nodeValuePool.find(nv); + if(find == d_nodeValuePool.end()) { return NULL; } else { return *find; @@ -87,7 +96,7 @@ void NodeManager::reclaimZombies() { NodeValue* nv = *i; // collect ONLY IF still zero - if((*i)->d_rc == 0) { + if(nv->d_rc == 0) { Debug("gc") << "deleting node value " << nv << " [" << nv->d_id << "]: " << nv->toString() << "\n"; @@ -101,8 +110,7 @@ void NodeManager::reclaimZombies() { // decr ref counts of children nv->decrRefCounts(); - //free(nv); -#warning NOT FREEING NODEVALUES + free(nv); } } } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b40ec2978..a3be61e48 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -30,6 +30,7 @@ #include "expr/expr.h" #include "expr/node_value.h" #include "context/context.h" +#include "expr/type.h" namespace CVC4 { @@ -44,7 +45,7 @@ struct Type {}; }/* CVC4::expr::attr namespace */ typedef Attribute VarNameAttr; -typedef Attribute TypeAttr; +typedef ManagedAttribute TypeAttr; }/* CVC4::expr namespace */ @@ -55,12 +56,12 @@ class NodeManager { typedef __gnu_cxx::hash_set NodeValueSet; + expr::NodeValue::NodeValueEq> NodeValuePool; typedef __gnu_cxx::hash_set ZombieSet; - NodeValueSet d_nodeValueSet; + NodeValuePool d_nodeValuePool; expr::attr::AttributeManager d_attrManager; @@ -108,6 +109,8 @@ public: poolInsert( &expr::NodeValue::s_null ); } + ~NodeManager(); + static NodeManager* currentNM() { return s_current; } // general expression-builders @@ -121,8 +124,8 @@ public: Node mkNode(Kind kind, const std::vector& children); // variables are special, because duplicates are permitted - Node mkVar(const Type* type, const std::string& name); - Node mkVar(const Type* type); + Node mkVar(Type* type, const std::string& name); + Node mkVar(Type* type); Node mkVar(); template @@ -172,27 +175,26 @@ public: const typename AttrKind::value_type& value); /** Get the type for booleans. */ - inline const BooleanType* booleanType() const { + inline BooleanType* booleanType() const { return BooleanType::getInstance(); } /** Get the type for sorts. */ - inline const KindType* kindType() const { + inline KindType* kindType() const { return KindType::getInstance(); } /** Make a function type from domain to range. */ - inline const FunctionType* - mkFunctionType(const Type* domain, const Type* range) const; + inline FunctionType* mkFunctionType(Type* domain, Type* range) const; /** Make a function type with input types from argTypes. */ - inline const FunctionType* - mkFunctionType(const std::vector& argTypes, const Type* range) const; + inline FunctionType* mkFunctionType(const std::vector& argTypes, + Type* range) const; /** Make a new sort with the given name. */ - inline const Type* mkSort(const std::string& name) const; + inline Type* mkSort(const std::string& name) const; - inline const Type* getType(TNode n) const; + inline Type* getType(TNode n) const; }; /** @@ -308,41 +310,39 @@ inline void NodeManager::setAttribute(TNode n, /** Make a function type from domain to range. * TODO: Function types should be unique for this manager. */ -const FunctionType* -NodeManager::mkFunctionType(const Type* domain, - const Type* range) const { - std::vector argTypes; +FunctionType* NodeManager::mkFunctionType(Type* domain, + Type* range) const { + std::vector argTypes; argTypes.push_back(domain); return new FunctionType(argTypes, range); } /** Make a function type with input types from argTypes. * TODO: Function types should be unique for this manager. */ -const FunctionType* -NodeManager::mkFunctionType(const std::vector& argTypes, - const Type* range) const { +FunctionType* NodeManager::mkFunctionType(const std::vector& argTypes, + Type* range) const { Assert( argTypes.size() > 0 ); return new FunctionType(argTypes, range); } -const Type* -NodeManager::mkSort(const std::string& name) const { +Type* NodeManager::mkSort(const std::string& name) const { return new SortType(name); } -inline const Type* NodeManager::getType(TNode n) const { + +inline Type* NodeManager::getType(TNode n) const { return getAttribute(n, CVC4::expr::TypeAttr()); } inline void NodeManager::poolInsert(expr::NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) == d_nodeValueSet.end(), + Assert(d_nodeValuePool.find(nv) == d_nodeValuePool.end(), "NodeValue already in the pool!"); - d_nodeValueSet.insert(nv);// FIXME multithreading + d_nodeValuePool.insert(nv);// FIXME multithreading } inline void NodeManager::poolRemove(expr::NodeValue* nv) { - Assert(d_nodeValueSet.find(nv) != d_nodeValueSet.end(), + Assert(d_nodeValuePool.find(nv) != d_nodeValuePool.end(), "NodeValue is not in the pool!"); - d_nodeValueSet.erase(nv);// FIXME multithreading + d_nodeValuePool.erase(nv);// FIXME multithreading } }/* CVC4 namespace */ @@ -382,14 +382,15 @@ inline Node NodeManager::mkNode(Kind kind, const std::vector& children) { return NodeBuilder<>(this, kind).append(children); } -inline Node NodeManager::mkVar(const Type* type, const std::string& name) { +inline Node NodeManager::mkVar(Type* type, const std::string& name) { Node n = mkVar(type); n.setAttribute(expr::VarNameAttr(), name); return n; } -inline Node NodeManager::mkVar(const Type* type) { +inline Node NodeManager::mkVar(Type* type) { Node n = mkVar(); + type->inc();// reference-count the type n.setAttribute(expr::TypeAttr(), type); return n; } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 4bdda6810..2549f02ca 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -26,11 +26,12 @@ std::ostream& operator<<(std::ostream& out, const Type& e) { } Type::Type() : - d_name(std::string("")) { + d_name(std::string("")), + d_rc(0) { } Type::Type(std::string name) : - d_name(name) { + d_name(name) { } std::string Type::getName() const { @@ -39,7 +40,9 @@ std::string Type::getName() const { BooleanType BooleanType::s_instance; -BooleanType::BooleanType() : Type(std::string("BOOLEAN")) { +BooleanType::BooleanType() : + Type(std::string("BOOLEAN")) { + d_rc = RC_MAX;// singleton, not heap-allocated } BooleanType::~BooleanType() { @@ -54,22 +57,23 @@ bool BooleanType::isBoolean() const { return true; } -FunctionType::FunctionType(const std::vector& argTypes, - const Type* range) - : d_argTypes(argTypes), - d_rangeType(range) { +FunctionType::FunctionType(const std::vector& argTypes, + Type* range) : + d_argTypes(argTypes), + d_rangeType(range) { + Assert( argTypes.size() > 0 ); } - // FIXME: What becomes of argument types? +// FIXME: What becomes of argument types? FunctionType::~FunctionType() { } -const std::vector FunctionType::getArgTypes() const { +const std::vector FunctionType::getArgTypes() const { return d_argTypes; } -const Type* FunctionType::getRangeType() const { +Type* FunctionType::getRangeType() const { return d_rangeType; } @@ -100,7 +104,9 @@ void FunctionType::toStream(std::ostream& out) const { KindType KindType::s_instance; -KindType::KindType() : Type(std::string("KIND")) { +KindType::KindType() : + Type(std::string("KIND")) { + d_rc = RC_MAX;// singleton, not heap-allocated } KindType::~KindType() { @@ -115,12 +121,11 @@ KindType::getInstance() { return &s_instance; } -SortType::SortType(std::string name) - : Type(name) { +SortType::SortType(std::string name) : + Type(name) { } SortType::~SortType() { } - } diff --git a/src/expr/type.h b/src/expr/type.h index 7009ed504..fd9ea01d7 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -17,19 +17,32 @@ #define __CVC4__TYPE_H #include "cvc4_config.h" +#include "util/output.h" +#include "util/Assert.h" #include #include +#include namespace CVC4 { +namespace expr { + namespace attr { + struct TypeCleanupFcn; + }/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + class NodeManager; /** * Class encapsulating CVC4 expression types. */ class CVC4_PUBLIC Type { +protected: + static const unsigned RC_MAX = UINT_MAX; + public: + /** Comparision for equality */ bool operator==(const Type& t) const; @@ -72,11 +85,38 @@ protected: /** Create a type with the given name. */ Type(std::string name); - /** Destructor */ - virtual ~Type() { }; - /** The name of the type (may be empty). */ std::string d_name; + + /** + * The reference count for this Type (how many times it's referred + * to in the Type attribute table) + */ + unsigned d_rc; + + /** Force a virtual destructor for safety. */ + virtual ~Type() { + Assert(d_rc == RC_MAX || d_rc == 0, + "illegal ref count %u for destructed Type", d_rc); + } + + /** Increment the reference count */ + void inc() { + if(d_rc != RC_MAX) { + ++d_rc; + } + } + + /** Decrement the reference count */ + void dec() { + if(d_rc != RC_MAX) { + Assert(d_rc != 0, "illegal ref count %u for dec()", d_rc); + --d_rc; + } + } + + friend class ::CVC4::NodeManager; + friend struct ::CVC4::expr::attr::TypeCleanupFcn; }; /** @@ -117,10 +157,10 @@ class FunctionType : public Type { public: /** Retrieve the argument types. The vector will be non-empty. */ - const std::vector getArgTypes() const; + const std::vector getArgTypes() const; /** Get the range type (i.e., the type of the result). */ - const Type* getRangeType() const; + Type* getRangeType() const; /** Is this as function type? (Returns true.) */ bool isFunction() const; @@ -141,17 +181,17 @@ private: * @param argTypes a non-empty vector of input types * @param range the result type */ - FunctionType(const std::vector& argTypes, - const Type* range); + FunctionType(const std::vector& argTypes, + Type* range); /** Destructor */ ~FunctionType(); /** The list of input types. */ - const std::vector d_argTypes; + const std::vector d_argTypes; /** The result type. */ - const Type* d_rangeType; + Type* d_rangeType; friend class NodeManager; }; @@ -211,6 +251,22 @@ private: */ std::ostream& operator<<(std::ostream& out, const Type& t) CVC4_PUBLIC; -} +namespace expr { +namespace attr { + +struct TypeCleanupFcn { + static void cleanup(Type* t) { + // reference-count the Type + t->dec(); + if(t->d_rc == 0) { + delete t; + } + } +}; + +}/* CVC4::expr::attr namespace */ +}/* CVC4::expr namespace */ + +}/* CVC4 namespace */ #endif /* __CVC4__TYPE_H */ diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 593a89873..d20e59db3 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -60,7 +60,7 @@ Expr AntlrParser::getSymbol(const std::string& name, SymbolType type) { return d_varSymbolTable.getObject(name); default: - Unhandled("Unhandled symbol type!"); + Unhandled(type); } } @@ -72,17 +72,16 @@ Expr AntlrParser::getFunction(const std::string& name) { return getSymbol(name, SYM_FUNCTION); } -const Type* -AntlrParser::getType(const std::string& var_name, - SymbolType type) { +Type* AntlrParser::getType(const std::string& var_name, + SymbolType type) { Assert( isDeclared(var_name, type) ); - const Type* t = getSymbol(var_name,type).getType(); + Type* t = getSymbol(var_name, type).getType(); return t; } -const Type* AntlrParser::getSort(const std::string& name) { +Type* AntlrParser::getSort(const std::string& name) { Assert( isDeclared(name, SYM_SORT) ); - const Type* t = d_sortTable.getObject(name); + Type* t = d_sortTable.getObject(name); return t; } @@ -134,33 +133,30 @@ Expr AntlrParser::mkExpr(Kind kind, const std::vector& children) { return result; } -const Type* -AntlrParser::functionType(const Type* domainType, - const Type* rangeType) { - return d_exprManager->mkFunctionType(domainType,rangeType); +Type* AntlrParser::functionType(Type* domainType, + Type* rangeType) { + return d_exprManager->mkFunctionType(domainType, rangeType); } -const Type* -AntlrParser::functionType(const std::vector& argTypes, - const Type* rangeType) { +Type* AntlrParser::functionType(const std::vector& argTypes, + Type* rangeType) { Assert( argTypes.size() > 0 ); - return d_exprManager->mkFunctionType(argTypes,rangeType); + return d_exprManager->mkFunctionType(argTypes, rangeType); } -const Type* -AntlrParser::functionType(const std::vector& sorts) { +Type* AntlrParser::functionType(const std::vector& sorts) { Assert( sorts.size() > 0 ); if( sorts.size() == 1 ) { return sorts[0]; } else { - std::vector argTypes(sorts); - const Type* rangeType = argTypes.back(); + std::vector argTypes(sorts); + Type* rangeType = argTypes.back(); argTypes.pop_back(); - return functionType(argTypes,rangeType); + return functionType(argTypes, rangeType); } } -const Type* AntlrParser::predicateType(const std::vector& sorts) { +Type* AntlrParser::predicateType(const std::vector& sorts) { if(sorts.size() == 0) { return d_exprManager->booleanType(); } else { @@ -168,17 +164,16 @@ const Type* AntlrParser::predicateType(const std::vector& sorts) { } } -Expr -AntlrParser::mkVar(const std::string& name, const Type* type) { +Expr AntlrParser::mkVar(const std::string& name, Type* type) { Debug("parser") << "mkVar(" << name << "," << *type << ")" << std::endl; Expr expr = d_exprManager->mkVar(type, name); - defineVar(name,expr); + defineVar(name, expr); return expr; } -const std::vector -AntlrParser::mkVars(const std::vector names, - const Type* type) { +const std::vector +AntlrParser::mkVars(const std::vector names, + Type* type) { std::vector vars; for(unsigned i = 0; i < names.size(); ++i) { vars.push_back(mkVar(names[i], type)); @@ -186,55 +181,51 @@ AntlrParser::mkVars(const std::vector names, return vars; } -void -AntlrParser::defineVar(const std::string& name, const Expr& val) { +void AntlrParser::defineVar(const std::string& name, const Expr& val) { Assert(!isDeclared(name)); - d_varSymbolTable.bindName(name,val); + d_varSymbolTable.bindName(name, val); Assert(isDeclared(name)); } -void -AntlrParser::undefineVar(const std::string& name) { +void AntlrParser::undefineVar(const std::string& name) { Assert(isDeclared(name)); d_varSymbolTable.unbindName(name); Assert(!isDeclared(name)); } -const Type* -AntlrParser::newSort(const std::string& name) { +Type* AntlrParser::newSort(const std::string& name) { Debug("parser") << "newSort(" << name << ")" << std::endl; Assert( !isDeclared(name, SYM_SORT) ); - const Type* type = d_exprManager->mkSort(name); + Type* type = d_exprManager->mkSort(name); d_sortTable.bindName(name, type); Assert( isDeclared(name, SYM_SORT) ); return type; } -const std::vector +const std::vector AntlrParser::newSorts(const std::vector& names) { - std::vector types; + std::vector types; for(unsigned i = 0; i < names.size(); ++i) { types.push_back(newSort(names[i])); } return types; } -void -AntlrParser::setLogic(const std::string& name) { +void AntlrParser::setLogic(const std::string& name) { if( name == "QF_UF" ) { newSort("U"); } else { - Unhandled("setLogic: " + name); + Unhandled(name); } } -const BooleanType* AntlrParser::booleanType() { - return d_exprManager->booleanType(); +BooleanType* AntlrParser::booleanType() { + return d_exprManager->booleanType(); } -const KindType* AntlrParser::kindType() { - return d_exprManager->kindType(); +KindType* AntlrParser::kindType() { + return d_exprManager->kindType(); } unsigned int AntlrParser::minArity(Kind kind) { @@ -251,7 +242,7 @@ unsigned int AntlrParser::minArity(Kind kind) { return 1; case APPLY: - case EQUAL: + case EQUAL: case IFF: case IMPLIES: case PLUS: @@ -262,7 +253,7 @@ unsigned int AntlrParser::minArity(Kind kind) { return 3; default: - Unhandled("kind in minArity"); + Unhandled(kind); } } @@ -277,7 +268,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { case NOT: return 1; - case EQUAL: + case EQUAL: case IFF: case IMPLIES: case XOR: @@ -293,7 +284,7 @@ unsigned int AntlrParser::maxArity(Kind kind) { return UINT_MAX; default: - Unhandled("kind in maxArity"); + Unhandled(kind); } } @@ -309,7 +300,7 @@ bool AntlrParser::isDeclared(const std::string& name, SymbolType type) { case SYM_SORT: return d_sortTable.isBound(name); default: - Unhandled("Unhandled symbol type!"); + Unhandled(type); } } @@ -345,7 +336,7 @@ void AntlrParser::checkDeclaration(const std::string& varName, break; default: - Unhandled("Unknown check type!"); + Unhandled(check); } } @@ -353,7 +344,7 @@ void AntlrParser::checkFunction(const std::string& name) throw (antlr::SemanticException) { if( d_checksEnabled && !isFunction(name) ) { parseError("Expecting function symbol, found '" + name + "'"); - } + } } void AntlrParser::checkArity(Kind kind, unsigned int numArgs) diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h index 94d919555..e970ebd52 100644 --- a/src/parser/antlr_parser.h +++ b/src/parser/antlr_parser.h @@ -137,7 +137,7 @@ protected: /** * Returns a sort, given a name */ - const Type* getSort(const std::string& sort_name); + Type* getSort(const std::string& sort_name); /** * Types of symbols. Used to define namespaces. @@ -193,7 +193,7 @@ protected: * @param name the symbol to lookup * @param type the (namespace) type of the symbol */ - const Type* getType(const std::string& var_name, + Type* getType(const std::string& var_name, SymbolType type = SYM_VARIABLE); /** @@ -244,13 +244,13 @@ protected: Expr mkExpr(Kind kind, const std::vector& children); /** Create a new CVC4 variable expression of the given type. */ - Expr mkVar(const std::string& name, const Type* type); + Expr mkVar(const std::string& name, Type* type); /** Create a set of new CVC4 variable expressions of the given type. */ const std::vector mkVars(const std::vector names, - const Type* type); + Type* type); /** Create a new variable definition (e.g., from a let binding). */ void defineVar(const std::string& name, const Expr& val); @@ -258,12 +258,12 @@ protected: void undefineVar(const std::string& name); /** Returns a function type over the given domain and range types. */ - const Type* functionType(const Type* domain, const Type* range); + Type* functionType(Type* domain, Type* range); /** Returns a function type over the given types. argTypes must be non-empty. */ - const Type* functionType(const std::vector& argTypes, - const Type* rangeType); + Type* functionType(const std::vector& argTypes, + Type* rangeType); /** * Returns a function type over the given types. If types has only @@ -271,7 +271,7 @@ protected: * * @param types a non-empty list of input and output types. */ - const Type* functionType(const std::vector& types); + Type* functionType(const std::vector& types); /** * Returns a predicate type over the given sorts. If sorts is empty, @@ -279,17 +279,17 @@ protected: * @param sorts a list of input types */ - const Type* predicateType(const std::vector& sorts); + Type* predicateType(const std::vector& sorts); /** * Creates a new sort with the given name. */ - const Type* newSort(const std::string& name); + Type* newSort(const std::string& name); /** * Creates a new sorts with the given names. */ - const std::vector + const std::vector newSorts(const std::vector& names); /** Is the symbol bound to a boolean variable? */ @@ -302,10 +302,10 @@ protected: bool isPredicate(const std::string& name); /** Returns the boolean type. */ - const BooleanType* booleanType(); + BooleanType* booleanType(); /** Returns the kind type (i.e., the type of types). */ - const KindType* kindType(); + KindType* kindType(); /** Returns the minimum arity of the given kind. */ static unsigned int minArity(Kind kind); @@ -346,7 +346,7 @@ private: SymbolTable d_varSymbolTable; /** The sort table */ - SymbolTable d_sortTable; + SymbolTable d_sortTable; /** Are semantic checks enabled during parsing? */ bool d_checksEnabled; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 9492b36d9..55ae0ff73 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -89,15 +89,15 @@ command returns [CVC4::Command* cmd = 0] declaration returns [CVC4::DeclarationCommand* cmd] { vector ids; - const Type* t; + Type* t; Debug("parser") << "declaration: " << LT(1)->getText() << endl; -} +} : identifierList[ids, CHECK_UNDECLARED] COLON t = declType[ids] SEMICOLON { cmd = new DeclarationCommand(ids,t); } ; /** Match the right-hand side of a declaration. Returns the type. */ -declType[std::vector& idList] returns [const CVC4::Type* t] +declType[std::vector& idList] returns [CVC4::Type* t] { Debug("parser") << "declType: " << LT(1)->getText() << endl; } @@ -111,9 +111,9 @@ declType[std::vector& idList] returns [const CVC4::Type* t] * Match the type in a declaration and do the declaration binding. * TODO: Actually parse sorts into Type objects. */ -type returns [const CVC4::Type* t] +type returns [CVC4::Type* t] { - const Type *t1, *t2; + Type *t1, *t2; Debug("parser") << "type: " << LT(1)->getText() << endl; } : /* Simple type */ @@ -122,10 +122,10 @@ type returns [const CVC4::Type* t] t1 = baseType RIGHT_ARROW t2 = baseType { t = functionType(t1,t2); } | /* Multi-parameter function type */ - LPAREN t1 = baseType - { std::vector argTypes; + LPAREN t1 = baseType + { std::vector argTypes; argTypes.push_back(t1); } - (COMMA t1 = baseType { argTypes.push_back(t1); } )+ + (COMMA t1 = baseType { argTypes.push_back(t1); } )+ RPAREN RIGHT_ARROW t2 = baseType { t = functionType(argTypes,t2); } ; @@ -136,7 +136,7 @@ type returns [const CVC4::Type* t] * @param idList the list to fill with identifiers. * @param check what kinds of check to perform on the symbols */ -identifierList[std::vector& idList, +identifierList[std::vector& idList, DeclarationCheck check = CHECK_NONE] { string id; @@ -150,10 +150,10 @@ identifierList[std::vector& idList, * Matches an identifier and returns a string. */ identifier[DeclarationCheck check = CHECK_NONE, - SymbolType type = SYM_VARIABLE] + SymbolType type = SYM_VARIABLE] returns [std::string id] : x:IDENTIFIER - { id = x->getText(); + { id = x->getText(); checkDeclaration(id, check, type); } ; @@ -161,7 +161,7 @@ returns [std::string id] * Matches a type. * TODO: parse more types */ -baseType returns [const CVC4::Type* t] +baseType returns [CVC4::Type* t] { std::string id; Debug("parser") << "base type: " << LT(1)->getText() << endl; @@ -173,7 +173,7 @@ baseType returns [const CVC4::Type* t] /** * Matches a type identifier */ -typeSymbol returns [const CVC4::Type* t] +typeSymbol returns [CVC4::Type* t] { std::string id; Debug("parser") << "type symbol: " << LT(1)->getText() << endl; @@ -228,7 +228,7 @@ impliesFormula returns [CVC4::Expr f] Expr e; Debug("parser") << "=> Formula: " << LT(1)->getText() << endl; } - : f = orFormula + : f = orFormula ( IMPLIES e = impliesFormula { f = mkExpr(CVC4::kind::IMPLIES, f, e); } )? @@ -259,7 +259,7 @@ xorFormula returns [CVC4::Expr f] Debug("parser") << "XOR formula: " << LT(1)->getText() << endl; } : f = andFormula - ( XOR e = andFormula + ( XOR e = andFormula { f = mkExpr(CVC4::kind::XOR,f, e); } )* ; @@ -289,7 +289,7 @@ notFormula returns [CVC4::Expr f] Debug("parser") << "NOT formula: " << LT(1)->getText() << endl; } : /* negation */ - NOT f = notFormula + NOT f = notFormula { f = mkExpr(CVC4::kind::NOT, f); } | /* a boolean atom */ f = predFormula @@ -300,7 +300,7 @@ predFormula returns [CVC4::Expr f] Debug("parser") << "predicate formula: " << LT(1)->getText() << endl; } : { Expr e; } - f = term + f = term (EQUAL e = term { f = mkExpr(CVC4::kind::EQUAL, f, e); } )? @@ -315,8 +315,8 @@ term returns [CVC4::Expr t] Debug("parser") << "term: " << LT(1)->getText() << endl; } : /* function application */ - // { isFunction(LT(1)->getText()) }? - { Expr f; + // { isFunction(LT(1)->getText()) }? + { Expr f; std::vector args; } f = functionSymbol[CHECK_DECLARED] { args.push_back( f ); } @@ -343,16 +343,16 @@ term returns [CVC4::Expr t] /** * Parses an ITE term. */ -iteTerm returns [CVC4::Expr t] +iteTerm returns [CVC4::Expr t] { Expr iteCondition, iteThen, iteElse; Debug("parser") << "ite: " << LT(1)->getText() << endl; } - : IF iteCondition = formula + : IF iteCondition = formula THEN iteThen = formula iteElse = iteElseTerm - ENDIF - { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } + ENDIF + { t = mkExpr(CVC4::kind::ITE, iteCondition, iteThen, iteElse); } ; /** @@ -379,8 +379,8 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f] { Debug("parser") << "function symbol: " << LT(1)->getText() << endl; std::string name; -} +} : name = identifier[check,SYM_FUNCTION] - { checkFunction(name); + { checkFunction(name); f = getFunction(name); } ; diff --git a/src/parser/smt/smt_lexer.g b/src/parser/smt/smt_lexer.g index e3985818c..d694cd93f 100644 --- a/src/parser/smt/smt_lexer.g +++ b/src/parser/smt/smt_lexer.g @@ -115,11 +115,11 @@ C_IDENTIFIER options { paraphrase = "an attribute (e.g., ':x')"; testLiterals = ; VAR_IDENTIFIER options { paraphrase = "a variable (e.g., '?x')"; testLiterals = false; } - : '?' IDENTIFIER + : '?' IDENTIFIER ; FUN_IDENTIFIER options { paraphrase = "a function variable (e.g, '$x')"; testLiterals = false; } - : '$' IDENTIFIER + : '$' IDENTIFIER ; diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index d1ac50651..f9758dc5c 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -102,12 +102,12 @@ benchAttribute returns [Command* smt_command = 0] { smt_command = new AssertCommand(formula); } | FORMULA_ATTR formula = annotatedFormula { smt_command = new CheckSatCommand(formula); } - | STATUS_ATTR b_status = status - { smt_command = new SetBenchmarkStatusCommand(b_status); } - | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN - | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN - | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN - | NOTES_ATTR STRING_LITERAL + | STATUS_ATTR b_status = status + { smt_command = new SetBenchmarkStatusCommand(b_status); } + | EXTRAFUNS_ATTR LPAREN (functionDeclaration)+ RPAREN + | EXTRAPREDS_ATTR LPAREN (predicateDeclaration)+ RPAREN + | EXTRASORTS_ATTR LPAREN (sortDeclaration)+ RPAREN + | NOTES_ATTR STRING_LITERAL | annotation ; @@ -119,12 +119,12 @@ annotatedFormula returns [CVC4::Expr formula] { Debug("parser") << "annotated formula: " << LT(1)->getText() << endl; Kind kind = CVC4::kind::UNDEFINED_KIND; - vector args; + vector args; std::string name; Expr expr1, expr2, expr3; } : /* a built-in operator application */ - LPAREN kind = builtinOp annotatedFormulas[args] RPAREN + LPAREN kind = builtinOp annotatedFormulas[args] RPAREN { checkArity(kind, args.size()); formula = mkExpr(kind,args); } @@ -134,16 +134,16 @@ annotatedFormula returns [CVC4::Expr formula] { std::vector diseqs; for(unsigned i = 0; i < args.size(); ++i) { for(unsigned j = i+1; j < args.size(); ++j) { - diseqs.push_back(mkExpr(CVC4::kind::NOT, + diseqs.push_back(mkExpr(CVC4::kind::NOT, mkExpr(CVC4::kind::EQUAL,args[i],args[j]))); } } formula = mkExpr(CVC4::kind::AND, diseqs); } | /* An ite expression */ - LPAREN (ITE | IF_THEN_ELSE) + LPAREN (ITE | IF_THEN_ELSE) { Expr test, trueExpr, falseExpr; } - test = annotatedFormula + test = annotatedFormula trueExpr = annotatedFormula falseExpr = annotatedFormula RPAREN @@ -164,12 +164,12 @@ annotatedFormula returns [CVC4::Expr formula] formula=annotatedFormula { undefineVar(name); } RPAREN - + | /* A non-built-in function application */ // Semantic predicate not necessary if parenthesized subexpressions // are disallowed - // { isFunction(LT(2)->getText()) }? + // { isFunction(LT(2)->getText()) }? { Expr f; } LPAREN f = functionSymbol @@ -180,7 +180,7 @@ annotatedFormula returns [CVC4::Expr formula] | /* a variable */ { std::string name; } - ( name = identifier[CHECK_DECLARED] + ( name = identifier[CHECK_DECLARED] | name = variable[CHECK_DECLARED] | name = function_var[CHECK_DECLARED] ) { formula = getVariable(name); } @@ -195,7 +195,7 @@ annotatedFormula returns [CVC4::Expr formula] * Matches a sequence of annotaed formulas and puts them into the formulas * vector. * @param formulas the vector to fill with formulas - */ + */ annotatedFormulas[std::vector& formulas] { Expr f; @@ -222,7 +222,7 @@ builtinOp returns [CVC4::Kind kind] ; /** - * Matches a (possibly undeclared) predicate identifier (returning the string). + * Matches a (possibly undeclared) predicate identifier (returning the string). * @param check what kind of check to do with the symbol */ predicateName[DeclarationCheck check = CHECK_NONE] returns [std::string p] @@ -241,14 +241,14 @@ functionName[DeclarationCheck check = CHECK_NONE] returns [std::string name] * Matches an previously declared function symbol (returning an Expr) */ functionSymbol returns [CVC4::Expr fun] -{ +{ string name; } : name = functionName[CHECK_DECLARED] { checkFunction(name); fun = getFunction(name); } ; - + /** * Matches an attribute name from the input (:attribute_name). */ @@ -272,12 +272,12 @@ function_var[DeclarationCheck check = CHECK_NONE] returns [std::string name] * Matches the sort symbol, which can be an arbitrary identifier. * @param check the check to perform on the name */ -sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] - : name = identifier[check,SYM_SORT] +sortName[DeclarationCheck check = CHECK_NONE] returns [std::string name] + : name = identifier[check,SYM_SORT] ; -sortSymbol returns [const CVC4::Type* t] -{ +sortSymbol returns [CVC4::Type* t] +{ std::string name; } : name = sortName { t = getSort(name); } @@ -286,47 +286,47 @@ sortSymbol returns [const CVC4::Type* t] functionDeclaration { string name; - const Type* t; - std::vector sorts; + Type* t; + std::vector sorts; } - : LPAREN name = functionName[CHECK_UNDECLARED] + : LPAREN name = functionName[CHECK_UNDECLARED] t = sortSymbol // require at least one sort { sorts.push_back(t); } sortList[sorts] RPAREN { t = functionType(sorts); - mkVar(name, t); } + mkVar(name, t); } ; - + /** * Matches the declaration of a predicate and declares it */ predicateDeclaration { string p_name; - std::vector p_sorts; - const Type *t; + std::vector p_sorts; + Type *t; } : LPAREN p_name = predicateName[CHECK_UNDECLARED] sortList[p_sorts] RPAREN { t = predicateType(p_sorts); - mkVar(p_name, t); } + mkVar(p_name, t); } ; -sortDeclaration +sortDeclaration { string name; } : name = sortName[CHECK_UNDECLARED] { newSort(name); } ; - + /** * Matches a sequence of sort symbols and fills them into the given vector. */ -sortList[std::vector& sorts] +sortList[std::vector& sorts] { - const Type* t; + Type* t; } - : ( t = sortSymbol { sorts.push_back(t); })* + : ( t = sortSymbol { sorts.push_back(t); })* ; /** @@ -350,11 +350,11 @@ annotation * @param check what kinds of check to do on the symbol * @return the id string */ -identifier[DeclarationCheck check = CHECK_NONE, - SymbolType type = SYM_VARIABLE] +identifier[DeclarationCheck check = CHECK_NONE, + SymbolType type = SYM_VARIABLE] returns [std::string id] { - Debug("parser") << "identifier: " << LT(1)->getText() + Debug("parser") << "identifier: " << LT(1)->getText() << " check? " << toString(check) << " type? " << toString(type) << endl; } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c00112cd0..a55c146b8 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -51,12 +51,12 @@ public: * 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); + static Node preprocess(SmtEngine& smt, TNode n); /** * Adds a formula to the current context. */ - static void addFormula(SmtEngine& smt, TNode node); + static void addFormula(SmtEngine& smt, TNode n); };/* class SmtEnginePrivate */ }/* namespace CVC4::smt */ @@ -97,8 +97,8 @@ void SmtEngine::doCommand(Command* c) { c->invoke(this); } -Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) { - return smt.d_theoryEngine->preprocess(e); +Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode n) { + return smt.d_theoryEngine->preprocess(n); } Result SmtEngine::check() { @@ -111,9 +111,9 @@ Result SmtEngine::quickCheck() { return Result(Result::VALIDITY_UNKNOWN); } -void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode e) { - Debug("smt") << "push_back assertion " << e << std::endl; - smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, e)); +void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n) { + Debug("smt") << "push_back assertion " << n << std::endl; + smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n)); } Result SmtEngine::checkSat(const BoolExpr& e) { diff --git a/src/theory/interrupted.h b/src/theory/interrupted.h index f7a269f0b..00afd3b2b 100644 --- a/src/theory/interrupted.h +++ b/src/theory/interrupted.h @@ -13,6 +13,8 @@ ** The theory output channel interface. **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__INTERRUPTED_H #define __CVC4__THEORY__INTERRUPTED_H @@ -21,14 +23,7 @@ namespace CVC4 { namespace theory { -class CVC4_PUBLIC Interrupted : public CVC4::Exception { -public: - - // Constructors - Interrupted() : CVC4::Exception("CVC4::Theory::Interrupted") {} - Interrupted(const std::string& msg) : CVC4::Exception(msg) {} - Interrupted(const char* msg) : CVC4::Exception(msg) {} - +class Interrupted : public CVC4::Exception { };/* class Interrupted */ }/* CVC4::theory namespace */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 128e28ca2..ccbfa327a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -183,7 +183,8 @@ private: * a ECAttr is being destructed. */ struct ECCleanupFcn{ - static void cleanup(ECData* & ec){ + static void cleanup(ECData* ec){ + Debug("ufgc") << "cleaning up ECData " << ec << "\n"; ec->deleteSelf(); } }; diff --git a/src/util/output.h b/src/util/output.h index 5c265e699..77b755ad5 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -109,6 +109,9 @@ public: void off(const char* tag) { d_tags.erase (std::string(tag)); } void off(std::string tag) { d_tags.erase (tag); } + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + void setStream(std::ostream& os) { d_os = &os; } };/* class Debug */ @@ -241,6 +244,9 @@ public: void off(const char* tag) { d_tags.erase (std::string(tag)); }; void off(std::string tag) { d_tags.erase (tag); }; + bool isOn(const char* tag) { return d_tags.find(std::string(tag)) != d_tags.end(); } + bool isOn(std::string tag) { return d_tags.find(tag) != d_tags.end(); } + void setStream(std::ostream& os) { d_os = &os; } };/* class Trace */ @@ -289,6 +295,9 @@ public: void off(const char* tag) {} void off(std::string tag) {} + bool isOn(const char* tag) { return false; } + bool isOn(std::string tag) { return false; } + void setStream(std::ostream& os) {} };/* class NullDebugC */ diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 305731f5b..f78171dac 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -4,6 +4,7 @@ UNIT_TESTS = \ expr/node_black \ expr/kind_black \ expr/node_builder_black \ + expr/attribute_white \ expr/attribute_black \ parser/parser_black \ context/context_black \ diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h index b5e897e89..12ecd347a 100644 --- a/test/unit/expr/attribute_black.h +++ b/test/unit/expr/attribute_black.h @@ -62,7 +62,7 @@ public: struct MyDataAttributeId {}; struct MyDataCleanupFunction { - static void cleanup(MyData*& myData){ + static void cleanup(MyData* myData){ delete myData; } }; diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h new file mode 100644 index 000000000..7a0e538f6 --- /dev/null +++ b/test/unit/expr/attribute_white.h @@ -0,0 +1,565 @@ +/********************* */ +/** attribute_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 Node attributes. + **/ + +#include + +#include + +#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 "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; + +struct Test1; +struct Test2; +struct Test3; +struct Test4; +struct Test5; + +typedef Attribute TestStringAttr1; +typedef Attribute TestStringAttr2; + +// it would be nice to have CDAttribute<> for context-dependence +typedef CDAttribute TestCDFlag; + +typedef Attribute TestFlag1; +typedef Attribute TestFlag2; +typedef Attribute TestFlag3; +typedef Attribute TestFlag4; +typedef Attribute TestFlag5; + +typedef CDAttribute TestFlag1cd; +typedef CDAttribute TestFlag2cd; + +class AttributeWhite : public CxxTest::TestSuite { + + Context* d_ctxt; + NodeManager* d_nm; + NodeManagerScope* d_scope; + +public: + + void setUp() { + 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 testAttributeIds() { + TS_ASSERT(VarNameAttr::s_id == 0); + TS_ASSERT(TestStringAttr1::s_id == 1); + TS_ASSERT(TestStringAttr2::s_id == 2); + TS_ASSERT((attr::LastAttributeId::s_id == 3)); + + TS_ASSERT(TypeAttr::s_id == 0); + TS_ASSERT((attr::LastAttributeId::s_id == 1)); + + TS_ASSERT(TestFlag1::s_id == 0); + TS_ASSERT(TestFlag2::s_id == 1); + TS_ASSERT(TestFlag3::s_id == 2); + TS_ASSERT(TestFlag4::s_id == 3); + TS_ASSERT(TestFlag5::s_id == 4); + TS_ASSERT((attr::LastAttributeId::s_id == 5)); + + TS_ASSERT(TestFlag1cd::s_id == 0); + TS_ASSERT(TestFlag2cd::s_id == 1); + TS_ASSERT((attr::LastAttributeId::s_id == 2)); + } + + void testCDAttributes() { + AttributeManager& am = d_nm->d_attrManager; + + //Debug.on("boolattr"); + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 1 + + // test that all boolean flags are FALSE to start + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + // test that they all HAVE the boolean attributes + TS_ASSERT(a.hasAttribute(TestFlag1cd())); + TS_ASSERT(b.hasAttribute(TestFlag1cd())); + TS_ASSERT(c.hasAttribute(TestFlag1cd())); + + // test two-arg version of hasAttribute() + bool bb; + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb)); + TS_ASSERT(! bb); + + // setting boolean flags + Debug("boolattr", "set flag 1 on a to T\n"); + a.setAttribute(TestFlag1cd(), true); + Debug("boolattr", "set flag 1 on b to F\n"); + b.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on c to F\n"); + c.setAttribute(TestFlag1cd(), false); + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on a to F\n"); + a.setAttribute(TestFlag1cd(), false); + Debug("boolattr", "set flag 1 on b to T\n"); + b.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->push(); // level 3 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + Debug("boolattr", "set flag 1 on c to T\n"); + c.setAttribute(TestFlag1cd(), true); + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 2 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 1 + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + + d_ctxt->pop(); // level 0 + + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1cd())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1cd())); + +#ifdef CVC4_ASSERTIONS + TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); +#endif /* CVC4_ASSERTIONS */ + } + + void testAttributes() { + AttributeManager& am = d_nm->d_attrManager; + + //Debug.on("boolattr"); + + Node a = d_nm->mkVar(); + Node b = d_nm->mkVar(); + Node c = d_nm->mkVar(); + Node unnamed = d_nm->mkVar(); + + a.setAttribute(VarNameAttr(), "a"); + b.setAttribute(VarNameAttr(), "b"); + c.setAttribute(VarNameAttr(), "c"); + + // test that all boolean flags are FALSE to start + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag1())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1())); + Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); + TS_ASSERT(! unnamed.getAttribute(TestFlag1())); + + Debug("boolattr", "get flag 2 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag2())); + Debug("boolattr", "get flag 2 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag2())); + Debug("boolattr", "get flag 2 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag2())); + Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + TS_ASSERT(! unnamed.getAttribute(TestFlag2())); + + Debug("boolattr", "get flag 3 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag3())); + Debug("boolattr", "get flag 3 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag3())); + Debug("boolattr", "get flag 3 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag3())); + Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); + TS_ASSERT(! unnamed.getAttribute(TestFlag3())); + + Debug("boolattr", "get flag 4 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag4())); + Debug("boolattr", "get flag 4 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag4())); + Debug("boolattr", "get flag 4 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag4())); + Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); + TS_ASSERT(! unnamed.getAttribute(TestFlag4())); + + Debug("boolattr", "get flag 5 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag5())); + Debug("boolattr", "get flag 5 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag5())); + Debug("boolattr", "get flag 5 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag5())); + Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); + TS_ASSERT(! unnamed.getAttribute(TestFlag5())); + + // test that they all HAVE the boolean attributes + TS_ASSERT(a.hasAttribute(TestFlag1())); + TS_ASSERT(b.hasAttribute(TestFlag1())); + TS_ASSERT(c.hasAttribute(TestFlag1())); + TS_ASSERT(unnamed.hasAttribute(TestFlag1())); + + TS_ASSERT(a.hasAttribute(TestFlag2())); + TS_ASSERT(b.hasAttribute(TestFlag2())); + TS_ASSERT(c.hasAttribute(TestFlag2())); + TS_ASSERT(unnamed.hasAttribute(TestFlag2())); + + TS_ASSERT(a.hasAttribute(TestFlag3())); + TS_ASSERT(b.hasAttribute(TestFlag3())); + TS_ASSERT(c.hasAttribute(TestFlag3())); + TS_ASSERT(unnamed.hasAttribute(TestFlag3())); + + TS_ASSERT(a.hasAttribute(TestFlag4())); + TS_ASSERT(b.hasAttribute(TestFlag4())); + TS_ASSERT(c.hasAttribute(TestFlag4())); + TS_ASSERT(unnamed.hasAttribute(TestFlag4())); + + TS_ASSERT(a.hasAttribute(TestFlag5())); + TS_ASSERT(b.hasAttribute(TestFlag5())); + TS_ASSERT(c.hasAttribute(TestFlag5())); + TS_ASSERT(unnamed.hasAttribute(TestFlag5())); + + // test two-arg version of hasAttribute() + bool bb; + Debug("boolattr", "get flag 1 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 2 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 2 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 2 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 3 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 3 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 3 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 4 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 4 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 4 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb)); + TS_ASSERT(! bb); + + Debug("boolattr", "get flag 5 on a (should be F)\n"); + TS_ASSERT(a.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 5 on b (should be F)\n"); + TS_ASSERT(b.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 5 on c (should be F)\n"); + TS_ASSERT(c.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); + TS_ASSERT(unnamed.hasAttribute(TestFlag5(), bb)); + TS_ASSERT(! bb); + + // setting boolean flags + Debug("boolattr", "set flag 1 on a to T\n"); + a.setAttribute(TestFlag1(), true); + Debug("boolattr", "set flag 1 on b to F\n"); + b.setAttribute(TestFlag1(), false); + Debug("boolattr", "set flag 1 on c to F\n"); + c.setAttribute(TestFlag1(), false); + Debug("boolattr", "set flag 1 on unnamed to T\n"); + unnamed.setAttribute(TestFlag1(), true); + + Debug("boolattr", "set flag 2 on a to F\n"); + a.setAttribute(TestFlag2(), false); + Debug("boolattr", "set flag 2 on b to T\n"); + b.setAttribute(TestFlag2(), true); + Debug("boolattr", "set flag 2 on c to T\n"); + c.setAttribute(TestFlag2(), true); + Debug("boolattr", "set flag 2 on unnamed to F\n"); + unnamed.setAttribute(TestFlag2(), false); + + Debug("boolattr", "set flag 3 on a to T\n"); + a.setAttribute(TestFlag3(), true); + Debug("boolattr", "set flag 3 on b to T\n"); + b.setAttribute(TestFlag3(), true); + Debug("boolattr", "set flag 3 on c to T\n"); + c.setAttribute(TestFlag3(), true); + Debug("boolattr", "set flag 3 on unnamed to T\n"); + unnamed.setAttribute(TestFlag3(), true); + + Debug("boolattr", "set flag 4 on a to T\n"); + a.setAttribute(TestFlag4(), true); + Debug("boolattr", "set flag 4 on b to T\n"); + b.setAttribute(TestFlag4(), true); + Debug("boolattr", "set flag 4 on c to T\n"); + c.setAttribute(TestFlag4(), true); + Debug("boolattr", "set flag 4 on unnamed to T\n"); + unnamed.setAttribute(TestFlag4(), true); + + Debug("boolattr", "set flag 5 on a to T\n"); + a.setAttribute(TestFlag5(), true); + Debug("boolattr", "set flag 5 on b to T\n"); + b.setAttribute(TestFlag5(), true); + Debug("boolattr", "set flag 5 on c to F\n"); + c.setAttribute(TestFlag5(), false); + Debug("boolattr", "set flag 5 on unnamed to T\n"); + unnamed.setAttribute(TestFlag5(), true); + + TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr1())); + TS_ASSERT(! b.hasAttribute(TestStringAttr1())); + TS_ASSERT(! c.hasAttribute(TestStringAttr1())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr2())); + TS_ASSERT(! b.hasAttribute(TestStringAttr2())); + TS_ASSERT(! c.hasAttribute(TestStringAttr2())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); + + Debug("boolattr", "get flag 1 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag1())); + Debug("boolattr", "get flag 1 on b (should be F)\n"); + TS_ASSERT(! b.getAttribute(TestFlag1())); + Debug("boolattr", "get flag 1 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag1())); + Debug("boolattr", "get flag 1 on unnamed (should be T)\n"); + TS_ASSERT(unnamed.getAttribute(TestFlag1())); + + Debug("boolattr", "get flag 2 on a (should be F)\n"); + TS_ASSERT(! a.getAttribute(TestFlag2())); + Debug("boolattr", "get flag 2 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag2())); + Debug("boolattr", "get flag 2 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag2())); + Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); + TS_ASSERT(! unnamed.getAttribute(TestFlag2())); + + Debug("boolattr", "get flag 3 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag3())); + Debug("boolattr", "get flag 3 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag3())); + Debug("boolattr", "get flag 3 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag3())); + Debug("boolattr", "get flag 3 on unnamed (should be T)\n"); + TS_ASSERT(unnamed.getAttribute(TestFlag3())); + + Debug("boolattr", "get flag 4 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag4())); + Debug("boolattr", "get flag 4 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag4())); + Debug("boolattr", "get flag 4 on c (should be T)\n"); + TS_ASSERT(c.getAttribute(TestFlag4())); + Debug("boolattr", "get flag 4 on unnamed (should be T)\n"); + TS_ASSERT(unnamed.getAttribute(TestFlag4())); + + Debug("boolattr", "get flag 5 on a (should be T)\n"); + TS_ASSERT(a.getAttribute(TestFlag5())); + Debug("boolattr", "get flag 5 on b (should be T)\n"); + TS_ASSERT(b.getAttribute(TestFlag5())); + Debug("boolattr", "get flag 5 on c (should be F)\n"); + TS_ASSERT(! c.getAttribute(TestFlag5())); + Debug("boolattr", "get flag 5 on unnamed (should be T)\n"); + TS_ASSERT(unnamed.getAttribute(TestFlag5())); + + a.setAttribute(TestStringAttr1(), "foo"); + b.setAttribute(TestStringAttr1(), "bar"); + c.setAttribute(TestStringAttr1(), "baz"); + + TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + + TS_ASSERT(a.hasAttribute(TestStringAttr1())); + TS_ASSERT(b.hasAttribute(TestStringAttr1())); + TS_ASSERT(c.hasAttribute(TestStringAttr1())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); + + TS_ASSERT(! a.hasAttribute(TestStringAttr2())); + TS_ASSERT(! b.hasAttribute(TestStringAttr2())); + TS_ASSERT(! c.hasAttribute(TestStringAttr2())); + TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); + + a.setAttribute(VarNameAttr(), "b"); + b.setAttribute(VarNameAttr(), "c"); + c.setAttribute(VarNameAttr(), "a"); + + TS_ASSERT(c.getAttribute(VarNameAttr()) == "a"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(a.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(a.getAttribute(VarNameAttr()) == "b"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(b.getAttribute(VarNameAttr()) == "c"); + TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); + + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); + TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); + + TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); + } +}; diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index c1ece1145..21c19a8f9 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -72,7 +72,7 @@ public: TS_ASSERT(b.isNull()); Node c = b; - + TS_ASSERT(c.isNull()); } @@ -93,7 +93,7 @@ public: /*tests: bool operator==(const Node& e) const */ void testOperatorEquals() { Node a, b, c; - + b = d_nodeManager->mkVar(); a = b; @@ -113,7 +113,7 @@ public: TS_ASSERT(c==a); TS_ASSERT(c==b); - TS_ASSERT(c==c); + TS_ASSERT(c==c); TS_ASSERT(d==d); @@ -133,7 +133,7 @@ public: Node a, b, c; - + b = d_nodeManager->mkVar(); a = b; @@ -142,19 +142,19 @@ public: Node d = d_nodeManager->mkVar(); /*structed assuming operator == works */ - TS_ASSERT(iff(a!=a,!(a==a))); - TS_ASSERT(iff(a!=b,!(a==b))); - TS_ASSERT(iff(a!=c,!(a==c))); + TS_ASSERT(iff(a!=a, !(a==a))); + TS_ASSERT(iff(a!=b, !(a==b))); + TS_ASSERT(iff(a!=c, !(a==c))); - TS_ASSERT(iff(b!=a,!(b==a))); - TS_ASSERT(iff(b!=b,!(b==b))); - TS_ASSERT(iff(b!=c,!(b==c))); + TS_ASSERT(iff(b!=a, !(b==a))); + TS_ASSERT(iff(b!=b, !(b==b))); + TS_ASSERT(iff(b!=c, !(b==c))); - TS_ASSERT(iff(c!=a,!(c==a))); - TS_ASSERT(iff(c!=b,!(c==b))); - TS_ASSERT(iff(c!=c,!(c==c))); + TS_ASSERT(iff(c!=a, !(c==a))); + TS_ASSERT(iff(c!=b, !(c==b))); + TS_ASSERT(iff(c!=c, !(c==c))); TS_ASSERT(!(d!=d)); @@ -164,7 +164,7 @@ public: } - void testOperatorSquare() { + void testOperatorSquare() { /*Node operator[](int i) const */ #ifdef CVC4_ASSERTIONS @@ -177,7 +177,7 @@ public: Node tb = d_nodeManager->mkNode(TRUE); Node eb = d_nodeManager->mkNode(FALSE); Node cnd = d_nodeManager->mkNode(XOR, tb, eb); - Node ite = cnd.iteNode(tb,eb); + Node ite = cnd.iteNode(tb, eb); TS_ASSERT(tb == cnd[0]); TS_ASSERT(eb == cnd[1]); @@ -188,8 +188,8 @@ public: #ifdef CVC4_ASSERTIONS //Bounds check on a node with children - TS_ASSERT_THROWS(ite == ite[-1],AssertionException); - TS_ASSERT_THROWS(ite == ite[4],AssertionException); + TS_ASSERT_THROWS(ite == ite[-1], AssertionException); + TS_ASSERT_THROWS(ite == ite[4], AssertionException); #endif /* CVC4_ASSERTIONS */ } @@ -197,23 +197,23 @@ public: void testOperatorAssign() { Node a, b; Node c = d_nodeManager->mkNode(NOT); - + b = c; TS_ASSERT(b==c); - + a = b = c; TS_ASSERT(a==b); TS_ASSERT(a==c); } - + void testOperatorLessThan() { /* We don't have access to the ids so we can't test the implementation - * in the black box tests. + * in the black box tests. */ - + Node a = d_nodeManager->mkVar(); Node b = d_nodeManager->mkVar(); @@ -225,14 +225,14 @@ public: TS_ASSERT(!(cmkNode(TRUE); Node parent = d_nodeManager->mkNode(NOT, child); @@ -245,9 +245,9 @@ public: Node curr = d_nodeManager->mkNode(NULL_EXPR); for(int i=0;imkNode(AND,curr); + curr = d_nodeManager->mkNode(AND, curr); } - + for(int i=0;imkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.eqNode(right); - + TS_ASSERT(EQUAL == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -283,31 +283,31 @@ public: TS_ASSERT(1 == parent.getNumChildren()); TS_ASSERT(parent[0] == child); - + } void testAndNode() { /*Node andNode(const Node& right) const;*/ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.andNode(right); - + TS_ASSERT(AND == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); TS_ASSERT(*(eq.begin()) == left); TS_ASSERT(*(++eq.begin()) == right); - + } void testOrNode() { /*Node orNode(const Node& right) const;*/ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.orNode(right); - + TS_ASSERT(OR == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -322,9 +322,9 @@ public: Node cnd = d_nodeManager->mkNode(PLUS); Node thenBranch = d_nodeManager->mkNode(TRUE); - Node elseBranch = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); - Node ite = cnd.iteNode(thenBranch,elseBranch); - + Node elseBranch = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); + Node ite = cnd.iteNode(thenBranch, elseBranch); + TS_ASSERT(ITE == ite.getKind()); TS_ASSERT(3 == ite.getNumChildren()); @@ -336,11 +336,11 @@ public: void testIffNode() { /* Node iffNode(const Node& right) const; */ - + Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.iffNode(right); - + TS_ASSERT(IFF == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -349,13 +349,13 @@ public: TS_ASSERT(*(++eq.begin()) == right); } - + void testImpNode() { /* Node impNode(const Node& right) const; */ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.impNode(right); - + TS_ASSERT(IMPLIES == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -367,9 +367,9 @@ public: void testXorNode() { /*Node xorNode(const Node& right) const;*/ Node left = d_nodeManager->mkNode(TRUE); - Node right = d_nodeManager->mkNode(NOT,(d_nodeManager->mkNode(FALSE))); + Node right = d_nodeManager->mkNode(NOT, (d_nodeManager->mkNode(FALSE))); Node eq = left.xorNode(right); - + TS_ASSERT(XOR == eq.getKind()); TS_ASSERT(2 == eq.getNumChildren()); @@ -394,13 +394,13 @@ public: void testGetOperator() { - const Type* sort = d_nodeManager->mkSort("T"); - const Type* booleanType = d_nodeManager->booleanType(); - const Type* predType = d_nodeManager->mkFunctionType(sort,booleanType); + Type* sort = d_nodeManager->mkSort("T"); + Type* booleanType = d_nodeManager->booleanType(); + Type* predType = d_nodeManager->mkFunctionType(sort, booleanType); Node f = d_nodeManager->mkVar(predType); Node a = d_nodeManager->mkVar(booleanType); - Node fa = d_nodeManager->mkNode(kind::APPLY,f,a); + Node fa = d_nodeManager->mkNode(kind::APPLY, f, a); TS_ASSERT( fa.hasOperator() ); TS_ASSERT( !f.hasOperator() ); @@ -410,7 +410,7 @@ public: TS_ASSERT_THROWS( f.getOperator(), AssertionException ); TS_ASSERT_THROWS( a.getOperator(), AssertionException ); } - + void testNaryExpForSize(Kind k, int N){ NodeBuilder<> nbz(k); for(int i=0;imkVar(NULL, "w"); - Node x = d_nodeManager->mkVar(NULL, "x"); - Node y = d_nodeManager->mkVar(NULL, "y"); - Node z = d_nodeManager->mkVar(NULL, "z"); + Type* booleanType = d_nodeManager->booleanType(); + + Node w = d_nodeManager->mkVar(booleanType, "w"); + Node x = d_nodeManager->mkVar(booleanType, "x"); + Node y = d_nodeManager->mkVar(booleanType, "y"); + Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << w << x << kind::OR; Node n = NodeBuilder<>() << m << y << z << kind::AND; @@ -480,11 +482,12 @@ public: } void testToStream(){ - NodeBuilder<> b; - Node w = d_nodeManager->mkVar(NULL, "w"); - Node x = d_nodeManager->mkVar(NULL, "x"); - Node y = d_nodeManager->mkVar(NULL, "y"); - Node z = d_nodeManager->mkVar(NULL, "z"); + Type* booleanType = d_nodeManager->booleanType(); + + Node w = d_nodeManager->mkVar(booleanType, "w"); + Node x = d_nodeManager->mkVar(booleanType, "x"); + Node y = d_nodeManager->mkVar(booleanType, "y"); + Node z = d_nodeManager->mkVar(booleanType, "z"); Node m = NodeBuilder<>() << x << y << kind::OR; Node n = NodeBuilder<>() << w << m << z << kind::AND; diff --git a/test/unit/expr/node_white.h b/test/unit/expr/node_white.h index 5b63557ba..28dbde933 100644 --- a/test/unit/expr/node_white.h +++ b/test/unit/expr/node_white.h @@ -21,7 +21,6 @@ #include "expr/node_builder.h" #include "expr/node_manager.h" #include "expr/node.h" -#include "expr/attribute.h" #include "context/context.h" #include "util/Assert.h" @@ -29,30 +28,8 @@ using namespace CVC4; using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::expr; -using namespace CVC4::expr::attr; using namespace std; -struct Test1; -struct Test2; -struct Test3; -struct Test4; -struct Test5; - -typedef Attribute TestStringAttr1; -typedef Attribute TestStringAttr2; - -// it would be nice to have CDAttribute<> for context-dependence -typedef CDAttribute TestCDFlag; - -typedef Attribute TestFlag1; -typedef Attribute TestFlag2; -typedef Attribute TestFlag3; -typedef Attribute TestFlag4; -typedef Attribute TestFlag5; - -typedef CDAttribute TestFlag1cd; -typedef CDAttribute TestFlag2cd; - class NodeWhite : public CxxTest::TestSuite { Context* d_ctxt; @@ -88,494 +65,4 @@ public: TS_ASSERT(b.d_nv->getNumChildren() == 0); /* etc. */ } - - void testAttributeIds() { - TS_ASSERT(VarNameAttr::s_id == 0); - TS_ASSERT(TestStringAttr1::s_id == 1); - TS_ASSERT(TestStringAttr2::s_id == 2); - TS_ASSERT((attr::LastAttributeId::s_id == 3)); - - TS_ASSERT(TypeAttr::s_id == 0); - TS_ASSERT((attr::LastAttributeId::s_id == 1)); - - TS_ASSERT(TestFlag1::s_id == 0); - TS_ASSERT(TestFlag2::s_id == 1); - TS_ASSERT(TestFlag3::s_id == 2); - TS_ASSERT(TestFlag4::s_id == 3); - TS_ASSERT(TestFlag5::s_id == 4); - TS_ASSERT((attr::LastAttributeId::s_id == 5)); - - TS_ASSERT(TestFlag1cd::s_id == 0); - TS_ASSERT(TestFlag2cd::s_id == 1); - TS_ASSERT((attr::LastAttributeId::s_id == 2)); - } - - void testCDAttributes() { - AttributeManager& am = d_nm->d_attrManager; - - //Debug.on("boolattr"); - - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->push(); // level 1 - - // test that all boolean flags are FALSE to start - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - // test that they all HAVE the boolean attributes - TS_ASSERT(a.hasAttribute(TestFlag1cd())); - TS_ASSERT(b.hasAttribute(TestFlag1cd())); - TS_ASSERT(c.hasAttribute(TestFlag1cd())); - - // test two-arg version of hasAttribute() - bool bb; - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag1cd(), bb)); - TS_ASSERT(! bb); - - // setting boolean flags - Debug("boolattr", "set flag 1 on a to T\n"); - a.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "set flag 1 on b to F\n"); - b.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on c to F\n"); - c.setAttribute(TestFlag1cd(), false); - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->push(); // level 2 - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - Debug("boolattr", "set flag 1 on a to F\n"); - a.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on b to T\n"); - b.setAttribute(TestFlag1cd(), true); - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->push(); // level 3 - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - Debug("boolattr", "set flag 1 on c to T\n"); - c.setAttribute(TestFlag1cd(), true); - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be T)\n"); - TS_ASSERT(c.getAttribute(TestFlag1cd())); - - d_ctxt->pop(); // level 2 - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->pop(); // level 1 - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - - d_ctxt->pop(); // level 0 - - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1cd())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1cd())); - -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( d_ctxt->pop(), AssertionException ); -#endif /* CVC4_ASSERTIONS */ - } - - void testAttributes() { - AttributeManager& am = d_nm->d_attrManager; - - //Debug.on("boolattr"); - - Node a = d_nm->mkVar(); - Node b = d_nm->mkVar(); - Node c = d_nm->mkVar(); - Node unnamed = d_nm->mkVar(); - - a.setAttribute(VarNameAttr(), "a"); - b.setAttribute(VarNameAttr(), "b"); - c.setAttribute(VarNameAttr(), "c"); - - // test that all boolean flags are FALSE to start - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); - TS_ASSERT(! unnamed.getAttribute(TestFlag1())); - - Debug("boolattr", "get flag 2 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); - TS_ASSERT(! unnamed.getAttribute(TestFlag2())); - - Debug("boolattr", "get flag 3 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); - TS_ASSERT(! unnamed.getAttribute(TestFlag3())); - - Debug("boolattr", "get flag 4 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); - TS_ASSERT(! unnamed.getAttribute(TestFlag4())); - - Debug("boolattr", "get flag 5 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); - TS_ASSERT(! unnamed.getAttribute(TestFlag5())); - - // test that they all HAVE the boolean attributes - TS_ASSERT(a.hasAttribute(TestFlag1())); - TS_ASSERT(b.hasAttribute(TestFlag1())); - TS_ASSERT(c.hasAttribute(TestFlag1())); - TS_ASSERT(unnamed.hasAttribute(TestFlag1())); - - TS_ASSERT(a.hasAttribute(TestFlag2())); - TS_ASSERT(b.hasAttribute(TestFlag2())); - TS_ASSERT(c.hasAttribute(TestFlag2())); - TS_ASSERT(unnamed.hasAttribute(TestFlag2())); - - TS_ASSERT(a.hasAttribute(TestFlag3())); - TS_ASSERT(b.hasAttribute(TestFlag3())); - TS_ASSERT(c.hasAttribute(TestFlag3())); - TS_ASSERT(unnamed.hasAttribute(TestFlag3())); - - TS_ASSERT(a.hasAttribute(TestFlag4())); - TS_ASSERT(b.hasAttribute(TestFlag4())); - TS_ASSERT(c.hasAttribute(TestFlag4())); - TS_ASSERT(unnamed.hasAttribute(TestFlag4())); - - TS_ASSERT(a.hasAttribute(TestFlag5())); - TS_ASSERT(b.hasAttribute(TestFlag5())); - TS_ASSERT(c.hasAttribute(TestFlag5())); - TS_ASSERT(unnamed.hasAttribute(TestFlag5())); - - // test two-arg version of hasAttribute() - bool bb; - Debug("boolattr", "get flag 1 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag1(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 2 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag2(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 3 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 3 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag3(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 4 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 4 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag4(), bb)); - TS_ASSERT(! bb); - - Debug("boolattr", "get flag 5 on a (should be F)\n"); - TS_ASSERT(a.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on b (should be F)\n"); - TS_ASSERT(b.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on c (should be F)\n"); - TS_ASSERT(c.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - Debug("boolattr", "get flag 5 on unnamed (should be F)\n"); - TS_ASSERT(unnamed.hasAttribute(TestFlag5(), bb)); - TS_ASSERT(! bb); - - // setting boolean flags - Debug("boolattr", "set flag 1 on a to T\n"); - a.setAttribute(TestFlag1(), true); - Debug("boolattr", "set flag 1 on b to F\n"); - b.setAttribute(TestFlag1(), false); - Debug("boolattr", "set flag 1 on c to F\n"); - c.setAttribute(TestFlag1(), false); - Debug("boolattr", "set flag 1 on unnamed to T\n"); - unnamed.setAttribute(TestFlag1(), true); - - Debug("boolattr", "set flag 2 on a to F\n"); - a.setAttribute(TestFlag2(), false); - Debug("boolattr", "set flag 2 on b to T\n"); - b.setAttribute(TestFlag2(), true); - Debug("boolattr", "set flag 2 on c to T\n"); - c.setAttribute(TestFlag2(), true); - Debug("boolattr", "set flag 2 on unnamed to F\n"); - unnamed.setAttribute(TestFlag2(), false); - - Debug("boolattr", "set flag 3 on a to T\n"); - a.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 3 on b to T\n"); - b.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 3 on c to T\n"); - c.setAttribute(TestFlag3(), true); - Debug("boolattr", "set flag 3 on unnamed to T\n"); - unnamed.setAttribute(TestFlag3(), true); - - Debug("boolattr", "set flag 4 on a to T\n"); - a.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 4 on b to T\n"); - b.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 4 on c to T\n"); - c.setAttribute(TestFlag4(), true); - Debug("boolattr", "set flag 4 on unnamed to T\n"); - unnamed.setAttribute(TestFlag4(), true); - - Debug("boolattr", "set flag 5 on a to T\n"); - a.setAttribute(TestFlag5(), true); - Debug("boolattr", "set flag 5 on b to T\n"); - b.setAttribute(TestFlag5(), true); - Debug("boolattr", "set flag 5 on c to F\n"); - c.setAttribute(TestFlag5(), false); - Debug("boolattr", "set flag 5 on unnamed to T\n"); - unnamed.setAttribute(TestFlag5(), true); - - TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); - - TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - - TS_ASSERT(! a.hasAttribute(TestStringAttr1())); - TS_ASSERT(! b.hasAttribute(TestStringAttr1())); - TS_ASSERT(! c.hasAttribute(TestStringAttr1())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); - - TS_ASSERT(! a.hasAttribute(TestStringAttr2())); - TS_ASSERT(! b.hasAttribute(TestStringAttr2())); - TS_ASSERT(! c.hasAttribute(TestStringAttr2())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); - - Debug("boolattr", "get flag 1 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on b (should be F)\n"); - TS_ASSERT(! b.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag1())); - Debug("boolattr", "get flag 1 on unnamed (should be T)\n"); - TS_ASSERT(unnamed.getAttribute(TestFlag1())); - - Debug("boolattr", "get flag 2 on a (should be F)\n"); - TS_ASSERT(! a.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on c (should be T)\n"); - TS_ASSERT(c.getAttribute(TestFlag2())); - Debug("boolattr", "get flag 2 on unnamed (should be F)\n"); - TS_ASSERT(! unnamed.getAttribute(TestFlag2())); - - Debug("boolattr", "get flag 3 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on c (should be T)\n"); - TS_ASSERT(c.getAttribute(TestFlag3())); - Debug("boolattr", "get flag 3 on unnamed (should be T)\n"); - TS_ASSERT(unnamed.getAttribute(TestFlag3())); - - Debug("boolattr", "get flag 4 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on c (should be T)\n"); - TS_ASSERT(c.getAttribute(TestFlag4())); - Debug("boolattr", "get flag 4 on unnamed (should be T)\n"); - TS_ASSERT(unnamed.getAttribute(TestFlag4())); - - Debug("boolattr", "get flag 5 on a (should be T)\n"); - TS_ASSERT(a.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on b (should be T)\n"); - TS_ASSERT(b.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on c (should be F)\n"); - TS_ASSERT(! c.getAttribute(TestFlag5())); - Debug("boolattr", "get flag 5 on unnamed (should be T)\n"); - TS_ASSERT(unnamed.getAttribute(TestFlag5())); - - a.setAttribute(TestStringAttr1(), "foo"); - b.setAttribute(TestStringAttr1(), "bar"); - c.setAttribute(TestStringAttr1(), "baz"); - - TS_ASSERT(a.getAttribute(VarNameAttr()) == "a"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(b.getAttribute(VarNameAttr()) == "b"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(c.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(c.getAttribute(VarNameAttr()) == "c"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); - - TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - - TS_ASSERT(a.hasAttribute(TestStringAttr1())); - TS_ASSERT(b.hasAttribute(TestStringAttr1())); - TS_ASSERT(c.hasAttribute(TestStringAttr1())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr1())); - - TS_ASSERT(! a.hasAttribute(TestStringAttr2())); - TS_ASSERT(! b.hasAttribute(TestStringAttr2())); - TS_ASSERT(! c.hasAttribute(TestStringAttr2())); - TS_ASSERT(! unnamed.hasAttribute(TestStringAttr2())); - - a.setAttribute(VarNameAttr(), "b"); - b.setAttribute(VarNameAttr(), "c"); - c.setAttribute(VarNameAttr(), "a"); - - TS_ASSERT(c.getAttribute(VarNameAttr()) == "a"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(c.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(a.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(a.getAttribute(VarNameAttr()) == "b"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(a.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(b.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(b.getAttribute(VarNameAttr()) == "c"); - TS_ASSERT(b.getAttribute(VarNameAttr()) != ""); - - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "a"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "b"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) != "c"); - TS_ASSERT(unnamed.getAttribute(VarNameAttr()) == ""); - - TS_ASSERT(! unnamed.hasAttribute(VarNameAttr())); - } }; diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 1b05f490e..f7d4eff24 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -170,7 +170,7 @@ class ParserBlack : public CxxTest::TestSuite { } catch (Exception& e) { cout << "\nGood input failed:\n" << goodInputs[i] << endl << e << endl; - throw e; + throw; } } @@ -226,6 +226,7 @@ class ParserBlack : public CxxTest::TestSuite { ( smtParser->parseNextExpression(); cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;, ParserException ); + delete smtParser; } //Debug.off("parser"); } @@ -235,6 +236,10 @@ public: d_exprManager = new ExprManager(); } + void tearDown() { + delete d_exprManager; + } + void testGoodCvc4Inputs() { tryGoodInputs(Parser::LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs); } -- cgit v1.2.3