ExplainOutputChannel. Safer and stops a compiler warning.
* node attributes: fix compiler warnings on 64-bit.
* Node: add asserts to make sure the current NodeManager is non-NULL
when it's needed. This can happen when public-facing functions
don't properly set the node manager, and it can look like a bug in
another part of the library. Also some code format cleanup.
* configure.ac, config/cvc4.m4: added --enable-static-binary (see
discussion on bug 32), fixed bad configure lines (bug 19), added
documentation for some things.
* config.h.in: removed; it's auto-generated.
+++ /dev/null
-/* config.h.in. Generated from configure.ac by autoheader. */
-
-/* Major component of the version of CVC4. */
-#undef CVC4_MAJOR
-
-/* Minor component of the version of CVC4. */
-#undef CVC4_MINOR
-
-/* Release component of the version of CVC4. */
-#undef CVC4_RELEASE
-
-/* Full release string for CVC4. */
-#undef CVC4_RELEASE_STRING
-
-/* Define to 1 if you have the <dlfcn.h> header file. */
-#undef HAVE_DLFCN_H
-
-/* Define to 1 if you have the <getopt.h> header file. */
-#undef HAVE_GETOPT_H
-
-/* Define to 1 if you have the <inttypes.h> header file. */
-#undef HAVE_INTTYPES_H
-
-/* Define to 1 if you have the `gmp' library (-lgmp). */
-#undef HAVE_LIBGMP
-
-/* Define to 1 if you have the <memory.h> header file. */
-#undef HAVE_MEMORY_H
-
-/* Define to 1 if stdbool.h conforms to C99. */
-#undef HAVE_STDBOOL_H
-
-/* Define to 1 if you have the <stdint.h> header file. */
-#undef HAVE_STDINT_H
-
-/* Define to 1 if you have the <stdlib.h> header file. */
-#undef HAVE_STDLIB_H
-
-/* Define to 1 if you have the <strings.h> header file. */
-#undef HAVE_STRINGS_H
-
-/* Define to 1 if you have the <string.h> header file. */
-#undef HAVE_STRING_H
-
-/* Define to 1 if you have the <sys/stat.h> header file. */
-#undef HAVE_SYS_STAT_H
-
-/* Define to 1 if you have the <sys/types.h> header file. */
-#undef HAVE_SYS_TYPES_H
-
-/* Define to 1 if you have the <unistd.h> header file. */
-#undef HAVE_UNISTD_H
-
-/* Define to 1 if the system has the type `_Bool'. */
-#undef HAVE__BOOL
-
-/* Define to the sub-directory in which libtool stores uninstalled libraries.
- */
-#undef LT_OBJDIR
-
-/* Name of package */
-#undef PACKAGE
-
-/* Define to the address where bug reports for this package should be sent. */
-#undef PACKAGE_BUGREPORT
-
-/* Define to the full name of this package. */
-#undef PACKAGE_NAME
-
-/* Define to the full name and version of this package. */
-#undef PACKAGE_STRING
-
-/* Define to the one symbol short name of this package. */
-#undef PACKAGE_TARNAME
-
-/* Define to the home page for this package. */
-#undef PACKAGE_URL
-
-/* Define to the version of this package. */
-#undef PACKAGE_VERSION
-
-/* Define to 1 if you have the ANSI C header files. */
-#undef STDC_HEADERS
-
-/* Version number of package */
-#undef VERSION
-
-/* Define for Solaris 2.5.1 so the uint32_t typedef from <sys/synch.h>,
- <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
- #define below would cause a syntax error. */
-#undef _UINT32_T
-
-/* Define for Solaris 2.5.1 so the uint64_t typedef from <sys/synch.h>,
- <pthread.h>, or <semaphore.h> is not used. If the typedef were allowed, the
- #define below would cause a syntax error. */
-#undef _UINT64_T
-
-/* Define to `unsigned int' if <sys/types.h> does not define. */
-#undef size_t
-
-/* Define to the type of an unsigned integer type of width exactly 16 bits if
- such a type exists and the standard includes do not define it. */
-#undef uint16_t
-
-/* Define to the type of an unsigned integer type of width exactly 32 bits if
- such a type exists and the standard includes do not define it. */
-#undef uint32_t
-
-/* Define to the type of an unsigned integer type of width exactly 64 bits if
- such a type exists and the standard includes do not define it. */
-#undef uint64_t
do
case $ac_option in
-*|*=*) ;;
- *) ac_cvc4_build_profile_set=yes
+ production|debug|default|competition)
+ ac_cvc4_build_profile_set=yes
AC_MSG_NOTICE([CVC4: building profile $ac_option])
ac_option="--with-build=$ac_option" ;;
esac
dnl Preprocess CL args. Defined in config/cvc4.m4
CVC4_AC_INIT
-AC_PREREQ(2.64)
+AC_PREREQ(2.61)
AC_INIT
AC_CONFIG_SRCDIR([src/include/cvc4_config.h])
AC_CONFIG_AUX_DIR([config])
#
# For more information, see:
# http://www.gnu.org/software/libtool/manual/libtool.html#Versioning
-# For guidance on when to change the version number, refer to the
+# For guidance on when to change the version number, refer to the
# developer's guide.
CVC4_LIBRARY_VERSION=$CVC4_MAJOR:$CVC4_MINOR:$CVC4_RELEASE
;;
esac
+# permit a static binary
+AC_MSG_CHECKING([whether to build a static binary])
+AC_ARG_ENABLE([static-binary],
+ [AS_HELP_STRING([--enable-static-binary],
+ [build a statically-linked binary [default=no]])])
+if test -z "${enable_static_binary+set}"; then
+ enable_static_binary=no
+fi
+AC_MSG_RESULT([$enable_static_binary])
+if test "${enable_static_binary}" = yes -a "${enable_static}" != yes; then
+ enable_static=yes
+ AC_MSG_WARN([forcing static-library building, --enable-static-binary given])
+fi
+
AC_MSG_CHECKING([whether to optimize libcvc4])
AC_ARG_ENABLE([optimized],
- [AS_HELP_STRING([--enable-optimized],
+ [AS_HELP_STRING([--enable-optimized],
[optimize the build])])
if test -z "${enable_optimized+set}"; then
AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
-AC_ARG_ENABLE([debug-symbols],
- [AS_HELP_STRING([--disable-debug-symbols],
+AC_ARG_ENABLE([debug-symbols],
+ [AS_HELP_STRING([--disable-debug-symbols],
[do not include debug symbols in libcvc4])])
if test -z "${enable_debug_symbols+set}"; then
AC_MSG_CHECKING([whether to include assertions in build])
-AC_ARG_ENABLE([assertions],
- [AS_HELP_STRING([--disable-assertions],
+AC_ARG_ENABLE([assertions],
+ [AS_HELP_STRING([--disable-assertions],
[turn off assertions in build])])
if test -z "${enable_assertions+set}"; then
fi
AC_MSG_CHECKING([whether to do a traceable build of CVC4])
-AC_ARG_ENABLE([tracing],
- [AS_HELP_STRING([--disable-tracing],
+AC_ARG_ENABLE([tracing],
+ [AS_HELP_STRING([--disable-tracing],
[remove all tracing code from CVC4])])
if test -z "${enable_tracing+set}"; then
fi
AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
-AC_ARG_ENABLE([muzzle],
- [AS_HELP_STRING([--enable-muzzle],
+AC_ARG_ENABLE([muzzle],
+ [AS_HELP_STRING([--enable-muzzle],
[completely silence CVC4; remove ALL non-result output from build])])
if test -z "${enable_muzzle+set}"; then
fi
AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
-AC_ARG_ENABLE([coverage],
- [AS_HELP_STRING([--enable-coverage],
+AC_ARG_ENABLE([coverage],
+ [AS_HELP_STRING([--enable-coverage],
[build with support for gcov coverage testing])])
if test -z "${enable_coverage+set}"; then
AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
-AC_ARG_ENABLE([profiling],
- [AS_HELP_STRING([--enable-profiling],
+AC_ARG_ENABLE([profiling],
+ [AS_HELP_STRING([--enable-profiling],
[build with support for gprof profiling])])
if test -z "${enable_profiling+set}"; then
DX_DOT_FEATURE(OFF)
DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
+AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
+
AC_SUBST([CXXTEST])
-AC_ARG_WITH([cxxtest-dir],
+AC_ARG_WITH([cxxtest-dir],
[AS_HELP_STRING([--with-cxxtest-dir=DIR], [path to CxxTest installation])],
[CXXTEST="$withval"])
AC_CHECK_HEADERS([getopt.h unistd.h])
# Checks for typedefs, structures, and compiler characteristics.
-AC_HEADER_STDBOOL
+#AC_HEADER_STDBOOL
AC_TYPE_UINT16_T
AC_TYPE_UINT32_T
AC_TYPE_UINT64_T
if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
AC_SUBST(BUILDING_SHARED)
AC_SUBST(BUILDING_STATIC)
-AM_CONDITIONAL([STATIC_BINARY], [test "$enable_shared" != yes -a "$enable_static" = yes])
+AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
AC_SUBST(CVC4_LIBRARY_VERSION)
AC_SUBST(CVC4_PARSER_LIBRARY_VERSION)
gprof support: $enable_profiling
unit tests : $support_unit_tests
+static libs : $enable_static
+shared libs : $enable_shared
+static binary: $enable_static_binary
+
CPPFLAGS : $CPPFLAGS
CXXFLAGS : $CXXFLAGS
LDFLAGS : $LDFLAGS
struct AttrHashFcn {
enum { LARGE_PRIME = 1 };
- std::size_t operator()(const std::pair<unsigned, SoftNode>& p) const {
+ std::size_t operator()(const std::pair<uint64_t, SoftNode>& p) const {
return p.first * LARGE_PRIME + p.second.hash();
}
};
// use a TAG to indicate which table it should be in
template <class value_type>
-struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
+struct AttrHash : public __gnu_cxx::hash_map<std::pair<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
template <>
class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
public:
- typedef std::pair<unsigned, SoftNode> key_type;
+ typedef std::pair<uint64_t, SoftNode> key_type;
typedef bool data_type;
typedef std::pair<const key_type, data_type> value_type;
typedef BitIterator iterator;
typedef ConstBitIterator const_iterator;
- BitIterator find(const std::pair<unsigned, SoftNode>& k) {
+ BitIterator find(const std::pair<uint64_t, SoftNode>& k) {
super::iterator i = super::find(k.second);
if(i == super::end()) {
return BitIterator();
}
- Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
+ Debug.printf("boolattr",
+ "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);
}
return BitIterator();
}
- ConstBitIterator find(const std::pair<unsigned, SoftNode>& k) const {
+ ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
super::const_iterator i = super::find(k.second);
if(i == super::end()) {
return ConstBitIterator();
}
- Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
+ Debug.printf("boolattr",
+ "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
+ &(*i).second,
+ (unsigned long long)((*i).second),
+ unsigned(k.first));
return ConstBitIterator(*i, k.first);
}
return ConstBitIterator();
}
- BitAccessor operator[](const std::pair<unsigned, SoftNode>& k) {
+ BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
uint64_t& word = super::operator[](k.second);
return BitAccessor(word, k.first);
}
/** cleanup routine when the Node goes away */
static inline void cleanup(const value_t&) {}
- static inline unsigned getId() { return s_id; }
- static inline unsigned getHashValue() { return s_hashValue; }
+ static inline uint64_t getId() { return s_id; }
+ static inline uint64_t getHashValue() { return s_hashValue; }
static const bool has_default_value = false;
private:
/** an id */
- static const unsigned s_id;
+ static const uint64_t s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static const unsigned s_hashValue;
+ static const uint64_t s_hashValue;
};
/**
/** cleanup routine when the Node goes away */
static inline void cleanup(const bool&) {}
- static inline unsigned getId() { return s_id; }
- static inline unsigned getHashValue() { return s_hashValue; }
+ static inline uint64_t getId() { return s_id; }
+ static inline uint64_t getHashValue() { return s_hashValue; }
static const bool has_default_value = true;
static const bool default_value = false;
- static inline unsigned checkID(unsigned id) {
+ static inline uint64_t checkID(uint64_t id) {
AlwaysAssert(id <= 63,
"Too many boolean node attributes registered during initialization !");
return id;
private:
/** a bit assignment */
- static const unsigned s_id;
+ static const uint64_t s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static const unsigned s_hashValue;
+ static const uint64_t s_hashValue;
};
// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
template <class T>
struct LastAttributeId {
- static unsigned s_id;
+ static uint64_t s_id;
};
template <class T>
- unsigned LastAttributeId<T>::s_id = 0;
+ uint64_t LastAttributeId<T>::s_id = 0;
}/* CVC4::expr::attr namespace */
typedef Attribute<attr::VarName, std::string> VarNameAttr;
// ATTRIBUTE IDENTIFIER ASSIGNMENT =============================================
template <class T, class value_t>
-const unsigned Attribute<T, value_t>::s_id =
+const uint64_t Attribute<T, value_t>::s_id =
attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
template <class T, class value_t>
-const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
template <class T>
-const unsigned Attribute<T, bool>::s_id =
+const uint64_t Attribute<T, bool>::s_id =
Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
template <class T>
-const unsigned Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
class AttributeManager;
}
Node Node::eqExpr(const Node& right) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
}
Node Node::notExpr() const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(NOT, *this);
}
Node Node::andExpr(const Node& right) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(AND, *this, right);
}
Node Node::orExpr(const Node& right) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(OR, *this, right);
}
Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
}
Node Node::iffExpr(const Node& right) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(IFF, *this, right);
}
Node Node::impExpr(const Node& right) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
}
Node Node::xorExpr(const Node& right) const {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->mkNode(XOR, *this, right);
}
-static void indent(ostream & o, int indent){
- for(int i=0; i < indent; i++)
+static void indent(ostream & o, int indent) {
+ for(int i=0; i < indent; i++) {
o << ' ';
+ }
}
void Node::printAst(ostream & o, int ind) const {
indent(o, ind);
o << '(';
o << getKind();
- if(getKind() == VARIABLE){
+ if(getKind() == VARIABLE) {
o << ' ' << getId();
-
- }else if(getNumChildren() >= 1){
- for(Node::iterator child = begin(); child != end(); ++child){
+ } else if(getNumChildren() >= 1) {
+ for(Node::iterator child = begin(); child != end(); ++child) {
o << endl;
(*child).printAst(o, ind + 1);
}
class Node {
friend class NodeValue;
- friend class SoftNode;
/** A convenient null-valued encapsulated pointer */
static Node s_null;
bool operator!=(const Node& e) const { return d_ev != e.d_ev; }
Node operator[](int i) const {
- Assert(i >= 0 && i < d_ev->d_nchildren);
+ Assert(i >= 0 && unsigned(i) < d_ev->d_nchildren);
return Node(d_ev->d_children[i]);
}
Node impExpr(const Node& right) const;
Node xorExpr(const Node& right) const;
+ /*
Node plusExpr(const Node& right) const;
Node uMinusExpr() const;
Node multExpr(const Node& right) const;
+ */
inline Kind getKind() const;
* @param indent number of spaces to indent the formula by.
*/
void printAst(std::ostream & o, int indent = 0) const;
-
+
private:
-
+
/**
* Pretty printer for use within gdb
* This is not intended to be used outside of gdb.
template <class AttrKind>
inline typename AttrKind::value_type Node::getAttribute(const AttrKind&) {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->getAttribute(*this, AttrKind());
}
template <class AttrKind>
inline bool Node::hasAttribute(const AttrKind&,
typename AttrKind::value_type* ret) {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
return NodeManager::currentNM()->hasAttribute(*this, AttrKind(), ret);
}
template <class AttrKind>
inline void Node::setAttribute(const AttrKind&,
const typename AttrKind::value_type& value) {
+ Assert( NodeManager::currentNM() != NULL,
+ "There is no current CVC4::NodeManager associated to this thread.\n"
+ "Perhaps a public-facing function is missing a NodeManagerScope ?" );
+
NodeManager::currentNM()->setAttribute(*this, AttrKind(), value);
}
*/
CnfStream(SatSolver* satSolver);
+ /**
+ * Destructs a CnfStream. This implementation does nothing, but we
+ * need a virtual destructor for safety in case subclasses have a
+ * destructor.
+ */
+ virtual ~CnfStream() {
+ }
+
/**
* Converts and asserts a formula.
* @param node node to convert and assert
class OutputChannel {
public:
+ /**
+ * Destructs an OutputChannel. This implementation does nothing,
+ * but we need a virtual destructor for safety in case subclasses
+ * have a destructor.
+ */
+ virtual ~OutputChannel() {
+ }
+
/**
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted.
class ExplainOutputChannel {
public:
+ /**
+ * Destructs an ExplainOutputChannel. This implementation does
+ * nothing, but we need a virtual destructor for safety in case
+ * subclasses have a destructor.
+ */
+ virtual ~ExplainOutputChannel() {
+ }
+
/**
* With safePoint(), the theory signals that it is at a safe point
* and can be interrupted. The default implementation never
static bool fullEffort(Effort e) { return e >= FULL_EFFORT; }
/**
- * Construct a theory.
+ * Construct a Theory.
*/
Theory() {
}
+ /**
+ * Destructs a Theory. This implementation does nothing, but we
+ * need a virtual destructor for safety in case subclasses have a
+ * destructor.
+ */
+ virtual ~Theory() {
+ }
+
/**
* Prepare for a Node.
*
projects / cvc5.git / commitdiff