diff options
Diffstat (limited to 'src')
41 files changed, 569 insertions, 176 deletions
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h index 82bc9cc15..a1e50c7c8 100644 --- a/src/context/cdlist_forward.h +++ b/src/context/cdlist_forward.h @@ -37,7 +37,7 @@ #include <memory> namespace __gnu_cxx { - template <class Key> class hash; + template <class Key> struct hash; }/* __gnu_cxx namespace */ namespace CVC4 { diff --git a/src/context/cdmap_forward.h b/src/context/cdmap_forward.h index 1024f0b54..214d9e700 100644 --- a/src/context/cdmap_forward.h +++ b/src/context/cdmap_forward.h @@ -29,7 +29,7 @@ #define __CVC4__CONTEXT__CDMAP_FORWARD_H namespace __gnu_cxx { - template <class Key> class hash; + template <class Key> struct hash; }/* __gnu_cxx namespace */ namespace CVC4 { diff --git a/src/context/cdset_forward.h b/src/context/cdset_forward.h index 135db8751..af3c6f85c 100644 --- a/src/context/cdset_forward.h +++ b/src/context/cdset_forward.h @@ -29,7 +29,7 @@ #define __CVC4__CONTEXT__CDSET_FORWARD_H namespace __gnu_cxx { - template <class Key> class hash; + template <class Key> struct hash; }/* __gnu_cxx namespace */ namespace CVC4 { diff --git a/src/context/context.h b/src/context/context.h index 053d5cb1a..aabe4e7c2 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -497,6 +497,15 @@ protected: public: /** + * Disable delete: objects allocated with new(ContextMemorymanager) should + * never be deleted. Objects allocated with new(bool) should be deleted by + * calling deleteSelf(). + */ + static void operator delete(void* pMem) { + AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); + } + + /** * operator new using ContextMemoryManager (common case used by * subclasses during save()). No delete is required for memory * allocated this way, since it is automatically released when the @@ -573,15 +582,6 @@ public: ::operator delete(this); } - /** - * Disable delete: objects allocated with new(ContextMemorymanager) should - * never be deleted. Objects allocated with new(bool) should be deleted by - * calling deleteSelf(). - */ - static void operator delete(void* pMem) { - AlwaysAssert(false, "It is not allowed to delete a ContextObj this way!"); - } - };/* class ContextObj */ /** 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: diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c index b1bc24ed8..97c8f28a8 100644 --- a/src/lib/clock_gettime.c +++ b/src/lib/clock_gettime.c @@ -18,6 +18,8 @@ ** OS X). **/ +#include "cvc4_private.h" + #include <stdio.h> #include <errno.h> #include <time.h> diff --git a/src/parser/input.h b/src/parser/input.h index 6ed9bb441..b9123fc45 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -94,10 +94,11 @@ class CVC4_PUBLIC Input { InputStream *d_inputStream; /* Since we own d_inputStream and it needs to be freed, we need to prevent - * copy construction and assignment. + * copy construction and assignment. Mark them private and do not define + * them. */ - Input(const Input& input) { Unimplemented("Copy constructor for Input."); } - Input& operator=(const Input& input) { Unimplemented("operator= for Input."); } + Input(const Input& input) CVC4_UNUSED; + Input& operator=(const Input& input) CVC4_UNUSED; public: diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g index f125826d3..39d834891 100644 --- a/src/parser/smt/Smt.g +++ b/src/parser/smt/Smt.g @@ -595,7 +595,7 @@ ROTATE_LEFT_TOK : 'rotate_left'; ROTATE_RIGHT_TOK : 'rotate_right'; /** - * Mathces a bit-vector constant of the form bv123 + * Matches a bit-vector constant of the form bv123 */ BITVECTOR_BV_CONST : 'bv' DIGIT+ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 705eee4d4..f34279149 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): mdeters, taking ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -27,7 +27,7 @@ options { @header { /** ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009, 2010, 2011 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 @@ -321,6 +321,7 @@ term[CVC4::Expr& expr] @init { Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl; Kind kind; + Expr op; std::string name; std::vector<Expr> args; SExpr sexpr; @@ -356,18 +357,27 @@ term[CVC4::Expr& expr] | /* A non-built-in function application */ LPAREN_TOK functionName[name,CHECK_DECLARED] - { args.push_back(Expr()); } - termList[args,expr] RPAREN_TOK { PARSER_STATE->checkFunction(name); const bool isDefinedFunction = PARSER_STATE->isDefinedFunction(name); - expr = isDefinedFunction ? - PARSER_STATE->getFunction(name) : - PARSER_STATE->getVariable(name); - args[0] = expr; - expr = MK_EXPR(isDefinedFunction ? - CVC4::kind::APPLY : - CVC4::kind::APPLY_UF, args); } + if(isDefinedFunction) { + expr = PARSER_STATE->getFunction(name); + kind = CVC4::kind::APPLY; + } else { + expr = PARSER_STATE->getVariable(name); + kind = CVC4::kind::APPLY_UF; + } + args.push_back(expr); + } + termList[args,expr] RPAREN_TOK + { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl; + for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) + Debug("parser") << "++ " << *i << std::endl; + expr = MK_EXPR(kind, args); } + + | /* An indexed function application */ + LPAREN_TOK indexedFunctionName[op] termList[args,expr] RPAREN_TOK + { expr = MK_EXPR(op, args); } | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK @@ -421,19 +431,62 @@ term[CVC4::Expr& expr] // valid GMP rational string expr = MK_CONST( AntlrInput::tokenToRational($DECIMAL_LITERAL) ); } + | LPAREN_TOK INDEX_TOK bvLit=SYMBOL size=INTEGER_LITERAL RPAREN_TOK + { if(AntlrInput::tokenText($bvLit).find("bv") == 0) { + expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) ); + } else { + PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'"); + } + } + | HEX_LITERAL { Assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); - std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL,2); + std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); expr = MK_CONST( BitVector(hexString, 16) ); } | BINARY_LITERAL { Assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); - std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL,2); + std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); expr = MK_CONST( BitVector(binString, 2) ); } // NOTE: Theory constants go here ; /** + * Matches a bit-vector operator (the ones parametrized by numbers) + */ +indexedFunctionName[CVC4::Expr& op] + : LPAREN_TOK INDEX_TOK + ( 'extract' n1=INTEGER_LITERAL n2=INTEGER_LITERAL + { op = MK_CONST(BitVectorExtract(AntlrInput::tokenToUnsigned($n1), + AntlrInput::tokenToUnsigned($n2))); } + | 'repeat' n=INTEGER_LITERAL + { op = MK_CONST(BitVectorRepeat(AntlrInput::tokenToUnsigned($n))); } + | 'zero_extend' n=INTEGER_LITERAL + { op = MK_CONST(BitVectorZeroExtend(AntlrInput::tokenToUnsigned($n))); } + | 'sign_extend' n=INTEGER_LITERAL + { op = MK_CONST(BitVectorSignExtend(AntlrInput::tokenToUnsigned($n))); } + | 'rotate_left' n=INTEGER_LITERAL + { op = MK_CONST(BitVectorRotateLeft(AntlrInput::tokenToUnsigned($n))); } + | 'rotate_right' n=INTEGER_LITERAL + { op = MK_CONST(BitVectorRotateRight(AntlrInput::tokenToUnsigned($n))); } + | badIndexedFunctionName + ) + RPAREN_TOK + ; + +/** + * Matches an erroneous indexed function name (and args) for better + * error reporting. + */ +badIndexedFunctionName +@declarations { + std::string name; +} + : symbol[name,CHECK_NONE,SYM_VARIABLE] INTEGER_LITERAL+ + { PARSER_STATE->parseError(std::string("Unknown indexed function `") + name + "'"); } + ; + +/** * Matches a sequence of terms and puts them into the formulas * vector. * @param formulas the vector to fill with terms @@ -472,8 +525,40 @@ builtinOp[CVC4::Kind& kind] | MINUS_TOK { $kind = CVC4::kind::MINUS; } | STAR_TOK { $kind = CVC4::kind::MULT; } | DIV_TOK { $kind = CVC4::kind::DIVISION; } + | SELECT_TOK { $kind = CVC4::kind::SELECT; } | STORE_TOK { $kind = CVC4::kind::STORE; } + + | CONCAT_TOK { $kind = CVC4::kind::BITVECTOR_CONCAT; } + | BVNOT_TOK { $kind = CVC4::kind::BITVECTOR_NOT; } + | BVAND_TOK { $kind = CVC4::kind::BITVECTOR_AND; } + | BVOR_TOK { $kind = CVC4::kind::BITVECTOR_OR; } + | BVNEG_TOK { $kind = CVC4::kind::BITVECTOR_NEG; } + | BVADD_TOK { $kind = CVC4::kind::BITVECTOR_PLUS; } + | BVMUL_TOK { $kind = CVC4::kind::BITVECTOR_MULT; } + | BVUDIV_TOK { $kind = CVC4::kind::BITVECTOR_UDIV; } + | BVUREM_TOK { $kind = CVC4::kind::BITVECTOR_UREM; } + | BVSHL_TOK { $kind = CVC4::kind::BITVECTOR_SHL; } + | BVLSHR_TOK { $kind = CVC4::kind::BITVECTOR_LSHR; } + | BVULT_TOK { $kind = CVC4::kind::BITVECTOR_ULT; } + | BVNAND_TOK { $kind = CVC4::kind::BITVECTOR_NAND; } + | BVNOR_TOK { $kind = CVC4::kind::BITVECTOR_NOR; } + | BVXOR_TOK { $kind = CVC4::kind::BITVECTOR_XOR; } + | BVXNOR_TOK { $kind = CVC4::kind::BITVECTOR_XNOR; } + | BVCOMP_TOK { $kind = CVC4::kind::BITVECTOR_COMP; } + | BVSUB_TOK { $kind = CVC4::kind::BITVECTOR_SUB; } + | BVSDIV_TOK { $kind = CVC4::kind::BITVECTOR_SDIV; } + | BVSREM_TOK { $kind = CVC4::kind::BITVECTOR_SREM; } + | BVSMOD_TOK { $kind = CVC4::kind::BITVECTOR_SMOD; } + | BVASHR_TOK { $kind = CVC4::kind::BITVECTOR_ASHR; } + | BVULE_TOK { $kind = CVC4::kind::BITVECTOR_ULE; } + | BVUGT_TOK { $kind = CVC4::kind::BITVECTOR_UGT; } + | BVUGE_TOK { $kind = CVC4::kind::BITVECTOR_UGE; } + | BVSLT_TOK { $kind = CVC4::kind::BITVECTOR_SLT; } + | BVSLE_TOK { $kind = CVC4::kind::BITVECTOR_SLE; } + | BVSGT_TOK { $kind = CVC4::kind::BITVECTOR_SGT; } + | BVSGE_TOK { $kind = CVC4::kind::BITVECTOR_SGE; } + // NOTE: Theory operators go here ; @@ -534,9 +619,21 @@ sortSymbol[CVC4::Type& t] @declarations { std::string name; std::vector<CVC4::Type> args; + std::vector<uint64_t> numerals; } : sortName[name,CHECK_NONE] { t = PARSER_STATE->getSort(name); } + | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK + { + if( name == "BitVec" ) { + if( numerals.size() != 1 ) { + PARSER_STATE->parseError("Illegal bitvector type."); + } + t = EXPR_MANAGER->mkBitVectorType(numerals.front()); + } else { + Unhandled(name); + } + } | LPAREN_TOK symbol[name,CHECK_NONE,SYM_SORT] sortList[args] RPAREN_TOK { if( name == "Array" ) { @@ -580,6 +677,16 @@ symbol[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } ; +/** + * Matches a nonempty list of numerals. + * @param numerals the (empty) vector to house the numerals. + */ +nonemptyNumeralList[std::vector<uint64_t>& numerals] + : ( INTEGER_LITERAL + { numerals.push_back(AntlrInput::tokenToUnsigned($INTEGER_LITERAL)); } + )+ + ; + // Base SMT-LIB tokens ASSERT_TOK : 'assert'; CHECKSAT_TOK : 'check-sat'; @@ -596,6 +703,7 @@ LET_TOK : 'let'; ATTRIBUTE_TOK : '!'; LPAREN_TOK : '('; RPAREN_TOK : ')'; +INDEX_TOK : '_'; SET_LOGIC_TOK : 'set-logic'; SET_INFO_TOK : 'set-info'; GET_INFO_TOK : 'get-info'; @@ -631,6 +739,36 @@ STORE_TOK : 'store'; TILDE_TOK : '~'; XOR_TOK : 'xor'; +CONCAT_TOK : 'concat'; +BVNOT_TOK : 'bvnot'; +BVAND_TOK : 'bvand'; +BVOR_TOK : 'bvor'; +BVNEG_TOK : 'bvneg'; +BVADD_TOK : 'bvadd'; +BVMUL_TOK : 'bvmul'; +BVUDIV_TOK : 'bvudiv'; +BVUREM_TOK : 'bvurem'; +BVSHL_TOK : 'bvshl'; +BVLSHR_TOK : 'bvlshr'; +BVULT_TOK : 'bvult'; +BVNAND_TOK : 'bvnand'; +BVNOR_TOK : 'bvnor'; +BVXOR_TOK : 'bvxor'; +BVXNOR_TOK : 'bvxnor'; +BVCOMP_TOK : 'bvcomp'; +BVSUB_TOK : 'bvsub'; +BVSDIV_TOK : 'bvsdiv'; +BVSREM_TOK : 'bvsrem'; +BVSMOD_TOK : 'bvsmod'; +BVASHR_TOK : 'bvashr'; +BVULE_TOK : 'bvule'; +BVUGT_TOK : 'bvugt'; +BVUGE_TOK : 'bvuge'; +BVSLT_TOK : 'bvslt'; +BVSLE_TOK : 'bvsle'; +BVSGT_TOK : 'bvsgt'; +BVSGE_TOK : 'bvsge'; + /** * Matches a symbol from the input. A symbol is a "simple" symbol or a * sequence of printable ASCII characters that starts and ends with | and @@ -651,10 +789,12 @@ KEYWORD /** Matches a "simple" symbol: a non-empty sequence of letters, digits and * the characters + - / * = % ? ! . $ ~ & ^ < > @ that does not start with a - * digit. + * digit, and is not the special reserved symbol '_'. */ fragment SIMPLE_SYMBOL - : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)* + : (ALPHA | SYMBOL_CHAR) (ALPHA | DIGIT | SYMBOL_CHAR)+ + | ALPHA + | SYMBOL_CHAR_NOUNDERSCORE ; /** @@ -703,14 +843,14 @@ DECIMAL_LITERAL /** * Matches a hexadecimal constant. */ - HEX_LITERAL +HEX_LITERAL : '#x' HEX_DIGIT+ ; /** * Matches a binary constant. */ - BINARY_LITERAL +BINARY_LITERAL : '#b' ('0' | '1')+ ; @@ -730,7 +870,6 @@ COMMENT : ';' (~('\n' | '\r'))* { SKIP(); } ; - /** * Matches any letter ('a'-'z' and 'A'-'Z'). */ @@ -750,11 +889,15 @@ fragment HEX_DIGIT : DIGIT | 'a'..'f' | 'A'..'F'; /** * Matches the characters that may appear in a "symbol" (i.e., an identifier) */ -fragment SYMBOL_CHAR - : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '_' | '~' +fragment SYMBOL_CHAR_NOUNDERSCORE + : '+' | '-' | '/' | '*' | '=' | '%' | '?' | '!' | '.' | '$' | '~' | '&' | '^' | '<' | '>' | '@' ; +fragment SYMBOL_CHAR + : SYMBOL_CHAR_NOUNDERSCORE | '_' + ; + /** * Matches an allowed escaped character. */ diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e41e0e26a..03b901164 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -82,6 +82,9 @@ void Smt2::addTheory(Theory theory) { addArithmeticOperators(); break; + case THEORY_BITVECTORS: + break; + default: Unhandled(theory); } @@ -134,6 +137,10 @@ void Smt2::setLogic(const std::string& name) { addOperator(kind::APPLY_UF); break; + case Smt::QF_BV: + addTheory(THEORY_BITVECTORS); + break; + case Smt::AUFLIA: case Smt::AUFLIRA: case Smt::AUFNIRA: @@ -141,7 +148,6 @@ void Smt2::setLogic(const std::string& name) { case Smt::UFNIA: case Smt::QF_AUFBV: case Smt::QF_AUFLIA: - case Smt::QF_BV: Unhandled(name); } } diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5aff8ebba..1e36b211d 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -176,6 +176,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } else { out << "(...)"; } + if(n.getNumChildren() > 0) { + out << ' '; + } } for(TNode::iterator i = n.begin(), iend = n.end(); diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index b320d9584..3e844ef79 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -3,7 +3,7 @@ AM_CPPFLAGS = \ -D __STDC_LIMIT_MACROS \ -D __STDC_FORMAT_MACROS \ -I@srcdir@/ -I@srcdir@/../.. -I@builddir@/../.. -I@srcdir@/../../include -AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -DNDEBUG +AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = libminisat.la libminisat_la_SOURCES = \ diff --git a/src/prop/sat.h b/src/prop/sat.h index cc81ea5c6..88df366e2 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -53,12 +53,13 @@ class CnfStream; /** Type of the SAT variables */ typedef Minisat::Var SatVariable; -/** Type of the Sat literals */ +/** Type of the SAT literals */ typedef Minisat::Lit SatLiteral; /** Type of the SAT clauses */ typedef Minisat::vec<SatLiteral> SatClause; +/** Type of a SAT variable assignment (T, F, unknown) */ typedef Minisat::lbool SatLiteralValue; /** diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index dfa81cb3f..4b40e582c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -55,8 +55,8 @@ using namespace CVC4::theory::arith; struct SlackAttrID; typedef expr::Attribute<SlackAttrID, Node> Slack; -TheoryArith::TheoryArith(context::Context* c, OutputChannel& out) : - Theory(THEORY_ARITH, c, out), +TheoryArith::TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_ARITH, c, out, valuation), d_partialModel(c), d_userVariables(), d_diseq(c), @@ -497,7 +497,7 @@ void TheoryArith::propagate(Effort e) { } } -Node TheoryArith::getValue(TNode n, Valuation* valuation) { +Node TheoryArith::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -508,7 +508,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) { Node eq = d_removedRows.find(var)->second; Assert(n == eq[0]); Node rhs = eq[1]; - return getValue(rhs, valuation); + return getValue(rhs); } DeltaRational drat = d_partialModel.getAssignment(var); @@ -521,7 +521,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); case kind::PLUS: { // 2+ args Rational value(0); @@ -529,7 +529,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) { iend = n.end(); i != iend; ++i) { - value += valuation->getValue(*i).getConst<Rational>(); + value += d_valuation.getValue(*i).getConst<Rational>(); } return nodeManager->mkConst(value); } @@ -540,7 +540,7 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) { iend = n.end(); i != iend; ++i) { - value *= valuation->getValue(*i).getConst<Rational>(); + value *= d_valuation.getValue(*i).getConst<Rational>(); } return nodeManager->mkConst(value); } @@ -554,24 +554,24 @@ Node TheoryArith::getValue(TNode n, Valuation* valuation) { Unreachable(); case kind::DIVISION: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() / - valuation->getValue(n[1]).getConst<Rational>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() / + d_valuation.getValue(n[1]).getConst<Rational>() ); case kind::LT: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() < - valuation->getValue(n[1]).getConst<Rational>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() < + d_valuation.getValue(n[1]).getConst<Rational>() ); case kind::LEQ: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() <= - valuation->getValue(n[1]).getConst<Rational>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() <= + d_valuation.getValue(n[1]).getConst<Rational>() ); case kind::GT: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() > - valuation->getValue(n[1]).getConst<Rational>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() > + d_valuation.getValue(n[1]).getConst<Rational>() ); case kind::GEQ: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<Rational>() >= - valuation->getValue(n[1]).getConst<Rational>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<Rational>() >= + d_valuation.getValue(n[1]).getConst<Rational>() ); default: Unhandled(n.getKind()); diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 07ba08e9c..11cbfb425 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -144,7 +144,7 @@ private: SimplexDecisionProcedure d_simplex; public: - TheoryArith(context::Context* c, OutputChannel& out); + TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation); ~TheoryArith(); /** @@ -161,7 +161,7 @@ public: void notifyEq(TNode lhs, TNode rhs); - Node getValue(TNode n, Valuation* valuation); + Node getValue(TNode n); void shutdown(){ } diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp index d45320266..8b625613a 100644 --- a/src/theory/arrays/theory_arrays.cpp +++ b/src/theory/arrays/theory_arrays.cpp @@ -30,8 +30,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::arrays; -TheoryArrays::TheoryArrays(Context* c, OutputChannel& out) : - Theory(THEORY_ARRAY, c, out) +TheoryArrays::TheoryArrays(Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_ARRAY, c, out, valuation) { } @@ -60,7 +60,7 @@ void TheoryArrays::check(Effort e) { Debug("arrays") << "TheoryArrays::check(): done" << endl; } -Node TheoryArrays::getValue(TNode n, Valuation* valuation) { +Node TheoryArrays::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -70,7 +70,7 @@ Node TheoryArrays::getValue(TNode n, Valuation* valuation) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); default: Unhandled(n.getKind()); diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h index 5a63fd26c..64fdd8303 100644 --- a/src/theory/arrays/theory_arrays.h +++ b/src/theory/arrays/theory_arrays.h @@ -31,7 +31,7 @@ namespace arrays { class TheoryArrays : public Theory { public: - TheoryArrays(context::Context* c, OutputChannel& out); + TheoryArrays(context::Context* c, OutputChannel& out, Valuation valuation); ~TheoryArrays(); void preRegisterTerm(TNode n) { } void registerTerm(TNode n) { } @@ -43,7 +43,7 @@ public: void check(Effort e); void propagate(Effort e) { } void explain(TNode n) { } - Node getValue(TNode n, Valuation* valuation); + Node getValue(TNode n); void shutdown() { } std::string identify() const { return std::string("TheoryArrays"); } };/* class TheoryArrays */ diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp index 44f5d60a6..878b18478 100644 --- a/src/theory/booleans/theory_bool.cpp +++ b/src/theory/booleans/theory_bool.cpp @@ -24,7 +24,7 @@ namespace CVC4 { namespace theory { namespace booleans { -Node TheoryBool::getValue(TNode n, Valuation* valuation) { +Node TheoryBool::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -38,14 +38,14 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) { Unreachable(); case kind::NOT: // 1 arg - return nodeManager->mkConst(! valuation->getValue(n[0]).getConst<bool>()); + return nodeManager->mkConst(! d_valuation.getValue(n[0]).getConst<bool>()); case kind::AND: { // 2+ args for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(! valuation->getValue(*i).getConst<bool>()) { + if(! d_valuation.getValue(*i).getConst<bool>()) { return nodeManager->mkConst(false); } } @@ -53,19 +53,19 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) { } case kind::IFF: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() == - valuation->getValue(n[1]).getConst<bool>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() == + d_valuation.getValue(n[1]).getConst<bool>() ); case kind::IMPLIES: // 2 args - return nodeManager->mkConst( (! valuation->getValue(n[0]).getConst<bool>()) || - valuation->getValue(n[1]).getConst<bool>() ); + return nodeManager->mkConst( (! d_valuation.getValue(n[0]).getConst<bool>()) || + d_valuation.getValue(n[1]).getConst<bool>() ); case kind::OR: { // 2+ args for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) { - if(valuation->getValue(*i).getConst<bool>()) { + if(d_valuation.getValue(*i).getConst<bool>()) { return nodeManager->mkConst(true); } } @@ -73,16 +73,16 @@ Node TheoryBool::getValue(TNode n, Valuation* valuation) { } case kind::XOR: // 2 args - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() != - valuation->getValue(n[1]).getConst<bool>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() != + d_valuation.getValue(n[1]).getConst<bool>() ); case kind::ITE: // 3 args // all ITEs should be gone except (bool,bool,bool) ones Assert( n[1].getType() == nodeManager->booleanType() && n[2].getType() == nodeManager->booleanType() ); - return nodeManager->mkConst( valuation->getValue(n[0]).getConst<bool>() ? - valuation->getValue(n[1]).getConst<bool>() : - valuation->getValue(n[2]).getConst<bool>() ); + return nodeManager->mkConst( d_valuation.getValue(n[0]).getConst<bool>() ? + d_valuation.getValue(n[1]).getConst<bool>() : + d_valuation.getValue(n[2]).getConst<bool>() ); default: Unhandled(n.getKind()); diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h index 4120159df..dfcdd22b8 100644 --- a/src/theory/booleans/theory_bool.h +++ b/src/theory/booleans/theory_bool.h @@ -30,8 +30,8 @@ namespace booleans { class TheoryBool : public Theory { public: - TheoryBool(context::Context* c, OutputChannel& out) : - Theory(THEORY_BOOL, c, out) { + TheoryBool(context::Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_BOOL, c, out, valuation) { } void preRegisterTerm(TNode n) { @@ -43,7 +43,7 @@ public: Debug("bool") << "bool: end preRegisterTerm(" << n << ")" << std::endl; } - Node getValue(TNode n, Valuation* valuation); + Node getValue(TNode n); std::string identify() const { return std::string("TheoryBool"); } }; diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp index a276fa0ce..1c779bd79 100644 --- a/src/theory/builtin/theory_builtin.cpp +++ b/src/theory/builtin/theory_builtin.cpp @@ -26,7 +26,7 @@ namespace CVC4 { namespace theory { namespace builtin { -Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { +Node TheoryBuiltin::getValue(TNode n) { switch(n.getKind()) { case kind::VARIABLE: @@ -39,7 +39,7 @@ Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { Assert(n[0].getKind() == kind::TUPLE && n[1].getKind() == kind::TUPLE); return NodeManager::currentNM()-> - mkConst( getValue(n[0], valuation) == getValue(n[1], valuation) ); + mkConst( getValue(n[0]) == getValue(n[1]) ); } case kind::TUPLE: { // 2+ args @@ -48,7 +48,7 @@ Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) { iend = n.end(); i != iend; ++i) { - nb << valuation->getValue(*i); + nb << d_valuation.getValue(*i); } return Node(nb); } diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h index 5b9810326..4e62401ff 100644 --- a/src/theory/builtin/theory_builtin.h +++ b/src/theory/builtin/theory_builtin.h @@ -29,9 +29,9 @@ namespace builtin { class TheoryBuiltin : public Theory { public: - TheoryBuiltin(context::Context* c, OutputChannel& out) : - Theory(THEORY_BUILTIN, c, out) {} - Node getValue(TNode n, Valuation* valuation); + TheoryBuiltin(context::Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_BUILTIN, c, out, valuation) {} + Node getValue(TNode n); std::string identify() const { return std::string("TheoryBuiltin"); } };/* class TheoryBuiltin */ diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 258345ad8..e106f3b84 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -155,7 +155,7 @@ bool TheoryBV::triggerEquality(size_t triggerId) { return true; } -Node TheoryBV::getValue(TNode n, Valuation* valuation) { +Node TheoryBV::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -165,7 +165,7 @@ Node TheoryBV::getValue(TNode n, Valuation* valuation) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); default: Unhandled(n.getKind()); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index f2c2fa332..d65f0388b 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -103,8 +103,8 @@ private: public: - TheoryBV(context::Context* c, OutputChannel& out) : - Theory(THEORY_BV, c, out), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) { + TheoryBV(context::Context* c, OutputChannel& out, Valuation valuation) : + Theory(THEORY_BV, c, out, valuation), d_eqEngine(*this, c, "theory::bv::EqualityEngine"), d_sliceManager(*this, c), d_assertions(c), d_disequalities(c) { } BvEqualityEngine& getEqualityEngine() { @@ -123,7 +123,7 @@ public: void explain(TNode n); - Node getValue(TNode n, Valuation* valuation); + Node getValue(TNode n); std::string identify() const { return std::string("TheoryBV"); } };/* class TheoryBV */ diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index bdf1c8d51..7af5b4496 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -28,7 +28,7 @@ namespace CVC4 { namespace theory { namespace bv { -class AllRewriteRules; +struct AllRewriteRules; class TheoryBVRewriter { diff --git a/src/theory/theory.h b/src/theory/theory.h index 620c70710..72341869d 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -23,6 +23,7 @@ #include "expr/node.h" #include "expr/attribute.h" +#include "theory/valuation.h" #include "theory/output_channel.h" #include "context/context.h" #include "context/cdlist.h" @@ -37,10 +38,11 @@ namespace CVC4 { class TheoryEngine; namespace theory { - class Valuation; -}/* CVC4::theory namespace */ -namespace theory { +/** Tag for the "newFact()-has-been-called-in-this-context" flag on Nodes */ +struct AssertedAttrTag {}; +/** The "newFact()-has-been-called-in-this-context" flag on Nodes */ +typedef CVC4::expr::CDAttribute<AssertedAttrTag, bool> Asserted; /** * Base class for T-solvers. Abstract DPLL(T). @@ -88,16 +90,15 @@ protected: /** * Construct a Theory. */ - Theory(TheoryId id, context::Context* ctxt, OutputChannel& out) throw() : + Theory(TheoryId id, context::Context* ctxt, OutputChannel& out, Valuation valuation) throw() : d_id(id), d_context(ctxt), d_facts(ctxt), d_factsHead(ctxt, 0), - d_out(&out) { + d_out(&out), + d_valuation(valuation) { } - - /** * This is called at shutdown time by the TheoryEngine, just before * destruction. It is important because there are destruction @@ -114,10 +115,11 @@ protected: */ OutputChannel* d_out; - /** Tag for the "preRegisterTerm()-has-been-called" flag on Nodes */ - struct PreRegistered {}; - /** The "preRegisterTerm()-has-been-called" flag on Nodes */ - typedef CVC4::expr::Attribute<PreRegistered, bool> PreRegisteredAttr; + /** + * The valuation proxy for the Theory to communicate back with the + * theory engine (and other theories). + */ + Valuation d_valuation; /** * Returns the next atom in the assertFact() queue. Guarantees that @@ -135,6 +137,26 @@ protected: return fact; } + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the beginning of the fact queue + */ + context::CDList<Node>::const_iterator facts_begin() const { + return d_facts.begin(); + } + + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the end of the fact queue + */ + context::CDList<Node>::const_iterator facts_end() const { + return d_facts.end(); + } + public: static inline TheoryId theoryOf(TypeNode typeNode) { @@ -345,7 +367,7 @@ public: * and suspect this situation is the case, return Node::null() * rather than throwing an exception. */ - virtual Node getValue(TNode n, Valuation* valuation) { + virtual Node getValue(TNode n) { Unimplemented("Theory %s doesn't support Theory::getValue interface", identify().c_str()); return Node::null(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f8eece3df..2411956f5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -36,18 +36,18 @@ using namespace CVC4::theory; namespace CVC4 { +namespace theory { + /** Tag for the "registerTerm()-has-been-called" flag on Nodes */ -struct Registered {}; +struct RegisteredAttrTag {}; /** The "registerTerm()-has-been-called" flag on Nodes */ -typedef CVC4::expr::CDAttribute<Registered, bool> RegisteredAttr; - -namespace theory { +typedef CVC4::expr::CDAttribute<RegisteredAttrTag, bool> RegisteredAttr; -struct PreRegisteredTag {}; -typedef expr::Attribute<PreRegisteredTag, bool> PreRegistered; +struct PreRegisteredAttrTag {}; +typedef expr::Attribute<PreRegisteredAttrTag, bool> PreRegistered; -struct IteRewriteTag {}; -typedef expr::Attribute<IteRewriteTag, Node> IteRewriteAttr; +struct IteRewriteAttrTag {}; +typedef expr::Attribute<IteRewriteAttrTag, Node> IteRewriteAttr; }/* CVC4::theory namespace */ @@ -136,7 +136,6 @@ TheoryEngine::TheoryEngine(context::Context* ctxt, const Options& opts) : d_theoryRegistration(opts.theoryRegistration), d_hasShutDown(false), d_incomplete(ctxt, false), - d_valuation(this), d_opts(opts), d_statistics() { @@ -347,7 +346,7 @@ Node TheoryEngine::getValue(TNode node) { } // otherwise ask the theory-in-charge - return theoryOf(node)->getValue(node, &d_valuation); + return theoryOf(node)->getValue(node); }/* TheoryEngine::getValue(TNode node) */ bool TheoryEngine::presolve() { diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7553b1f0c..787323495 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -151,12 +151,6 @@ class TheoryEngine { context::CDO<bool> d_incomplete; /** - * A "valuation proxy" for this TheoryEngine. Used only in getValue() - * for decoupled Theory-to-TheoryEngine communication. - */ - theory::Valuation d_valuation; - - /** * Replace ITE forms in a node. */ Node removeITEs(TNode t); @@ -180,7 +174,7 @@ public: */ template <class TheoryClass> void addTheory() { - TheoryClass* theory = new TheoryClass(d_context, d_theoryOut); + TheoryClass* theory = new TheoryClass(d_context, d_theoryOut, theory::Valuation(this)); d_theoryTable[theory->getId()] = theory; d_sharedTermManager->registerTheory(static_cast<TheoryClass*>(theory)); @@ -258,6 +252,12 @@ public: inline void assertFact(TNode node) { Debug("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl; + // Mark it as asserted in this context + // + // [MGD] removed for now, this appears to have a nontrivial + // performance penalty + // node.setAttribute(theory::Asserted(), true); + // Get the atom TNode atom = node.getKind() == kind::NOT ? node[0] : node; diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp index 5d4d44d0a..e15467bff 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.cpp +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -31,8 +31,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; using namespace CVC4::theory::uf::morgan; -TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out) : - TheoryUF(ctxt, out), +TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out, Valuation valuation) : + TheoryUF(ctxt, out, valuation), d_assertions(ctxt), d_ccChannel(this), d_cc(ctxt, &d_ccChannel), @@ -567,7 +567,7 @@ void TheoryUFMorgan::notifyRestart() { Debug("uf") << "uf: end notifyDecisionLevelZero()" << endl; } -Node TheoryUFMorgan::getValue(TNode n, Valuation* valuation) { +Node TheoryUFMorgan::getValue(TNode n) { NodeManager* nodeManager = NodeManager::currentNM(); switch(n.getKind()) { @@ -585,7 +585,7 @@ Node TheoryUFMorgan::getValue(TNode n, Valuation* valuation) { case kind::EQUAL: // 2 args return nodeManager-> - mkConst( valuation->getValue(n[0]) == valuation->getValue(n[1]) ); + mkConst( d_valuation.getValue(n[0]) == d_valuation.getValue(n[1]) ); default: Unhandled(n.getKind()); diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h index 47c860c9a..c2feef349 100644 --- a/src/theory/uf/morgan/theory_uf_morgan.h +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -132,7 +132,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFMorgan(context::Context* ctxt, OutputChannel& out); + TheoryUFMorgan(context::Context* ctxt, OutputChannel& out, Valuation valuation); /** Destructor for UF theory, cleans up memory and statistics. */ ~TheoryUFMorgan(); @@ -214,7 +214,7 @@ public: * Overloads Node getValue(TNode n); from theory.h. * See theory/theory.h for more information about this method. */ - Node getValue(TNode n, Valuation* valuation); + Node getValue(TNode n); std::string identify() const { return std::string("TheoryUFMorgan"); } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index be3d7ac69..9746b38ab 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -37,8 +37,8 @@ class TheoryUF : public Theory { public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* ctxt, OutputChannel& out) - : Theory(THEORY_UF, ctxt, out) {} + TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation) + : Theory(THEORY_UF, ctxt, out, valuation) { } };/* class TheoryUF */ diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp index db0574d4f..ef1704426 100644 --- a/src/theory/uf/tim/theory_uf_tim.cpp +++ b/src/theory/uf/tim/theory_uf_tim.cpp @@ -27,8 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; using namespace CVC4::theory::uf::tim; -TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out) : - TheoryUF(c, out), +TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) : + TheoryUF(c, out, valuation), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h index d07f49f03..70c60728f 100644 --- a/src/theory/uf/tim/theory_uf_tim.h +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -85,13 +85,11 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, OutputChannel& out); + TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation); /** Destructor for the TheoryUF object. */ ~TheoryUFTim(); - - /** * Registers a previously unseen [in this context] node n. * For TheoryUF, this sets up and maintains invaraints about @@ -150,7 +148,7 @@ public: * Overloads Node getValue(TNode n); from theory.h. * See theory/theory.h for more information about this method. */ - Node getValue(TNode n, Valuation* valuation) { + Node getValue(TNode n) { Unimplemented("TheoryUFTim doesn't support model generation"); } |