diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-03-25 05:32:31 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-03-25 05:32:31 +0000 |
| commit | a2472774f053ed0ab98f1508ebb313466b0fe29a (patch) | |
| tree | 2241c713acff99b23b1b51cb33c8a7a63c5afac4 | |
| parent | ee36b95b8f722fe6501cc6ac635efd49ca673791 (diff) | |
This is a merge from the "theoryfixes+cdattrhash" branch. The changes
are somewhat disparate but belonged on the same branch because they were
held back from trunk all for the same reason (to keep the trunk stable
for furious bitvector development). Dejan has now given me the go-ahead
for a merge.
=========================================
THIS COMMIT CHANGES THE THEORY INTERFACE!
=========================================
Theory constructors are expected to take an additional "Valuation*"
parameter that each Theory should send along to the base class
constructor. The base class Theory keeps the Valuation* in a
d_valuation field for use by it and by its derived classes.
Theory::getValue() no longer takes a Valuation* (it is expected
to use d_valuation instead). This allows other theory functions
to take advantage of getValue() for debugging or heuristic
purposes.
TODO BEFORE MERGE TO TRUNK:
****implement BitIterator find() in CDAttrHash<bool>.
Specifically:
* Added QF_BV support for SMT-LIB v2.
* Two adjustments to the theory interface as requested by Tim King:
1. As described above.
2. Theories now have const access to the fact queue through base
class functions facts_begin() and facts_end(); useful for
debugging.
* Added an "Asserted" attribute so that theories can check if something
has been asserted or not (and therefore not propagate it). However, this
has been disabled for now, pending more data on the overhead of it, and
pending discussion at the 3/25/2011 meeting.
* Do not define NDEBUG in MiniSat in assertion-enabled builds (so
that MiniSat asserts are evaluated).
* As a result of the new MiniSat assertions, some --incremental
regressions had to be disabled; also, some bitvectors ?!!
* Bug 71 is resolved by adding a specialization for CDAttrHash<> in the
attribute package.
* Fixes for some warnings flagged by clang.
* System tests have arrived! So far mainly infrastructure for having
system tests, but there is a system test aimed at improving code
coverage of the printer package.
* Minor other adjustments to documentation and coding to be more
conformant to CVC4 policy.
Tests have been performed to demonstrate that these changes have no or
negligible effect on performance. In particular, changing the
CDAttrHash<> doesn't have any real effect on performance or memory right
now, since there is only one context-dependent boolean flag (as soon
as another is added, the effect is noticeable but probably still slight).
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()); } |