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
# 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
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 <<EOF
-CVC4 $VERSION will be built as a $debug build $withassertions assertions.
+CVC4 $VERSION
+
+Build profile: $with_build$non_standard
+Optimized : $enable_optimized
+Debug symbols: $enable_debug_symbols
+Assertions : $enable_assertions
+Tracing : $enable_tracing
+Muzzle : $enable_muzzle
+gcov support : $enable_coverage
+gprof support: $enable_profiling
+
+CPPFLAGS : $CPPFLAGS
+CXXFLAGS : $CXXFLAGS
+LDFLAGS : $LDFLAGS
Now just type make, followed by make check or make install, as you like.
+You can also use 'make build_profile' to reconfigure for a different profile.
+Build profiles: production optimized default competition
+
EOF
+
+if test "$user_cppflags" = yes; then
+ AC_MSG_WARN([])
+ AC_MSG_WARN([I won't override your CPPFLAGS setting. But some of your build options to configure may not be honored.])
+ AC_MSG_WARN([To support your options to configure, I would like to set CPPFLAGS to:])
+ AC_MSG_WARN([ $CVC4CPPFLAGS])
+ AC_MSG_WARN([])
+else
+ CPPFLAGS="$CVC4CPPFLAGS"
+fi
+if test "$user_cxxflags" = yes; then
+ AC_MSG_WARN([])
+ AC_MSG_WARN([I won't override your CXXFLAGS setting. But some of your build options to configure may not be honored.])
+ AC_MSG_WARN([To support your options to configure, I would like to set CXXFLAGS to:])
+ AC_MSG_WARN([ $CVC4CXXFLAGS])
+ AC_MSG_WARN([])
+else
+ CXXFLAGS="$CVC4CXXFLAGS"
+fi
+if test "$user_ldflags" = yes; then
+ AC_MSG_WARN([])
+ AC_MSG_WARN([I won't override your LDFLAGS setting. But some of your build options to configure may not be honored.])
+ AC_MSG_WARN([To support your options to configure, I would like to set LDFLAGS to:])
+ AC_MSG_WARN([ $CVC4LDFLAGS])
+ AC_MSG_WARN([])
+else
+ LDFLAGS="$CVC4LDFLAGS"
+fi
+
+non_standard=
+if test "$non_standard_build_profile" = yes; then
+ if test "$with_build" = default; then
+ with_build=custom
+ else
+ AC_MSG_WARN([])
+ AC_MSG_WARN([This is a non-standard $with_build build profile.])
+ AC_MSG_WARN([])
+ non_standard=-custom
+ fi
+fi
(setq c-basic-offset 2)
(c-set-offset 'innamespace 0)
(setq indent-tabs-mode nil))
-(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist))
+(setq auto-mode-alist (cons '("/home/mdeters/cvc4.*/.*\\.\\(cc\\|cpp\\|h\\|hh\\|hpp\\|y\\|yy\\|ypp\\|lex\\|l\\|ll\\|lpp\\)$" . cvc4-c++-editing-mode) auto-mode-alist))
-- Morgan Deters <mdeters@cs.nyu.edu> Mon, 02 Nov 2009 18:19:22 -0500
last if $line =~ /^ \*\*\s*$/;
}
} else {
+ my $line = $_;
print "adding\n";
if($file =~ /\.(y|yy|ypp|Y)$/) {
print $OUT "%{/******************* -*- C++ -*- */\n";
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;
** 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"
--- /dev/null
+/********************* -*- 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 <vector>
+#include <stdint.h>
+
+#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<Expr>& oldTerms,
+ const std::vector<Expr>& 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 */
#include <stdint.h>
#include "config.h"
#include "context/context.h"
-#include "cvc4_expr.h"
+#include "expr/expr.h"
namespace CVC4 {
namespace expr {
}
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<Expr>();
// 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<Expr>& oldTerms,
- const std::vector<Expr>& 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) {
// 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 */
public:
+ AndExprBuilder(const ExprBuilder&);
+
AndExprBuilder& operator&&(Expr);
OrExprBuilder operator||(Expr);
public:
+ OrExprBuilder(const ExprBuilder&);
+
AndExprBuilder operator&&(Expr);
OrExprBuilder& operator||(Expr);
public:
+ PlusExprBuilder(const ExprBuilder&);
+
PlusExprBuilder& operator+(Expr);
PlusExprBuilder& operator-(Expr);
MultExprBuilder operator*(Expr);
public:
+ MultExprBuilder(const ExprBuilder&);
+
PlusExprBuilder operator+(Expr);
PlusExprBuilder operator-(Expr);
MultExprBuilder& operator*(Expr);
#define __CVC4__EXPR_MANAGER_H
#include <vector>
-#include "cvc4_expr.h"
+#include "expr/expr.h"
#include "kind.h"
namespace CVC4 {
/* 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
AND,
IFF,
+ IMPLIES,
OR,
XOR,
/* from arith */
PLUS,
- MINUS
+ MINUS,
+ MULT
};/* enum Kind */
# define CVC4_PUBLIC
#endif /* __BUILDING_CVC4LIB */
+
+#define EXPECT_TRUE(x) __builtin_expect( (x), true)
+#define EXPECT_FALSE(x) __builtin_expect( (x), false)
Expr substExpr(const std::vector<Expr>& oldTerms,
const std::vector<Expr>& 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; }
** [[ Add file-specific comments here ]]
**/
+#ifndef __CVC4__MAIN__ABOUT_H
#define __CVC4__MAIN__ABOUT_H
namespace CVC4 {
** [[ Add file-specific comments here ]]
**/
+#include <cstdio>
#include <cstdlib>
#include <new>
#include <unistd.h>
using namespace CVC4;
namespace CVC4 {
-namespace Main {
+namespace main {
static const char lang_help[] = "\
Languages currently supported to the -L / --lang option:\n\
return optind;
}
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
}/* CVC4 namespace */
** [[ Add file-specific comments here ]]
**/
+#include <cstdio>
#include <cstdlib>
#include <cerrno>
#include <new>
using namespace std;
using namespace CVC4;
-using namespace CVC4::Main;
+using namespace CVC4::main;
int main(int argc, char *argv[]) {
struct Options opts;
// delete cmd;
// }
}
- } catch(CVC4::Main::OptionException* e) {
+ } catch(CVC4::main::OptionException* e) {
if(opts.smtcomp_mode) {
printf("unknown");
fflush(stdout);
** [[ Add file-specific comments here ]]
**/
+#ifndef __CVC4__MAIN__USAGE_H
#define __CVC4__MAIN__USAGE_H
namespace CVC4 {
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");
throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
}
-}/* CVC4::Main namespace */
+}/* CVC4::main namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* -*- 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 <vector>
+#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<Expr> 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 */
#ifndef __CVC4__THEORY__THEORY_H
#define __CVC4__THEORY__THEORY_H
-#include "cvc4_expr.h"
+#include "expr/expr.h"
#include "util/literal.h"
namespace CVC4 {
** 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 <cassert>
+#include <string>
+#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 */
** [[ Add file-specific comments here ]]
**/
+#include <iostream>
+
+#ifndef __CVC4__OPTIONS_H
#define __CVC4__OPTIONS_H
namespace CVC4 {
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 */
Options() : binary_name(),
smtcomp_mode(false),
statistics(false),
+ out(0),
+ err(0),
verbosity(0),
lang()
{}
--- /dev/null
+/********************* -*- 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 <iostream>
+#include <string>
+#include <set>
+#include "util/exception.h"
+
+namespace CVC4 {
+
+
+class Debug {
+ std::set<std::string> 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 */
projects / cvc5.git / commitdiff