libdir = @libdir@
abs_builddir = @abs_builddir@
-# Are we building static/dynamic libraries? One or the other can be
+# Are we building static/dynamic libraries/binaries? One or the other can be
# on, or both.
BUILDING_STATIC = @BUILDING_STATIC@
BUILDING_SHARED = @BUILDING_SHARED@
+STATIC_BINARY = @STATIC_BINARY@
.PHONY: _default_build_ all
_default_build_: all
$(CURRENT_BUILD)/libtool --mode=install install -v \
$(CURRENT_BUILD)/src/parser/libcvc4parser.la \
"$(abs_builddir)$(libdir)"
-ifeq ($(BUILDING_SHARED),1)
-# if we're building shared libs, relink
+ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10)
+# if we're building shared libs and the binary is not static, relink
thelibdir="$(abs_builddir)$(libdir)"; \
progdir="$(abs_builddir)$(bindir)"; file=cvc4; \
eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/libcvc4.la "`pwd`$(libdir)"
# install libcvc4parser
$(CURRENT_BUILD)/libtool --mode=install install -v $(CURRENT_BUILD)/src/parser/libcvc4parser.la "`pwd`$(libdir)"
-ifeq ($(BUILDING_SHARED),1)
-# if we're building shared libs, relink
+ifeq ($(BUILDING_SHARED)$(STATIC_BINARY),10)
+# if we're building shared libs and the binary is not static, relink
thelibdir="`pwd`$(libdir)"; progdir="`pwd`$(bindir)"; file=cvc4; \
eval `grep '^relink_command=' $(CURRENT_BUILD)/src/main/cvc4 | sed 's:-Wl,-rpath:-Wl,-rpath -Wl,\\\\$$thelibdir -Wl,-rpath:'`; \
eval "(cd $(CURRENT_BUILD)/src/main && $$relink_command)"
# some things.)
config_cmdline="$@"
+# remember if the user set these explicitly (or whether autoconf does)
+user_specified_enable_or_disable_static=${enable_static+yes}
+user_specified_enable_or_disable_shared=${enable_shared+yes}
+
# turn off static lib building by default
AC_ENABLE_SHARED
AC_DISABLE_STATIC
cd "builds/$target/$build_type"
CVC4_CONFIGURE_IN_BUILDS=yes; export CVC4_CONFIGURE_IN_BUILDS
echo ../../../configure $config_cmdline
- exec ../../../configure $config_cmdline
+ `pwd`/../../../configure $config_cmdline
+ exitval=$?
+ cd ../../..
+ if test $exitval -eq 0; then
+ cat >config.status <<EOF
+#!/bin/sh -ex
+# Generated by configure, `date`
+# This script part of CVC4.
+
+target='$target'
+build_type='$build_type'
+
+cd "builds/$target/$build_type"
+./config.status "\$@"
+EOF
+ chmod +x config.status
+ fi
+ exit $exitval
else
AC_MSG_RESULT([this one (user-specified)])
fi
CVC4CXXFLAGS=
CVC4CFLAGS=
CVC4LDFLAGS=
+ FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=3 ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
CVC4CXXFLAGS='-fno-inline'
CVC4CFLAGS='-fno-inline'
CVC4LDFLAGS=
+ FLAG_VISIBILITY_HIDDEN=
if test -z "${enable_optimized+set}" ; then enable_optimized=no ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
if test -z "${enable_assertions+set}" ; then enable_assertions=yes ; fi
CVC4CXXFLAGS=
CVC4CFLAGS=
CVC4LDFLAGS=
+ FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=2 ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=yes ; fi
CVC4CXXFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
CVC4CFLAGS='-funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs'
CVC4LDFLAGS=
+ FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
if test -z "${OPTLEVEL+set}" ; then OPTLEVEL=9 ; fi
if test -z "${enable_optimized+set}" ; then enable_optimized=yes ; fi
if test -z "${enable_debug_symbols+set}"; then enable_debug_symbols=no ; fi
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]])])
+ [build a fully 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
+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_RESULT([$enable_optimized])
if test "$enable_optimized" = yes; then
- CVC4CXXFLAGS="$CVC4CXXFLAGS -O$OPTLEVEL"
- CVC4CFLAGS="$CVC4CFLAGS -O$OPTLEVEL"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O$OPTLEVEL"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O$OPTLEVEL"
else
- CVC4CXXFLAGS="$CVC4CXXFLAGS -O0"
- CVC4CFLAGS="$CVC4CFLAGS -O0"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-O0"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-O0"
fi
AC_MSG_CHECKING([whether to include debugging symbols in libcvc4])
AC_MSG_RESULT([$enable_debug_symbols])
if test "$enable_debug_symbols" = yes; then
- CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3"
- CVC4CFLAGS="$CVC4CFLAGS -ggdb3"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3"
fi
AC_MSG_CHECKING([whether to include assertions in build])
AC_MSG_RESULT([$enable_assertions])
if test "$enable_assertions" = yes; then
- CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_ASSERTIONS"
fi
AC_MSG_CHECKING([whether to do a traceable build of CVC4])
AC_MSG_RESULT([$enable_tracing])
if test "$enable_tracing" = yes; then
- CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_TRACING"
fi
AC_MSG_CHECKING([whether to do a muzzled build of CVC4])
AC_MSG_RESULT([$enable_muzzle])
if test "$enable_muzzle" = yes; then
- CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_MUZZLE"
fi
AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4])
AC_MSG_RESULT([$enable_coverage])
if test "$enable_coverage" = yes; then
-dnl TODO: Is there someway to detect if enable_shared is set by default,
-dnl so that we can automatically disable shared and enable static?
- if test "$enable_shared" = yes; then
- AC_MSG_ERROR([Gcov requires static libraries. Use --disable-shared.])
+ # For coverage testing, we prefer:
+ # --enable-static --disable-shared --disable-static-binary
+ # If the user didn't specify these, we force them here. If the
+ # user specified them in opposite phase, give warnings that they
+ # shouldn't do that, or bomb out.
+ if test "$user_specified_enable_or_disable_shared" != yes; then
+ enable_shared=no
+ AC_MSG_WARN([turning off shared library building due to --enable-coverage])
+ elif test "$enable_shared" = yes; then
+ AC_MSG_WARN([])
+ AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-shared])
+ AC_MSG_WARN([gcov does not support shared libraries, so only your static libraries will be coverage-testable.])
+ AC_MSG_WARN([Your cvc4 driver and testing binaries will not be coverage-testable.])
+ AC_MSG_WARN([])
+ fi
+ if test "${enable_static_binary+set}" = set -a "$enable_static_binary" = yes; then
+ AC_MSG_WARN([])
+ AC_MSG_WARN([It is not recommended to configure with --enable-coverage --enable-static-binary])
+ AC_MSG_WARN([Your cvc4 driver and testing binaries will be fully-statically linked and may not be coverage-testable.])
+ AC_MSG_WARN([])
+ fi
+ if test "$user_specified_enable_or_disable_static" != yes; then
+ enable_static=yes
+ AC_MSG_WARN([turning on static library building due to --enable-coverage])
+ elif test "$enable_static" != yes; then
+ AC_MSG_ERROR([--enable-coverage and --disable-static are incompatible; gcov only supports static libraries.])
fi
- CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_COVERAGE"
- CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage"
- CVC4CFLAGS="$CVC4CFLAGS --coverage"
- CVC4LDFLAGS="$CVC4LDFLAGS --coverage"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COVERAGE"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }--coverage"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }--coverage"
+ CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }--coverage"
fi
AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4])
AC_MSG_RESULT([$enable_profiling])
if test "$enable_profiling" = yes; then
- CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_PROFILING"
- CVC4CXXFLAGS="$CVC4CXXFLAGS -pg"
- CVC4CFLAGS="$CVC4CFLAGS -pg"
- CVC4LDFLAGS="$CVC4LDFLAGS -pg"
+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_PROFILING"
+ CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-pg"
+ CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-pg"
+ CVC4LDFLAGS="${CVC4LDFLAGS:+$CVC4LDFLAGS }-pg"
fi
AM_INIT_AUTOMAKE([1.11 no-define])
# Prepare configure output
-if test "$enable_shared" = yes; then BUILDING_SHARED=1; fi
-if test "$enable_static" = yes; then BUILDING_STATIC=1; fi
+if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
+if test "$enable_static" = yes; then BUILDING_STATIC=1; else BUILDING_STATIC=0; fi
+if test "$enable_static_binary" = yes; then STATIC_BINARY=1; else STATIC_BINARY=0; fi
AC_SUBST(BUILDING_SHARED)
AC_SUBST(BUILDING_STATIC)
+AC_SUBST(STATIC_BINARY)
AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
AC_SUBST(CVC4_LIBRARY_VERSION)
CFLAGS="${CFLAGS:+$CFLAGS }$CVC4CFLAGS -Wno-deprecated -fexceptions"
LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
-FLAG_VISIBILITY_HIDDEN='-fvisibility=hidden'
AC_SUBST(FLAG_VISIBILITY_HIDDEN)
# mk_include
if test "$with_build" = default; then
with_build=custom
else
- AC_MSG_WARN([])
- AC_MSG_WARN([This is a customized $with_build build profile.])
- AC_MSG_WARN([])
- with_build="$with_build-custom"
+ with_build="$with_build (customized)"
fi
fi
echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
$(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
done
-
-include/cvc4.h: smt/smt_engine.h
- @srcdir@/headergen.pl $< $@
-include/cvc4_expr.h: expr/expr.h
AM_CPPFLAGS = \
-I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" \
$(TEST_CPPFLAGS)
-AM_CXXFLAGS = $(TEST_CXXFLAGS)
+AM_CXXFLAGS = -Wall $(TEST_CXXFLAGS)
AM_LDFLAGS = $(TEST_LDFLAGS)
AM_CXXFLAGS_WHITE = -fno-access-control -D__BUILDING_CVC4LIB_UNIT_TEST -D__BUILDING_CVC4PARSERLIB_UNIT_TEST
$(AM_V_at)mkdir -p `dirname "$@"`
$(AM_V_GEN)$(CXXTESTGEN) --have-eh --have-std --error-printer -o "$@" "$<"
$(WHITE_TESTS): %_white: %_white.cpp $(TEST_DEPS)
- $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
+ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo @abs_builddir@/$<
$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_WHITE) $@.lo
$(BLACK_TESTS): %_black: %_black.cpp $(TEST_DEPS)
- $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
+ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo @abs_builddir@/$<
$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_BLACK) $@.lo
$(PUBLIC_TESTS): %_public: %_public.cpp $(TEST_DEPS)
- $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
+ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo @abs_builddir@/$<
$(AM_V_CXXLD)$(unit_LINK) $(AM_LDFLAGS_PUBLIC) $@.lo
else
TS_ASSERT(list.empty());
for(int i = 0; i < N; ++i) {
- TS_ASSERT(list.size() == i);
+ TS_ASSERT_EQUALS(list.size(), unsigned(i));
list.push_back(i);
TS_ASSERT(!list.empty());
- TS_ASSERT(list.back() == i);
+ TS_ASSERT_EQUALS(list.back(), i);
int i2 = 0;
for(CDList<int>::const_iterator j = list.begin();
j != list.end();
++j) {
- TS_ASSERT(*j == i2++);
+ TS_ASSERT_EQUALS(*j, i2++);
}
}
- TS_ASSERT(list.size() == N);
+ TS_ASSERT_EQUALS(list.size(), unsigned(N));
for(int i = 0; i < N; ++i) {
- TS_ASSERT(list[i] == i);
+ TS_ASSERT_EQUALS(list[i], i);
}
}
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** Black box testing of CVC4::Node.
+ ** Black box testing of CVC4::context::ContextMemoryManager.
**/
#include <cxxtest/TestSuite.h>
// Push, then allocate, then pop
// We make sure that we don't allocate too much so that all the regions
// should be reclaimed
- int chunkSizeBytes = 16384;
- int maxFreeChunks = 100;
- int piecesPerChunk = 13;
- int len = chunkSizeBytes / piecesPerChunk; // Length of the individual block
- int N = maxFreeChunks*piecesPerChunk;
- for (int p = 0; p < 5; ++ p) {
+ unsigned chunkSizeBytes = 16384;
+ unsigned maxFreeChunks = 100;
+ unsigned piecesPerChunk = 13;
+ unsigned len = chunkSizeBytes / piecesPerChunk; // Length of the individual block
+ unsigned N = maxFreeChunks*piecesPerChunk;
+ for(unsigned p = 0; p < 5; ++ p) {
d_cmm->push();
- for (int i = 0; i < N; ++i) {
+ for(unsigned i = 0; i < N; ++i) {
char* newMem = (char*)d_cmm->newData(len);
// We only setup the memory in the first run, the others should
// reclaim the same memory
- if (p == 0) {
- for(int k = 0; k < len - 1; k ++)
+ if(p == 0) {
+ for(unsigned k = 0; k < len - 1; k ++) {
newMem[k] = 'a';
+ }
newMem[len-1] = 0;
}
- if (strlen(newMem) != len - 1) {
+ if(strlen(newMem) != len - 1) {
cout << strlen(newMem) << " : " << len - 1 << endl;
}
TS_ASSERT(strlen(newMem) == len - 1);
d_cmm->pop();
}
- int factor = 3;
- N = 16384/factor;
+ unsigned factor = 3;
+ N = 16384 / factor;
// Push, then allocate, then pop all at once
- for (int p = 0; p < 5; ++ p) {
+ for(unsigned p = 0; p < 5; ++ p) {
d_cmm->push();
- for (int i = 1; i < N; ++i) {
- int len = i*factor;
+ for(unsigned i = 1; i < N; ++i) {
+ unsigned len = i * factor;
char* newMem = (char*)d_cmm->newData(len);
- for(int k = 0; k < len - 1; k ++)
+ for(unsigned k = 0; k < len - 1; k ++) {
newMem[k] = 'a';
+ }
newMem[len-1] = 0;
TS_ASSERT(strlen(newMem) == len - 1);
}
}
- for (int p = 0; p < 5; ++ p) {
+ for(unsigned p = 0; p < 5; ++ p) {
d_cmm->pop();
}
}
void testCDAttributes() {
- AttributeManager& am = d_nm->d_attrManager;
-
//Debug.on("boolattr");
Node a = d_nm->mkVar(d_booleanType);
}
void testAttributes() {
- AttributeManager& am = d_nm->d_attrManager;
-
//Debug.on("boolattr");
Node a = d_nm->mkVar(d_booleanType);
#endif /* CVC4_ASSERTIONS */
}
- void testNaryExpForSize(Kind k, int N) {
+ void testNaryExpForSize(Kind k, unsigned N) {
NodeBuilder<> nbz(k);
Node trueNode = d_nodeManager->mkConst(true);
- for(int i = 0; i < N; ++i) {
+ for(unsigned i = 0; i < N; ++i) {
nbz << trueNode;
}
Node result = nbz;
srand(0);
int trials = 500;
for(int i = 0; i < trials; ++i) {
- int N = rand() % 1000 + 2;
+ unsigned N = rand() % 1000 + 2;
testNaryExpForSize(AND, N);
}
}
}
-#define K 30
-#define LARGE_K UINT_MAX/40
+#define K 30u
+#define LARGE_K UINT_MAX / 40
Kind specKind;
/* default size tests */
NodeBuilder<> def;
TS_ASSERT_EQUALS(def.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(def.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(def.getNumChildren(), 0u);
TS_ASSERT_EQUALS(def.begin(), def.end());
NodeBuilder<> spec(specKind);
TS_ASSERT_EQUALS(spec.getKind(), specKind);
- TS_ASSERT_EQUALS(spec.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(spec.getNumChildren(), 0u);
TS_ASSERT_EQUALS(spec.begin(), spec.end());
NodeBuilder<> from_nm(d_nm);
TS_ASSERT_EQUALS(from_nm.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(from_nm.getNumChildren(), 0u);
TS_ASSERT_EQUALS(from_nm.begin(), from_nm.end());
NodeBuilder<> from_nm_kind(d_nm, specKind);
TS_ASSERT_EQUALS(from_nm_kind.getKind(), specKind);
- TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(from_nm_kind.getNumChildren(), 0u);
TS_ASSERT_EQUALS(from_nm_kind.begin(), from_nm_kind.end());
NodeBuilder<K> ws;
TS_ASSERT_EQUALS(ws.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(ws.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws.begin(), ws.end());
NodeBuilder<K> ws_kind(specKind);
TS_ASSERT_EQUALS(ws_kind.getKind(), specKind);
- TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws_kind.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws_kind.begin(), ws_kind.end());
NodeBuilder<K> ws_from_nm(d_nm);
TS_ASSERT_EQUALS(ws_from_nm.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws_from_nm.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws_from_nm.begin(), ws_from_nm.end());
NodeBuilder<K> ws_from_nm_kind(d_nm, specKind);
TS_ASSERT_EQUALS(ws_from_nm_kind.getKind(), specKind);
- TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(ws_from_nm_kind.getNumChildren(), 0u);
TS_ASSERT_EQUALS(ws_from_nm_kind.begin(), ws_from_nm_kind.end());
NodeBuilder<> copy(def);
TS_ASSERT_EQUALS(copy.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(copy.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(copy.getNumChildren(), 0u);
TS_ASSERT_EQUALS(copy.begin(), copy.end());
NodeBuilder<K> cp_ws(ws);
TS_ASSERT_EQUALS(cp_ws.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(cp_ws.getNumChildren(), 0u);
TS_ASSERT_EQUALS(cp_ws.begin(), cp_ws.end());
NodeBuilder<K-10> cp_from_larger(ws);
TS_ASSERT_EQUALS(cp_from_larger.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(cp_from_larger.getNumChildren(), 0u);
TS_ASSERT_EQUALS(cp_from_larger.begin(), cp_from_larger.end());
NodeBuilder<K+10> cp_from_smaller(ws);
TS_ASSERT_EQUALS(cp_from_smaller.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(cp_from_smaller.getNumChildren(), 0u);
TS_ASSERT_EQUALS(cp_from_smaller.begin(), cp_from_smaller.end());
}
TS_ASSERT_DIFFERS(ws.begin(), ws.end());
NodeBuilder<K>::iterator iter = ws.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(iter, ws.end());
++iter;
}
TS_ASSERT_EQUALS(iter, ws.end());
NodeBuilder<K>::const_iterator citer = ws.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(citer, ws.end());
++citer;
}
TS_ASSERT_DIFFERS(smaller.begin(), smaller.end());
NodeBuilder<>::iterator smaller_iter = smaller.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(smaller_iter, smaller.end());
++smaller_iter;
}
TS_ASSERT_EQUALS(iter, ws.end());
NodeBuilder<>::const_iterator smaller_citer = smaller.begin();
- for(int i = 0; i < K; ++i){
+ for(unsigned i = 0; i < K; ++i){
TS_ASSERT_DIFFERS(smaller_citer, smaller.end());
++smaller_citer;
}
/* unsigned getNumChildren() const; */
NodeBuilder<> noKind;
- TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
push_back(noKind, K);
TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
push_back(noKind, K);
- TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
noKind << AND;// avoid exception on marking it used
Node n = noKind;// avoid warning on clear()
noKind.clear();
- TS_ASSERT_EQUALS(noKind.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), 0u);
push_back(noKind, K);
TS_ASSERT_EQUALS(noKind.getNumChildren(), K);
push_back(noKind, K);
- TS_ASSERT_EQUALS(noKind.getNumChildren(), K+K);
+ TS_ASSERT_EQUALS(noKind.getNumChildren(), K + K);
#ifdef CVC4_ASSERTIONS
noKind << specKind;
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- for(int i = 3; i < K; ++i) {
+ for(unsigned i = 3; i < K; ++i) {
TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
}
TS_ASSERT_EQUALS(arr[0], i_0);
TS_ASSERT_EQUALS(arr[2], i_2);
- for(int i = 3; i < K; ++i) {
+ for(unsigned i = 3; i < K; ++i) {
TS_ASSERT_EQUALS(arr[i], d_nm->mkConst(true));
}
TS_ASSERT_EQUALS(arr[K], i_K);
NodeBuilder<> nb;
TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
nb << specKind;
nb.clear();
TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
nb << specKind;
nb.clear(specKind);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
push_back(nb, K);
nb.clear();
TS_ASSERT_EQUALS(nb.getKind(), UNDEFINED_KIND);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
}
/* NodeBuilder& operator<<(const Node& n); */
NodeBuilder<K> nb(specKind);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
- TS_ASSERT_EQUALS(nb.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(nb.getNumChildren(), 0u);
TS_ASSERT_EQUALS(nb.begin(), nb.end());
push_back(nb,K);
TS_ASSERT_EQUALS(nb.getKind(), specKind);
NodeBuilder<> overflow(specKind);
TS_ASSERT_EQUALS(overflow.getKind(), specKind);
- TS_ASSERT_EQUALS(overflow.getNumChildren(), 0);
+ TS_ASSERT_EQUALS(overflow.getNumChildren(), 0u);
TS_ASSERT_EQUALS(overflow.begin(), overflow.end());
push_back(overflow,5*K+1);
TS_ASSERT_EQUALS(overflow.getKind(), specKind);
- TS_ASSERT_EQUALS(overflow.getNumChildren(), 5*K+1);
+ TS_ASSERT_EQUALS(overflow.getNumChildren(), 5 * K + 1);
TS_ASSERT_DIFFERS(overflow.begin(), overflow.end());
}
Node f = d_nm->mkVar(d_booleanType);
Node m = a && b;
- Node n = a && b || c;
+ Node n = (a && b) || c;
Node o = d + e - b;
- Node p = a && o || c;
+ Node p = (a && o) || c;
Node x = d + e + o - m;
Node y = f - a - c + e;
Node q = a && b && c;
- Node r = e && d && b && a || x && y || f || q && a;
+ Node r = (e && d && b && a) || (x && y) || f || (q && a);
TS_ASSERT_EQUALS(m, d_nm->mkNode(AND, a, b));
TS_ASSERT_EQUALS(n, d_nm->mkNode(OR, m, c));
void testMkNode1() {
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(NOT, x);
- TS_ASSERT_EQUALS( n.getNumChildren(), 1 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 1u );
TS_ASSERT_EQUALS( n.getKind(), NOT);
TS_ASSERT_EQUALS( n[0], x);
}
Node x = d_nodeManager->mkVar("x",d_nodeManager->booleanType());
Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(IMPLIES, x, y);
- TS_ASSERT_EQUALS( n.getNumChildren(), 2 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 2u );
TS_ASSERT_EQUALS( n.getKind(), IMPLIES);
TS_ASSERT_EQUALS( n[0], x);
TS_ASSERT_EQUALS( n[1], y);
Node y = d_nodeManager->mkVar("y",d_nodeManager->booleanType());
Node z = d_nodeManager->mkVar("z",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x, y, z);
- TS_ASSERT_EQUALS( n.getNumChildren(), 3 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 3u );
TS_ASSERT_EQUALS( n.getKind(), AND);
TS_ASSERT_EQUALS( n[0], x);
TS_ASSERT_EQUALS( n[1], y);
Node x3 = d_nodeManager->mkVar("x3",d_nodeManager->booleanType());
Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4);
- TS_ASSERT_EQUALS( n.getNumChildren(), 4 );
- TS_ASSERT_EQUALS( n.getKind(), AND);
- TS_ASSERT_EQUALS( n[0], x1);
- TS_ASSERT_EQUALS( n[1], x2);
- TS_ASSERT_EQUALS( n[2], x3);
- TS_ASSERT_EQUALS( n[3], x4);
+ TS_ASSERT_EQUALS( n.getNumChildren(), 4u );
+ TS_ASSERT_EQUALS( n.getKind(), AND );
+ TS_ASSERT_EQUALS( n[0], x1 );
+ TS_ASSERT_EQUALS( n[1], x2 );
+ TS_ASSERT_EQUALS( n[2], x3 );
+ TS_ASSERT_EQUALS( n[3], x4 );
}
void testMkNode5() {
Node x4 = d_nodeManager->mkVar("x4",d_nodeManager->booleanType());
Node x5 = d_nodeManager->mkVar("x5",d_nodeManager->booleanType());
Node n = d_nodeManager->mkNode(AND, x1, x2, x3, x4, x5);
- TS_ASSERT_EQUALS( n.getNumChildren(), 5 );
+ TS_ASSERT_EQUALS( n.getNumChildren(), 5u );
TS_ASSERT_EQUALS( n.getKind(), AND);
TS_ASSERT_EQUALS( n[0], x1);
TS_ASSERT_EQUALS( n[1], x2);
Node n = d_nodeManager->mkNode(AND, args);
TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
TS_ASSERT_EQUALS( n.getKind(), AND);
- for( int i=0; i < args.size(); ++i ) {
+ for( unsigned i = 0; i < args.size(); ++i ) {
TS_ASSERT_EQUALS( n[i], args[i]);
}
}
Node n = d_nodeManager->mkNode(AND, args);
TS_ASSERT_EQUALS( n.getNumChildren(), args.size() );
TS_ASSERT_EQUALS( n.getKind(), AND);
- for( int i=0; i < args.size(); ++i ) {
+ for( unsigned i = 0; i < args.size(); ++i ) {
TS_ASSERT_EQUALS( n[i], args[i]);
}
}
Type* booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar(booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
- TS_ASSERT_EQUALS(x.getNumChildren(),0);
+ TS_ASSERT_EQUALS(x.getNumChildren(),0u);
TS_ASSERT_EQUALS(x.getType(),booleanType);
}
Type* booleanType = d_nodeManager->booleanType();
Node x = d_nodeManager->mkVar("x", booleanType);
TS_ASSERT_EQUALS(x.getKind(),VARIABLE);
- TS_ASSERT_EQUALS(x.getNumChildren(),0);
+ TS_ASSERT_EQUALS(x.getNumChildren(),0u);
TS_ASSERT_EQUALS(x.getAttribute(VarNameAttr()),"x");
TS_ASSERT_EQUALS(x.getType(),booleanType);
}
TS_ASSERT( t->isFunction() );
FunctionType* ft = (FunctionType*)t;
- TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1);
+ TS_ASSERT_EQUALS(ft->getArgTypes().size(), 1u);
TS_ASSERT_EQUALS(ft->getArgTypes()[0], booleanType);
TS_ASSERT_EQUALS(ft->getRangeType(), booleanType);
}
void testNull() {
- Node::s_null;
+ TS_ASSERT_EQUALS(Node::null(), Node::s_null);
}
void testCopyCtor() {
TS_ASSERT_EQUALS(got, f_x_eq_x);
- TS_ASSERT_EQUALS(5, d_dummy->d_registered.size());
+ TS_ASSERT_EQUALS(5u, d_dummy->d_registered.size());
TS_ASSERT(d_dummy->d_registered.find(x) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(f) != d_dummy->d_registered.end());
TS_ASSERT(d_dummy->d_registered.find(f_x) != d_dummy->d_registered.end());
d_euf->assertFact( f5_x_eq_x );
d_euf->check(d_level);
- TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls());
+ TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
Node realConflict = d_outputChannel.getIthNode(0);
TS_ASSERT_EQUALS(expectedConflict, realConflict);
TS_ASSERT_EQUALS(z4.getLong(), 0);
Integer z5("7896890");
- TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890);
+ TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
Integer z6(z5);
- TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890);
- TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890);
+ TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890ul);
+ TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890ul);
string bigValue("1536729");
Integer z7(bigValue);
- TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729);
+ TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729ul);
}
void testOperatorAssign(){
Integer y(79);
Integer z(45789);
- TS_ASSERT_EQUALS(x.getUnsignedLong(), 0);
- TS_ASSERT_EQUALS(y.getUnsignedLong(), 79);
- TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(x.getUnsignedLong(), 0ul);
+ TS_ASSERT_EQUALS(y.getUnsignedLong(), 79ul);
+ TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
x = y = z;
- TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789);
- TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789);
- TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
+ TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789ul);
+ TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
Integer a(2);
y = a;
- TS_ASSERT_EQUALS(a.getUnsignedLong(), 2);
- TS_ASSERT_EQUALS(y.getUnsignedLong(), 2);
- TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789);
- TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(a.getUnsignedLong(), 2ul);
+ TS_ASSERT_EQUALS(y.getUnsignedLong(), 2ul);
+ TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789ul);
+ TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789ul);
}
void testOperatorEquals(){
Integer fits_in_16_bytes("7890D789D33234027890D789D3323402", 16);
- TS_ASSERT_THROWS_NOTHING(size_t res0 = zero.hash());
- TS_ASSERT_THROWS_NOTHING(size_t res1 = fits_in_2_bytes.hash());
- TS_ASSERT_THROWS_NOTHING(size_t res2 = fits_in_16_bytes.hash());
- TS_ASSERT_THROWS_NOTHING(size_t res3 = large.hash());
+ TS_ASSERT_THROWS_NOTHING(zero.hash());
+ TS_ASSERT_THROWS_NOTHING(fits_in_2_bytes.hash());
+ TS_ASSERT_THROWS_NOTHING(fits_in_16_bytes.hash());
+ TS_ASSERT_THROWS_NOTHING(large.hash());
}
};
Rational y(78,6);
Rational z(45789,1);
- TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0);
- TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13);
- TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0ul);
+ TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13ul);
+ TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul);
x = y = z;
- TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789);
- TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789);
- TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789ul);
+ TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789ul);
+ TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul);
Rational a(78,91);
y = a;
- TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6);
- TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7);
- TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6);
- TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7);
- TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789);
- TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6ul);
+ TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7ul);
+ TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6ul);
+ TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7ul);
+ TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789ul);
+ TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789ul);
}
void testToStringStuff(){
Rational one_word(75890L,590L);
Rational two_words("7890D789D33234027890D789D3323402", 16);
- TS_ASSERT_EQUALS(zero.hash(), 1);
- TS_ASSERT_EQUALS(one_word.hash(), 7589 xor 59);
+ TS_ASSERT_EQUALS(zero.hash(), 1u);
+ TS_ASSERT_EQUALS(one_word.hash(), 7589u xor 59u);
TS_ASSERT_EQUALS(two_words.hash(),
(two_words.getNumerator().hash()) xor 1);
TS_ASSERT_EQUALS(large.hash(),
projects / cvc5.git / commitdiff