summaryrefslogtreecommitdiff
path: root/test/system
diff options
context:
space:
mode:
Diffstat (limited to 'test/system')
-rw-r--r--test/system/Makefile.am43
-rw-r--r--test/system/boilerplate.cpp38
-rw-r--r--test/system/ouroborous.cpp103
3 files changed, 175 insertions, 9 deletions
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 954798e6c..7e0192340 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -1,5 +1,7 @@
TESTS_ENVIRONMENT =
-TESTS =
+TESTS = \
+ boilerplate \
+ ouroborous
# Things that aren't tests but that tests rely on and need to
# go into the distribution
@@ -28,20 +30,43 @@ else
system_LINK = $(CXXLINK)
endif
+AM_CPPFLAGS = \
+ -I. \
+ "-I@top_srcdir@/src/include" \
+ "-I@top_srcdir@/lib" \
+ "-I@top_srcdir@/src" \
+ "-I@top_builddir@/src" \
+ "-I@top_srcdir@/src/prop/minisat" \
+ -D __STDC_LIMIT_MACROS \
+ -D __STDC_FORMAT_MACROS \
+ $(TEST_CPPFLAGS)
+LIBADD = \
+ @abs_top_builddir@/src/parser/libcvc4parser.la \
+ @abs_top_builddir@/src/libcvc4.la
+
# WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS:
-# system_test: system_test.cpp
-# $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@.lo $<
-# $(AM_V_CXXLD)$(system_LINK) $(AM_LDFLAGS) $@.lo
+$(TESTS:%=%.lo): %.lo: %.cpp
+ $(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+
+$(TESTS): %: %.lo $(LIBADD)
+ $(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $<
+
+# trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
+if CVC4_FALSE
+noinst_LTLIBRARIES = libdummy.la
+nodist_libdummy_la_SOURCES = ouroborous.cpp
+libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
+endif
# rebuild tests if a library changes
-$(TESTS):: $(TEST_DEPS)
+#$(TESTS):: $(TEST_DEPS)
+MAKEFLAGS = -k
export VERBOSE = 1
-# synonyms for "check"
-.PHONY: test
-test: check
+# synonyms for "checK" in this directory in this directory
+.PHONY: test systemtests
+test systemtests: check
# no-ops here
-.PHONY: units regress regress0 regress1 regress2 regress3s
+.PHONY: units regress regress0 regress1 regress2 regress3
units regress regress0 regress1 regress2 regress3:
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
new file mode 100644
index 000000000..89d5174e3
--- /dev/null
+++ b/test/system/boilerplate.cpp
@@ -0,0 +1,38 @@
+/********************* */
+/*! \file boilerplate.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A simple start-up/tear-down test for CVC4.
+ **
+ ** This simple test just makes sure that the public interface is
+ ** minimally functional. It is useful as a template to use for other
+ ** system tests.
+ **/
+
+#include <iostream>
+#include <sstream>
+
+#include "expr/expr.h"
+#include "smt/smt_engine.h"
+
+using namespace CVC4;
+using namespace std;
+
+int main() {
+ ExprManager em;
+ Options opts;
+ SmtEngine smt(&em, opts);
+ Result r = smt.query(em.mkConst(true));
+
+ return r == Result::VALID ? 0 : 1;
+}
+
diff --git a/test/system/ouroborous.cpp b/test/system/ouroborous.cpp
new file mode 100644
index 000000000..4473b42bb
--- /dev/null
+++ b/test/system/ouroborous.cpp
@@ -0,0 +1,103 @@
+/********************* */
+/*! \file ouroborous.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief "Ouroborous" test: does CVC4 read its own output?
+ **
+ ** The "Ouroborous" test, named after the serpent that swallows its own
+ ** tail, ensures that CVC4 can parse some input, output it again (in any
+ ** of its languages) and then parse it again. The result of the first
+ ** parse must be equal to the result of the second parse (up to renaming
+ ** variables), or the test fails.
+ **/
+
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "expr/expr.h"
+#include "expr/command.h"
+#include "parser/parser.h"
+#include "parser/parser_builder.h"
+
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::language;
+using namespace std;
+
+const string declarations = "\
+(declare-sort U 0)\n\
+(declare-fun f (U) U)\n\
+(declare-fun x () U)\n\
+(declare-fun y () U)\n\
+(assert (= (f x) x))\n\
+";
+
+int runTest();
+
+int main() {
+ try {
+ return runTest();
+ } catch(Exception& e) {
+ cerr << e << endl;
+ } catch(...) {
+ cerr << "non-cvc4 exception thrown." << endl;
+ }
+ return 1;
+}
+
+string translate(Parser* parser, string in, InputLanguage inlang, OutputLanguage outlang) {
+ cout << "==============================================" << endl
+ << "translating from " << inlang << " to " << outlang << " this string:" << endl
+ << in << endl;
+ parser->setInput(Input::newStringInput(inlang, in, "internal-buffer"));
+ stringstream ss;
+ ss << Expr::setlanguage(outlang) << parser->nextExpression();
+ AlwaysAssert(parser->nextExpression().isNull(), "next expr should be null");
+ AlwaysAssert(parser->done(), "parser should be done");
+ string s = ss.str();
+ cout << "got this:" << endl
+ << s << endl
+ << "==============================================" << endl;
+ return s;
+}
+
+int runTest() {
+ ExprManager em;
+ Parser* parser =
+ ParserBuilder(em, "internal-buffer")
+ .withStringInput(declarations)
+ .withInputLanguage(input::LANG_SMTLIB_V2)
+ .build();
+
+ // we don't need to execute them, but we DO need to parse them to
+ // get the declarations
+ while(Command* c = parser->nextCommand()) {
+ delete c;
+ }
+
+ AlwaysAssert(parser->done(), "parser should be done");
+
+ string instr = "(= (f (f y)) x)";
+ string smt2 = translate(parser, instr, input::LANG_SMTLIB_V2, output::LANG_SMTLIB_V2);
+ string smt1 = translate(parser, smt2, input::LANG_SMTLIB_V2, output::LANG_SMTLIB);
+ //string cvc = translate(parser, smt1, input::LANG_SMTLIB, output::LANG_CVC4);
+ //string out = translate(parser, cvc, input::LANG_CVC4, output::LANG_SMTLIB_V2);
+ string out = smt1;
+
+ AlwaysAssert(out == smt2, "differences in output");
+
+ delete parser;
+
+ return 0;
+}
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback