--- /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
-*|*=*) ;;
- production|debug|default|competition)
- ac_cvc4_build_profile_set=yes
+ *) 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.61)
+AC_PREREQ(2.64)
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_static_binary" = yes])
+AM_CONDITIONAL([STATIC_BINARY], [test "$enable_shared" != yes -a "$enable_static" = 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<uint64_t, SoftNode>& p) const {
+ std::size_t operator()(const std::pair<unsigned, 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<uint64_t, SoftNode>, value_type, AttrHashFcn> {};
+struct AttrHash : public __gnu_cxx::hash_map<std::pair<unsigned, SoftNode>, value_type, AttrHashFcn> {};
template <>
class AttrHash<bool> : protected __gnu_cxx::hash_map<SoftNode, uint64_t, AttrHashBoolFcn> {
public:
- typedef std::pair<uint64_t, SoftNode> key_type;
+ typedef std::pair<unsigned, 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<uint64_t, SoftNode>& k) {
+ BitIterator find(const std::pair<unsigned, 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,
- (unsigned long long)((*i).second),
- unsigned(k.first));
+ Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
return BitIterator(*i, k.first);
}
return BitIterator();
}
- ConstBitIterator find(const std::pair<uint64_t, SoftNode>& k) const {
+ ConstBitIterator find(const std::pair<unsigned, 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,
- (unsigned long long)((*i).second),
- unsigned(k.first));
+ Debug.printf("boolattr", "underlying word at 0x%p looks like 0x%016llx, bit is %u\n", &(*i).second, (*i).second, k.first);
return ConstBitIterator(*i, k.first);
}
return ConstBitIterator();
}
- BitAccessor operator[](const std::pair<uint64_t, SoftNode>& k) {
+ BitAccessor operator[](const std::pair<unsigned, 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 uint64_t getId() { return s_id; }
- static inline uint64_t getHashValue() { return s_hashValue; }
+ static inline unsigned getId() { return s_id; }
+ static inline unsigned getHashValue() { return s_hashValue; }
static const bool has_default_value = false;
private:
/** an id */
- static const uint64_t s_id;
+ static const unsigned s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static const uint64_t s_hashValue;
+ static const unsigned s_hashValue;
};
/**
/** cleanup routine when the Node goes away */
static inline void cleanup(const bool&) {}
- static inline uint64_t getId() { return s_id; }
- static inline uint64_t getHashValue() { return s_hashValue; }
+ static inline unsigned getId() { return s_id; }
+ static inline unsigned getHashValue() { return s_hashValue; }
static const bool has_default_value = true;
static const bool default_value = false;
- static inline uint64_t checkID(uint64_t id) {
+ static inline unsigned checkID(unsigned id) {
AlwaysAssert(id <= 63,
"Too many boolean node attributes registered during initialization !");
return id;
private:
/** a bit assignment */
- static const uint64_t s_id;
+ static const unsigned s_id;
/** an extra hash value (to avoid same-value-type collisions) */
- static const uint64_t s_hashValue;
+ static const unsigned s_hashValue;
};
// SPECIFIC, GLOBAL ATTRIBUTE DEFINITIONS ======================================
template <class T>
struct LastAttributeId {
- static uint64_t s_id;
+ static unsigned s_id;
};
template <class T>
- uint64_t LastAttributeId<T>::s_id = 0;
+ unsigned 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 uint64_t Attribute<T, value_t>::s_id =
+const unsigned Attribute<T, value_t>::s_id =
attr::LastAttributeId<typename KindValueToTableValueMapping<value_t>::table_value_type>::s_id++;
template <class T, class value_t>
-const uint64_t Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
+const unsigned Attribute<T, value_t>::s_hashValue = Attribute<T, value_t>::s_id;
template <class T>
-const uint64_t Attribute<T, bool>::s_id =
+const unsigned Attribute<T, bool>::s_id =
Attribute<T, bool>::checkID(attr::LastAttributeId<bool>::s_id++);
template <class T>
-const uint64_t Attribute<T, bool>::s_hashValue = Attribute<T, bool>::s_id;
+const unsigned 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 && unsigned(i) < d_ev->d_nchildren);
+ Assert(i >= 0 && 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