From: Morgan Deters Date: Tue, 24 Nov 2009 21:03:35 +0000 (+0000) Subject: configure option adjustments as per 11/24 meeting; various fixes and improvements X-Git-Tag: cvc5-1.0.0~9415 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=811158832b74e3b101af2c7473f4e11a41377dd4;p=cvc5.git configure option adjustments as per 11/24 meeting; various fixes and improvements --- diff --git a/configure.ac b/configure.ac index b7e7975f7..0aba48aa3 100644 --- a/configure.ac +++ b/configure.ac @@ -8,29 +8,142 @@ AC_CONFIG_AUX_DIR([config]) AC_CONFIG_MACRO_DIR([config]) AM_INIT_AUTOMAKE(cvc4, prerelease) AC_CONFIG_HEADERS([config.h]) + +# keep track of whether the user set these (check here, because +# autoconf might set a default later) +if test -z "${CPPFLAGS+set}"; then user_cppflags=no; else user_cppflags=yes; fi +if test -z "${CXXFLAGS+set}"; then user_cxxflags=no; else user_cxxflags=yes; fi +if test -z "${LDFLAGS+set}" ; then user_ldflags=no ; else user_ldflags=yes ; fi + LT_INIT AC_LIBTOOL_WIN32_DLL # Features requested by the user -AC_MSG_CHECKING([whether to do a debug build of CVC4]) -AC_ARG_ENABLE([debug], [AS_HELP_STRING([--enable-debug] ,[do a debug build of CVC4])]) -if test -z "${enable_debug+set}"; then - enable_debug=no +AC_MSG_CHECKING([for requested build profile]) +AC_ARG_WITH([build], [AS_HELP_STRING([--with-build=profile], [for profile in {production,debug,default,competition}])]) +if test -z "${with_build+set}" -o "$with_build" = default; then + with_build=default +fi +if test "$user_cppflags" = no -a "$user_cxxflags" = no -a "$user_ldflags" = no -a -z "${enable_optimized+set}" -a -z "${enable_debug_symbols+set}" -a -z "${enable_assertions+set}" -a -z "${enable_tracing+set}" -a -z "${enable_muzzle+set}" -a -z "${enable_coverage+set}" -a -z "${enable_profiling+set}"; then + non_standard_build_profile=no +else + non_standard_build_profile=yes +fi +case "$with_build" in + production) + CVC4CPPFLAGS= + CVC4CXXFLAGS=-O3 + CVC4LDFLAGS= + if test -z "${enable_assertions+set}"; then enable_assertions=no ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + ;; + debug) + CVC4CPPFLAGS=-DCVC4_DEBUG + CVC4CXXFLAGS='-O0 -fno-inline -ggdb3' + CVC4LDFLAGS= + if test -z "${enable_assertions+set}"; then enable_assertions=yes ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + ;; + default) + CVC4CPPFLAGS= + CVC4CXXFLAGS=-O2 + CVC4LDFLAGS= + if test -z "${enable_assertions+set}"; then enable_assertions=yes ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + ;; + competition) + CVC4CPPFLAGS= + CVC4CXXFLAGS='-O9 -funroll-all-loops -fexpensive-optimizations -fno-enforce-eh-specs' + CVC4LDFLAGS= + if test -z "${enable_assertions+set}"; then enable_assertions=no ; fi + if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi + if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi + ;; + *) + AC_MSG_FAILURE([unknown build profile: $with_build]) + ;; +esac +AC_MSG_RESULT([$with_build]) + +AC_MSG_CHECKING([whether to optimize libcvc4]) +AC_ARG_ENABLE([optimized], [AS_HELP_STRING([--enable-optimized], [optimize the build])]) +if test -z "${enable_optimized+set}"; then + enable_optimized=no +fi +AC_MSG_RESULT([$enable_optimized]) +if test "$enable_optimized" = yes; then + CVC4CXXFLAGS="$CVC4CXXFLAGS -O3" +fi + +AC_MSG_CHECKING([whether to include debugging symbols in libcvc4]) +AC_ARG_ENABLE([debug-symbols], [AS_HELP_STRING([--disable-debug-symbols], [do not include debug symbols in libcvc4])]) +if test -z "${enable_debug_symbols+set}"; then + enable_debug_symbols=yes +fi +AC_MSG_RESULT([$enable_debug_symbols]) +if test "$enable_debug_symbols" = yes; then + CVC4CXXFLAGS="$CVC4CXXFLAGS -ggdb3" fi -AC_MSG_RESULT([$enable_debug]) AC_MSG_CHECKING([whether to include assertions in build]) -AC_ARG_ENABLE([assertions], [AS_HELP_STRING([--disable-assertions],[turn off assertions in build])]) +AC_ARG_ENABLE([assertions], [AS_HELP_STRING([--disable-assertions], [turn off assertions in build])]) if test -z "${enable_assertions+set}"; then enable_assertions=yes fi AC_MSG_RESULT([$enable_assertions]) +if test "$enable_assertions" = yes; then + CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_ASSERTIONS" +fi -if test "$enable_assertions" = no -a "$enable_debug" = yes; then - AC_MSG_FAILURE([when debugging is on, so must assertions be.]) +AC_MSG_CHECKING([whether to do a traceable build of CVC4]) +AC_ARG_ENABLE([tracing], [AS_HELP_STRING([--disable-tracing], [remove all tracing code from CVC4])]) +if test -z "${enable_tracing+set}"; then + enable_tracing=yes +fi +AC_MSG_RESULT([$enable_tracing]) +if test "$enable_tracing" = yes; then + CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_TRACING" +fi + +AC_MSG_CHECKING([whether to do a muzzled build of CVC4]) +AC_ARG_ENABLE([muzzle], [AS_HELP_STRING([--enable-muzzle], [completely silence CVC4; remove ALL non-result output from build])]) +if test -z "${enable_muzzle+set}"; then + enable_muzzle=no +fi +AC_MSG_RESULT([$enable_muzzle]) +if test "$enable_muzzle" = yes; then + CVC4CPPFLAGS="$CVC4CPPFLAGS -DCVC4_MUZZLE" +fi + +AC_MSG_CHECKING([whether to do a gcov-enabled build of CVC4]) +AC_ARG_ENABLE([coverage], [AS_HELP_STRING([--enable-coverage], [build with support for gcov coverage testing])]) +if test -z "${enable_coverage+set}"; then + enable_coverage=no +fi +AC_MSG_RESULT([$enable_coverage]) +if test "$enable_coverage" = yes; then + CVC4CXXFLAGS="$CVC4CXXFLAGS --coverage" + CVC4LDFLAGS="$CVC4LDFLAGS --coverage" +fi + +AC_MSG_CHECKING([whether to do a profiling-enabled build of CVC4]) +AC_ARG_ENABLE([profiling], [AS_HELP_STRING([--enable-profiling], [build with support for gprof profiling])]) +if test -z "${enable_profiling+set}"; then + enable_profiling=no +fi +AC_MSG_RESULT([$enable_profiling]) +if test "$enable_profiling" = yes; then + CVC4CXXFLAGS="$CVC4CXXFLAGS -pg" + CVC4LDFLAGS="$CVC4LDFLAGS -pg" fi + + + # Checks for programs. AC_PROG_CC AC_PROG_CXX @@ -93,13 +206,6 @@ AC_TYPE_SIZE_T # Checks for library functions. # Some definitions for config.h -if test "$enable_debug" = yes; then - AC_DEFINE([CVC4_DEBUG], [], [Whether or not to include debugging code.]) -fi - -if test "$enable_assertions" = yes; then - AC_DEFINE([CVC4_ASSERTIONS], [], [Whether or not assertions are enabled.]) -fi # Prepare configure output @@ -125,19 +231,67 @@ AC_CONFIG_FILES([ AC_OUTPUT # Final information to the user -debug=debug -if test "$enable_debug" = no; then - debug=non-debug -fi -withassertions=with -if test "$enable_assertions" = no; then - withassertions=without -fi cat < Mon, 02 Nov 2009 18:19:22 -0500 diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index 74030e810..a270e7362 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -103,6 +103,7 @@ sub recurse { last if $line =~ /^ \*\*\s*$/; } } else { + my $line = $_; print "adding\n"; if($file =~ /\.(y|yy|ypp|Y)$/) { print $OUT "%{/******************* -*- C++ -*- */\n"; @@ -119,6 +120,7 @@ sub recurse { print $OUT " **\n"; print $OUT " ** [[ Add file-specific comments here ]]\n"; print $OUT " **/\n\n"; + print $OUT $line; if($file =~ /\.(y|yy|ypp|Y)$/) { while(my $line = <$IN>) { chomp $line; diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp index f1b334ff8..e25cf8595 100644 --- a/src/expr/expr.cpp +++ b/src/expr/expr.cpp @@ -10,7 +10,7 @@ ** Reference-counted encapsulation of a pointer to an expression. **/ -#include "cvc4_expr.h" +#include "expr/expr.h" #include "expr_value.h" #include "expr_builder.h" diff --git a/src/expr/expr.h b/src/expr/expr.h new file mode 100644 index 000000000..d99708991 --- /dev/null +++ b/src/expr/expr.h @@ -0,0 +1,103 @@ +/********************* -*- C++ -*- */ +/** cvc4_expr.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Reference-counted encapsulation of a pointer to an expression. + **/ + +#ifndef __CVC4_EXPR_H +#define __CVC4_EXPR_H + +#include +#include + +#include "cvc4_config.h" +#include "expr/kind.h" + +namespace CVC4 { + +namespace expr { + class ExprValue; +}/* CVC4::expr namespace */ + +using CVC4::expr::ExprValue; + +/** + * Encapsulation of an ExprValue pointer. The reference count is + * maintained in the ExprValue. + */ +class CVC4_PUBLIC Expr { + /** A convenient null-valued encapsulated pointer */ + static Expr s_null; + + /** The referenced ExprValue */ + ExprValue* d_ev; + + /** This constructor is reserved for use by the Expr package; one + * must construct an Expr using one of the build mechanisms of the + * Expr package. + * + * Increments the reference count. */ + explicit Expr(ExprValue*); + + typedef Expr* iterator; + typedef Expr const* const_iterator; + + friend class ExprBuilder; + +public: + CVC4_PUBLIC Expr(const Expr&); + + /** Destructor. Decrements the reference count and, if zero, + * collects the ExprValue. */ + CVC4_PUBLIC ~Expr(); + + Expr& operator=(const Expr&) CVC4_PUBLIC; + + /** Access to the encapsulated expression. + * @return the encapsulated expression. */ + ExprValue* operator->() const CVC4_PUBLIC; + + uint64_t hash() const; + + Expr eqExpr(const Expr& right) const; + Expr notExpr() const; + Expr negate() const; // avoid double-negatives + Expr andExpr(const Expr& right) const; + Expr orExpr(const Expr& right) const; + Expr iteExpr(const Expr& thenpart, const Expr& elsepart) const; + Expr iffExpr(const Expr& right) const; + Expr impExpr(const Expr& right) const; + Expr xorExpr(const Expr& right) const; + Expr skolemExpr(int i) const; + Expr substExpr(const std::vector& oldTerms, + const std::vector& newTerms) const; + + Expr plusExpr(const Expr& right) const; + Expr uMinusExpr() const; + Expr multExpr(const Expr& right) const; + + inline Kind getKind() const; + + static Expr null() { return s_null; } + +};/* class Expr */ + +}/* 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/expr/expr_attribute.h b/src/expr/expr_attribute.h index b44c9af6f..03140c4eb 100644 --- a/src/expr/expr_attribute.h +++ b/src/expr/expr_attribute.h @@ -17,7 +17,7 @@ #include #include "config.h" #include "context/context.h" -#include "cvc4_expr.h" +#include "expr/expr.h" namespace CVC4 { namespace expr { diff --git a/src/expr/expr_builder.cpp b/src/expr/expr_builder.cpp index c5f366654..bf572cfbc 100644 --- a/src/expr/expr_builder.cpp +++ b/src/expr/expr_builder.cpp @@ -38,7 +38,7 @@ ExprBuilder& ExprBuilder::reset(const ExprValue* ev) { } ExprBuilder::ExprBuilder(const ExprBuilder& eb) : d_em(eb.d_em), d_kind(eb.d_kind), d_used(eb.d_used), d_nchildren(eb.d_nchildren) { - cvc4assert(!d_used); + Assert( !d_used ); if(d_nchildren > nchild_thresh) { d_children.u_vec = new vector(); @@ -74,59 +74,104 @@ ExprBuilder::~ExprBuilder() { // Compound expression constructors ExprBuilder& ExprBuilder::eqExpr(const Expr& right) { - if(d_kind != UNDEFINED_KIND && d_kind != EQUAL) + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != EQUAL )) { collapse(); - d_kind = EQUAL; + d_kind = EQUAL; + } + addChild(right); return *this; } ExprBuilder& ExprBuilder::notExpr() { - if(d_kind != UNDEFINED_KIND) - collapse(); + Assert( d_kind != UNDEFINED_KIND ); + collapse(); d_kind = NOT; return *this; } // avoid double-negatives ExprBuilder& ExprBuilder::negate() { - if(d_kind == NOT) + if(EXPECT_FALSE( d_kind == NOT )) return reset(d_children.u_arr[0]); - if(d_kind != UNDEFINED_KIND) - collapse(); + Assert( d_kind != UNDEFINED_KIND ); + collapse(); d_kind = NOT; return *this; } ExprBuilder& ExprBuilder::andExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(d_kind != AND) { + collapse(); + d_kind = AND; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::orExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != OR )) { + collapse(); + d_kind = OR; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::iteExpr(const Expr& thenpart, const Expr& elsepart) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = ITE; + addChild(thenpart); + addChild(elsepart); + return *this; } ExprBuilder& ExprBuilder::iffExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != IFF )) { + collapse(); + d_kind = IFF; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::impExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = IMPLIES; + addChild(right); + return *this; } ExprBuilder& ExprBuilder::xorExpr(const Expr& right) { + Assert( d_kind != UNDEFINED_KIND ); + if(EXPECT_TRUE( d_kind != XOR )) { + collapse(); + d_kind = XOR; + } + addChild(right); + return *this; } ExprBuilder& ExprBuilder::skolemExpr(int i) { -} - -ExprBuilder& ExprBuilder::substExpr(const std::vector& oldTerms, - const std::vector& newTerms) { + Assert( d_kind != UNDEFINED_KIND ); + collapse(); + d_kind = SKOLEM; + //addChild(i);//FIXME: int constant + return *this; } // "Stream" expression constructor syntax ExprBuilder& ExprBuilder::operator<<(const Kind& op) { + return *this; } ExprBuilder& ExprBuilder::operator<<(const Expr& child) { + return *this; } void ExprBuilder::addChild(const Expr& e) { @@ -182,21 +227,27 @@ void ExprBuilder::collapse() { // not const ExprBuilder::operator Expr() { + // FIXME } -AndExprBuilder ExprBuilder::operator&&(Expr) { +AndExprBuilder ExprBuilder::operator&&(Expr e) { + return AndExprBuilder(*this) && e; } -OrExprBuilder ExprBuilder::operator||(Expr) { +OrExprBuilder ExprBuilder::operator||(Expr e) { + return OrExprBuilder(*this) || e; } -PlusExprBuilder ExprBuilder::operator+ (Expr) { +PlusExprBuilder ExprBuilder::operator+ (Expr e) { + return PlusExprBuilder(*this) + e; } -PlusExprBuilder ExprBuilder::operator- (Expr) { +PlusExprBuilder ExprBuilder::operator- (Expr e) { + return PlusExprBuilder(*this) - e; } -MultExprBuilder ExprBuilder::operator* (Expr) { +MultExprBuilder ExprBuilder::operator* (Expr e) { + return MultExprBuilder(*this) * e; } }/* CVC4 namespace */ diff --git a/src/expr/expr_builder.h b/src/expr/expr_builder.h index 07d069a9e..97f18ca6d 100644 --- a/src/expr/expr_builder.h +++ b/src/expr/expr_builder.h @@ -109,6 +109,8 @@ class AndExprBuilder { public: + AndExprBuilder(const ExprBuilder&); + AndExprBuilder& operator&&(Expr); OrExprBuilder operator||(Expr); @@ -121,6 +123,8 @@ class OrExprBuilder { public: + OrExprBuilder(const ExprBuilder&); + AndExprBuilder operator&&(Expr); OrExprBuilder& operator||(Expr); @@ -133,6 +137,8 @@ class PlusExprBuilder { public: + PlusExprBuilder(const ExprBuilder&); + PlusExprBuilder& operator+(Expr); PlusExprBuilder& operator-(Expr); MultExprBuilder operator*(Expr); @@ -146,6 +152,8 @@ class MultExprBuilder { public: + MultExprBuilder(const ExprBuilder&); + PlusExprBuilder operator+(Expr); PlusExprBuilder operator-(Expr); MultExprBuilder& operator*(Expr); diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 802cfe9c0..e3fbd91bf 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -13,7 +13,7 @@ #define __CVC4__EXPR_MANAGER_H #include -#include "cvc4_expr.h" +#include "expr/expr.h" #include "kind.h" namespace CVC4 { diff --git a/src/expr/expr_value.h b/src/expr/expr_value.h index e0451f7a6..0b97dfdae 100644 --- a/src/expr/expr_value.h +++ b/src/expr/expr_value.h @@ -16,7 +16,7 @@ /* this must be above the check for __CVC4__EXPR__EXPR_VALUE_H */ /* to resolve a circular dependency */ -#include "cvc4_expr.h" +#include "expr/expr.h" #ifndef __CVC4__EXPR__EXPR_VALUE_H #define __CVC4__EXPR__EXPR_VALUE_H diff --git a/src/expr/kind.h b/src/expr/kind.h index 98cc7e2e3..db25d914e 100644 --- a/src/expr/kind.h +++ b/src/expr/kind.h @@ -36,12 +36,14 @@ enum Kind { AND, IFF, + IMPLIES, OR, XOR, /* from arith */ PLUS, - MINUS + MINUS, + MULT };/* enum Kind */ diff --git a/src/include/cvc4_config.h b/src/include/cvc4_config.h index e571f5969..ccc07b40a 100644 --- a/src/include/cvc4_config.h +++ b/src/include/cvc4_config.h @@ -39,3 +39,6 @@ # define CVC4_PUBLIC #endif /* __BUILDING_CVC4LIB */ + +#define EXPECT_TRUE(x) __builtin_expect( (x), true) +#define EXPECT_FALSE(x) __builtin_expect( (x), false) diff --git a/src/include/cvc4_expr.h b/src/include/cvc4_expr.h index 36d771647..d99708991 100644 --- a/src/include/cvc4_expr.h +++ b/src/include/cvc4_expr.h @@ -78,6 +78,10 @@ public: Expr substExpr(const std::vector& oldTerms, const std::vector& newTerms) const; + Expr plusExpr(const Expr& right) const; + Expr uMinusExpr() const; + Expr multExpr(const Expr& right) const; + inline Kind getKind() const; static Expr null() { return s_null; } diff --git a/src/main/about.h b/src/main/about.h index 458716842..e81e04288 100644 --- a/src/main/about.h +++ b/src/main/about.h @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#ifndef __CVC4__MAIN__ABOUT_H #define __CVC4__MAIN__ABOUT_H namespace CVC4 { diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index f1fe375b6..dcb23c303 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#include #include #include #include @@ -29,7 +30,7 @@ using namespace std; using namespace CVC4; namespace CVC4 { -namespace Main { +namespace main { static const char lang_help[] = "\ Languages currently supported to the -L / --lang option:\n\ @@ -135,5 +136,5 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) { return optind; } -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/main/main.cpp b/src/main/main.cpp index 44543a75f..8529f2ca2 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#include #include #include #include @@ -25,7 +26,7 @@ using namespace std; using namespace CVC4; -using namespace CVC4::Main; +using namespace CVC4::main; int main(int argc, char *argv[]) { struct Options opts; @@ -57,7 +58,7 @@ int main(int argc, char *argv[]) { // delete cmd; // } } - } catch(CVC4::Main::OptionException* e) { + } catch(CVC4::main::OptionException* e) { if(opts.smtcomp_mode) { printf("unknown"); fflush(stdout); diff --git a/src/main/usage.h b/src/main/usage.h index 3326108ac..0b503cdb2 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -10,6 +10,7 @@ ** [[ Add file-specific comments here ]] **/ +#ifndef __CVC4__MAIN__USAGE_H #define __CVC4__MAIN__USAGE_H namespace CVC4 { diff --git a/src/main/util.cpp b/src/main/util.cpp index 572aea00f..e2333b417 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -23,7 +23,7 @@ using CVC4::Exception; using namespace std; namespace CVC4 { -namespace Main { +namespace main { void sigint_handler(int sig, siginfo_t* info, void*) { fprintf(stderr, "CVC4 interrupted by user.\n"); @@ -51,5 +51,5 @@ void cvc4_init() throw() { throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno)); } -}/* CVC4::Main namespace */ +}/* CVC4::main namespace */ }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h new file mode 100644 index 000000000..078bf9cde --- /dev/null +++ b/src/smt/smt_engine.h @@ -0,0 +1,116 @@ +/********************* -*- C++ -*- */ +/** prover.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + **/ + +#ifndef __CVC4__SMT__SMT_ENGINE_H +#define __CVC4__SMT__SMT_ENGINE_H + +#include +#include "core/cvc4_expr.h" +#include "core/result.h" +#include "core/model.h" + +// In terms of abstraction, this is below (and provides services to) +// ValidityChecker and above (and requires the services of) +// 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 +// SmtEngine and override check()? +// +// Probably better than that is to have a configuration object that +// indicates which passes are desired. The configuration occurs +// elsewhere (and can even occur at runtime). A simple "pass manager" +// of sorts determines check()'s behavior. +// +// The CNF conversion can go on in PropEngine. + +class SmtEngine { + /** Current set of assertions. */ + // TODO: make context-aware to handle user-level push/pop. + std::vector d_assertList; + +private: + /** + * Pre-process an Expr. This is expected to be highly-variable, + * with a lot of "source-level configurability" to add multiple + * passes over the Expr. TODO: may need to specify a LEVEL of + * preprocessing (certain contexts need more/less ?). + */ + void preprocess(Expr); + + /** + * Adds a formula to the current context. + */ + void addFormula(Expr); + + /** + * Full check of consistency in current context. Returns true iff + * consistent. + */ + Result check(); + + /** + * Quick check of consistency in current context: calls + * processAssertionList() then look for inconsistency (based only on + * that). + */ + Result quickCheck(); + + /** + * Process the assertion list: for literals and conjunctions of + * literals, assert to T-solver. + */ + void processAssertionList(); + +public: + /** + * Add a formula to the current context: preprocess, do per-theory + * setup, use processAssertionList(), asserting to T-solver for + * literals and conjunction of literals. Returns false iff + * inconsistent. + */ + Result assert(Expr); + + /** + * Add a formula to the current context and call check(). Returns + * true iff consistent. + */ + Result query(Expr); + + /** + * Simplify a formula without doing "much" work. Requires assist + * from the SAT Engine. + */ + Expr simplify(Expr); + + /** + * Get a (counter)model (only if preceded by a SAT or INVALID query. + */ + Model getModel(); + + /** + * Push a user-level context. + */ + void push(); + + /** + * Pop a user-level context. Throws an exception if nothing to pop. + */ + void pop(); +};/* class SmtEngine */ + +}/* CVC4::smt namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__SMT__SMT_ENGINE_H */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 1369d5f0b..5e5f053a6 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -12,7 +12,7 @@ #ifndef __CVC4__THEORY__THEORY_H #define __CVC4__THEORY__THEORY_H -#include "cvc4_expr.h" +#include "expr/expr.h" #include "util/literal.h" namespace CVC4 { diff --git a/src/util/assert.h b/src/util/assert.h index 24e3a4cdf..6691c1b04 100644 --- a/src/util/assert.h +++ b/src/util/assert.h @@ -7,20 +7,78 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** + ** Assertion utility classes, functions, and exceptions. **/ #ifndef __CVC4__ASSERT_H #define __CVC4__ASSERT_H -#include +#include +#include "util/exception.h" +#include "cvc4_config.h" +#include "config.h" -#ifdef DEBUG -// the __builtin_expect() helps us if assert is built-in or a macro -# define cvc4assert(x) assert(__builtin_expect((x), 1)) -#else -// TODO: use a compiler annotation when assertions are off ? -// (to improve optimization) -# define cvc4assert(x) -#endif /* DEBUG */ +namespace CVC4 { + +class AssertionException : public Exception { +public: + AssertionException() : Exception() {} + AssertionException(std::string msg) : Exception(msg) {} + AssertionException(const char* msg) : Exception(msg) {} +};/* class AssertionException */ + +class UnreachableCodeException : public AssertionException { +public: + UnreachableCodeException() : AssertionException() {} + UnreachableCodeException(std::string msg) : AssertionException(msg) {} + UnreachableCodeException(const char* msg) : AssertionException(msg) {} +};/* class UnreachableCodeException */ + +#ifdef CVC4_ASSERTIONS +# define Assert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#else /* ! CVC4_ASSERTIONS */ +# define Assert(cond, msg...) /*EXPECT_TRUE( cond )*/ +#endif /* CVC4_ASSERTIONS */ + +#define AlwaysAssert(cond, msg...) __CVC4_ASSERTGLUE("Assertion failure at " __FILE__ ":", __LINE__, ": " #cond, __builtin_expect((cond), 1), ## msg) +#define Unreachable(cond, msg...) __CVC4_UNREACHABLEGLUE("Hit a section of unreachable code at " __FILE__ ":", __LINE__, __builtin_expect((cond), 1), ## msg) + +#define __CVC4_ASSERTGLUE(str1, line, str2, cond, msg...) AssertImpl(str1 #line str2, cond, ## msg) +#define __CVC4_UNREACHABLEGLUE(str, line, cond, msg...) AssertImpl(str #line, cond, ## msg) + +inline void AssertImpl(const char* info, bool cond, std::string msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond, const char* msg) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(std::string(info) + "\n" + msg); +} + +inline void AssertImpl(const char* info, bool cond) { + if(EXPECT_FALSE( ! cond )) + throw new AssertionException(info); +} + +#ifdef __GNUC__ +inline void UnreachableImpl(const char* info, std::string msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info, const char* msg) __attribute__ ((noreturn)); +inline void UnreachableImpl(const char* info) __attribute__ ((noreturn)); +#endif /* __GNUC__ */ + +inline void UnreachableImpl(const char* info, std::string msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info, const char* msg) { + throw new UnreachableCodeException(std::string(info) + "\n" + msg); +} + +inline void UnreachableImpl(const char* info) { + throw new UnreachableCodeException(info); +} + +}/* CVC4 namespace */ #endif /* __CVC4__ASSERT_H */ diff --git a/src/util/options.h b/src/util/options.h index 490cd607b..54b4e2f9b 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -10,6 +10,9 @@ ** [[ Add file-specific comments here ]] **/ +#include + +#ifndef __CVC4__OPTIONS_H #define __CVC4__OPTIONS_H namespace CVC4 { @@ -20,6 +23,9 @@ struct Options { bool smtcomp_mode; bool statistics; + std::ostream *out; + std::ostream *err; + /* -1 means no output */ /* 0 is normal (and default) -- warnings only */ /* 1 is warnings + notices so the user doesn't get too bored */ @@ -32,6 +38,8 @@ struct Options { Options() : binary_name(), smtcomp_mode(false), statistics(false), + out(0), + err(0), verbosity(0), lang() {} diff --git a/src/util/output.h b/src/util/output.h new file mode 100644 index 000000000..4d3752849 --- /dev/null +++ b/src/util/output.h @@ -0,0 +1,135 @@ +/********************* -*- C++ -*- */ +/** output.h + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009 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. + ** + ** Output utility classes and functions. + **/ + +#ifndef __CVC4__OUTPUT_H +#define __CVC4__OUTPUT_H + +#include +#include +#include +#include "util/exception.h" + +namespace CVC4 { + + +class Debug { + std::set d_tags; + std::ostream &d_out; + +public: + static void operator()(const char* tag, const char*); + static void operator()(const char* tag, std::string); + static void operator()(string tag, const char*); + static void operator()(string tag, std::string); + + static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(const char* tag); + static std::ostream& operator()(std::string tag); + + static void on (const char* tag) { d_tags.insert(std::string(tag)); }; + static void on (std::string tag) { d_tags.insert(tag); }; + static void off(const char* tag) { d_tags.erase (std::string(tag)); }; + static void off(std::string tag) { d_tags.erase (tag); }; + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Debug */ + + +class Warning { + std::ostream &d_out; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Warning */ + + +class Notice { + std::ostream &d_os; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Notice */ + + +class Chat { + std::ostream &d_os; + +public: + static void operator()(const char*); + static void operator()(std::string); + + static void printf(const char* fmt, ...) __attribute__ ((format(printf, 2, 3))); + static void printf(std::string fmt, ...) __attribute__ ((format(printf, 2, 3))); + + static std::ostream& operator()(); + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Chat */ + + +class Trace { + std::ostream &d_os; + +public: + static void operator()(const char* tag, const char*); + static void operator()(const char* tag, std::string); + static void operator()(string tag, const char*); + static void operator()(string tag, std::string); + + static void printf(const char* tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + va_list vl; + va_start(vl, fmt); + vfprintf(buf, 1024, fmt, vl); + va_end(vl); + } + static void printf(const char* tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + static void printf(std::string tag, const char* fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + static void printf(std::string tag, std::string fmt, ...) __attribute__ ((format(printf, 2, 3))) { + } + + static std::ostream& operator()(const char* tag); + static std::ostream& operator()(std::string tag); + + static void on (const char* tag) { d_tags.insert(std::string(tag)); }; + static void on (std::string tag) { d_tags.insert(tag); }; + static void off(const char* tag) { d_tags.erase (std::string(tag)); }; + static void off(std::string tag) { d_tags.erase (tag); }; + + static void setStream(std::ostream& os) { d_out = os; } +};/* class Trace */ + + +}/* CVC4 namespace */ + +#endif /* __CVC4__OUTPUT_H */