From cd98370b338a0cc5343067151884a06431a1d92c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 19 Nov 2009 22:07:01 +0000 Subject: [PATCH] testing framework, configure fixes, incorporations from meeting, continued work --- Makefile.am | 5 +++- autogen.sh | 2 +- configure.ac | 25 ++++++++++++++++ src/Makefile.am | 1 + src/context/Makefile.am | 2 +- src/context/context.h | 8 ++++-- src/expr/Makefile.am | 2 +- src/expr/attr_type.h | 10 ++++--- src/expr/expr.cpp | 18 ++++++------ src/expr/expr_attribute.h | 10 ++++--- src/expr/expr_builder.cpp | 21 ++++++-------- src/expr/expr_builder.h | 12 ++++---- src/expr/expr_manager.cpp | 2 +- src/expr/expr_manager.h | 8 +++--- src/expr/expr_value.cpp | 2 +- src/expr/expr_value.h | 24 ++++++++++------ src/expr/kind.h | 30 +++++++++++++------ src/include/cvc4.h | 10 +++---- src/include/cvc4_expr.h | 24 ++++++++++++++-- src/main/Makefile.am | 2 +- src/main/about.h | 8 +++--- src/main/main.cpp | 9 ++++++ src/main/main.h | 10 +++---- src/main/usage.h | 10 +++---- src/main/util.cpp | 4 +-- src/parser/Makefile.am | 4 +-- src/parser/parser.h | 8 ++++-- src/parser/parser_exception.h | 10 ++++--- src/parser/parser_state.h | 17 ++++++----- src/parser/pl.ypp | 23 ++++++++------- src/parser/pl_scanner.lpp | 28 +++++++++--------- src/parser/smtlib.ypp | 6 ++-- src/parser/smtlib_scanner.lpp | 4 +-- src/prop/Makefile.am | 2 +- src/prop/minisat/Makefile.am | 1 + src/prop/prop_engine.h | 10 ++++--- src/prop/sat.h | 10 ++++--- src/smt/Makefile.am | 2 +- src/smt/smt_engine.h | 10 ++++--- src/theory/Makefile.am | 2 +- src/theory/theory.h | 8 ++++-- src/theory/theory_engine.h | 8 ++++-- src/util/Makefile.am | 2 +- src/util/assert.h | 6 ++-- src/util/command.h | 8 +++--- src/util/debug.h | 6 ++-- src/util/decision_engine.h | 6 ++-- src/util/exception.h | 54 +++++++++++++++++------------------ src/util/literal.h | 6 ++-- src/util/model.h | 6 ++-- src/util/options.h | 6 ++-- src/util/result.h | 6 ++-- src/util/unique_id.h | 8 +++--- test/Makefile.am | 23 +++++++++++++++ test/expr/expr_black.h | 19 ++++++++++++ test/expr/expr_white.h | 19 ++++++++++++ test/no_cxxtest | 12 ++++++++ 57 files changed, 386 insertions(+), 213 deletions(-) create mode 100644 test/Makefile.am create mode 100644 test/expr/expr_black.h create mode 100644 test/expr/expr_white.h create mode 100755 test/no_cxxtest diff --git a/Makefile.am b/Makefile.am index 5b0f8d11a..74a28a51c 100644 --- a/Makefile.am +++ b/Makefile.am @@ -3,4 +3,7 @@ AM_CXXFLAGS = -Wall AUTOMAKE_OPTIONS = foreign ACLOCAL_AMFLAGS = -I config -SUBDIRS = src doc contrib +SUBDIRS = src test doc contrib + +.PHONY: test +test: check diff --git a/autogen.sh b/autogen.sh index a250f6b82..c9e4200da 100755 --- a/autogen.sh +++ b/autogen.sh @@ -8,4 +8,4 @@ touch NEWS README AUTHORS ChangeLog touch stamp-h aclocal -I config autoconf -I config -automake -ac --foreign +automake -ac --foreign -Woverride diff --git a/configure.ac b/configure.ac index 77c03ef2c..57dde9b35 100644 --- a/configure.ac +++ b/configure.ac @@ -43,6 +43,30 @@ AC_CHECK_PROG(DOXYGEN, doxygen, doxygen, []) if test -z "$DOXYGEN"; then AC_MSG_WARN([documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.]) fi +AC_ARG_VAR(DOXYGEN, [location of doxygen binary]) + +CXXTESTGEN= +AC_PATH_PROG(CXXTESTGEN, cxxtestgen.pl, [], [$CXXTEST:$PATH]) +if test -z "$CXXTESTGEN"; then + AC_MSG_NOTICE([unit tests disabled, cxxtestgen.pl not found.]) +elif test -z "$CXXTEST"; then + CXXTEST=$(dirname "$CXXTESTGEN") + AC_MSG_CHECKING([for location of CxxTest headers]) + if test -e "$CXXTEST/cxxtest/TestRunner.h"; then + AC_MSG_RESULT([$CXXTEST]) + else + AC_MSG_RESULT([not found]) + AC_MSG_WARN([unit tests disabled, CxxTest headers not found.]) + CXXTESTGEN= + CXXTEST= + fi +fi +AC_ARG_VAR(CXXTEST, [path to CxxTest installation]) +AM_CONDITIONAL([HAVE_CXXTESTGEN], [test -n "$CXXTESTGEN"]) + +AC_ARG_VAR(TEST_CPPFLAGS, [CXXFLAGS to use when testing (default=$CPPFLAGS)]) +AC_ARG_VAR(TEST_CXXFLAGS, [CXXFLAGS to use when testing (default=$CXXFLAGS)]) +AC_ARG_VAR(TEST_LDFLAGS, [LDFLAGS to use when testing (default=$LDFLAGS)]) # Checks for libraries. AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])]) @@ -84,6 +108,7 @@ AC_CONFIG_FILES([ src/context/Makefile src/parser/Makefile src/theory/Makefile + test/Makefile ]) AC_OUTPUT diff --git a/src/Makefile.am b/src/Makefile.am index 8b897bf0f..57a67d6e5 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -1,4 +1,5 @@ INCLUDES = -I@srcdir@/include -I@srcdir@ +AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = util expr context prop smt theory parser main diff --git a/src/context/Makefile.am b/src/context/Makefile.am index e3226e88b..00858fb7b 100644 --- a/src/context/Makefile.am +++ b/src/context/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libcontext.a diff --git a/src/context/context.h b/src/context/context.h index fce2f0b8d..6cc36ae9b 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -9,10 +9,11 @@ ** **/ -#ifndef __CVC4_CONTEXT_H -#define __CVC4_CONTEXT_H +#ifndef __CVC4__CONTEXT__CONTEXT_H +#define __CVC4__CONTEXT__CONTEXT_H namespace CVC4 { +namespace context { class Context; @@ -40,6 +41,7 @@ class CDList; template class CDSet; +}/* CVC4::context namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_CONTEXT_H */ +#endif /* __CVC4__CONTEXT__CONTEXT_H */ diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 6833f9f97..17b7d8dcd 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libexpr.a diff --git a/src/expr/attr_type.h b/src/expr/attr_type.h index d24385f8e..1d5e8eb0c 100644 --- a/src/expr/attr_type.h +++ b/src/expr/attr_type.h @@ -9,12 +9,13 @@ ** **/ -#ifndef __CVC4_ATTR_TYPE_H -#define __CVC4_ATTR_TYPE_H +#ifndef __CVC4__EXPR__ATTR_TYPE_H +#define __CVC4__EXPR__ATTR_TYPE_H #include "expr_attribute.h" namespace CVC4 { +namespace expr { class Type; @@ -29,6 +30,7 @@ public: extern AttrTable type_table; -} /* CVC4 namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_ATTR_TYPE_H */ +#endif /* __CVC4__EXPR__ATTR_TYPE_H */ diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index b6484ef25..f1b334ff8 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -14,33 +14,31 @@ #include "expr_value.h" #include "expr_builder.h" +using namespace CVC4::expr; + namespace CVC4 { Expr Expr::s_null(0); Expr::Expr(ExprValue* ev) : d_ev(ev) { - // FIXME: thread-safety - ++d_ev->d_rc; + d_ev->inc(); } Expr::Expr(const Expr& e) { - // FIXME: thread-safety if((d_ev = e.d_ev)) - ++d_ev->d_rc; + d_ev->inc(); } Expr::~Expr() { - // FIXME: thread-safety - --d_ev->d_rc; + d_ev->dec(); } Expr& Expr::operator=(const Expr& e) { - // FIXME: thread-safety if(d_ev) - --d_ev->d_rc; + d_ev->dec(); if((d_ev = e.d_ev)) - ++d_ev->d_rc; + d_ev->inc(); return *this; } @@ -97,4 +95,4 @@ Expr Expr::substExpr(const std::vector& oldTerms, return ExprBuilder(*this).substExpr(oldTerms, newTerms); } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_attribute.h b/src/expr/expr_attribute.h index 3525a8370..b44c9af6f 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_EXPR_ATTRIBUTE_H -#define __CVC4_EXPR_ATTRIBUTE_H +#ifndef __CVC4__EXPR__EXPR_ATTRIBUTE_H +#define __CVC4__EXPR__EXPR_ATTRIBUTE_H // TODO WARNING this file needs work ! @@ -20,6 +20,7 @@ #include "cvc4_expr.h" namespace CVC4 { +namespace expr { template class AttrTables; @@ -93,6 +94,7 @@ class AttributeTable { }; -} /* CVC4 namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_ATTRIBUTE_H */ +#endif /* __CVC4__EXPR__EXPR_ATTRIBUTE_H */ diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index 2f7114a9b..3b0cf4041 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -139,43 +139,41 @@ void ExprBuilder::addChild(const Expr& e) { v->reserve(nchild_thresh + 5); for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { v->push_back(Expr(*i)); - i->dec(); + (*i)->dec(); } - v.push_back(e); + v->push_back(e); d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { - d_children.u_vec.push_back(e); + d_children.u_vec->push_back(e); ++d_nchildren; } else { - ExprValue *ev = e->d_ev; + ExprValue *ev = e.d_ev; d_children.u_arr[d_nchildren] = ev; ev->inc(); ++d_nchildren; } - return *this; } -void ExprBuilder::addChild(const ExprValue* ev) { +void ExprBuilder::addChild(ExprValue* ev) { if(d_nchildren == nchild_thresh) { vector* v = new vector(); v->reserve(nchild_thresh + 5); for(ExprValue** i = d_children.u_arr; i != d_children.u_arr + nchild_thresh; ++i) { v->push_back(Expr(*i)); - i->dec(); + (*i)->dec(); } - v.push_back(Expr(ev)); + v->push_back(Expr(ev)); d_children.u_vec = v; ++d_nchildren; } else if(d_nchildren > nchild_thresh) { - d_children.u_vec.push_back(Expr(ev)); + d_children.u_vec->push_back(Expr(ev)); ++d_nchildren; } else { d_children.u_arr[d_nchildren] = ev; ev->inc(); ++d_nchildren; } - return *this; } void ExprBuilder::collapse() { @@ -184,7 +182,6 @@ void ExprBuilder::collapse() { v->reserve(nchild_thresh + 5); } - return *this; } // not const @@ -206,4 +203,4 @@ PlusExprBuilder ExprBuilder::operator- (Expr) { MultExprBuilder ExprBuilder::operator* (Expr) { } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 1104c17f5..fc303572d 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_EXPR_BUILDER_H -#define __CVC4_EXPR_BUILDER_H +#ifndef __CVC4__EXPR_BUILDER_H +#define __CVC4__EXPR_BUILDER_H #include #include "expr_manager.h" @@ -42,13 +42,13 @@ class ExprBuilder { } d_children; void addChild(const Expr&); - void addChild(const ExprValue*); + void addChild(ExprValue*); void collapse(); typedef ExprValue** ev_iterator; typedef ExprValue const** const_ev_iterator; - void reset(const ExprValue*); + ExprBuilder& reset(const ExprValue*); public: @@ -154,6 +154,6 @@ public: };/* class MultExprBuilder */ -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_BUILDER_H */ +#endif /* __CVC4__EXPR_BUILDER_H */ diff --git a/src/expr/expr_manager.cpp b/src/expr/expr_manager.cpp index 80091bef6..a65a2f3cd 100644 --- a/src/expr/expr_manager.cpp +++ b/src/expr/expr_manager.cpp @@ -49,4 +49,4 @@ Expr ExprManager::mkExpr(Kind kind, std::vector children) { return ExprBuilder(this, kind).append(children); } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 7e0da01c6..802cfe9c0 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_EXPR_MANAGER_H -#define __CVC4_EXPR_MANAGER_H +#ifndef __CVC4__EXPR_MANAGER_H +#define __CVC4__EXPR_MANAGER_H #include #include "cvc4_expr.h" @@ -53,6 +53,6 @@ public: // do we want a varargs one? perhaps not.. }; -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_MANAGER_H */ +#endif /* __CVC4__EXPR_MANAGER_H */ diff --git a/src/expr/expr_value.cpp b/src/expr/expr_value.cpp index 451538f3f..fa5628e26 100644 --- a/src/expr/expr_value.cpp +++ b/src/expr/expr_value.cpp @@ -76,4 +76,4 @@ ExprValue::const_iterator ExprValue::rend() const { return d_children - 1; } -} /* CVC4 namespace */ +}/* CVC4 namespace */ diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index 4b4b4f612..88984d286 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -14,14 +14,19 @@ ** reference count on ExprValue instances and **/ -#ifndef __CVC4_EXPR_VALUE_H -#define __CVC4_EXPR_VALUE_H +#ifndef __CVC4__EXPR__EXPR_VALUE_H +#define __CVC4__EXPR__EXPR_VALUE_H #include #include "cvc4_expr.h" namespace CVC4 { +class Expr; +class ExprBuilder; + +namespace expr { + /** * This is an ExprValue. */ @@ -47,11 +52,13 @@ class ExprValue { /** Variable number of child nodes */ Expr d_children[0]; - friend class Expr; - friend class ExprBuilder; + // todo add exprMgr ref in debug case + + friend class CVC4::Expr; + friend class CVC4::ExprBuilder; - ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; } - ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; } + ExprValue* inc(); + ExprValue* dec(); public: /** Hash this expression. @@ -74,6 +81,7 @@ public: const_iterator rend() const; }; -} /* CVC4 namespace */ +}/* CVC4::expr namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_EXPR_VALUE_H */ +#endif /* __CVC4__EXPR__EXPR_VALUE_H */ diff --git a/src/expr/kind.h b/src/expr/kind.h index 9c4e4d5ab..98cc7e2e3 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_KIND_H -#define __CVC4_KIND_H +#ifndef __CVC4__KIND_H +#define __CVC4__KIND_H namespace CVC4 { @@ -19,20 +19,32 @@ namespace CVC4 { // placeholder for design & development work. enum Kind { + /* undefined */ UNDEFINED_KIND = -1, + + /* built-ins */ EQUAL, + ITE, + SKOLEM, + VARIABLE, + + /* propositional connectives */ + FALSE, + TRUE, + + NOT, + AND, + IFF, OR, XOR, - NOT, + + /* from arith */ PLUS, - MINUS, - ITE, - IFF, - SKOLEM, - SUBST + MINUS + };/* enum Kind */ }/* CVC4 namespace */ -#endif /* __CVC4_KIND_H */ +#endif /* __CVC4__KIND_H */ diff --git a/src/include/cvc4.h b/src/include/cvc4.h index 109496001..c5e3bb013 100644 --- a/src/include/cvc4.h +++ b/src/include/cvc4.h @@ -9,10 +9,10 @@ ** **/ -#ifndef __CVC4_VC_H -#define __CVC4_VC_H +#ifndef __CVC4_H +#define __CVC4_H -#include "command.h" +#include "util/command.h" #include "cvc4_expr.h" /* TODO provide way of querying whether you fall into a fragment / @@ -37,6 +37,6 @@ public: void query(Expr); }; -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_VC_H */ +#endif /* __CVC4_H */ diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index 3d7a35fc8..1f5ac659d 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -15,10 +15,15 @@ #include #include +#include "expr/kind.h" namespace CVC4 { -class ExprValue; +namespace expr { + class ExprValue; +}/* CVC4::expr namespace */ + +using CVC4::expr::ExprValue; /** * Encapsulation of an ExprValue pointer. The reference count is @@ -41,6 +46,8 @@ class Expr { typedef Expr* iterator; typedef Expr const* const_iterator; + friend class ExprBuilder; + public: Expr(const Expr&); @@ -69,11 +76,22 @@ public: Expr substExpr(const std::vector& oldTerms, const std::vector& newTerms) const; + inline Kind getKind() const; + static Expr null() { return s_null; } - friend class ExprBuilder; };/* class Expr */ -} /* CVC4 namespace */ +}/* CVC4 namespace */ + +#include "expr/expr_value.h" + +namespace CVC4 { + +inline Kind Expr::getKind() const { + return Kind(d_ev->d_kind); +} + +}/* CVC4 namespace */ #endif /* __CVC4_EXPR_H */ diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 3b2ccb05a..8f400241b 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden bin_PROGRAMS = cvc4 diff --git a/src/main/about.h b/src/main/about.h index f582debf0..e02183ba7 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -1,8 +1,8 @@ -#ifndef __CVC4_ABOUT_H -#define __CVC4_ABOUT_H +#ifndef __CVC4__MAIN__ABOUT_H +#define __CVC4__MAIN__ABOUT_H namespace CVC4 { -namespace Main { +namespace main { const char about[] = "\ This is a pre-release of CVC4.\n\ @@ -11,7 +11,7 @@ Copyright (C) 2009 The ACSys Group\n\ New York University\n\ "; -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ #endif /* __CVC4_MAIN_H */ diff --git a/src/main/main.cpp b/src/main/main.cpp index 4850d475f..d2c6cb26d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -36,6 +36,15 @@ int main(int argc, char *argv[]) { throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno)); exit(1); } + + // ExprManager *exprMgr = ...; + // SmtEngine smt(exprMgr, &opts); + // Parser parser(infile, exprMgr, &opts); + // while(!parser.done) { + // Command *cmd = parser.get(); + // cmd->invoke(smt); + // delete cmd; + // } } } catch(CVC4::Main::OptionException* e) { if(opts.smtcomp_mode) { diff --git a/src/main/main.h b/src/main/main.h index 4101f4fe4..d0a517967 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -6,11 +6,11 @@ #include "util/exception.h" #include "util/options.h" -#ifndef __CVC4_MAIN_H -#define __CVC4_MAIN_H +#ifndef __CVC4__MAIN__MAIN_H +#define __CVC4__MAIN__MAIN_H namespace CVC4 { -namespace Main { +namespace main { class OptionException : public CVC4::Exception { public: @@ -20,7 +20,7 @@ public: int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*); void cvc4_init() throw(); -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_MAIN_H */ +#endif /* __CVC4__MAIN__MAIN_H */ diff --git a/src/main/usage.h b/src/main/usage.h index 971ba7640..edc9ad1d1 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -1,8 +1,8 @@ -#ifndef __CVC4_USAGE_H -#define __CVC4_USAGE_H +#ifndef __CVC4__MAIN__USAGE_H +#define __CVC4__MAIN__USAGE_H namespace CVC4 { -namespace Main { +namespace main { // no more % chars in here without being escaped; it's used as a // printf() format string @@ -23,7 +23,7 @@ CVC4 options:\n\ --stats give statistics on exit\n\ "; -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_USAGE_H */ +#endif /* __CVC4__MAIN__USAGE_H */ diff --git a/src/main/util.cpp b/src/main/util.cpp index da4d4b0c0..63c8cc860 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -16,12 +16,12 @@ namespace Main { void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); - exit(info->si_signo + 128); + abort(); } void segv_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 suffered a segfault.\n"); - exit(info->si_signo + 128); + abort(); } void cvc4_init() throw() { diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am index 918ab2fb2..2a1b83dba 100644 --- a/src/parser/Makefile.am +++ b/src/parser/Makefile.am @@ -1,5 +1,5 @@ -INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -I@builddir@ +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libparser.a diff --git a/src/parser/parser.h b/src/parser/parser.h index 967f20e95..36b8c34eb 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -10,13 +10,14 @@ ** Parser abstraction. **/ -#ifndef __CVC4_PARSER_H -#define __CVC4_PARSER_H +#ifndef __CVC4__PARSER__PARSER_H +#define __CVC4__PARSER__PARSER_H #include "core/exception.h" #include "core/lang.h" namespace CVC4 { +namespace parser { class ValidityChecker; class Expr; @@ -59,6 +60,7 @@ namespace CVC4 { class ParserTemp; extern ParserTemp* parserTemp; +}/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_PARSER_H */ +#endif /* __CVC4__PARSER__PARSER_H */ diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index 18f027e44..89490fad8 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -10,14 +10,15 @@ ** Exception class. **/ -#ifndef __CVC4_PARSER_EXCEPTION_H -#define __CVC4_PARSER_EXCEPTION_H +#ifndef __CVC4__PARSER__PARSER_EXCEPTION_H +#define __CVC4__PARSER__PARSER_EXCEPTION_H -#include "core/exception.h" +#include "util/exception.h" #include #include namespace CVC4 { +namespace parser { class ParserException: public Exception { public: @@ -32,6 +33,7 @@ namespace CVC4 { } }; // end of class ParserException +}/* CVC4::parser namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_PARSER_EXCEPTION_H */ +#endif /* __CVC4__PARSER__PARSER_EXCEPTION_H */ diff --git a/src/parser/parser_state.h b/src/parser/parser_state.h index f82980196..c1fd0ae96 100644 --- a/src/parser/parser_state.h +++ b/src/parser/parser_state.h @@ -14,17 +14,19 @@ ** New York University **/ -#ifndef __CVC4_PARSER_STATE_H -#define __CVC4_PARSER_STATE_H +#ifndef __CVC4__PARSER__PARSER_STATE_H +#define __CVC4__PARSER__PARSER_STATE_H #include #include #include "cvc4_expr.h" -#include "exception.h" +#include "util/exception.h" namespace CVC4 { -class ValidityChecker; +class SmtEngine; + +namespace parser { class ParserState { private: @@ -37,7 +39,7 @@ private: // The currently used prompt std::string prompt; public: - ValidityChecker* vc; + SmtEngine* vc; std::istream* is; // The current input line int lineNum; @@ -89,6 +91,7 @@ public: void setPrompt2() { prompt = prompt2; } }; -} /* CVC4 namespace */ +}/* CVC4::parser namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_PARSER_STATE_H */ +#endif /* __CVC4__PARSER__PARSER_STATE_H */ diff --git a/src/parser/pl.ypp b/src/parser/pl.ypp index d8fd57c8c..012f468eb 100644 --- a/src/parser/pl.ypp +++ b/src/parser/pl.ypp @@ -13,19 +13,22 @@ %{ -#include "vc.h" -#include "parser_exception.h" -#include "parser_state.h" +#include "cvc4.h" +#include "parser/parser_exception.h" +#include "parser/parser_state.h" //#include "rational.h" // Exported shared data namespace CVC4 { - extern ParserState* parserState; -} + namespace parser { + extern ParserState* parserState; + }/* CVC4::parser namespace */ +}/* CVC4 hnamespace */ + // Define shortcuts for various things -#define TMP CVC4::parserState -#define EXPR CVC4::parserState->expr -#define VC (CVC4::parserState->vc) +#define TMP CVC4::parser::parserState +#define EXPR CVC4::parser::parserState->expr +#define VC (CVC4::parser::parserState->vc) #define RAT(args) CVC4::newRational args // Suppress the bogus warning suppression in bison (it generates @@ -38,9 +41,9 @@ extern int PLlex(void); int PLerror(const char *s) { std::ostringstream ss; - ss << CVC4::parserState->fileName << ":" << CVC4::parserState->lineNum + ss << CVC4::parser::parserState->fileName << ":" << CVC4::parser::parserState->lineNum << ": " << s; - return CVC4::parserState->error(ss.str()); + return CVC4::parser::parserState->error(ss.str()); } diff --git a/src/parser/pl_scanner.lpp b/src/parser/pl_scanner.lpp index ba8a8e85d..262eb5c88 100644 --- a/src/parser/pl_scanner.lpp +++ b/src/parser/pl_scanner.lpp @@ -21,30 +21,32 @@ %{ #include -#include "expr_manager.h" /* for the benefit of parsePL_defs.h */ -#include "parser_state.h" -#include "pl.hpp" -#include "debug.h" +#include "expr/expr_manager.h" /* for the benefit of parsePL_defs.h */ +#include "parser/parser_state.h" +#include "parser/pl.hpp" +#include "util/debug.h" namespace CVC4 { - extern ParserState* parserState; -} + namespace parser { + extern ParserState* parserState; + }/* CVC4::parser namespace */ +}/* CVC4 namespace */ extern int PL_inputLine; extern char *PLtext; -extern int PLerror (const char *msg); +extern int PLerror(const char *msg); static int PLinput(std::istream& is, char* buf, int size) { int res; if(is) { // If interactive, read line by line; otherwise read as much as we // can gobble - if(CVC4::parserState->interactive) { + if(CVC4::parser::parserState->interactive) { // Print the current prompt - std::cout << CVC4::parserState->getPrompt() << std::flush; + std::cout << CVC4::parser::parserState->getPrompt() << std::flush; // Set the prompt to "middle of the command" one - CVC4::parserState->setPrompt2(); + CVC4::parser::parserState->setPrompt2(); // Read the line is.getline(buf, size-1); } else // Set the terminator char to 0 @@ -69,7 +71,7 @@ static int PLinput(std::istream& is, char* buf, int size) { // Redefine the input buffer function to read from an istream #define YY_INPUT(buf,result,max_size) \ - result = PLinput(*CVC4::parserState->is, buf, max_size); + result = PLinput(*CVC4::parser::parserState->is, buf, max_size); int PL_bufSize() { return YY_BUF_SIZE; } YY_BUFFER_STATE PL_buf_state() { return YY_CURRENT_BUFFER; } @@ -123,7 +125,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) %% -[\n] { CVC4::parserState->lineNum++; } +[\n] { CVC4::parser::parserState->lineNum++; } [ \t\r\f] { /* skip whitespace */ } @@ -136,7 +138,7 @@ ANYTHING ({LETTER}|{DIGIT}|{OPCHAR}) "%" { BEGIN COMMENT; } "\n" { BEGIN INITIAL; /* return to normal mode */ - CVC4::parserState->lineNum++; } + CVC4::parser::parserState->lineNum++; } . { /* stay in comment mode */ } "\"" { BEGIN STRING_LITERAL; diff --git a/src/parser/smtlib.ypp b/src/parser/smtlib.ypp index 0f3aa8cf4..692a9cda5 100644 --- a/src/parser/smtlib.ypp +++ b/src/parser/smtlib.ypp @@ -11,9 +11,9 @@ ** commands in SMT-LIB language. **/ -#include "vc.h" -#include "parser_exception.h" -#include "parser_state.h" +#include "cvc4.h" +#include "parser/parser_exception.h" +#include "parser/parser_state.h" // Exported shared data namespace CVC4 { diff --git a/src/parser/smtlib_scanner.lpp b/src/parser/smtlib_scanner.lpp index bb5802aed..b367b0d93 100644 --- a/src/parser/smtlib_scanner.lpp +++ b/src/parser/smtlib_scanner.lpp @@ -20,8 +20,8 @@ %{ #include -#include "smtlib.hpp" -#include "debug.h" +#include "parser/smtlib.hpp" +#include "util/debug.h" namespace CVC4 { extern ParserTemp* parserTemp; diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am index 5051420a2..941b0c653 100644 --- a/src/prop/Makefile.am +++ b/src/prop/Makefile.am @@ -1,4 +1,4 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden SUBDIRS = minisat diff --git a/src/prop/minisat/Makefile.am b/src/prop/minisat/Makefile.am index 74d72d48d..97cfc438a 100644 --- a/src/prop/minisat/Makefile.am +++ b/src/prop/minisat/Makefile.am @@ -1,4 +1,5 @@ INCLUDES = -I@srcdir@/mtl -I@srcdir@/core -I@srcdir@/../../include +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libminisat.a libminisat_a_SOURCES = \ diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 0febd2927..5572b47f7 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -9,14 +9,15 @@ ** **/ -#ifndef __CVC4_PROP_ENGINE_H -#define __CVC4_PROP_ENGINE_H +#ifndef __CVC4__PROP__PROP_ENGINE_H +#define __CVC4__PROP__PROP_ENGINE_H #include "core/cvc4_expr.h" #include "core/decision_engine.h" #include "core/theory_engine.h" namespace CVC4 { +namespace prop { // In terms of abstraction, this is below (and provides services to) // Prover and above (and requires the services of) a specific @@ -38,6 +39,7 @@ public: };/* class PropEngine */ -} +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_PROP_ENGINE_H */ +#endif /* __CVC4__PROP__PROP_ENGINE_H */ diff --git a/src/prop/sat.h b/src/prop/sat.h index 00a94c142..32ca9e983 100644 --- a/src/prop/sat.h +++ b/src/prop/sat.h @@ -9,11 +9,13 @@ ** **/ -#ifndef __CVC4_SAT_H -#define __CVC4_SAT_H +#ifndef __CVC4__PROP__SAT_H +#define __CVC4__PROP__SAT_H namespace CVC4 { +namespace prop { -} /* CVC4 namespace */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_SAT_H */ +#endif /* __CVC4__PROP__SAT_H */ diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am index f719b1283..ff740aa56 100644 --- a/src/smt/Makefile.am +++ b/src/smt/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libsmt.a diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 6f6fb355a..078bf9cde 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_PROVER_H -#define __CVC4_PROVER_H +#ifndef __CVC4__SMT__SMT_ENGINE_H +#define __CVC4__SMT__SMT_ENGINE_H #include #include "core/cvc4_expr.h" @@ -22,6 +22,7 @@ // PropEngine. namespace CVC4 { +namespace smt { // TODO: SAT layer (esp. CNF- versus non-clausal solvers under the // hood): use a type parameter and have check() delegate, or subclass @@ -109,6 +110,7 @@ public: void pop(); };/* class SmtEngine */ -} /* CVC4 namespace */ +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_PROVER_H */ +#endif /* __CVC4__SMT__SMT_ENGINE_H */ diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am index 5c64f4f38..f022d0445 100644 --- a/src/theory/Makefile.am +++ b/src/theory/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libtheory.a diff --git a/src/theory/theory.h b/src/theory/theory.h index eeaba58d1..05e8e1b01 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -9,13 +9,14 @@ ** **/ -#ifndef __CVC4_THEORY_H -#define __CVC4_THEORY_H +#ifndef __CVC4__THEORY__THEORY_H +#define __CVC4__THEORY__THEORY_H #include "core/cvc4_expr.h" #include "core/literal.h" namespace CVC4 { +namespace theory { /** * Base class for T-solvers. Abstract DPLL(T). @@ -78,6 +79,7 @@ public: };/* class Theory */ +}/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_THEORY_H */ +#endif /* __CVC4__THEORY__THEORY_H */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 2a0841d8d..fead8e224 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -9,10 +9,11 @@ ** **/ -#ifndef __CVC4_THEORY_ENGINE_H -#define __CVC4_THEORY_ENGINE_H +#ifndef __CVC4__THEORY__THEORY_ENGINE_H +#define __CVC4__THEORY__THEORY_ENGINE_H namespace CVC4 { +namespace theory { // In terms of abstraction, this is below (and provides services to) // PropEngine. @@ -27,6 +28,7 @@ class TheoryEngine { public: };/* class TheoryEngine */ +}/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4_THEORY_ENGINE_H */ +#endif /* __CVC4__THEORY__THEORY_ENGINE_H */ diff --git a/src/util/Makefile.am b/src/util/Makefile.am index de5f0da9d..415893680 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -1,5 +1,5 @@ INCLUDES = -I@srcdir@/../include -I@srcdir@/.. -AM_CXXFLAGS = -Wall +AM_CXXFLAGS = -Wall -fvisibility=hidden noinst_LIBRARIES = libutil.a diff --git a/src/util/assert.h b/src/util/assert.h index a66503641..24e3a4cdf 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_ASSERT_H -#define __CVC4_ASSERT_H +#ifndef __CVC4__ASSERT_H +#define __CVC4__ASSERT_H #include @@ -23,4 +23,4 @@ # define cvc4assert(x) #endif /* DEBUG */ -#endif /* __CVC4_ASSERT_H */ +#endif /* __CVC4__ASSERT_H */ diff --git a/src/util/command.h b/src/util/command.h index 944b9c621..d1257f323 100644 --- a/src/util/command.h +++ b/src/util/command.h @@ -9,14 +9,14 @@ ** **/ -#ifndef __CVC4_COMMAND_H -#define __CVC4_COMMAND_H +#ifndef __CVC4__COMMAND_H +#define __CVC4__COMMAND_H namespace CVC4 { class Command { // distinct from Exprs }; -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_COMMAND_H */ +#endif /* __CVC4__COMMAND_H */ diff --git a/src/util/debug.h b/src/util/debug.h index 36942d1ae..14dc0fbd1 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_DEBUG_H -#define __CVC4_DEBUG_H +#ifndef __CVC4__DEBUG_H +#define __CVC4__DEBUG_H #include @@ -23,4 +23,4 @@ # define cvc4assert(x) #endif /* DEBUG */ -#endif /* __CVC4_DEBUG_H */ +#endif /* __CVC4__DEBUG_H */ diff --git a/src/util/decision_engine.h b/src/util/decision_engine.h index 81d820eaa..2064e3687 100644 --- a/src/util/decision_engine.h +++ b/src/util/decision_engine.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_DECISION_ENGINE_H -#define __CVC4_DECISION_ENGINE_H +#ifndef __CVC4__DECISION_ENGINE_H +#define __CVC4__DECISION_ENGINE_H #include "core/literal.h" @@ -39,4 +39,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4_DECISION_ENGINE_H */ +#endif /* __CVC4__DECISION_ENGINE_H */ diff --git a/src/util/exception.h b/src/util/exception.h index 792a98701..e3b8f2293 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -10,39 +10,39 @@ ** Exception class. **/ -#ifndef __CVC4_EXCEPTION_H -#define __CVC4_EXCEPTION_H +#ifndef __CVC4__EXCEPTION_H +#define __CVC4__EXCEPTION_H #include #include namespace CVC4 { - class Exception { - protected: - std::string d_msg; - public: - // Constructors - Exception(): d_msg("Unknown exception") { } - Exception(const std::string& msg): d_msg(msg) { } - Exception(const char* msg): d_msg(msg) { } - // Destructor - virtual ~Exception() { } - // NON-VIRTUAL METHODs for setting and printing the error message - void setMessage(const std::string& msg) { d_msg = msg; } - // Printing: feel free to redefine toString(). When inherited, - // it's recommended that this method print the type of exception - // before the actual message. - virtual std::string toString() const { return d_msg; } - // No need to overload operator<< for the inherited classes - friend std::ostream& operator<<(std::ostream& os, const Exception& e); - - }; // end of class Exception - - inline std::ostream& operator<<(std::ostream& os, const Exception& e) { - return os << e.toString(); - } +class Exception { +protected: + std::string d_msg; +public: + // Constructors + Exception(): d_msg("Unknown exception") { } + Exception(const std::string& msg): d_msg(msg) { } + Exception(const char* msg): d_msg(msg) { } + // Destructor + virtual ~Exception() { } + // NON-VIRTUAL METHODs for setting and printing the error message + void setMessage(const std::string& msg) { d_msg = msg; } + // Printing: feel free to redefine toString(). When inherited, + // it's recommended that this method print the type of exception + // before the actual message. + virtual std::string toString() const { return d_msg; } + // No need to overload operator<< for the inherited classes + friend std::ostream& operator<<(std::ostream& os, const Exception& e); + +}; // end of class Exception + +inline std::ostream& operator<<(std::ostream& os, const Exception& e) { + return os << e.toString(); +} }/* CVC4 namespace */ -#endif /* __CVC4_EXCEPTION_H */ +#endif /* __CVC4__EXCEPTION_H */ diff --git a/src/util/literal.h b/src/util/literal.h index 8b147c640..7af9826bb 100644 --- a/src/util/literal.h +++ b/src/util/literal.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_LITERAL_H -#define __CVC4_LITERAL_H +#ifndef __CVC4__LITERAL_H +#define __CVC4__LITERAL_H namespace CVC4 { @@ -18,4 +18,4 @@ class Literal; }/* CVC4 namespace */ -#endif /* __CVC4_LITERAL_H */ +#endif /* __CVC4__LITERAL_H */ diff --git a/src/util/model.h b/src/util/model.h index c07b75dfa..cf006b3e1 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_MODEL_H -#define __CVC4_MODEL_H +#ifndef __CVC4__MODEL_H +#define __CVC4__MODEL_H namespace CVC4 { @@ -19,4 +19,4 @@ class Model { }/* CVC4 namespace */ -#endif /* __CVC4_MODEL_H */ +#endif /* __CVC4__MODEL_H */ diff --git a/src/util/options.h b/src/util/options.h index f04b06f10..6104470d2 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -1,5 +1,5 @@ -#ifndef __CVC4_OPTIONS_H -#define __CVC4_OPTIONS_H +#ifndef __CVC4__OPTIONS_H +#define __CVC4__OPTIONS_H namespace CVC4 { @@ -28,4 +28,4 @@ struct Options { }/* CVC4 namespace */ -#endif /* __CVC4_OPTIONS_H */ +#endif /* __CVC4__OPTIONS_H */ diff --git a/src/util/result.h b/src/util/result.h index 50f488682..1e2b61738 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_RESULT_H -#define __CVC4_RESULT_H +#ifndef __CVC4__RESULT_H +#define __CVC4__RESULT_H namespace CVC4 { @@ -62,4 +62,4 @@ public: }/* CVC4 namespace */ -#endif /* __CVC4_RESULT_H */ +#endif /* __CVC4__RESULT_H */ diff --git a/src/util/unique_id.h b/src/util/unique_id.h index 1a6f3427a..4ac80f772 100644 --- a/src/util/unique_id.h +++ b/src/util/unique_id.h @@ -9,8 +9,8 @@ ** **/ -#ifndef __CVC4_UNIQUE_ID_H -#define __CVC4_UNIQUE_ID_H +#ifndef __CVC4__UNIQUE_ID_H +#define __CVC4__UNIQUE_ID_H namespace CVC4 { @@ -30,6 +30,6 @@ public: template unsigned UniqueID::s_topID = 0; -} /* CVC4 namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4_UNIQUE_ID_H */ +#endif /* __CVC4__UNIQUE_ID_H */ diff --git a/test/Makefile.am b/test/Makefile.am new file mode 100644 index 000000000..bf74eaa47 --- /dev/null +++ b/test/Makefile.am @@ -0,0 +1,23 @@ +if HAVE_CXXTESTGEN + +AM_CPPFLAGS = -I. "-I$(CXXTEST)" "-I@top_srcdir@/src/include" "-I@top_srcdir@/src" +AM_CXXFLAGS = -fno-access-control +AM_LDFLAGS = -L@top_builddir@/src/libcvc4.a +TESTS = \ + expr/expr_black \ + expr/expr_white + +%.cpp: %.h + $(CXXTESTGEN) --have-eh --have-std --error-printer -o $@ $< +%: %.cpp + $(CXX) $(TEST_CPPFLAGS) $(AM_CPPFLAGS) $(TEST_CXXFLAGS) $(AM_CXXFLAGS) -o $@ $(TEST_LDFLAGS) $(AM_LDFLAGS) $< @top_builddir@/src/libcvc4.a + +MOSTLYCLEANFILES = $(TESTS) $(TESTS:%=%.cpp) + +else + +# force a user-visible failure for "make check" +TESTS = no_cxxtest + +endif + diff --git a/test/expr/expr_black.h b/test/expr/expr_black.h new file mode 100644 index 000000000..97746d1c4 --- /dev/null +++ b/test/expr/expr_black.h @@ -0,0 +1,19 @@ +/* Black box testing of CVC4::Expr. */ + +#include + +#include "cvc4_expr.h" + +using namespace CVC4; + +class ExprBlack : public CxxTest::TestSuite { +public: + + void testNull() { + Expr::s_null; + } + + void testCopyCtor() { + Expr e(Expr::s_null); + } +}; diff --git a/test/expr/expr_white.h b/test/expr/expr_white.h new file mode 100644 index 000000000..b6bfdd394 --- /dev/null +++ b/test/expr/expr_white.h @@ -0,0 +1,19 @@ +/* White box testing of CVC4::Expr. */ + +#include + +#include "cvc4_expr.h" + +using namespace CVC4; + +class ExprWhite : public CxxTest::TestSuite { +public: + + void testNull() { + Expr::s_null; + } + + void testCopyCtor() { + Expr e(Expr::s_null); + } +}; diff --git a/test/no_cxxtest b/test/no_cxxtest new file mode 100755 index 000000000..cf8b8d729 --- /dev/null +++ b/test/no_cxxtest @@ -0,0 +1,12 @@ +#!/bin/sh + +echo +echo '***************************************************************************' +echo '* *' +echo '* ERROR: CxxTest was not found at configure-time; tests cannot be run. *' +echo '* *' +echo '***************************************************************************' +echo + +exit 1 + -- 2.30.2