diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/attribute.h | 54 | ||||
-rw-r--r-- | src/expr/node.cpp | 44 | ||||
-rw-r--r-- | src/expr/node.h | 21 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 8 | ||||
-rw-r--r-- | src/theory/output_channel.h | 16 | ||||
-rw-r--r-- | src/theory/theory.h | 10 |
6 files changed, 119 insertions, 34 deletions
diff --git a/src/expr/attribute.h b/src/expr/attribute.h index 12de9eb5f..1d2705240 100644 --- a/src/expr/attribute.h +++ b/src/expr/attribute.h @@ -56,7 +56,7 @@ namespace expr { struct AttrHashFcn { enum { LARGE_PRIME = 1 }; - std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const { + std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const { return p.first * LARGE_PRIME + p.second.hash(); } }; @@ -122,7 +122,7 @@ struct KindTableMapping { // use a TAG to indicate which table it should be in template <class value_type> -struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {}; +struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {}; template <> class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> { @@ -215,19 +215,23 @@ class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHas public: - typedef std::pair<unsigned, SoftNode> key_type; + typedef std::pair<uint64_t, SoftNode> key_type; typedef bool data_type; typedef std::pair<const key_type, data_type> value_type; typedef BitIterator iterator; typedef ConstBitIterator const_iterator; - BitIterator find(const std::pair<unsigned, SoftNode>& k) { + BitIterator find(const std::pair<uint64_t, SoftNode>& k) { super::iterator i = super::find(k.second); if(i == super::end()) { return BitIterator(); } - Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first); + Debug.printf("boolattr", + "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", + &(*i).second, + (unsigned long long)((*i).second), + unsigned(k.first)); return BitIterator(*i, k.first); } @@ -235,12 +239,16 @@ public: return BitIterator(); } - ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const { + ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const { super::const_iterator i = super::find(k.second); if(i == super::end()) { return ConstBitIterator(); } - Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first); + Debug.printf("boolattr", + "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", + &(*i).second, + (unsigned long long)((*i).second), + unsigned(k.first)); return ConstBitIterator(*i, k.first); } @@ -248,7 +256,7 @@ public: return ConstBitIterator(); } - BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) { + BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) { uint64_t& word = super::operator[](k.second); return BitAccessor(word, k.first); } @@ -268,18 +276,18 @@ struct Attribute { /** cleanup routine when the Node goes away */ static inline void cleanup(const value_t&) {} - static inline unsigned getId() { return s_id; } - static inline unsigned getHashValue() { return s_hashValue; } + static inline uint64_t getId() { return s_id; } + static inline uint64_t getHashValue() { return s_hashValue; } static const bool has_default_value = false; private: /** an id */ - static const unsigned s_id; + static const uint64_t s_id; /** an extra hash value (to avoid same-value-type collisions) */ - static const unsigned s_hashValue; + static const uint64_t s_hashValue; }; /** @@ -294,13 +302,13 @@ struct Attribute<T, bool> { /** cleanup routine when the Node goes away */ static inline void cleanup(const bool&) {} - static inline unsigned getId() { return s_id; } - static inline unsigned getHashValue() { return s_hashValue; } + static inline uint64_t getId() { return s_id; } + static inline uint64_t getHashValue() { return s_hashValue; } static const bool has_default_value = true; static const bool default_value = false; - static inline unsigned checkID(unsigned id) { + static inline uint64_t checkID(uint64_t id) { AlwaysAssert(id <= 63, "Too many boolean node attributes registered during initialization !"); return id; @@ -309,10 +317,10 @@ struct Attribute<T, bool> { private: /** a bit assignment */ - static const unsigned s_id; + static const uint64_t s_id; /** an extra hash value (to avoid same-value-type collisions) */ - static const unsigned s_hashValue; + static const uint64_t s_hashValue; }; // SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ====================================== @@ -323,11 +331,11 @@ namespace attr { template <class T> struct LastAttributeId { - static unsigned s_id; + static uint64_t s_id; }; template <class T> - unsigned LastAttributeId<T>::s_id = 0; + uint64_t LastAttributeId<T>::s_id = 0; }/* CVC4::expr::attr namespace */ typedef Attribute<attr::VarName, std::string> VarNameAttr; @@ -336,16 +344,16 @@ typedef Attribute<attr::Type, const CVC4::Type*> TypeAttr; // ATTRIBUTE IDENTIFIER ASSIGNMENT ============================================= template <class T, class value_t> -const unsigned Attribute<T, value_t>::s_id = +const uint64_t Attribute<T, value_t>::s_id = attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++; template <class T, class value_t> -const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; +const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id; template <class T> -const unsigned Attribute<T, bool>::s_id = +const uint64_t Attribute<T, bool>::s_id = Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++); template <class T> -const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; +const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id; class AttributeManager; diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 644570b24..79490d58e 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -97,51 +97,83 @@ Node& Node::operator=(const Node& e) { } Node Node::eqExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(EQUAL, *this, right); } Node Node::notExpr() const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(NOT, *this); } Node Node::andExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(AND, *this, right); } Node Node::orExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(OR, *this, right); } Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart); } Node Node::iffExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(IFF, *this, right); } Node Node::impExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(IMPLIES, *this, right); } Node Node::xorExpr(const Node& right) const { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->mkNode(XOR, *this, right); } -static void indent(ostream & o, int indent){ - for(int i=0; i < indent; i++) +static void indent(ostream & o, int indent) { + for(int i=0; i < indent; i++) { o << ' '; + } } void Node::printAst(ostream & o, int ind) const { indent(o, ind); o << '('; o << getKind(); - if(getKind() == VARIABLE){ + if(getKind() == VARIABLE) { o << ' ' << getId(); - - }else if(getNumChildren() >= 1){ - for(Node::iterator child = begin(); child != end(); ++child){ + } else if(getNumChildren() >= 1) { + for(Node::iterator child = begin(); child != end(); ++child) { o << endl; (*child).printAst(o, ind + 1); } diff --git a/src/expr/node.h b/src/expr/node.h index 463ff8144..a39dc5b7e 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -48,7 +48,6 @@ using CVC4::expr::NodeValue; class Node { friend class NodeValue; - friend class SoftNode; /** A convenient null-valued encapsulated pointer */ static Node s_null; @@ -106,7 +105,7 @@ public: bool operator!=(const Node& e) const { return d_ev != e.d_ev; } Node operator[](int i) const { - Assert(i >= 0 && i < d_ev->d_nchildren); + Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren); return Node(d_ev->d_children[i]); } @@ -130,9 +129,11 @@ public: Node impExpr(const Node& right) const; Node xorExpr(const Node& right) const; + /* Node plusExpr(const Node& right) const; Node uMinusExpr() const; Node multExpr(const Node& right) const; + */ inline Kind getKind() const; @@ -171,9 +172,9 @@ public: * @param indent number of spaces to indent the formula by. */ void printAst(std::ostream & o, int indent = 0) const; - + private: - + /** * Pretty printer for use within gdb * This is not intended to be used outside of gdb. @@ -262,18 +263,30 @@ inline size_t Node::getNumChildren() const { template <class AttrKind> inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->getAttribute(*this, AttrKind()); } template <class AttrKind> inline bool Node::hasAttribute(const AttrKind&, typename AttrKind::value_type* ret) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret); } template <class AttrKind> inline void Node::setAttribute(const AttrKind&, const typename AttrKind::value_type& value) { + Assert( NodeManager::currentNM() != NULL, + "There is no current CVC4::NodeManager associated to this thread.\n" + "Perhaps a public-facing function is missing a NodeManagerScope ?" ); + NodeManager::currentNM()->setAttribute(*this, AttrKind(), value); } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 1bb71860c..d7bb3c265 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -116,6 +116,14 @@ public: CnfStream(SatSolver* satSolver); /** + * Destructs a CnfStream. This implementation does nothing, but we + * need a virtual destructor for safety in case subclasses have a + * destructor. + */ + virtual ~CnfStream() { + } + + /** * Converts and asserts a formula. * @param node node to convert and assert * @param whether the sat solver can choose to remove this clause diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index cec499a13..c530434f5 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -28,6 +28,14 @@ class OutputChannel { public: /** + * Destructs an OutputChannel. This implementation does nothing, + * but we need a virtual destructor for safety in case subclasses + * have a destructor. + */ + virtual ~OutputChannel() { + } + + /** * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. */ @@ -68,6 +76,14 @@ class ExplainOutputChannel { public: /** + * Destructs an ExplainOutputChannel. This implementation does + * nothing, but we need a virtual destructor for safety in case + * subclasses have a destructor. + */ + virtual ~ExplainOutputChannel() { + } + + /** * With safePoint(), the theory signals that it is at a safe point * and can be interrupted. The default implementation never * interrupts. diff --git a/src/theory/theory.h b/src/theory/theory.h index 8b83f71cf..dffc99053 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -58,12 +58,20 @@ public: static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** - * Construct a theory. + * Construct a Theory. */ Theory() { } /** + * Destructs a Theory. This implementation does nothing, but we + * need a virtual destructor for safety in case subclasses have a + * destructor. + */ + virtual ~Theory() { + } + + /** * Prepare for a Node. * * When get() is called to get the next thing off the theory queue, |