diff options
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/attribute.cpp | 5 | ||||
-rw-r--r-- | src/expr/attribute_internals.h | 231 | ||||
-rw-r--r-- | src/expr/command.cpp | 18 | ||||
-rw-r--r-- | src/expr/declaration_scope.h | 8 | ||||
-rw-r--r-- | src/expr/expr_manager_template.cpp | 28 | ||||
-rw-r--r-- | src/expr/expr_manager_template.h | 2 | ||||
-rw-r--r-- | src/expr/expr_template.cpp | 2 | ||||
-rw-r--r-- | src/expr/node.cpp | 2 | ||||
-rw-r--r-- | src/expr/node_manager.h | 2 | ||||
-rw-r--r-- | src/expr/type.h | 2 |
10 files changed, 259 insertions, 41 deletions
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 295244473..85c0fe528 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -37,8 +37,7 @@ void AttributeManager::deleteAllAttributes(NodeValue* nv) { deleteFromTable(d_strings, nv); deleteFromTable(d_ptrs, nv); - // FIXME CD-bools in optimized table - deleteFromTable(d_cdbools, nv); + d_cdbools.erase(nv); deleteFromTable(d_cdints, nv); deleteFromTable(d_cdtnodes, nv); deleteFromTable(d_cdnodes, nv); @@ -55,7 +54,6 @@ void AttributeManager::deleteAllAttributes() { deleteAllFromTable(d_strings); deleteAllFromTable(d_ptrs); - // FIXME CD-bools in optimized table d_cdbools.clear(); d_cdints.clear(); d_cdtnodes.clear(); @@ -64,7 +62,6 @@ void AttributeManager::deleteAllAttributes() { d_cdptrs.clear(); } - }/* CVC4::expr::attr namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h index a77d09c4d..3bbab17a4 100644 --- a/src/expr/attribute_internals.h +++ b/src/expr/attribute_internals.h @@ -153,11 +153,11 @@ namespace attr { * to value_type using our specialized hash function for these pairs. */ template <class value_type> -struct AttrHash : +class AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, NodeValue*>, value_type, AttrHashStrategy> { -}; +};/* class AttrHash<> */ /** * In the case of Boolean-valued attributes we have a special @@ -205,7 +205,7 @@ class AttrHash<bool> : operator bool() const { return (d_word & (1 << d_bit)) ? true : false; } - }; + };/* class AttrHash<bool>::BitAccessor */ /** * A (somewhat degenerate) iterator over boolean-valued attributes. @@ -239,7 +239,7 @@ class AttrHash<bool> : bool operator==(const BitIterator& b) { return d_entry == b.d_entry && d_bit == b.d_bit; } - }; + };/* class AttrHash<bool>::BitIterator */ /** * A (somewhat degenerate) const_iterator over boolean-valued @@ -274,7 +274,7 @@ class AttrHash<bool> : bool operator==(const ConstBitIterator& b) { return d_entry == b.d_entry && d_bit == b.d_bit; } - }; + };/* class AttrHash<bool>::ConstBitIterator */ public: @@ -374,7 +374,226 @@ public: value_type, AttrHashStrategy>(ctxt) { } -}; +};/* class CDAttrHash<> */ + +/** + * In the case of Boolean-valued attributes we have a special + * "CDAttrHash<bool>" to pack bits together in words. + */ +template <> +class CDAttrHash<bool> : + protected context::CDMap<NodeValue*, + uint64_t, + AttrHashBoolStrategy> { + + /** A "super" type, like in Java, for easy reference below. */ + typedef context::CDMap<NodeValue*, uint64_t, AttrHashBoolStrategy> super; + + /** + * BitAccessor allows us to return a bit "by reference." Of course, + * we don't require bit-addressibility supported by the system, we + * do it with a complex type. + */ + class BitAccessor { + + super& d_map; + + NodeValue* d_key; + + uint64_t d_word; + + unsigned d_bit; + + public: + + BitAccessor(super& map, NodeValue* key, uint64_t word, unsigned bit) : + d_map(map), + d_key(key), + d_word(word), + d_bit(bit) { + Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor(%p, %p, %lx, %u)\n", &map, key, word, bit); + } + + BitAccessor& operator=(bool b) { + if(b) { + // set the bit + d_word |= (1 << d_bit); + d_map.insert(d_key, d_word); + Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::set(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit); + } else { + // clear the bit + d_word &= ~(1 << d_bit); + d_map.insert(d_key, d_word); + Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit); + } + + return *this; + } + + operator bool() const { + Debug.printf("cdboolattr", "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %lx, %u)\n", &d_map, d_key, d_word, d_bit); + return (d_word & (1 << d_bit)) ? true : false; + } + };/* class CDAttrHash<bool>::BitAccessor */ + + /** + * A (somewhat degenerate) iterator over boolean-valued attributes. + * This iterator doesn't support anything except comparison and + * dereference. It's intended just for the result of find() on the + * table. + */ + class BitIterator { + + super* d_map; + + std::pair<NodeValue* const, uint64_t>* d_entry; + + unsigned d_bit; + + public: + + BitIterator() : + d_map(NULL), + d_entry(NULL), + d_bit(0) { + } + + BitIterator(super& map, std::pair<NodeValue* const, uint64_t>& entry, unsigned bit) : + d_map(&map), + d_entry(&entry), + d_bit(bit) { + } + + std::pair<NodeValue* const, BitAccessor> operator*() { + return std::make_pair(d_entry->first, + BitAccessor(*d_map, d_entry->first, d_entry->second, d_bit)); + } + + bool operator==(const BitIterator& b) { + return d_entry == b.d_entry && d_bit == b.d_bit; + } + };/* class CDAttrHash<bool>::BitIterator */ + + /** + * A (somewhat degenerate) const_iterator over boolean-valued + * attributes. This const_iterator doesn't support anything except + * comparison and dereference. It's intended just for the result of + * find() on the table. + */ + class ConstBitIterator { + + const std::pair<NodeValue* const, uint64_t> d_entry; + + unsigned d_bit; + + public: + + ConstBitIterator() : + d_entry(), + d_bit(0) { + } + + ConstBitIterator(const std::pair<NodeValue* const, uint64_t>& entry, + unsigned bit) : + d_entry(entry), + d_bit(bit) { + } + + std::pair<NodeValue* const, bool> operator*() { + return std::make_pair(d_entry.first, + (d_entry.second & (1 << d_bit)) ? true : false); + } + + bool operator==(const ConstBitIterator& b) { + return d_entry == b.d_entry && d_bit == b.d_bit; + } + };/* class CDAttrHash<bool>::ConstBitIterator */ + + /* remove non-permitted operations */ + CDAttrHash(const CDAttrHash<bool>&) CVC4_UNDEFINED; + CDAttrHash<bool>& operator=(const CDAttrHash<bool>&) CVC4_UNDEFINED; + +public: + + CDAttrHash(context::Context* context) : super(context) { } + + typedef std::pair<uint64_t, NodeValue*> key_type; + typedef bool data_type; + typedef std::pair<const key_type, data_type> value_type; + + /** an iterator type; see above for limitations */ + typedef BitIterator iterator; + /** a const_iterator type; see above for limitations */ + typedef ConstBitIterator const_iterator; + + /** + * Find the boolean value in the hash table. Returns something == + * end() if not found. + */ + /*BitIterator find(const std::pair<uint64_t, NodeValue*>& k) { + super::iterator i = super::find(k.second); + if(i == super::end()) { + return BitIterator(); + } + Debug.printf("cdboolattr", + "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); + }*/ + + /** The "off the end" iterator */ + BitIterator end() { + return BitIterator(); + } + + /** + * Find the boolean value in the hash table. Returns something == + * end() if not found. + */ + ConstBitIterator find(const std::pair<uint64_t, NodeValue*>& k) const { + super::const_iterator i = super::find(k.second); + if(i == super::end()) { + return ConstBitIterator(); + } + Debug.printf("cdboolattr", + "underlying word at address looks like 0x%016llx, bit is %u\n", + (unsigned long long)((*i).second), + unsigned(k.first)); + return ConstBitIterator(*i, k.first); + } + + /** The "off the end" const_iterator */ + ConstBitIterator end() const { + return ConstBitIterator(); + } + + /** + * Access the hash table using the underlying operator[]. Inserts + * the key into the table (associated to default value) if it's not + * already there. + */ + BitAccessor operator[](const std::pair<uint64_t, NodeValue*>& k) { + uint64_t word = super::operator[](k.second); + return BitAccessor(*this, k.second, word, k.first); + } + + /** + * Delete all flags from the given node. + */ + void erase(NodeValue* nv) { + super::obliterate(nv); + } + + /** + * Clear the hash table. + */ + void clear() { + super::clear(); + } + +};/* class CDAttrHash<bool> */ }/* CVC4::expr::attr namespace */ diff --git a/src/expr/command.cpp b/src/expr/command.cpp index b17e98b38..7c08293be 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -345,9 +345,9 @@ void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(":status", status); //d_result = "success"; - } catch(ModalException& m) { + } catch(ModalException&) { d_result = "error"; - } catch(BadOptionException& bo) { + } catch(BadOptionException&) { // should not happen d_result = "error"; } @@ -367,7 +367,7 @@ void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setLogic(d_logic); //d_result = "success"; - } catch(ModalException& m) { + } catch(ModalException&) { d_result = "error"; } } @@ -387,9 +387,9 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(d_flag, d_sexpr); //d_result = "success"; - } catch(ModalException& m) { + } catch(ModalException&) { d_result = "error"; - } catch(BadOptionException& bo) { + } catch(BadOptionException&) { d_result = "unsupported"; } } @@ -419,7 +419,7 @@ void GetInfoCommand::invoke(SmtEngine* smtEngine) { stringstream ss; ss << smtEngine->getInfo(d_flag); d_result = ss.str(); - } catch(BadOptionException& bo) { + } catch(BadOptionException&) { d_result = "unsupported"; } } @@ -449,9 +449,9 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setOption(d_flag, d_sexpr); //d_result = "success"; - } catch(ModalException& m) { + } catch(ModalException&) { d_result = "error"; - } catch(BadOptionException& bo) { + } catch(BadOptionException&) { d_result = "unsupported"; } } @@ -479,7 +479,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) : void GetOptionCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getOption(d_flag).getValue(); - } catch(BadOptionException& bo) { + } catch(BadOptionException&) { d_result = "unsupported"; } } diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h index 65574b6c9..9acc46b5f 100644 --- a/src/expr/declaration_scope.h +++ b/src/expr/declaration_scope.h @@ -16,8 +16,10 @@ ** Convenience class for scoping variable and type declarations. **/ -#ifndef DECLARATION_SCOPE_H -#define DECLARATION_SCOPE_H +#include "cvc4_public.h" + +#ifndef __CVC4__DECLARATION_SCOPE_H +#define __CVC4__DECLARATION_SCOPE_H #include <vector> #include <utility> @@ -182,4 +184,4 @@ public: }/* CVC4 namespace */ -#endif /* DECLARATION_SCOPE_H */ +#endif /* __CVC4__DECLARATION_SCOPE_H */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index eadbb73a2..9b8511de9 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -115,22 +115,22 @@ ExprManager::~ExprManager() { BooleanType ExprManager::booleanType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType())); + return BooleanType(Type(d_nodeManager, new TypeNode(d_nodeManager->booleanType()))); } KindType ExprManager::kindType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->kindType())); + return KindType(Type(d_nodeManager, new TypeNode(d_nodeManager->kindType()))); } RealType ExprManager::realType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->realType())); + return RealType(Type(d_nodeManager, new TypeNode(d_nodeManager->realType()))); } IntegerType ExprManager::integerType() const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->integerType())); + return IntegerType(Type(d_nodeManager, new TypeNode(d_nodeManager->integerType()))); } Expr ExprManager::mkExpr(Kind kind, const Expr& child1) { @@ -285,7 +285,7 @@ Expr ExprManager::mkExpr(Expr opExpr, const std::vector<Expr>& children) { /** Make a function type from domain to range. */ FunctionType ExprManager::mkFunctionType(const Type& domain, const Type& range) { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(*domain.d_typeNode, *range.d_typeNode)))); } /** Make a function type with input types from argTypes. */ @@ -296,7 +296,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& argTypes, cons for (unsigned i = 0, i_end = argTypes.size(); i < i_end; ++ i) { argTypeNodes.push_back(*argTypes[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(argTypeNodes, *range.d_typeNode)))); } FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { @@ -306,7 +306,7 @@ FunctionType ExprManager::mkFunctionType(const std::vector<Type>& sorts) { for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkFunctionType(sortNodes)))); } FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { @@ -316,7 +316,7 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { for (unsigned i = 0, i_end = sorts.size(); i < i_end; ++ i) { sortNodes.push_back(*sorts[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))); + return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)))); } TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { @@ -326,29 +326,29 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); } - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))); + return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)))); } BitVectorType ExprManager::mkBitVectorType(unsigned size) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size))); + return BitVectorType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)))); } ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))); + return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode)))); } SortType ExprManager::mkSort(const std::string& name) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name))); + return SortType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSort(name)))); } SortConstructorType ExprManager::mkSortConstructor(const std::string& name, size_t arity) const { NodeManagerScope nms(d_nodeManager); - return Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSortConstructor(name, arity))); + return SortConstructorType(Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); } /** diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index fba1a919c..83d306871 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -40,7 +40,7 @@ namespace CVC4 { class Expr; class SmtEngine; class NodeManager; -class Options; +struct Options; class IntStat; namespace context { diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index eb618a8c9..f6d346630 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -74,7 +74,7 @@ TypeCheckingException::~TypeCheckingException() throw () { std::string TypeCheckingException::toString() const { std::stringstream ss; - ss << "Error type-checking " << d_expr << ": " << d_msg; + ss << "Error type-checking " << d_expr << ": " << d_msg << std::endl << *d_expr; return ss.str(); } diff --git a/src/expr/node.cpp b/src/expr/node.cpp index efcd42999..445d91da8 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -37,7 +37,7 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { string TypeCheckingExceptionPrivate::toString() const { stringstream ss; - ss << "Error type-checking " << d_node << ": " << d_msg; + ss << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node; return ss.str(); } diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 117497539..d8a690da5 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -42,7 +42,7 @@ namespace CVC4 { -class Options; +struct Options; namespace expr { diff --git a/src/expr/type.h b/src/expr/type.h index d357c869e..cc1248510 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -73,7 +73,7 @@ class CVC4_PUBLIC Type { friend class SmtEngine; friend class ExprManager; friend class TypeNode; - friend class TypeHashStrategy; + friend struct TypeHashStrategy; friend std::ostream& operator<<(std::ostream& out, const Type& t); protected: |