#include "expr/node_value.h"
#include "util/output.h"
+#include <utility>
+
+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 <class T>
+inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
+ NodeValue* nv) {
+ for(uint64_t id = 0; id < attr::LastAttributeId<T, false>::s_id; ++id) {
+ typedef AttributeTraits<T, false> traits_t;
+ typedef AttrHash<T> hash_t;
+ pair<uint64_t, NodeValue*> 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<uint64_t, false>::s_id; ++id) {
- d_ints.erase(std::make_pair(id, nv));
- }
- for(unsigned id = 0; id < attr::LastAttributeId<TNode, false>::s_id; ++id) {
- d_exprs.erase(std::make_pair(id, nv));
- }
- for(unsigned id = 0; id < attr::LastAttributeId<std::string, false>::s_id; ++id) {
- d_strings.erase(std::make_pair(id, nv));
- }
- for(unsigned id = 0; id < attr::LastAttributeId<void*, false>::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
/*
namespace attr {
/** Default cleanup for unmanaged Attribute<> */
-template <class T>
-struct AttributeCleanupFcn {
- static inline void cleanup(const T&) {}
-};
+struct NullCleanupFcn {
+};/* struct NullCleanupFcn */
/** Default cleanup for ManagedAttribute<> */
template <class T>
struct ManagedAttributeCleanupFcn {
-};
+};/* struct ManagedAttributeCleanupFcn<> */
/** Specialization for T* */
template <class T>
struct ManagedAttributeCleanupFcn<T*> {
static inline void cleanup(T* p) { delete p; }
-};
+};/* struct ManagedAttributeCleanupFcn<T*> */
/** Specialization for const T* */
template <class T>
struct ManagedAttributeCleanupFcn<const T*> {
static inline void cleanup(const T* p) { delete p; }
+};/* struct ManagedAttributeCleanupFcn<const T*> */
+
+/**
+ * Helper for Attribute<> class below to determine whether a cleanup
+ * is defined or not.
+ */
+template <class T, class C>
+struct getCleanupFcn {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupFcn<> */
+
+/**
+ * Specialization for NullCleanupFcn.
+ */
+template <class T>
+struct getCleanupFcn<T, NullCleanupFcn> {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupFcn<T, NullCleanupFcn> */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupFcn<T, NullCleanupFcn>::fn)(typename getCleanupFcn<T, NullCleanupFcn>::mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<T>.
+ */
+template <class T>
+struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > {
+ typedef T value_type;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void (*const fn)(typename mapping::table_value_type);
+};/* struct getCleanupFcn<T, ManagedAttributeCleanupFcn<T> > */
+
+// out-of-class initialization required (because it's a non-integral type)
+template <class T>
+void (*const getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::fn)(typename getCleanupFcn<T, ManagedAttributeCleanupFcn<T> >::mapping::table_value_type) = NULL;
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<T*>.
+ */
+template <class T>
+struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > {
+ typedef T* value_type;
+ typedef ManagedAttributeCleanupFcn<value_type> C;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupFcn<T*, ManagedAttributeCleanupFcn<T*> > */
+
+/**
+ * Specialization for ManagedAttributeCleanupFcn<const T*>.
+ */
+template <class T>
+struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > {
+ typedef const T* value_type;
+ typedef ManagedAttributeCleanupFcn<value_type> C;
+ typedef KindValueToTableValueMapping<value_type> mapping;
+ static void fn(typename mapping::table_value_type t) {
+ C::cleanup(mapping::convertBack(t));
+ }
+};/* struct getCleanupFcn<const T*, ManagedAttributeCleanupFcn<const T*> > */
+
+/**
+ * Cause compile-time error for improperly-instantiated
+ * getCleanupFcn<>.
+ */
+template <class T, class U>
+struct getCleanupFcn<T, ManagedAttributeCleanupFcn<U> >;
+
+}/* 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 <class T, bool context_dep>
+struct LastAttributeId {
+ static uint64_t s_id;
+};
+
+/** Initially zero. */
+template <class T, bool context_dep>
+uint64_t LastAttributeId<T, context_dep>::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 <class T, bool context_dep>
+struct AttributeTraits {
+ typedef void (*cleanup_t)(T);
+ static std::vector<cleanup_t> cleanup;
};
+template <class T, bool context_dep>
+std::vector<typename AttributeTraits<T, context_dep>::cleanup_t>
+ AttributeTraits<T, context_dep>::cleanup;
+
}/* CVC4::expr::attr namespace */
// ATTRIBUTE DEFINITION ========================================================
*/
template <class T,
class value_t,
- class CleanupFcn = attr::AttributeCleanupFcn<value_t>,
+ 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;
*/
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<value_t>::table_value_type table_value_type;
+ typedef attr::AttributeTraits<table_value_type, context_dep> traits;
+ uint64_t id = attr::LastAttributeId<table_value_type, context_dep>::s_id++;
+ Assert(traits::cleanup.size() == id);// sanity check
+ traits::cleanup.push_back(attr::getCleanupFcn<value_t, CleanupFcn>::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 T, class CleanupFcn, bool context_dep>
+class Attribute<T, bool, CleanupFcn, context_dep> {
+ template <bool> struct ERROR_bool_attributes_cannot_have_cleanup_functions;
+ ERROR_bool_attributes_cannot_have_cleanup_functions<true> blah;
};
+*/
/**
* An "attribute type" structure for boolean flags (special).
*/
-template <class T, class CleanupFcn, bool context_dep>
-struct Attribute<T, bool, CleanupFcn, context_dep> {
+template <class T, bool context_dep>
+class Attribute<T, bool, attr::NullCleanupFcn, context_dep> {
+ /** 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;
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<bool, context_dep>::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
template <class T,
class value_type>
struct CDAttribute :
- public Attribute<T, value_type, attr::AttributeCleanupFcn<value_type>, true> {};
+ public Attribute<T, value_type, attr::NullCleanupFcn, true> {};
/**
* This is a managed attribute kind (the only difference between
// 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 <class T, bool context_dep>
-struct LastAttributeId {
- static uint64_t s_id;
-};
-
-/** Initially zero. */
-template <class T, bool context_dep>
-uint64_t LastAttributeId<T, context_dep>::s_id = 0;
-
-}/* CVC4::expr::attr namespace */
-
/** Assign unique IDs to attributes at load time. */
+// 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 <class T, class value_t, class CleanupFcn, bool context_dep>
const uint64_t Attribute<T, value_t, CleanupFcn, context_dep>::s_id =
- attr::LastAttributeId<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::s_id++;
+ ( attr::AttributeTraits<typename attr::KindValueToTableValueMapping<value_t>::table_value_type, context_dep>::cleanup.size(),
+ Attribute<T, value_t, CleanupFcn, context_dep>::registerAttribute() );
-/**
- * Assign unique IDs to bool-valued attributes at load time, checking
- * that they are in range.
- */
-template <class T, class CleanupFcn, bool context_dep>
-const uint64_t Attribute<T, bool, CleanupFcn, context_dep>::s_id =
- Attribute<T, bool, CleanupFcn, context_dep>::checkID(attr::LastAttributeId<bool, context_dep>::s_id++);
+/** Assign unique IDs to attributes at load time. */
+template <class T, bool context_dep>
+const uint64_t Attribute<T, bool, attr::NullCleanupFcn, context_dep>::s_id =
+ Attribute<T, bool, attr::NullCleanupFcn, context_dep>::registerAttribute();
// ATTRIBUTE MANAGER ===========================================================
/** Underlying hash table for context-dependent pointer-valued attributes */
CDAttrHash<void*> d_cdptrs;
+ template <class T>
+ void deleteFromTable(AttrHash<T>& table, NodeValue* nv);
+
/**
* getTable<> is a helper template that gets the right table from an
* AttributeManager given its type.
return d_node->getNumChildren();
}
-const Type* Expr::getType() const {
+Type* Expr::getType() const {
ExprManagerScope ems(*this);
return d_node->getType();
}
/** 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.
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();
}
}
/** 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<const Type*>& argTypes,
- const Type* range) {
+FunctionType* ExprManager::mkFunctionType(const std::vector<Type*>& 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)));
}
~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,...).
Expr mkExpr(Kind kind, const std::vector<Expr>& 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<const Type*>& argTypes,
- const Type* range);
+ FunctionType*
+ mkFunctionType(const std::vector<Type*>& 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 */
* Returns the type of this node.
* @return the type
*/
- const Type* getType() const;
+ Type* getType() const;
/**
* Returns the kind of this node.
}
template <bool ref_count>
-const Type* NodeTemplate<ref_count>::getType() const {
+Type* NodeTemplate<ref_count>::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 ?" );
__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;
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";
// decr ref counts of children
nv->decrRefCounts();
- //free(nv);
-#warning NOT FREEING NODEVALUES
+ free(nv);
}
}
}
#include "expr/expr.h"
#include "expr/node_value.h"
#include "context/context.h"
+#include "expr/type.h"
namespace CVC4 {
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarName, std::string> VarNameAttr;
-typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr;
+typedef ManagedAttribute<attr::Type, CVC4::Type*, attr::TypeCleanupFcn> TypeAttr;
}/* CVC4::expr namespace */
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueInternalHashFcn,
- expr::NodeValue::NodeValueEq> NodeValueSet;
+ expr::NodeValue::NodeValueEq> NodeValuePool;
typedef __gnu_cxx::hash_set<expr::NodeValue*,
expr::NodeValueIDHashFcn,
expr::NodeValue::NodeValueEq> ZombieSet;
- NodeValueSet d_nodeValueSet;
+ NodeValuePool d_nodeValuePool;
expr::attr::AttributeManager d_attrManager;
poolInsert( &expr::NodeValue::s_null );
}
+ ~NodeManager();
+
static NodeManager* currentNM() { return s_current; }
// general expression-builders
Node mkNode(Kind kind, const std::vector<Node>& 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 <class AttrKind>
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<const Type*>& argTypes, const Type* range) const;
+ inline FunctionType* mkFunctionType(const std::vector<Type*>& 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;
};
/**
/** 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<const Type*> argTypes;
+FunctionType* NodeManager::mkFunctionType(Type* domain,
+ Type* range) const {
+ std::vector<Type*> 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<const Type*>& argTypes,
- const Type* range) const {
+FunctionType* NodeManager::mkFunctionType(const std::vector<Type*>& 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 */
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;
}
}
Type::Type() :
- d_name(std::string("<undefined>")) {
+ d_name(std::string("<undefined>")),
+ d_rc(0) {
}
Type::Type(std::string name) :
- d_name(name) {
+ d_name(name) {
}
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() {
return true;
}
-FunctionType::FunctionType(const std::vector<const Type*>& argTypes,
- const Type* range)
- : d_argTypes(argTypes),
- d_rangeType(range) {
+FunctionType::FunctionType(const std::vector<Type*>& 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<const Type*> FunctionType::getArgTypes() const {
+const std::vector<Type*> FunctionType::getArgTypes() const {
return d_argTypes;
}
-const Type* FunctionType::getRangeType() const {
+Type* FunctionType::getRangeType() const {
return d_rangeType;
}
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() {
return &s_instance;
}
-SortType::SortType(std::string name)
- : Type(name) {
+SortType::SortType(std::string name) :
+ Type(name) {
}
SortType::~SortType() {
}
-
}
#define __CVC4__TYPE_H
#include "cvc4_config.h"
+#include "util/output.h"
+#include "util/Assert.h"
#include <string>
#include <vector>
+#include <limits.h>
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;
/** 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;
};
/**
public:
/** Retrieve the argument types. The vector will be non-empty. */
- const std::vector<const Type*> getArgTypes() const;
+ const std::vector<Type*> 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;
* @param argTypes a non-empty vector of input types
* @param range the result type
*/
- FunctionType(const std::vector<const Type*>& argTypes,
- const Type* range);
+ FunctionType(const std::vector<Type*>& argTypes,
+ Type* range);
/** Destructor */
~FunctionType();
/** The list of input types. */
- const std::vector<const Type*> d_argTypes;
+ const std::vector<Type*> d_argTypes;
/** The result type. */
- const Type* d_rangeType;
+ Type* d_rangeType;
friend class NodeManager;
};
*/
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 */
return d_varSymbolTable.getObject(name);
default:
- Unhandled("Unhandled symbol type!");
+ Unhandled(type);
}
}
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;
}
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<const Type*>& argTypes,
- const Type* rangeType) {
+Type* AntlrParser::functionType(const std::vector<Type*>& 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<const Type*>& sorts) {
+Type* AntlrParser::functionType(const std::vector<Type*>& sorts) {
Assert( sorts.size() > 0 );
if( sorts.size() == 1 ) {
return sorts[0];
} else {
- std::vector<const Type*> argTypes(sorts);
- const Type* rangeType = argTypes.back();
+ std::vector<Type*> argTypes(sorts);
+ Type* rangeType = argTypes.back();
argTypes.pop_back();
- return functionType(argTypes,rangeType);
+ return functionType(argTypes, rangeType);
}
}
-const Type* AntlrParser::predicateType(const std::vector<const Type*>& sorts) {
+Type* AntlrParser::predicateType(const std::vector<Type*>& sorts) {
if(sorts.size() == 0) {
return d_exprManager->booleanType();
} else {
}
}
-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<Expr>
-AntlrParser::mkVars(const std::vector<std::string> names,
- const Type* type) {
+const std::vector<Expr>
+AntlrParser::mkVars(const std::vector<std::string> names,
+ Type* type) {
std::vector<Expr> vars;
for(unsigned i = 0; i < names.size(); ++i) {
vars.push_back(mkVar(names[i], type));
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 Type*>
+const std::vector<Type*>
AntlrParser::newSorts(const std::vector<std::string>& names) {
- std::vector<const Type*> types;
+ std::vector<Type*> 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) {
return 1;
case APPLY:
- case EQUAL:
+ case EQUAL:
case IFF:
case IMPLIES:
case PLUS:
return 3;
default:
- Unhandled("kind in minArity");
+ Unhandled(kind);
}
}
case NOT:
return 1;
- case EQUAL:
+ case EQUAL:
case IFF:
case IMPLIES:
case XOR:
return UINT_MAX;
default:
- Unhandled("kind in maxArity");
+ Unhandled(kind);
}
}
case SYM_SORT:
return d_sortTable.isBound(name);
default:
- Unhandled("Unhandled symbol type!");
+ Unhandled(type);
}
}
break;
default:
- Unhandled("Unknown check type!");
+ Unhandled(check);
}
}
throw (antlr::SemanticException) {
if( d_checksEnabled && !isFunction(name) ) {
parseError("Expecting function symbol, found '" + name + "'");
- }
+ }
}
void AntlrParser::checkArity(Kind kind, unsigned int numArgs)
/**
* 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.
* @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);
/**
Expr mkExpr(Kind kind, const std::vector<Expr>& 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<Expr>
mkVars(const std::vector<std::string> 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);
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<const Type*>& argTypes,
- const Type* rangeType);
+ Type* functionType(const std::vector<Type*>& argTypes,
+ Type* rangeType);
/**
* Returns a function type over the given types. If types has only
*
* @param types a non-empty list of input and output types.
*/
- const Type* functionType(const std::vector<const Type*>& types);
+ Type* functionType(const std::vector<Type*>& types);
/**
* Returns a predicate type over the given sorts. If sorts is empty,
* @param sorts a list of input types
*/
- const Type* predicateType(const std::vector<const Type*>& sorts);
+ Type* predicateType(const std::vector<Type*>& 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 Type*>
+ const std::vector<Type*>
newSorts(const std::vector<std::string>& names);
/** Is the symbol bound to a boolean variable? */
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);
SymbolTable<Expr> d_varSymbolTable;
/** The sort table */
- SymbolTable<const Type*> d_sortTable;
+ SymbolTable<Type*> d_sortTable;
/** Are semantic checks enabled during parsing? */
bool d_checksEnabled;
declaration returns [CVC4::DeclarationCommand* cmd]
{
vector<string> 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<std::string>& idList] returns [const CVC4::Type* t]
+declType[std::vector<std::string>& idList] returns [CVC4::Type* t]
{
Debug("parser") << "declType: " << LT(1)->getText() << endl;
}
* 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 */
t1 = baseType RIGHT_ARROW t2 = baseType
{ t = functionType(t1,t2); }
| /* Multi-parameter function type */
- LPAREN t1 = baseType
- { std::vector<const Type*> argTypes;
+ LPAREN t1 = baseType
+ { std::vector<Type*> 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); }
;
* @param idList the list to fill with identifiers.
* @param check what kinds of check to perform on the symbols
*/
-identifierList[std::vector<std::string>& idList,
+identifierList[std::vector<std::string>& idList,
DeclarationCheck check = CHECK_NONE]
{
string id;
* 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); }
;
* 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;
/**
* 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;
Expr e;
Debug("parser") << "=> Formula: " << LT(1)->getText() << endl;
}
- : f = orFormula
+ : f = orFormula
( IMPLIES e = impliesFormula
{ f = mkExpr(CVC4::kind::IMPLIES, f, e); }
)?
Debug("parser") << "XOR formula: " << LT(1)->getText() << endl;
}
: f = andFormula
- ( XOR e = andFormula
+ ( XOR e = andFormula
{ f = mkExpr(CVC4::kind::XOR,f, e); }
)*
;
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
Debug("parser") << "predicate formula: " << LT(1)->getText() << endl;
}
: { Expr e; }
- f = term
+ f = term
(EQUAL e = term
{ f = mkExpr(CVC4::kind::EQUAL, f, e); }
)?
Debug("parser") << "term: " << LT(1)->getText() << endl;
}
: /* function application */
- // { isFunction(LT(1)->getText()) }?
- { Expr f;
+ // { isFunction(LT(1)->getText()) }?
+ { Expr f;
std::vector<CVC4::Expr> args; }
f = functionSymbol[CHECK_DECLARED]
{ args.push_back( f ); }
/**
* 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); }
;
/**
{
Debug("parser") << "function symbol: " << LT(1)->getText() << endl;
std::string name;
-}
+}
: name = identifier[check,SYM_FUNCTION]
- { checkFunction(name);
+ { checkFunction(name);
f = getFunction(name); }
;
;
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
;
{ 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
;
{
Debug("parser") << "annotated formula: " << LT(1)->getText() << endl;
Kind kind = CVC4::kind::UNDEFINED_KIND;
- vector<Expr> args;
+ vector<Expr> 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); }
{ std::vector<Expr> 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
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
| /* 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); }
* Matches a sequence of annotaed formulas and puts them into the formulas
* vector.
* @param formulas the vector to fill with formulas
- */
+ */
annotatedFormulas[std::vector<Expr>& formulas]
{
Expr f;
;
/**
- * 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]
* 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).
*/
* 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); }
functionDeclaration
{
string name;
- const Type* t;
- std::vector<const Type*> sorts;
+ Type* t;
+ std::vector<Type*> 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<const Type*> p_sorts;
- const Type *t;
+ std::vector<Type*> 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<const Type*>& sorts]
+sortList[std::vector<Type*>& sorts]
{
- const Type* t;
+ Type* t;
}
- : ( t = sortSymbol { sorts.push_back(t); })*
+ : ( t = sortSymbol { sorts.push_back(t); })*
;
/**
* @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;
}
* 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 */
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() {
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) {
** The theory output channel interface.
**/
+#include "cvc4_private.h"
+
#ifndef __CVC4__THEORY__INTERRUPTED_H
#define __CVC4__THEORY__INTERRUPTED_H
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 */
* 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();
}
};
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 */
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 */
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 */
expr/node_black \
expr/kind_black \
expr/node_builder_black \
+ expr/attribute_white \
expr/attribute_black \
parser/parser_black \
context/context_black \
struct MyDataAttributeId {};
struct MyDataCleanupFunction {
- static void cleanup(MyData*& myData){
+ static void cleanup(MyData* myData){
delete myData;
}
};
--- /dev/null
+/********************* */
+/** 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 <cxxtest/TestSuite.h>
+
+#include <string>
+
+#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<Test1, std::string> TestStringAttr1;
+typedef Attribute<Test2, std::string> TestStringAttr2;
+
+// it would be nice to have CDAttribute<> for context-dependence
+typedef CDAttribute<Test1, bool> TestCDFlag;
+
+typedef Attribute<Test1, bool> TestFlag1;
+typedef Attribute<Test2, bool> TestFlag2;
+typedef Attribute<Test3, bool> TestFlag3;
+typedef Attribute<Test4, bool> TestFlag4;
+typedef Attribute<Test5, bool> TestFlag5;
+
+typedef CDAttribute<Test1, bool> TestFlag1cd;
+typedef CDAttribute<Test2, bool> 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<string, false>::s_id == 3));
+
+ TS_ASSERT(TypeAttr::s_id == 0);
+ TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1));
+
+ TS_ASSERT(TestFlag1::s_id == 0);
+ TS_ASSERT(TestFlag2::s_id == 1);
+ TS_ASSERT(TestFlag3::s_id == 2);
+ TS_ASSERT(TestFlag4::s_id == 3);
+ TS_ASSERT(TestFlag5::s_id == 4);
+ TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5));
+
+ TS_ASSERT(TestFlag1cd::s_id == 0);
+ TS_ASSERT(TestFlag2cd::s_id == 1);
+ TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2));
+ }
+
+ 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()));
+ }
+};
TS_ASSERT(b.isNull());
Node c = b;
-
+
TS_ASSERT(c.isNull());
}
/*tests: bool operator==(const Node& e) const */
void testOperatorEquals() {
Node a, b, c;
-
+
b = d_nodeManager->mkVar();
a = b;
TS_ASSERT(c==a);
TS_ASSERT(c==b);
- TS_ASSERT(c==c);
+ TS_ASSERT(c==c);
TS_ASSERT(d==d);
Node a, b, c;
-
+
b = d_nodeManager->mkVar();
a = b;
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));
}
- void testOperatorSquare() {
+ void testOperatorSquare() {
/*Node operator[](int i) const */
#ifdef CVC4_ASSERTIONS
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]);
#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 */
}
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();
TS_ASSERT(!(c<d));
TS_ASSERT(!(d<c));
-
+
/* TODO:
* Less than has the rather difficult to test property that subexpressions
* are less than enclosing expressions.
*
* But what would be a convincing test of this property?
*/
-
+
//Simple test of descending descendant property
Node child = d_nodeManager->mkNode(TRUE);
Node parent = d_nodeManager->mkNode(NOT, child);
Node curr = d_nodeManager->mkNode(NULL_EXPR);
for(int i=0;i<N;i++) {
chain.push_back(curr);
- curr = d_nodeManager->mkNode(AND,curr);
+ curr = d_nodeManager->mkNode(AND, curr);
}
-
+
for(int i=0;i<N;i++) {
for(int j=i+1;j<N;j++) {
Node chain_i = chain[i];
TS_ASSERT(chain_i<chain_j);
}
}
-
+
}
void testEqNode() {
/*Node eqNode(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.eqNode(right);
-
+
TS_ASSERT(EQUAL == eq.getKind());
TS_ASSERT(2 == eq.getNumChildren());
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());
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());
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());
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());
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());
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() );
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;i<N;i++){
//Bigger tests
- srand(0);
+ srand(0);
int trials = 500;
for(int i=0;i<trials; i++){
int N = rand() % 1000;
testNaryExpForSize(NOT, N);
}
-
+
}
void testIterator(){
}
void testToString(){
- 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<>() << w << x << kind::OR;
Node n = NodeBuilder<>() << m << y << z << kind::AND;
}
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;
#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::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<Test1, std::string> TestStringAttr1;
-typedef Attribute<Test2, std::string> TestStringAttr2;
-
-// it would be nice to have CDAttribute<> for context-dependence
-typedef CDAttribute<Test1, bool> TestCDFlag;
-
-typedef Attribute<Test1, bool> TestFlag1;
-typedef Attribute<Test2, bool> TestFlag2;
-typedef Attribute<Test3, bool> TestFlag3;
-typedef Attribute<Test4, bool> TestFlag4;
-typedef Attribute<Test5, bool> TestFlag5;
-
-typedef CDAttribute<Test1, bool> TestFlag1cd;
-typedef CDAttribute<Test2, bool> TestFlag2cd;
-
class NodeWhite : public CxxTest::TestSuite {
Context* d_ctxt;
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<string, false>::s_id == 3));
-
- TS_ASSERT(TypeAttr::s_id == 0);
- TS_ASSERT((attr::LastAttributeId<void*, false>::s_id == 1));
-
- TS_ASSERT(TestFlag1::s_id == 0);
- TS_ASSERT(TestFlag2::s_id == 1);
- TS_ASSERT(TestFlag3::s_id == 2);
- TS_ASSERT(TestFlag4::s_id == 3);
- TS_ASSERT(TestFlag5::s_id == 4);
- TS_ASSERT((attr::LastAttributeId<bool, false>::s_id == 5));
-
- TS_ASSERT(TestFlag1cd::s_id == 0);
- TS_ASSERT(TestFlag2cd::s_id == 1);
- TS_ASSERT((attr::LastAttributeId<bool, true>::s_id == 2));
- }
-
- 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()));
- }
};
} catch (Exception& e) {
cout << "\nGood input failed:\n" << goodInputs[i] << endl
<< e << endl;
- throw e;
+ throw;
}
}
( smtParser->parseNextExpression();
cout << "\nBad expr succeeded: " << badBooleanExprs[i] << endl;,
ParserException );
+ delete smtParser;
}
//Debug.off("parser");
}
d_exprManager = new ExprManager();
}
+ void tearDown() {
+ delete d_exprManager;
+ }
+
void testGoodCvc4Inputs() {
tryGoodInputs(Parser::LANG_CVC4,goodCvc4Inputs,numGoodCvc4Inputs);
}
projects / cvc5.git / commitdiff