mk_include=include
-ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/unit/Makefile"
+ac_config_files="$ac_config_files Makefile.builds Makefile contrib/Makefile doc/Makefile src/Makefile src/expr/Makefile src/smt/Makefile src/main/Makefile src/prop/minisat/Makefile src/prop/Makefile src/util/Makefile src/context/Makefile src/parser/Makefile src/parser/cvc/Makefile src/parser/smt/Makefile src/theory/Makefile src/theory/uf/Makefile test/Makefile test/regress/Makefile test/system/Makefile test/unit/Makefile"
cat >confcache <<\_ACEOF
"src/theory/uf/Makefile") CONFIG_FILES="$CONFIG_FILES src/theory/uf/Makefile" ;;
"test/Makefile") CONFIG_FILES="$CONFIG_FILES test/Makefile" ;;
"test/regress/Makefile") CONFIG_FILES="$CONFIG_FILES test/regress/Makefile" ;;
+ "test/system/Makefile") CONFIG_FILES="$CONFIG_FILES test/system/Makefile" ;;
"test/unit/Makefile") CONFIG_FILES="$CONFIG_FILES test/unit/Makefile" ;;
*) as_fn_error "invalid argument: \`$ac_config_target'" "$LINENO" 5;;
}
Expr ExprManager::mkExpr(Kind kind) {
- return Expr(this, new Node(d_nm->mkExpr(kind)));
+ return Expr(this, new Node(d_nm->mkNode(kind)));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1) {
- return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode())));
+ return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2) {
- return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+ return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3) {
- return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+ return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode(), child3.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4) {
- return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+ return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode(), child3.getNode(),
child4.getNode())));
}
Expr ExprManager::mkExpr(Kind kind, const Expr& child1, const Expr& child2,
const Expr& child3, const Expr& child4,
const Expr& child5) {
- return Expr(this, new Node(d_nm->mkExpr(kind, child1.getNode(),
+ return Expr(this, new Node(d_nm->mkNode(kind, child1.getNode(),
child2.getNode(), child3.getNode(),
child5.getNode())));
}
nodes.push_back(it->getNode());
++it;
}
- return Expr(this, new Node(d_nm->mkExpr(kind, nodes)));
+ return Expr(this, new Node(d_nm->mkNode(kind, nodes)));
}
Expr ExprManager::mkVar() {
}
Node Node::eqExpr(const Node& right) const {
- return NodeManager::currentNM()->mkExpr(EQUAL, *this, right);
+ return NodeManager::currentNM()->mkNode(EQUAL, *this, right);
}
Node Node::notExpr() const {
- return NodeManager::currentNM()->mkExpr(NOT, *this);
+ return NodeManager::currentNM()->mkNode(NOT, *this);
}
Node Node::andExpr(const Node& right) const {
- return NodeManager::currentNM()->mkExpr(AND, *this, right);
+ return NodeManager::currentNM()->mkNode(AND, *this, right);
}
Node Node::orExpr(const Node& right) const {
- return NodeManager::currentNM()->mkExpr(OR, *this, right);
+ return NodeManager::currentNM()->mkNode(OR, *this, right);
}
Node Node::iteExpr(const Node& thenpart, const Node& elsepart) const {
- return NodeManager::currentNM()->mkExpr(ITE, *this, thenpart, elsepart);
+ return NodeManager::currentNM()->mkNode(ITE, *this, thenpart, elsepart);
}
Node Node::iffExpr(const Node& right) const {
- return NodeManager::currentNM()->mkExpr(IFF, *this, right);
+ return NodeManager::currentNM()->mkNode(IFF, *this, right);
}
Node Node::impExpr(const Node& right) const {
- return NodeManager::currentNM()->mkExpr(IMPLIES, *this, right);
+ return NodeManager::currentNM()->mkNode(IMPLIES, *this, right);
}
Node Node::xorExpr(const Node& right) const {
- return NodeManager::currentNM()->mkExpr(XOR, *this, right);
+ return NodeManager::currentNM()->mkNode(XOR, *this, right);
}
}/* CVC4 namespace */
// general expression-builders
-Node NodeManager::mkExpr(Kind kind) {
+Node NodeManager::mkNode(Kind kind) {
return NodeBuilder<>(this, kind);
}
-Node NodeManager::mkExpr(Kind kind, const Node& child1) {
+Node NodeManager::mkNode(Kind kind, const Node& child1) {
return NodeBuilder<>(this, kind) << child1;
}
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2) {
return NodeBuilder<>(this, kind) << child1 << child2;
}
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3) {
return NodeBuilder<>(this, kind) << child1 << child2 << child3;
}
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4) {
return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4;
}
-Node NodeManager::mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
+Node NodeManager::mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5) {
return NodeBuilder<>(this, kind) << child1 << child2 << child3 << child4 << child5;
}
// N-ary version
-Node NodeManager::mkExpr(Kind kind, const std::vector<Node>& children) {
+Node NodeManager::mkNode(Kind kind, const std::vector<Node>& children) {
return NodeBuilder<>(this, kind).append(children);
}
static NodeManager* currentNM() { return s_current; }
// general expression-builders
- Node mkExpr(Kind kind);
- Node mkExpr(Kind kind, const Node& child1);
- Node mkExpr(Kind kind, const Node& child1, const Node& child2);
- Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3);
- Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
- Node mkExpr(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
+ Node mkNode(Kind kind);
+ Node mkNode(Kind kind, const Node& child1);
+ Node mkNode(Kind kind, const Node& child1, const Node& child2);
+ Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3);
+ Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4);
+ Node mkNode(Kind kind, const Node& child1, const Node& child2, const Node& child3, const Node& child4, const Node& child5);
// N-ary version
- Node mkExpr(Kind kind, const std::vector<Node>& children);
+ Node mkNode(Kind kind, const std::vector<Node>& children);
// variables are special, because duplicates are permitted
Node mkVar();
Trace.setStream(CVC4::null_os);
Notice.setStream(CVC4::null_os);
Chat.setStream(CVC4::null_os);
+ Message.setStream(CVC4::null_os);
Warning.setStream(CVC4::null_os);
} else {
if(options.verbosity < 2) {
Notice.setStream(CVC4::null_os);
}
if(options.verbosity < 0) {
+ Message.setStream(CVC4::null_os);
Warning.setStream(CVC4::null_os);
}
}
for(std::vector<Node>::iterator i = d_assertions.begin();
i != d_assertions.end();
++i)
- asserts = asserts.isNull() ? *i : d_em->mkExpr(AND, asserts, *i);
+ asserts = asserts.isNull() ? *i : d_em->mkNode(AND, asserts, *i);
return asserts;
}
va_list args;
va_start(args, fmt);
construct("Illegal argument detected",
- argDesc, function, file, line, fmt, args);
+ ( std::string(argDesc) + " invalid" ).c_str(),
+ function, file, line, fmt, args);
va_end(args);
}
const char* file, unsigned line) :
AssertionException() {
construct("Illegal argument detected",
- argDesc, function, file, line);
+ ( std::string(argDesc) + " invalid" ).c_str(),
+ function, file, line);
+ }
+
+ IllegalArgumentException(const char* condStr, const char* argDesc,
+ const char* function, const char* file,
+ unsigned line, const char* fmt, ...) :
+ AssertionException() {
+ va_list args;
+ va_start(args, fmt);
+ construct("Illegal argument detected",
+ ( std::string(argDesc) + " invalid; expected " +
+ condStr + " to hold" ).c_str(),
+ function, file, line, fmt, args);
+ va_end(args);
+ }
+
+ IllegalArgumentException(const char* condStr, const char* argDesc,
+ const char* function, const char* file,
+ unsigned line) :
+ AssertionException() {
+ construct("Illegal argument detected",
+ ( std::string(argDesc) + " invalid; expected " +
+ condStr + " to hold" ).c_str(),
+ function, file, line);
}
};/* class IllegalArgumentException */
throw UnhandledCaseException(__PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
#define IllegalArgument(arg, msg...) \
throw IllegalArgumentException(#arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg)
+#define CheckArgument(cond, arg, msg...) \
+ AlwaysAssertArgument(cond, arg, ## msg)
+#define AlwaysAssertArgument(cond, arg, msg...) \
+ do { \
+ if(EXPECT_FALSE( ! (cond) )) { \
+ throw IllegalArgumentException(#cond, #arg, __PRETTY_FUNCTION__, __FILE__, __LINE__, ## msg); \
+ } \
+ } while(0)
#ifdef CVC4_ASSERTIONS
# define Assert(cond, msg...) AlwaysAssert(cond, ## msg)
+# define AssertArgument(cond, arg, msg...) AlwaysAssertArgument(cond, arg, ## msg)
#else /* ! CVC4_ASSERTIONS */
# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/
+# define AssertArgument(cond, arg, msg...) /*EXPECT_TRUE( cond )*/
#endif /* CVC4_ASSERTIONS */
}/* CVC4 namespace */
DebugC Debug (&std::cout);
WarningC Warning(&std::cerr);
+MessageC Message(&std::cout);
NoticeC Notice (&std::cout);
ChatC Chat (&std::cout);
TraceC Trace (&std::cout);
extern WarningC Warning CVC4_PUBLIC;
+class CVC4_PUBLIC MessageC {
+ std::ostream *d_os;
+
+public:
+ MessageC(std::ostream* os) : d_os(os) {}
+
+ void operator()(const char* s) { *d_os << s; }
+ void operator()(std::string s) { *d_os << s; }
+
+ void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3)));
+
+ std::ostream& operator()() { return *d_os; }
+
+ void setStream(std::ostream& os) { d_os = &os; }
+};/* class Message */
+
+extern MessageC Message CVC4_PUBLIC;
+
class CVC4_PUBLIC NoticeC {
std::ostream *d_os;
top_build_prefix = @top_build_prefix@
top_builddir = @top_builddir@
top_srcdir = @top_srcdir@
-SUBDIRS = unit regress
+SUBDIRS = unit system regress
all: all-recursive
.SUFFIXES:
--- /dev/null
+# Makefile.in generated by automake 1.11 from Makefile.am.
+# @configure_input@
+
+# Copyright (C) 1994, 1995, 1996, 1997, 1998, 1999, 2000, 2001, 2002,
+# 2003, 2004, 2005, 2006, 2007, 2008, 2009 Free Software Foundation,
+# Inc.
+# This Makefile.in is free software; the Free Software Foundation
+# gives unlimited permission to copy and/or distribute it,
+# with or without modifications, as long as this notice is preserved.
+
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY, to the extent permitted by law; without
+# even the implied warranty of MERCHANTABILITY or FITNESS FOR A
+# PARTICULAR PURPOSE.
+
+@SET_MAKE@
+VPATH = @srcdir@
+pkgdatadir = $(datadir)/@PACKAGE@
+pkgincludedir = $(includedir)/@PACKAGE@
+pkglibdir = $(libdir)/@PACKAGE@
+pkglibexecdir = $(libexecdir)/@PACKAGE@
+am__cd = CDPATH="$${ZSH_VERSION+.}$(PATH_SEPARATOR)" && cd
+install_sh_DATA = $(install_sh) -c -m 644
+install_sh_PROGRAM = $(install_sh) -c
+install_sh_SCRIPT = $(install_sh) -c
+INSTALL_HEADER = $(INSTALL_DATA)
+transform = $(program_transform_name)
+NORMAL_INSTALL = :
+PRE_INSTALL = :
+POST_INSTALL = :
+NORMAL_UNINSTALL = :
+PRE_UNINSTALL = :
+POST_UNINSTALL = :
+build_triplet = @build@
+host_triplet = @host@
+target_triplet = @target@
+subdir = test/system
+DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
+ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
+am__aclocal_m4_deps = $(top_srcdir)/config/antlr.m4 \
+ $(top_srcdir)/config/cvc4.m4 $(top_srcdir)/config/libtool.m4 \
+ $(top_srcdir)/config/ltoptions.m4 \
+ $(top_srcdir)/config/ltsugar.m4 \
+ $(top_srcdir)/config/ltversion.m4 \
+ $(top_srcdir)/config/lt~obsolete.m4 $(top_srcdir)/configure.ac
+am__configure_deps = $(am__aclocal_m4_deps) $(CONFIGURE_DEPENDENCIES) \
+ $(ACLOCAL_M4)
+mkinstalldirs = $(install_sh) -d
+CONFIG_HEADER = $(top_builddir)/config.h
+CONFIG_CLEAN_FILES =
+CONFIG_CLEAN_VPATH_FILES =
+SOURCES =
+DIST_SOURCES =
+am__tty_colors = \
+red=; grn=; lgn=; blu=; std=
+DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
+ACLOCAL = @ACLOCAL@
+AMTAR = @AMTAR@
+ANTLR = @ANTLR@
+ANTLR_INCLUDES = @ANTLR_INCLUDES@
+ANTLR_LDFLAGS = @ANTLR_LDFLAGS@
+AR = @AR@
+AS = @AS@
+AUTOCONF = @AUTOCONF@
+AUTOHEADER = @AUTOHEADER@
+AUTOMAKE = @AUTOMAKE@
+AWK = @AWK@
+CC = @CC@
+CCDEPMODE = @CCDEPMODE@
+CFLAGS = @CFLAGS@
+CPP = @CPP@
+CPPFLAGS = @CPPFLAGS@
+CVC4_LIBRARY_RELEASE_CODE = @CVC4_LIBRARY_RELEASE_CODE@
+CVC4_LIBRARY_VERSION = @CVC4_LIBRARY_VERSION@
+CVC4_PARSER_LIBRARY_VERSION = @CVC4_PARSER_LIBRARY_VERSION@
+CXX = @CXX@
+CXXCPP = @CXXCPP@
+CXXDEPMODE = @CXXDEPMODE@
+CXXFLAGS = @CXXFLAGS@
+CXXTEST = @CXXTEST@
+CXXTESTGEN = @CXXTESTGEN@
+CYGPATH_W = @CYGPATH_W@
+DEFS = @DEFS@
+DEPDIR = @DEPDIR@
+DLLTOOL = @DLLTOOL@
+DOXYGEN = @DOXYGEN@
+DSYMUTIL = @DSYMUTIL@
+DUMPBIN = @DUMPBIN@
+ECHO_C = @ECHO_C@
+ECHO_N = @ECHO_N@
+ECHO_T = @ECHO_T@
+EGREP = @EGREP@
+EXEEXT = @EXEEXT@
+FGREP = @FGREP@
+GREP = @GREP@
+INSTALL = @INSTALL@
+INSTALL_DATA = @INSTALL_DATA@
+INSTALL_PROGRAM = @INSTALL_PROGRAM@
+INSTALL_SCRIPT = @INSTALL_SCRIPT@
+INSTALL_STRIP_PROGRAM = @INSTALL_STRIP_PROGRAM@
+LD = @LD@
+LDFLAGS = @LDFLAGS@
+LIBOBJS = @LIBOBJS@
+LIBS = @LIBS@
+LIBTOOL = @LIBTOOL@
+LIPO = @LIPO@
+LN_S = @LN_S@
+LTLIBOBJS = @LTLIBOBJS@
+MAKEINFO = @MAKEINFO@
+MKDIR_P = @MKDIR_P@
+NM = @NM@
+NMEDIT = @NMEDIT@
+OBJDUMP = @OBJDUMP@
+OBJEXT = @OBJEXT@
+OTOOL = @OTOOL@
+OTOOL64 = @OTOOL64@
+PACKAGE = @PACKAGE@
+PACKAGE_BUGREPORT = @PACKAGE_BUGREPORT@
+PACKAGE_NAME = @PACKAGE_NAME@
+PACKAGE_STRING = @PACKAGE_STRING@
+PACKAGE_TARNAME = @PACKAGE_TARNAME@
+PACKAGE_URL = @PACKAGE_URL@
+PACKAGE_VERSION = @PACKAGE_VERSION@
+PATH_SEPARATOR = @PATH_SEPARATOR@
+PERL = @PERL@
+RANLIB = @RANLIB@
+SED = @SED@
+SET_MAKE = @SET_MAKE@
+SHELL = @SHELL@
+STRIP = @STRIP@
+TEST_CPPFLAGS = @TEST_CPPFLAGS@
+TEST_CXXFLAGS = @TEST_CXXFLAGS@
+TEST_LDFLAGS = @TEST_LDFLAGS@
+VERSION = @VERSION@
+abs_builddir = @abs_builddir@
+abs_srcdir = @abs_srcdir@
+abs_top_builddir = @abs_top_builddir@
+abs_top_srcdir = @abs_top_srcdir@
+ac_ct_CC = @ac_ct_CC@
+ac_ct_CXX = @ac_ct_CXX@
+ac_ct_DUMPBIN = @ac_ct_DUMPBIN@
+am__include = @am__include@
+am__leading_dot = @am__leading_dot@
+am__quote = @am__quote@
+am__tar = @am__tar@
+am__untar = @am__untar@
+bindir = @bindir@
+build = @build@
+build_alias = @build_alias@
+build_cpu = @build_cpu@
+build_os = @build_os@
+build_vendor = @build_vendor@
+builddir = @builddir@
+datadir = @datadir@
+datarootdir = @datarootdir@
+docdir = @docdir@
+dvidir = @dvidir@
+exec_prefix = @exec_prefix@
+host = @host@
+host_alias = @host_alias@
+host_cpu = @host_cpu@
+host_os = @host_os@
+host_vendor = @host_vendor@
+htmldir = @htmldir@
+includedir = @includedir@
+infodir = @infodir@
+install_sh = @install_sh@
+libdir = @libdir@
+libexecdir = @libexecdir@
+localedir = @localedir@
+localstatedir = @localstatedir@
+lt_ECHO = @lt_ECHO@
+mandir = @mandir@
+mk_include = @mk_include@
+mkdir_p = @mkdir_p@
+oldincludedir = @oldincludedir@
+pdfdir = @pdfdir@
+prefix = @prefix@
+program_transform_name = @program_transform_name@
+psdir = @psdir@
+sbindir = @sbindir@
+sharedstatedir = @sharedstatedir@
+srcdir = @srcdir@
+sysconfdir = @sysconfdir@
+target = @target@
+target_alias = @target_alias@
+target_cpu = @target_cpu@
+target_os = @target_os@
+target_vendor = @target_vendor@
+top_build_prefix = @top_build_prefix@
+top_builddir = @top_builddir@
+top_srcdir = @top_srcdir@
+TESTS_ENVIRONMENT = @top_builddir@/bin/cvc4
+TESTS = \
+ simple.cvc \
+ simple.smt \
+ bug1.cvc
+
+all: all-am
+
+.SUFFIXES:
+$(srcdir)/Makefile.in: $(srcdir)/Makefile.am $(am__configure_deps)
+ @for dep in $?; do \
+ case '$(am__configure_deps)' in \
+ *$$dep*) \
+ ( cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh ) \
+ && { if test -f $@; then exit 0; else break; fi; }; \
+ exit 1;; \
+ esac; \
+ done; \
+ echo ' cd $(top_srcdir) && $(AUTOMAKE) --foreign test/system/Makefile'; \
+ $(am__cd) $(top_srcdir) && \
+ $(AUTOMAKE) --foreign test/system/Makefile
+.PRECIOUS: Makefile
+Makefile: $(srcdir)/Makefile.in $(top_builddir)/config.status
+ @case '$?' in \
+ *config.status*) \
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh;; \
+ *) \
+ echo ' cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe)'; \
+ cd $(top_builddir) && $(SHELL) ./config.status $(subdir)/$@ $(am__depfiles_maybe);; \
+ esac;
+
+$(top_builddir)/config.status: $(top_srcdir)/configure $(CONFIG_STATUS_DEPENDENCIES)
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+
+$(top_srcdir)/configure: $(am__configure_deps)
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(ACLOCAL_M4): $(am__aclocal_m4_deps)
+ cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
+$(am__aclocal_m4_deps):
+
+mostlyclean-libtool:
+ -rm -f *.lo
+
+clean-libtool:
+ -rm -rf .libs _libs
+tags: TAGS
+TAGS:
+
+ctags: CTAGS
+CTAGS:
+
+
+check-TESTS: $(TESTS)
+ @failed=0; all=0; xfail=0; xpass=0; skip=0; \
+ srcdir=$(srcdir); export srcdir; \
+ list=' $(TESTS) '; \
+ $(am__tty_colors); \
+ if test -n "$$list"; then \
+ for tst in $$list; do \
+ if test -f ./$$tst; then dir=./; \
+ elif test -f $$tst; then dir=; \
+ else dir="$(srcdir)/"; fi; \
+ if $(TESTS_ENVIRONMENT) $${dir}$$tst; then \
+ all=`expr $$all + 1`; \
+ case " $(XFAIL_TESTS) " in \
+ *[\ \ ]$$tst[\ \ ]*) \
+ xpass=`expr $$xpass + 1`; \
+ failed=`expr $$failed + 1`; \
+ col=$$red; res=XPASS; \
+ ;; \
+ *) \
+ col=$$grn; res=PASS; \
+ ;; \
+ esac; \
+ elif test $$? -ne 77; then \
+ all=`expr $$all + 1`; \
+ case " $(XFAIL_TESTS) " in \
+ *[\ \ ]$$tst[\ \ ]*) \
+ xfail=`expr $$xfail + 1`; \
+ col=$$lgn; res=XFAIL; \
+ ;; \
+ *) \
+ failed=`expr $$failed + 1`; \
+ col=$$red; res=FAIL; \
+ ;; \
+ esac; \
+ else \
+ skip=`expr $$skip + 1`; \
+ col=$$blu; res=SKIP; \
+ fi; \
+ echo "$${col}$$res$${std}: $$tst"; \
+ done; \
+ if test "$$all" -eq 1; then \
+ tests="test"; \
+ All=""; \
+ else \
+ tests="tests"; \
+ All="All "; \
+ fi; \
+ if test "$$failed" -eq 0; then \
+ if test "$$xfail" -eq 0; then \
+ banner="$$All$$all $$tests passed"; \
+ else \
+ if test "$$xfail" -eq 1; then failures=failure; else failures=failures; fi; \
+ banner="$$All$$all $$tests behaved as expected ($$xfail expected $$failures)"; \
+ fi; \
+ else \
+ if test "$$xpass" -eq 0; then \
+ banner="$$failed of $$all $$tests failed"; \
+ else \
+ if test "$$xpass" -eq 1; then passes=pass; else passes=passes; fi; \
+ banner="$$failed of $$all $$tests did not behave as expected ($$xpass unexpected $$passes)"; \
+ fi; \
+ fi; \
+ dashes="$$banner"; \
+ skipped=""; \
+ if test "$$skip" -ne 0; then \
+ if test "$$skip" -eq 1; then \
+ skipped="($$skip test was not run)"; \
+ else \
+ skipped="($$skip tests were not run)"; \
+ fi; \
+ test `echo "$$skipped" | wc -c` -le `echo "$$banner" | wc -c` || \
+ dashes="$$skipped"; \
+ fi; \
+ report=""; \
+ if test "$$failed" -ne 0 && test -n "$(PACKAGE_BUGREPORT)"; then \
+ report="Please report to $(PACKAGE_BUGREPORT)"; \
+ test `echo "$$report" | wc -c` -le `echo "$$banner" | wc -c` || \
+ dashes="$$report"; \
+ fi; \
+ dashes=`echo "$$dashes" | sed s/./=/g`; \
+ if test "$$failed" -eq 0; then \
+ echo "$$grn$$dashes"; \
+ else \
+ echo "$$red$$dashes"; \
+ fi; \
+ echo "$$banner"; \
+ test -z "$$skipped" || echo "$$skipped"; \
+ test -z "$$report" || echo "$$report"; \
+ echo "$$dashes$$std"; \
+ test "$$failed" -eq 0; \
+ else :; fi
+
+distdir: $(DISTFILES)
+ @srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+ topsrcdirstrip=`echo "$(top_srcdir)" | sed 's/[].[^$$\\*]/\\\\&/g'`; \
+ list='$(DISTFILES)'; \
+ dist_files=`for file in $$list; do echo $$file; done | \
+ sed -e "s|^$$srcdirstrip/||;t" \
+ -e "s|^$$topsrcdirstrip/|$(top_builddir)/|;t"`; \
+ case $$dist_files in \
+ */*) $(MKDIR_P) `echo "$$dist_files" | \
+ sed '/\//!d;s|^|$(distdir)/|;s,/[^/]*$$,,' | \
+ sort -u` ;; \
+ esac; \
+ for file in $$dist_files; do \
+ if test -f $$file || test -d $$file; then d=.; else d=$(srcdir); fi; \
+ if test -d $$d/$$file; then \
+ dir=`echo "/$$file" | sed -e 's,/[^/]*$$,,'`; \
+ if test -d "$(distdir)/$$file"; then \
+ find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+ fi; \
+ if test -d $(srcdir)/$$file && test $$d != $(srcdir); then \
+ cp -fpR $(srcdir)/$$file "$(distdir)$$dir" || exit 1; \
+ find "$(distdir)/$$file" -type d ! -perm -700 -exec chmod u+rwx {} \;; \
+ fi; \
+ cp -fpR $$d/$$file "$(distdir)$$dir" || exit 1; \
+ else \
+ test -f "$(distdir)/$$file" \
+ || cp -p $$d/$$file "$(distdir)/$$file" \
+ || exit 1; \
+ fi; \
+ done
+check-am: all-am
+ $(MAKE) $(AM_MAKEFLAGS) check-TESTS
+check: check-am
+all-am: Makefile
+installdirs:
+install: install-am
+install-exec: install-exec-am
+install-data: install-data-am
+uninstall: uninstall-am
+
+install-am: all-am
+ @$(MAKE) $(AM_MAKEFLAGS) install-exec-am install-data-am
+
+installcheck: installcheck-am
+install-strip:
+ $(MAKE) $(AM_MAKEFLAGS) INSTALL_PROGRAM="$(INSTALL_STRIP_PROGRAM)" \
+ install_sh_PROGRAM="$(INSTALL_STRIP_PROGRAM)" INSTALL_STRIP_FLAG=-s \
+ `test -z '$(STRIP)' || \
+ echo "INSTALL_PROGRAM_ENV=STRIPPROG='$(STRIP)'"` install
+mostlyclean-generic:
+
+clean-generic:
+
+distclean-generic:
+ -test -z "$(CONFIG_CLEAN_FILES)" || rm -f $(CONFIG_CLEAN_FILES)
+ -test . = "$(srcdir)" || test -z "$(CONFIG_CLEAN_VPATH_FILES)" || rm -f $(CONFIG_CLEAN_VPATH_FILES)
+
+maintainer-clean-generic:
+ @echo "This command is intended for maintainers to use"
+ @echo "it deletes files that may require special tools to rebuild."
+clean: clean-am
+
+clean-am: clean-generic clean-libtool mostlyclean-am
+
+distclean: distclean-am
+ -rm -f Makefile
+distclean-am: clean-am distclean-generic
+
+dvi: dvi-am
+
+dvi-am:
+
+html: html-am
+
+html-am:
+
+info: info-am
+
+info-am:
+
+install-data-am:
+
+install-dvi: install-dvi-am
+
+install-dvi-am:
+
+install-exec-am:
+
+install-html: install-html-am
+
+install-html-am:
+
+install-info: install-info-am
+
+install-info-am:
+
+install-man:
+
+install-pdf: install-pdf-am
+
+install-pdf-am:
+
+install-ps: install-ps-am
+
+install-ps-am:
+
+installcheck-am:
+
+maintainer-clean: maintainer-clean-am
+ -rm -f Makefile
+maintainer-clean-am: distclean-am maintainer-clean-generic
+
+mostlyclean: mostlyclean-am
+
+mostlyclean-am: mostlyclean-generic mostlyclean-libtool
+
+pdf: pdf-am
+
+pdf-am:
+
+ps: ps-am
+
+ps-am:
+
+uninstall-am:
+
+.MAKE: check-am install-am install-strip
+
+.PHONY: all all-am check check-TESTS check-am clean clean-generic \
+ clean-libtool distclean distclean-generic distclean-libtool \
+ distdir dvi dvi-am html html-am info info-am install \
+ install-am install-data install-data-am install-dvi \
+ install-dvi-am install-exec install-exec-am install-html \
+ install-html-am install-info install-info-am install-man \
+ install-pdf install-pdf-am install-ps install-ps-am \
+ install-strip installcheck installcheck-am installdirs \
+ maintainer-clean maintainer-clean-generic mostlyclean \
+ mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
+ uninstall uninstall-am
+
+
+# Tell versions [3.59,3.63) of GNU make to not export all variables.
+# Otherwise a system limit (for SysV at least) may be exceeded.
+.NOEXPORT:
@abs_top_builddir@/src/smt/libsmt.la \
@abs_top_builddir@/src/theory/libtheory.la \
@abs_top_builddir@/src/util/libutil.la \
+ @abs_top_builddir@/src/prop/libprop.la \
@abs_top_builddir@/src/prop/minisat/libminisat.la
AM_LDFLAGS_BLACK = \
$(AM_LDFLAGS_WHITE)
AM_LDFLAGS_PUBLIC = \
@abs_top_builddir@/src/libcvc4.la
-TESTS_WHITE = \
- expr/node_white
-
-TESTS_BLACK = \
- expr/node_black
-
-TESTS_PUBLIC =
-
TESTS = \
- $(TESTS_WHITE) \
- $(TESTS_BLACK) \
- $(TESTS_PUBLIC)
+ expr/node_white \
+ expr/node_black
-lib_LTLIBRARIES = libdummy.la
+# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
+noinst_LTLIBRARIES = libdummy.la
libdummy_la_SOURCES = expr/node_black.cpp
libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
$(TESTS:%=%.cpp): %.cpp: %.h
mkdir -p `dirname "$@"`
@CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
-$(TESTS_WHITE): %: %.cpp
+$(filter %_white,$(TESTS)): %_white: %_white.cpp
# get these in here somehow
# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
$(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
$(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
-$(TESTS_BLACK): %: %.cpp
+$(filter %_black,$(TESTS)): %_black: %_black.cpp
# get these in here somehow
# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
$(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
$(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
-$(TESTS_PUBLIC): %: %.cpp
+$(filter %_public,$(TESTS)): %_public: %_public.cpp
# get these in here somehow
# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
$(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
build_triplet = @build@
host_triplet = @host@
target_triplet = @target@
-@HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
-@HAVE_CXXTESTGEN_TRUE@TESTS = $(TESTS_WHITE) $(TESTS_BLACK) \
-@HAVE_CXXTESTGEN_TRUE@ $(am__EXEEXT_1)
subdir = test/unit
DIST_COMMON = $(srcdir)/Makefile.am $(srcdir)/Makefile.in
ACLOCAL_M4 = $(top_srcdir)/aclocal.m4
CONFIG_HEADER = $(top_builddir)/config.h
CONFIG_CLEAN_FILES =
CONFIG_CLEAN_VPATH_FILES =
-am__vpath_adj_setup = srcdirstrip=`echo "$(srcdir)" | sed 's|.|.|g'`;
-am__vpath_adj = case $$p in \
- $(srcdir)/*) f=`echo "$$p" | sed "s|^$$srcdirstrip/||"`;; \
- *) f=$$p;; \
- esac;
-am__strip_dir = f=`echo $$p | sed -e 's|^.*/||'`;
-am__install_max = 40
-am__nobase_strip_setup = \
- srcdirstrip=`echo "$(srcdir)" | sed 's/[].[^$$\\*|]/\\\\&/g'`
-am__nobase_strip = \
- for p in $$list; do echo "$$p"; done | sed -e "s|$$srcdirstrip/||"
-am__nobase_list = $(am__nobase_strip_setup); \
- for p in $$list; do echo "$$p $$p"; done | \
- sed "s| $$srcdirstrip/| |;"' / .*\//!s/ .*/ ./; s,\( .*\)/[^/]*$$,\1,' | \
- $(AWK) 'BEGIN { files["."] = "" } { files[$$2] = files[$$2] " " $$1; \
- if (++n[$$2] == $(am__install_max)) \
- { print $$2, files[$$2]; n[$$2] = 0; files[$$2] = "" } } \
- END { for (dir in files) print dir, files[dir] }'
-am__base_list = \
- sed '$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;$$!N;s/\n/ /g' | \
- sed '$$!N;$$!N;$$!N;$$!N;s/\n/ /g'
-am__installdirs = "$(DESTDIR)$(libdir)"
-LTLIBRARIES = $(lib_LTLIBRARIES)
+LTLIBRARIES = $(noinst_LTLIBRARIES)
@HAVE_CXXTESTGEN_TRUE@libdummy_la_DEPENDENCIES = \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4.la
am__libdummy_la_SOURCES_DIST = expr/node_black.cpp
@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_OBJECTS = node_black.lo
libdummy_la_OBJECTS = $(am_libdummy_la_OBJECTS)
-@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_rpath = -rpath $(libdir)
+@HAVE_CXXTESTGEN_TRUE@am_libdummy_la_rpath =
DEFAULT_INCLUDES = -I.@am__isrc@ -I$(top_builddir)
depcomp = $(SHELL) $(top_srcdir)/config/depcomp
am__depfiles_maybe = depfiles
CTAGS = ctags
am__tty_colors = \
red=; grn=; lgn=; blu=; std=
-am__EXEEXT_1 =
DISTFILES = $(DIST_COMMON) $(DIST_SOURCES) $(TEXINFOS) $(EXTRA_DIST)
ACLOCAL = @ACLOCAL@
AMTAR = @AMTAR@
@HAVE_CXXTESTGEN_TRUE@AM_CPPFLAGS = \
@HAVE_CXXTESTGEN_TRUE@ -I. "-I@CXXTEST@" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src"
-@HAVE_CXXTESTGEN_TRUE@AM_CXXFLGAS_WHITE = -fno-access-control
-@HAVE_CXXTESTGEN_TRUE@AM_CXXFLGAS_BLACK =
-@HAVE_CXXTESTGEN_TRUE@AM_CXXFLGAS_PUBLIC =
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_WHITE = -fno-access-control
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_BLACK =
+@HAVE_CXXTESTGEN_TRUE@AM_CXXFLAGS_PUBLIC =
@HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_WHITE = \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/context/libcontext.la \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/expr/libexpr.la \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/smt/libsmt.la \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/theory/libtheory.la \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/util/libutil.la \
+@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/prop/libprop.la \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/prop/minisat/libminisat.la
@HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_BLACK = \
@HAVE_CXXTESTGEN_TRUE@AM_LDFLAGS_PUBLIC = \
@HAVE_CXXTESTGEN_TRUE@ @abs_top_builddir@/src/libcvc4.la
-@HAVE_CXXTESTGEN_TRUE@TESTS_WHITE = \
-@HAVE_CXXTESTGEN_TRUE@ expr/node_white
-@HAVE_CXXTESTGEN_TRUE@TESTS_BLACK = \
+# force a user-visible failure for "make check"
+@HAVE_CXXTESTGEN_FALSE@TESTS = no_cxxtest
+@HAVE_CXXTESTGEN_TRUE@TESTS = \
+@HAVE_CXXTESTGEN_TRUE@ expr/node_white \
@HAVE_CXXTESTGEN_TRUE@ expr/node_black
-@HAVE_CXXTESTGEN_TRUE@TESTS_PUBLIC =
-@HAVE_CXXTESTGEN_TRUE@lib_LTLIBRARIES = libdummy.la
+
+# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
+@HAVE_CXXTESTGEN_TRUE@noinst_LTLIBRARIES = libdummy.la
@HAVE_CXXTESTGEN_TRUE@libdummy_la_SOURCES = expr/node_black.cpp
@HAVE_CXXTESTGEN_TRUE@libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
@HAVE_CXXTESTGEN_TRUE@MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp)
$(ACLOCAL_M4): $(am__aclocal_m4_deps)
cd $(top_builddir) && $(MAKE) $(AM_MAKEFLAGS) am--refresh
$(am__aclocal_m4_deps):
-install-libLTLIBRARIES: $(lib_LTLIBRARIES)
- @$(NORMAL_INSTALL)
- test -z "$(libdir)" || $(MKDIR_P) "$(DESTDIR)$(libdir)"
- @list='$(lib_LTLIBRARIES)'; test -n "$(libdir)" || list=; \
- list2=; for p in $$list; do \
- if test -f $$p; then \
- list2="$$list2 $$p"; \
- else :; fi; \
- done; \
- test -z "$$list2" || { \
- echo " $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=install $(INSTALL) $(INSTALL_STRIP_FLAG) $$list2 '$(DESTDIR)$(libdir)'"; \
- $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=install $(INSTALL) $(INSTALL_STRIP_FLAG) $$list2 "$(DESTDIR)$(libdir)"; \
- }
-
-uninstall-libLTLIBRARIES:
- @$(NORMAL_UNINSTALL)
- @list='$(lib_LTLIBRARIES)'; test -n "$(libdir)" || list=; \
- for p in $$list; do \
- $(am__strip_dir) \
- echo " $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=uninstall rm -f '$(DESTDIR)$(libdir)/$$f'"; \
- $(LIBTOOL) $(AM_LIBTOOLFLAGS) $(LIBTOOLFLAGS) --mode=uninstall rm -f "$(DESTDIR)$(libdir)/$$f"; \
- done
-clean-libLTLIBRARIES:
- -test -z "$(lib_LTLIBRARIES)" || rm -f $(lib_LTLIBRARIES)
- @list='$(lib_LTLIBRARIES)'; for p in $$list; do \
+clean-noinstLTLIBRARIES:
+ -test -z "$(noinst_LTLIBRARIES)" || rm -f $(noinst_LTLIBRARIES)
+ @list='$(noinst_LTLIBRARIES)'; for p in $$list; do \
dir="`echo $$p | sed -e 's|/[^/]*$$||'`"; \
test "$$dir" != "$$p" || dir=.; \
echo "rm -f \"$${dir}/so_locations\""; \
check: check-am
all-am: Makefile $(LTLIBRARIES)
installdirs:
- for dir in "$(DESTDIR)$(libdir)"; do \
- test -z "$$dir" || $(MKDIR_P) "$$dir"; \
- done
install: install-am
install-exec: install-exec-am
install-data: install-data-am
@echo "it deletes files that may require special tools to rebuild."
clean: clean-am
-clean-am: clean-generic clean-libLTLIBRARIES clean-libtool \
+clean-am: clean-generic clean-libtool clean-noinstLTLIBRARIES \
mostlyclean-am
distclean: distclean-am
install-dvi-am:
-install-exec-am: install-libLTLIBRARIES
+install-exec-am:
install-html: install-html-am
ps-am:
-uninstall-am: uninstall-libLTLIBRARIES
+uninstall-am:
.MAKE: check-am install-am install-strip
.PHONY: CTAGS GTAGS all all-am check check-TESTS check-am clean \
- clean-generic clean-libLTLIBRARIES clean-libtool ctags \
+ clean-generic clean-libtool clean-noinstLTLIBRARIES ctags \
distclean distclean-compile distclean-generic \
distclean-libtool distclean-tags distdir dvi dvi-am html \
html-am info info-am install install-am install-data \
install-data-am install-dvi install-dvi-am install-exec \
install-exec-am install-html install-html-am install-info \
- install-info-am install-libLTLIBRARIES install-man install-pdf \
- install-pdf-am install-ps install-ps-am install-strip \
- installcheck installcheck-am installdirs maintainer-clean \
+ install-info-am install-man install-pdf install-pdf-am \
+ install-ps install-ps-am install-strip installcheck \
+ installcheck-am installdirs maintainer-clean \
maintainer-clean-generic mostlyclean mostlyclean-compile \
mostlyclean-generic mostlyclean-libtool pdf pdf-am ps ps-am \
- tags uninstall uninstall-am uninstall-libLTLIBRARIES
+ tags uninstall uninstall-am
@HAVE_CXXTESTGEN_TRUE@$(TESTS:%=%.cpp): %.cpp: %.h
@HAVE_CXXTESTGEN_TRUE@ mkdir -p `dirname "$@"`
@HAVE_CXXTESTGEN_TRUE@ @CXXTESTGEN@ --have-eh --have-std --error-printer -o "$@" "$<"
-@HAVE_CXXTESTGEN_TRUE@$(TESTS_WHITE): %: %.cpp
+@HAVE_CXXTESTGEN_TRUE@$(filter %_white,$(TESTS)): %_white: %_white.cpp
# get these in here somehow
# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
@HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_WHITE) -c -o $@.lo $<
@HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_WHITE) $@.lo
-@HAVE_CXXTESTGEN_TRUE@$(TESTS_BLACK): %: %.cpp
+@HAVE_CXXTESTGEN_TRUE@$(filter %_black,$(TESTS)): %_black: %_black.cpp
# get these in here somehow
# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
@HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_BLACK) -c -o $@.lo $<
@HAVE_CXXTESTGEN_TRUE@ $(CXXLINK) $(AM_LDFLAGS_BLACK) $@.lo
-@HAVE_CXXTESTGEN_TRUE@$(TESTS_PUBLIC): %: %.cpp
+@HAVE_CXXTESTGEN_TRUE@$(filter %_public,$(TESTS)): %_public: %_public.cpp
# get these in here somehow
# $(TEST_CPPFLAGS) $(TEST_CXXFLAGS) $(TEST_LDFLAGS)
@HAVE_CXXTESTGEN_TRUE@ $(LTCXXCOMPILE) $(AM_CXXFLAGS_PUBLIC) -c -o $@.lo $<
projects / cvc5.git / commitdiff