diff options
66 files changed, 837 insertions, 274 deletions
diff --git a/Makefile.am b/Makefile.am index 288cfb2cc..ecb9c6eda 100644 --- a/Makefile.am +++ b/Makefile.am @@ -7,8 +7,8 @@ ACLOCAL_AMFLAGS = -I config SUBDIRS = src test contrib -.PHONY: units regress regress0 regress1 regress2 regress3 -regress regress0 regress1 regress2 regress3: all +.PHONY: units systemtests regress regress0 regress1 regress2 regress3 +systemtests regress regress0 regress1 regress2 regress3: all (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 units: all (cd test && $(MAKE) $(AM_MAKEFLAGS) $@) || exit 1 diff --git a/configure.ac b/configure.ac index 05e3bac8e..fae1ec329 100644 --- a/configure.ac +++ b/configure.ac @@ -491,6 +491,9 @@ AC_MSG_RESULT([$enable_assertions]) if test "$enable_assertions" = yes; then CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS" +else + # turn off regular C assert() also + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DNDEBUG" fi AC_MSG_CHECKING([whether to do a traceable build of CVC4]) 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"); } diff --git a/test/Makefile.am b/test/Makefile.am index e370752b6..98e1c8b86 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -2,15 +2,15 @@ SUBDIRS = unit system regress . MAKEFLAGS = -k -.PHONY: units regress regress0 regress1 regress2 regress3 -units regress regress0 regress1 regress2 regress3: +.PHONY: units systemtests regress regress0 regress1 regress2 regress3 +units systemtests regress regress0 regress1 regress2 regress3: @$(MAKE) check-pre; \ for dir in $(SUBDIRS); do \ test $$dir = . || (cd $$dir && $(MAKE) $(AM_MAKEFLAGS) $@); \ done; \ $(MAKE) check-local -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: test test: check @@ -37,6 +37,9 @@ check-local: if test -s "unit/test-suite.log"; then :; else \ echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \ fi; \ + if test -s "system/test-suite.log"; then :; else \ + echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \ + fi; \ for dir in $(subdirs_to_check); do \ log=$$dir/test-suite.log; \ if test -s "$$log"; then \ diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 3867ee860..37f474cfc 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -12,13 +12,13 @@ regress3: regress0 regress1 regress2 regress0 regress1 regress2 regress3: -cd $@ && $(MAKE) check -# synonyms for "check" +# synonyms for "checK" in this directory in this directory .PHONY: regress test regress test: check # no-ops here -.PHONY: units -units: +.PHONY: units systemtests +units systemtests: EXTRA_DIST = \ run_regression \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 37020d48e..dbc493678 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -84,7 +84,6 @@ BUG_TESTS = \ bug167.smt \ bug168.smt \ bug187.smt2 \ - bug216.smt2 \ bug220.smt2 \ bug239.smt \ buggy-ite.smt2 @@ -92,6 +91,7 @@ BUG_TESTS = \ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) \ + bug216.smt2 \ bug216.smt2.expect if CVC4_BUILD_PROFILE_COMPETITION @@ -104,7 +104,7 @@ endif EXTRA_DIST += \ error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index aca076d9f..83078c177 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -23,7 +23,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index e204a29b5..19d458403 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -41,7 +41,7 @@ TESTS = \ equality-00.smt \ equality-01.smt \ equality-02.smt \ - equality-05.smt \ + equality-05.smt \ bv_eq_diamond10.smt \ slice-01.smt \ slice-02.smt \ @@ -67,13 +67,13 @@ TESTS = \ a78test0002.smt \ a95test0002.smt \ bitvec0.smt \ - bitvec2.smt \ + bitvec2.smt + +EXTRA_DIST = $(TESTS) \ bitvec3.smt \ - bitvec5.smt - -EXTRA_DIST = $(TESTS) + bitvec5.smt -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index bc99f81af..65a009aa2 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -21,7 +21,7 @@ TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) EXTRA_DIST = $(TESTS) -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 88defc40b..36de2ceb3 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -35,7 +35,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index ee365e79d..223f2f9ee 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -9,14 +9,14 @@ MAKEFLAGS = -k # Regression tests for SMT inputs CVC_TESTS = \ - test.00.cvc \ - test.01.cvc + test.00.cvc TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -EXTRA_DIST = $(TESTS) +EXTRA_DIST = $(TESTS) \ + test.01.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 2e05386e0..06f45bca2 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -41,7 +41,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 3ebd95257..2f81b04eb 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -27,7 +27,7 @@ BUG_TESTS = TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 10fe5f01a..d58debe82 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -26,7 +26,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress1 test regress regress1 test: check diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am index 4bdff93d1..e23579fc7 100644 --- a/test/regress/regress1/arith/Makefile.am +++ b/test/regress/regress1/arith/Makefile.am @@ -12,7 +12,7 @@ TESTS = \ EXTRA_DIST = $(TESTS) -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress1 test regress regress1 test: check diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 28a814274..77d9ef158 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -36,7 +36,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress2 test regress regress2 test: check diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index fca3c4ef8..ada9664d3 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -25,7 +25,7 @@ EXTRA_DIST = $(TESTS) #EXTRA_DIST += \ # error.cvc -# synonyms for "check" +# synonyms for "checK" in this directory .PHONY: regress regress3 test regress regress3 test: check diff --git a/test/system/Makefile.am b/test/system/Makefile.am index 954798e6c..7e0192340 100644 --- a/test/system/Makefile.am +++ b/test/system/Makefile.am @@ -1,5 +1,7 @@ TESTS_ENVIRONMENT = -TESTS = +TESTS = \ + boilerplate \ + ouroborous # Things that aren't tests but that tests rely on and need to # go into the distribution @@ -28,20 +30,43 @@ else system_LINK = $(CXXLINK) endif +AM_CPPFLAGS = \ + -I. \ + "-I@top_srcdir@/src/include" \ + "-I@top_srcdir@/lib" \ + "-I@top_srcdir@/src" \ + "-I@top_builddir@/src" \ + "-I@top_srcdir@/src/prop/minisat" \ + -D __STDC_LIMIT_MACROS \ + -D __STDC_FORMAT_MACROS \ + $(TEST_CPPFLAGS) +LIBADD = \ + @abs_top_builddir@/src/parser/libcvc4parser.la \ + @abs_top_builddir@/src/libcvc4.la + # WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS: -# system_test: system_test.cpp -# $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@.lo $< -# $(AM_V_CXXLD)$(system_LINK) $(AM_LDFLAGS) $@.lo +$(TESTS:%=%.lo): %.lo: %.cpp + $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+ +$(TESTS): %: %.lo $(LIBADD) + $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $< + +# trick automake into setting LTCXXCOMPILE, CXXLINK, etc. +if CVC4_FALSE +noinst_LTLIBRARIES = libdummy.la +nodist_libdummy_la_SOURCES = ouroborous.cpp +libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la +endif # rebuild tests if a library changes -$(TESTS):: $(TEST_DEPS) +#$(TESTS):: $(TEST_DEPS) +MAKEFLAGS = -k export VERBOSE = 1 -# synonyms for "check" -.PHONY: test -test: check +# synonyms for "checK" in this directory in this directory +.PHONY: test systemtests +test systemtests: check # no-ops here -.PHONY: units regress regress0 regress1 regress2 regress3s +.PHONY: units regress regress0 regress1 regress2 regress3 units regress regress0 regress1 regress2 regress3: diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp new file mode 100644 index 000000000..89d5174e3 --- /dev/null +++ b/test/system/boilerplate.cpp @@ -0,0 +1,38 @@ +/********************* */ +/*! \file boilerplate.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief A simple start-up/tear-down test for CVC4. + ** + ** This simple test just makes sure that the public interface is + ** minimally functional. It is useful as a template to use for other + ** system tests. + **/ + +#include <iostream> +#include <sstream> + +#include "expr/expr.h" +#include "smt/smt_engine.h" + +using namespace CVC4; +using namespace std; + +int main() { + ExprManager em; + Options opts; + SmtEngine smt(&em, opts); + Result r = smt.query(em.mkConst(true)); + + return r == Result::VALID ? 0 : 1; +} + diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp new file mode 100644 index 000000000..4473b42bb --- /dev/null +++ b/test/system/ouroborous.cpp @@ -0,0 +1,103 @@ +/********************* */ +/*! \file ouroborous.cpp + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** 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 + ** information.\endverbatim + ** + ** \brief "Ouroborous" test: does CVC4 read its own output? + ** + ** The "Ouroborous" test, named after the serpent that swallows its own + ** tail, ensures that CVC4 can parse some input, output it again (in any + ** of its languages) and then parse it again. The result of the first + ** parse must be equal to the result of the second parse (up to renaming + ** variables), or the test fails. + **/ + +#include <iostream> +#include <sstream> +#include <string> + +#include "expr/expr.h" +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" + +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::language; +using namespace std; + +const string declarations = "\ +(declare-sort U 0)\n\ +(declare-fun f (U) U)\n\ +(declare-fun x () U)\n\ +(declare-fun y () U)\n\ +(assert (= (f x) x))\n\ +"; + +int runTest(); + +int main() { + try { + return runTest(); + } catch(Exception& e) { + cerr << e << endl; + } catch(...) { + cerr << "non-cvc4 exception thrown." << endl; + } + return 1; +} + +string translate(Parser* parser, string in, InputLanguage inlang, OutputLanguage outlang) { + cout << "==============================================" << endl + << "translating from " << inlang << " to " << outlang << " this string:" << endl + << in << endl; + parser->setInput(Input::newStringInput(inlang, in, "internal-buffer")); + stringstream ss; + ss << Expr::setlanguage(outlang) << parser->nextExpression(); + AlwaysAssert(parser->nextExpression().isNull(), "next expr should be null"); + AlwaysAssert(parser->done(), "parser should be done"); + string s = ss.str(); + cout << "got this:" << endl + << s << endl + << "==============================================" << endl; + return s; +} + +int runTest() { + ExprManager em; + Parser* parser = + ParserBuilder(em, "internal-buffer") + .withStringInput(declarations) + .withInputLanguage(input::LANG_SMTLIB_V2) + .build(); + + // we don't need to execute them, but we DO need to parse them to + // get the declarations + while(Command* c = parser->nextCommand()) { + delete c; + } + + AlwaysAssert(parser->done(), "parser should be done"); + + string instr = "(= (f (f y)) x)"; + string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2); + string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB); + //string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4); + //string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2); + string out = smt1; + + AlwaysAssert(out == smt2, "differences in output"); + + delete parser; + + return 0; +} + diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 725d4a4bb..eb70935e7 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -172,7 +172,7 @@ nodist_libdummy_la_SOURCES = expr/node_black.cpp libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la endif -# synonyms for "check" +# synonyms for "checK" in this directory in this directory .PHONY: units test units test: check diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index a121029f3..3dbee87eb 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -26,6 +26,7 @@ #include "expr/node_manager.h" #include "expr/attribute.h" #include "expr/node.h" +#include "theory/theory.h" #include "theory/theory_engine.h" #include "theory/uf/theory_uf.h" #include "util/Assert.h" @@ -108,17 +109,11 @@ public: //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId); lastId = attr::LastAttributeId<bool, false>::s_id; - TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag1::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag2::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag3::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag4::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag5::s_id, lastId); - TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag1::s_id); - TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag2::s_id); - TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag3::s_id); - TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag4::s_id); - TS_ASSERT_DIFFERS(theory::Theory::PreRegisteredAttr::s_id, TestFlag5::s_id); TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag2::s_id); TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag3::s_id); TS_ASSERT_DIFFERS(TestFlag1::s_id, TestFlag4::s_id); @@ -131,12 +126,15 @@ public: TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id); lastId = attr::LastAttributeId<bool, true>::s_id; -// TS_ASSERT_LESS_THAN(TheoryEngine::RegisteredAttr::s_id, lastId); + TS_ASSERT_LESS_THAN(theory::Asserted::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId); TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId); -// TS_ASSERT_DIFFERS(TheoryEngine::RegisteredAttr::s_id, TestFlag1cd::s_id); -// TS_ASSERT_DIFFERS(TheoryEngine::RegisteredAttr::s_id, TestFlag2cd::s_id); + TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag1cd::s_id); + TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag2cd::s_id); TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id); + cout << "A: " << theory::Asserted::s_id << endl; + cout << "1: " << TestFlag1cd::s_id << endl; + cout << "2: " << TestFlag2cd::s_id << endl; lastId = attr::LastAttributeId<Node, false>::s_id; // TS_ASSERT_LESS_THAN(theory::PreRewriteCache::s_id, lastId); @@ -156,27 +154,27 @@ public: } void testCDAttributes() { - //Debug.on("boolattr"); + //Debug.on("cdboolattr"); Node a = d_nm->mkVar(*d_booleanType); Node b = d_nm->mkVar(*d_booleanType); Node c = d_nm->mkVar(*d_booleanType); - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr", "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"); + Debug("cdboolattr", "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"); + Debug("cdboolattr", "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"); + Debug("cdboolattr", "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"); + Debug("cdboolattr", "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"); + Debug("cdboolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); // test that they all HAVE the boolean attributes @@ -186,96 +184,96 @@ public: // test two-arg version of hasAttribute() bool bb = false; - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdboolattr", "get flag 1 on a (should be F)\n"); TS_ASSERT(a.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on b (should be F)\n"); + Debug("cdboolattr", "get flag 1 on b (should be F)\n"); TS_ASSERT(b.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); - Debug("boolattr", "get flag 1 on c (should be F)\n"); + Debug("cdboolattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(c.getAttribute(TestFlag1cd(), bb)); TS_ASSERT(! bb); // setting boolean flags - Debug("boolattr", "set flag 1 on a to T\n"); + Debug("cdboolattr", "set flag 1 on a to T\n"); a.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "set flag 1 on b to F\n"); + Debug("cdboolattr", "set flag 1 on b to F\n"); b.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on c to F\n"); + Debug("cdboolattr", "set flag 1 on c to F\n"); c.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "get flag 1 on a (should be T)\n"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); - Debug("boolattr", "set flag 1 on a to F\n"); + Debug("cdbootattr", "set flag 1 on a to F\n"); a.setAttribute(TestFlag1cd(), false); - Debug("boolattr", "set flag 1 on b to T\n"); + Debug("cdbootattr", "set flag 1 on b to T\n"); b.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); - Debug("boolattr", "set flag 1 on c to T\n"); + Debug("cdbootattr", "set flag 1 on c to T\n"); c.setAttribute(TestFlag1cd(), true); - Debug("boolattr", "get flag 1 on a (should be F)\n"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "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"); + Debug("cdbootattr", "get flag 1 on c (should be F)\n"); TS_ASSERT(! c.getAttribute(TestFlag1cd())); #ifdef CVC4_ASSERTIONS @@ -284,7 +282,7 @@ public: } void testAttributes() { - //Debug.on("boolattr"); + //Debug.on("bootattr"); Node a = d_nm->mkVar(*d_booleanType); Node b = d_nm->mkVar(*d_booleanType); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 4aee8060f..9de8f94b4 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -96,7 +96,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_arith = new TheoryArith(d_ctxt, d_outputChannel); + d_arith = new TheoryArith(d_ctxt, d_outputChannel, Valuation(NULL)); preregistered = new std::set<Node>(); diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index 18408acd3..a362a597c 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -104,8 +104,8 @@ public: set<Node> d_registered; vector<Node> d_getSequence; - DummyTheory(Context* ctxt, OutputChannel& out) : - Theory(theory::THEORY_BUILTIN, ctxt, out) { + DummyTheory(Context* ctxt, OutputChannel& out, Valuation valuation) : + Theory(theory::THEORY_BUILTIN, ctxt, out, valuation) { } void registerTerm(TNode n) { @@ -142,7 +142,7 @@ public: void preRegisterTerm(TNode n) {} void propagate(Effort level) {} void explain(TNode n, Effort level) {} - Node getValue(TNode n, Valuation* valuation) { return Node::null(); } + Node getValue(TNode n) { return Node::null(); } string identify() const { return "DummyTheory"; } }; @@ -165,7 +165,7 @@ public: d_ctxt = new Context; d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); - d_dummy = new DummyTheory(d_ctxt, d_outputChannel); + d_dummy = new DummyTheory(d_ctxt, d_outputChannel, Valuation(NULL)); d_outputChannel.clear(); atom0 = d_nm->mkConst(true); atom1 = d_nm->mkConst(false); diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 5915ac1f7..f99698204 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -107,8 +107,8 @@ class FakeTheory : public Theory { // static std::deque<RewriteItem> s_expected; public: - FakeTheory(context::Context* ctxt, OutputChannel& out) : - Theory(theoryId, ctxt, out) + FakeTheory(context::Context* ctxt, OutputChannel& out, Valuation valuation) : + Theory(theoryId, ctxt, out, valuation) { } /** Register an expected rewrite call */ @@ -212,7 +212,7 @@ public: void check(Theory::Effort) { Unimplemented(); } void propagate(Theory::Effort) { Unimplemented(); } void explain(TNode, Theory::Effort) { Unimplemented(); } - Node getValue(TNode n, Valuation* valuation) { return Node::null(); } + Node getValue(TNode n) { return Node::null(); } };/* class FakeTheory */ diff --git a/test/unit/theory/theory_uf_tim_white.h b/test/unit/theory/theory_uf_tim_white.h index 19b289ae7..1940bc199 100644 --- a/test/unit/theory/theory_uf_tim_white.h +++ b/test/unit/theory/theory_uf_tim_white.h @@ -61,7 +61,7 @@ public: d_nm = new NodeManager(d_ctxt); d_scope = new NodeManagerScope(d_nm); d_outputChannel.clear(); - d_euf = new TheoryUFTim(d_ctxt, d_outputChannel); + d_euf = new TheoryUFTim(d_ctxt, d_outputChannel, Valuation(NULL)); d_booleanType = new TypeNode(d_nm->booleanType()); } |