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
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])
#include <memory>
namespace __gnu_cxx {
- template <class Key> class hash;
+ template <class Key> struct hash;
}/* __gnu_cxx namespace */
namespace CVC4 {
#define __CVC4__CONTEXT__CDMAP_FORWARD_H
namespace __gnu_cxx {
- template <class Key> class hash;
+ template <class Key> struct hash;
}/* __gnu_cxx namespace */
namespace CVC4 {
#define __CVC4__CONTEXT__CDSET_FORWARD_H
namespace __gnu_cxx {
- template <class Key> class hash;
+ template <class Key> struct hash;
}/* __gnu_cxx namespace */
namespace CVC4 {
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
::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 */
/**
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);
deleteAllFromTable(d_strings);
deleteAllFromTable(d_ptrs);
- // FIXME CD-bools in optimized table
d_cdbools.clear();
d_cdints.clear();
d_cdtnodes.clear();
d_cdptrs.clear();
}
-
}/* CVC4::expr::attr namespace */
}/* CVC4::expr namespace */
}/* CVC4 namespace */
* 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
operator bool() const {
return (d_word & (1 << d_bit)) ? true : false;
}
- };
+ };/* class AttrHash<bool>::BitAccessor */
/**
* A (somewhat degenerate) iterator over boolean-valued attributes.
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
bool operator==(const ConstBitIterator& b) {
return d_entry == b.d_entry && d_bit == b.d_bit;
}
- };
+ };/* class AttrHash<bool>::ConstBitIterator */
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 */
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";
}
try {
smtEngine->setLogic(d_logic);
//d_result = "success";
- } catch(ModalException& m) {
+ } catch(ModalException&) {
d_result = "error";
}
}
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";
}
}
stringstream ss;
ss << smtEngine->getInfo(d_flag);
d_result = ss.str();
- } catch(BadOptionException& bo) {
+ } catch(BadOptionException&) {
d_result = "unsupported";
}
}
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";
}
}
void GetOptionCommand::invoke(SmtEngine* smtEngine) {
try {
d_result = smtEngine->getOption(d_flag).getValue();
- } catch(BadOptionException& bo) {
+ } catch(BadOptionException&) {
d_result = "unsupported";
}
}
** 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>
}/* CVC4 namespace */
-#endif /* DECLARATION_SCOPE_H */
+#endif /* __CVC4__DECLARATION_SCOPE_H */
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) {
/** 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. */
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) {
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) {
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) {
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))));
}
/**
class Expr;
class SmtEngine;
class NodeManager;
-class Options;
+struct Options;
class IntStat;
namespace context {
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();
}
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();
}
namespace CVC4 {
-class Options;
+struct Options;
namespace expr {
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:
** OS X).
**/
+#include "cvc4_private.h"
+
#include <stdio.h>
#include <errno.h>
#include <time.h>
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:
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+
** 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
@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
@init {
Debug("parser") << "term: " << AntlrInput::tokenText(LT(1)) << std::endl;
Kind kind;
+ Expr op;
std::string name;
std::vector<Expr> args;
SExpr sexpr;
| /* 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
// 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.
| 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
;
@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" ) {
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';
ATTRIBUTE_TOK : '!';
LPAREN_TOK : '(';
RPAREN_TOK : ')';
+INDEX_TOK : '_';
SET_LOGIC_TOK : 'set-logic';
SET_INFO_TOK : 'set-info';
GET_INFO_TOK : 'get-info';
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
/** 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
;
/**
/**
* Matches a hexadecimal constant.
*/
- HEX_LITERAL
+HEX_LITERAL
: '#x' HEX_DIGIT+
;
/**
* Matches a binary constant.
*/
- BINARY_LITERAL
+BINARY_LITERAL
: '#b' ('0' | '1')+
;
: ';' (~('\n' | '\r'))* { SKIP(); }
;
-
/**
* Matches any letter ('a'-'z' and 'A'-'Z').
*/
/**
* 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.
*/
addArithmeticOperators();
break;
+ case THEORY_BITVECTORS:
+ break;
+
default:
Unhandled(theory);
}
addOperator(kind::APPLY_UF);
break;
+ case Smt::QF_BV:
+ addTheory(THEORY_BITVECTORS);
+ break;
+
case Smt::AUFLIA:
case Smt::AUFLIRA:
case Smt::AUFNIRA:
case Smt::UFNIA:
case Smt::QF_AUFBV:
case Smt::QF_AUFLIA:
- case Smt::QF_BV:
Unhandled(name);
}
}
} else {
out << "(...)";
}
+ if(n.getNumChildren() > 0) {
+ out << ' ';
+ }
}
for(TNode::iterator i = n.begin(),
iend = n.end();
-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 = \
/** 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;
/**
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),
}
}
-Node TheoryArith::getValue(TNode n, Valuation* valuation) {
+Node TheoryArith::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
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);
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);
iend = n.end();
i != iend;
++i) {
- value += valuation->getValue(*i).getConst<Rational>();
+ value += d_valuation.getValue(*i).getConst<Rational>();
}
return nodeManager->mkConst(value);
}
iend = n.end();
i != iend;
++i) {
- value *= valuation->getValue(*i).getConst<Rational>();
+ value *= d_valuation.getValue(*i).getConst<Rational>();
}
return nodeManager->mkConst(value);
}
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());
SimplexDecisionProcedure d_simplex;
public:
- TheoryArith(context::Context* c, OutputChannel& out);
+ TheoryArith(context::Context* c, OutputChannel& out, Valuation valuation);
~TheoryArith();
/**
void notifyEq(TNode lhs, TNode rhs);
- Node getValue(TNode n, Valuation* valuation);
+ Node getValue(TNode n);
void shutdown(){ }
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)
{
}
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()) {
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());
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) { }
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 */
namespace theory {
namespace booleans {
-Node TheoryBool::getValue(TNode n, Valuation* valuation) {
+Node TheoryBool::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
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);
}
}
}
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);
}
}
}
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());
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) {
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"); }
};
namespace theory {
namespace builtin {
-Node TheoryBuiltin::getValue(TNode n, Valuation* valuation) {
+Node TheoryBuiltin::getValue(TNode n) {
switch(n.getKind()) {
case kind::VARIABLE:
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
iend = n.end();
i != iend;
++i) {
- nb << valuation->getValue(*i);
+ nb << d_valuation.getValue(*i);
}
return Node(nb);
}
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 */
return true;
}
-Node TheoryBV::getValue(TNode n, Valuation* valuation) {
+Node TheoryBV::getValue(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
switch(n.getKind()) {
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());
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() {
void explain(TNode n);
- Node getValue(TNode n, Valuation* valuation);
+ Node getValue(TNode n);
std::string identify() const { return std::string("TheoryBV"); }
};/* class TheoryBV */
namespace theory {
namespace bv {
-class AllRewriteRules;
+struct AllRewriteRules;
class TheoryBVRewriter {
#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"
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).
/**
* 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
*/
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
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) {
* 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();
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 */
d_theoryRegistration(opts.theoryRegistration),
d_hasShutDown(false),
d_incomplete(ctxt, false),
- d_valuation(this),
d_opts(opts),
d_statistics() {
}
// 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() {
*/
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.
*/
*/
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));
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;
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),
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()) {
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());
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();
* 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"); }
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 */
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),
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
* 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");
}
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
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 \
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 \
bug167.smt \
bug168.smt \
bug187.smt2 \
- bug216.smt2 \
bug220.smt2 \
bug239.smt \
buggy-ite.smt2
TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS)
EXTRA_DIST = $(TESTS) \
+ bug216.smt2 \
bug216.smt2.expect
if CVC4_BUILD_PROFILE_COMPETITION
EXTRA_DIST += \
error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress0 test
regress regress0 test: check
#EXTRA_DIST += \
# error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress0 test
regress regress0 test: check
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 \
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
EXTRA_DIST = $(TESTS)
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress0 test
regress regress0 test: check
#EXTRA_DIST += \
# error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress0 test
regress regress0 test: check
# 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
#EXTRA_DIST += \
# error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress0 test
regress regress0 test: check
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
#EXTRA_DIST += \
# error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress1 test
regress regress1 test: check
EXTRA_DIST = $(TESTS)
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress1 test
regress regress1 test: check
#EXTRA_DIST += \
# error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress2 test
regress regress2 test: check
#EXTRA_DIST += \
# error.cvc
-# synonyms for "check"
+# synonyms for "checK" in this directory
.PHONY: regress regress3 test
regress regress3 test: check
TESTS_ENVIRONMENT =
-TESTS =
+TESTS = \
+ boilerplate \
+ ouroborous
# Things that aren't tests but that tests rely on and need to
# go into the distribution
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:
--- /dev/null
+/********************* */
+/*! \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;
+}
+
--- /dev/null
+/********************* */
+/*! \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;
+}
+
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
#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"
//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);
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);
}
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
// 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
}
void testAttributes() {
- //Debug.on("boolattr");
+ //Debug.on("bootattr");
Node a = d_nm->mkVar(*d_booleanType);
Node b = d_nm->mkVar(*d_booleanType);
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>();
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) {
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"; }
};
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);
// 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 */
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 */
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());
}
projects / cvc5.git / commitdiff