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
+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])])
+if test -z "${enable_assertions+set}"; then
+ enable_assertions=yes
+fi
+AC_MSG_RESULT([$enable_assertions])
+
+if test "$enable_assertions" = no -a "$enable_debug" = yes; then
+ AC_MSG_FAILURE([when debugging is on, so must assertions be.])
+fi
+
# Checks for programs.
AC_PROG_CC
AC_PROG_CXX
AM_PROG_LEX
AC_PROG_YACC
-AC_CHECK_PROG(DOXYGEN, doxygen, doxygen,)
-if test "$DOXYGEN" = ''; then
- echo 'WARNING: documentation targets require doxygen. Set your PATH appropriately or set DOXYGEN to point to a valid doxygen binary.'
+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
# Checks for libraries.
AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
# Checks for header files.
+AC_CHECK_HEADERS([getopt.h unistd.h])
# Checks for typedefs, structures, and compiler characteristics.
AC_HEADER_STDBOOL
# 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_CONFIG_FILES([
Makefile
contrib/Makefile
src/parser/Makefile
src/theory/Makefile
])
+
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.
+
+Now just type make, followed by make check or make install, as you like.
+
+EOF
# source files to match a template (inline, below). For files with no
# top comment, it adds a fresh one.
#
+# usage: contrib/update-copyright.pl [dirs...]
+# if dirs... are unspecified, the script scans its own parent directory's
+# "src" directory. Since it lives in contrib/ in the CVC4 source tree,
+# that means src/ in the CVC4 source tree.
+#
# It ignores any file/directory not starting with [a-zA-Z]
# (so, this includes . and .., vi swaps, .svn meta-info,
# .deps, etc.)
use strict;
use Fcntl ':mode';
-my $dir = $0;
-$dir =~ s,/[^/]+/*$,,;
+my @searchdirs = ();
+if($#ARGV == -1) {
+ my $dir = $0;
+ $dir =~ s,/[^/]+/*$,,;
-(chdir($dir."/..") && -f "src/include/expr.h") || die "can't find top-level source directory for CVC4";
-my $pwd = `pwd`; chomp $pwd;
+ (chdir($dir."/..") && -f "src/include/cvc4_expr.h") || die "can't find top-level source directory for CVC4";
+ my $pwd = `pwd`; chomp $pwd;
-print <<EOF;
+ print <<EOF;
Warning: this script is dangerous. It will overwrite the header comments in your
source files to match the template in the script, attempting to retain file-specific
comments, but this isn't guaranteed. You should run this in an svn working directory
Continue? y or n:
EOF
-$_ = <STDIN>; chomp;
-die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' );
+ $_ = <STDIN>; chomp;
+ die 'aborting operation' if !( $_ eq 'y' || $_ eq 'yes' || $_ eq 'Y' || $_ eq 'YES' );
+
+ $searchdirs[0] = 'src';
+} else {
+ @searchdirs = @ARGV;
+}
print "Updating sources...\n";
-recurse('src');
+recurse(shift @searchdirs) while $#searchdirs >= 0;
sub recurse {
my ($srcdir) = @_;
+ print "in dir $srcdir\n";
opendir(my $DIR, $srcdir);
while(my $file = readdir $DIR) {
next if !($file =~ /^[a-zA-Z]/);
#ifndef __CVC4_ATTR_TYPE_H
#define __CVC4_ATTR_TYPE_H
-#include "core/expr_attribute.h"
+#include "expr_attribute.h"
namespace CVC4 {
**/
#include "cvc4_expr.h"
-#include "core/expr_value.h"
-#include "core/expr_builder.h"
+#include "expr_value.h"
+#include "expr_builder.h"
namespace CVC4 {
return *this;
}
-ExprValue* Expr::operator->() {
- return d_ev;
-}
-
-const ExprValue* Expr::operator->() const {
+ExprValue* Expr::operator->() const {
return d_ev;
}
// TODO WARNING this file needs work !
#include <stdint.h>
-#include "core/config.h"
-#include "core/context.h"
-#include "core/cvc4_expr.h"
+#include "config.h"
+#include "context/context.h"
+#include "cvc4_expr.h"
namespace CVC4 {
**
**/
-#include "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/expr_value.h"
+#include "expr_builder.h"
+#include "expr_manager.h"
+#include "expr_value.h"
+#include "util/assert.h"
using namespace std;
d_children.u_arr[0] = v;
}
+ExprBuilder& ExprBuilder::reset(const ExprValue* ev) {
+ this->~ExprBuilder();
+ d_kind = Kind(ev->d_kind);
+ d_used = false;
+ d_nchildren = ev->d_nchildren;
+ for(Expr::const_iterator i = ev->begin(); i != ev->end(); ++i)
+ addChild(i->d_ev);
+ return *this;
+}
+
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);
d_children.u_vec->reserve(d_nchildren + 5);
copy(eb.d_children.u_vec->begin(), eb.d_children.u_vec->end(), back_inserter(*d_children.u_vec));
} else {
- iterator j = d_children.u_arr;
- for(iterator i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
- *j = i->inc();
+ ev_iterator j = d_children.u_arr;
+ for(ExprValue* const* i = eb.d_children.u_arr; i != eb.d_children.u_arr + eb.d_nchildren; ++i, ++j)
+ *j = (*i)->inc();
}
}
ExprBuilder::ExprBuilder(ExprManager* em, Kind k) : d_em(em), d_kind(k), d_used(false), d_nchildren(0) {
}
-ExprBuilder::ExprBuilder(ExprManager* em, const Expr&) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
+ExprBuilder::ExprBuilder(ExprManager* em, const Expr& e) : d_em(em), d_kind(UNDEFINED_KIND), d_used(false), d_nchildren(1) {
ExprValue *v = e->inc();
d_children.u_arr[0] = v;
}
if(d_nchildren > nchild_thresh) {
delete d_children.u_vec;
} else {
- for(iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
- *i
+ for(ev_iterator i = d_children.u_arr; i != d_children.u_arr + d_nchildren; ++i) {
+ (*i)->dec();
}
}
}
}
ExprBuilder& ExprBuilder::notExpr() {
+ if(d_kind != UNDEFINED_KIND)
+ collapse();
+ d_kind = NOT;
+ return *this;
}
// avoid double-negatives
ExprBuilder& ExprBuilder::negate() {
+ if(d_kind == NOT)
+ return reset(d_children.u_arr[0]);
+ if(d_kind != UNDEFINED_KIND)
+ collapse();
+ d_kind = NOT;
+ return *this;
}
ExprBuilder& ExprBuilder::andExpr(const Expr& right) {
if(d_nchildren == nchild_thresh) {
vector<Expr>* v = new vector<Expr>();
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();
+ }
+ 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_nchildren;
+ } else {
+ ExprValue *ev = e->d_ev;
+ d_children.u_arr[d_nchildren] = ev;
+ ev->inc();
+ ++d_nchildren;
+ }
+ return *this;
+}
+
+void ExprBuilder::addChild(const ExprValue* ev) {
+ if(d_nchildren == nchild_thresh) {
+ vector<Expr>* v = new vector<Expr>();
+ 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();
+ }
+ 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_nchildren;
+ } else {
+ d_children.u_arr[d_nchildren] = ev;
+ ev->inc();
+ ++d_nchildren;
}
return *this;
}
#define __CVC4_EXPR_BUILDER_H
#include <vector>
-#include "core/expr_manager.h"
-#include "core/kind.h"
+#include "expr_manager.h"
+#include "kind.h"
namespace CVC4 {
std::vector<Expr>* u_vec;
} d_children;
- void addChild();
+ void addChild(const Expr&);
+ void addChild(const ExprValue*);
void collapse();
+ typedef ExprValue** ev_iterator;
+ typedef ExprValue const** const_ev_iterator;
+
+ void reset(const ExprValue*);
+
public:
ExprBuilder();
** Expression manager implementation.
**/
-#include "core/expr_builder.h"
-#include "core/expr_manager.h"
-#include "core/cvc4_expr.h"
+#include "expr_builder.h"
+#include "expr_manager.h"
+#include "cvc4_expr.h"
namespace CVC4 {
#include <vector>
#include "cvc4_expr.h"
-#include "core/kind.h"
+#include "kind.h"
namespace CVC4 {
** reference count on ExprValue instances and
**/
-#include "core/expr_value.h"
+#include "expr_value.h"
namespace CVC4 {
Expr d_children[0];
friend class Expr;
+ friend class ExprBuilder;
+
+ ExprValue* inc() { /* FIXME thread safety */ ++d_rc; return this; }
+ ExprValue* dec() { /* FIXME thread safety */ --d_rc; return this; }
public:
/** Hash this expression.
* Increments the reference count. */
explicit Expr(ExprValue*);
+ typedef Expr* iterator;
+ typedef Expr const* const_iterator;
+
public:
Expr(const Expr&);
/** Access to the encapsulated expression.
* @return the encapsulated expression. */
- ExprValue* operator->();
-
- /** Const access to the encapsulated expression.
- * @return the encapsulated expression [const]. */
- const ExprValue* operator->() const;
+ ExprValue* operator->() const;
uint64_t hash() const;
INCLUDES = -I@srcdir@/../include -I@srcdir@/..
AM_CXXFLAGS = -Wall
-bin_BINARIES = cvc4
+bin_PROGRAMS = cvc4
-cvc4_SOURCES =
+cvc4_SOURCES = \
+ main.cpp \
+ getopt.cpp \
+ util.cpp
--- /dev/null
+#ifndef __CVC4_ABOUT_H
+#define __CVC4_ABOUT_H
+
+namespace CVC4 {
+namespace Main {
+
+const char about[] = "\
+This is a pre-release of CVC4.\n\
+Copyright (C) 2009 The ACSys Group\n\
+ Courant Institute of Mathematical Sciences,\n\
+ New York University\n\
+";
+
+}/* CVC4::Main namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4_MAIN_H */
--- /dev/null
+#include <cstdio>
+#include <cstdlib>
+#include <new>
+#include <unistd.h>
+#include <string.h>
+#include <stdint.h>
+#include <time.h>
+
+#include <getopt.h>
+
+#include "config.h"
+#include "main.h"
+#include "util/exception.h"
+#include "usage.h"
+#include "about.h"
+
+using namespace std;
+using namespace CVC4;
+
+namespace CVC4 {
+namespace Main {
+
+static const char lang_help[] = "\
+Languages currently supported to the -L / --lang option:\n\
+ auto attempt to automatically determine the input language\n\
+ pl | cvc4 CVC4 presentation language\n\
+ smt | smtlib SMT-LIB format\n\
+";
+
+enum Language {
+ AUTO = 0,
+ PL,
+ SMTLIB,
+};/* enum Language */
+
+enum OptionValue {
+ SMTCOMP = 256, /* no clash with char options */
+ STATS
+};/* enum OptionValue */
+
+static struct option cmdlineOptions[] = {
+ // name, has_arg, *flag, val
+ { "help" , no_argument , NULL, 'h' },
+ { "version", no_argument , NULL, 'V' },
+ { "verbose", no_argument , NULL, 'v' },
+ { "quiet" , no_argument , NULL, 'q' },
+ { "lang" , required_argument, NULL, 'L' },
+ { "debug" , required_argument, NULL, 'd' },
+ { "smtcomp", no_argument , NULL, SMTCOMP },
+ { "stats" , no_argument , NULL, STATS }
+};
+
+int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(Exception*) {
+ const char *progName = argv[0];
+ int c;
+
+ // find the base name of the program
+ const char *x = strrchr(progName, '/');
+ if(x != NULL)
+ progName = x + 1;
+ opts->binary_name = string(progName);
+
+ while((c = getopt_long(argc, argv, "+:hVvL:", cmdlineOptions, NULL)) != -1) {
+ switch(c) {
+
+ case 'h':
+ printf(usage, opts->binary_name.c_str());
+ exit(1);
+ break;
+
+ case 'V':
+ fputs(about, stdout);
+ break;
+
+ case 'v':
+ ++opts->verbosity;
+ break;
+
+ case 'q':
+ --opts->verbosity;
+ break;
+
+ case 'L':
+ if(!strcmp(argv[optind], "cvc4") || !strcmp(argv[optind], "pl")) {
+ opts->lang = PL;
+ break;
+ } else if(!strcmp(argv[optind], "smtlib") || !strcmp(argv[optind], "smt")) {
+ opts->lang = SMTLIB;
+ break;
+ } else if(!strcmp(argv[optind], "auto")) {
+ opts->lang = AUTO;
+ break;
+ }
+
+ if(strcmp(argv[optind], "help"))
+ throw new OptionException(string("unknown language for --lang: `") + argv[optind] + "'. Try --lang help.");
+
+ fputs(lang_help, stdout);
+ exit(1);
+
+ case STATS:
+ opts->statistics = true;
+ break;
+
+ case SMTCOMP:
+ // silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
+ opts->smtcomp_mode = true;
+ opts->verbosity = -1;
+ opts->lang = SMTLIB;
+ break;
+
+ case '?':
+ throw new OptionException(string("can't understand option: `") + argv[optind] + "'");
+
+ case ':':
+ throw new OptionException(string("option `") + argv[optind] + "' missing its required argument");
+
+ default:
+ throw new OptionException(string("can't understand option: `") + argv[optind] + "'");
+ }
+
+ }
+
+ return optind;
+}
+
+}/* CVC4::Main namespace */
+}/* CVC4 namespace */
--- /dev/null
+#include <cstdio>
+#include <cstdlib>
+#include <cerrno>
+#include <new>
+#include <exception>
+#include <unistd.h>
+#include <string.h>
+#include <stdint.h>
+#include <time.h>
+
+#include "config.h"
+#include "main.h"
+#include "usage.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::Main;
+
+int main(int argc, char *argv[]) {
+ struct Options opts;
+
+ try {
+ cvc4_init();
+
+ int firstArgIndex = parseOptions(argc, argv, &opts);
+
+ FILE *infile;
+
+ if(firstArgIndex >= argc) {
+ infile = stdin;
+ } else if(argc > firstArgIndex + 1) {
+ throw new Exception("Too many input files specified.");
+ } else {
+ infile = fopen(argv[firstArgIndex], "r");
+ if(!infile) {
+ throw new Exception(string("Could not open input file `") + argv[firstArgIndex] + "' for reading: " + strerror(errno));
+ exit(1);
+ }
+ }
+ } catch(CVC4::Main::OptionException* e) {
+ if(opts.smtcomp_mode) {
+ printf("unknown");
+ fflush(stdout);
+ }
+ fprintf(stderr, "CVC4 Error:\n%s\n\n", e->toString().c_str());
+ printf(usage, opts.binary_name.c_str());
+ exit(1);
+ } catch(CVC4::Exception* e) {
+ if(opts.smtcomp_mode) {
+ printf("unknown");
+ fflush(stdout);
+ }
+ fprintf(stderr, "CVC4 Error:\n%s\n", e->toString().c_str());
+ exit(1);
+ } catch(bad_alloc) {
+ if(opts.smtcomp_mode) {
+ printf("unknown");
+ fflush(stdout);
+ }
+ fprintf(stderr, "CVC4 ran out of memory.\n");
+ exit(1);
+ } catch(...) {
+ fprintf(stderr, "CVC4 threw an exception of unknown type.\n");
+ exit(1);
+ }
+
+ return 0;
+}
--- /dev/null
+#include <iostream>
+#include <exception>
+#include <string>
+
+#include "config.h"
+#include "util/exception.h"
+#include "util/options.h"
+
+#ifndef __CVC4_MAIN_H
+#define __CVC4_MAIN_H
+
+namespace CVC4 {
+namespace Main {
+
+class OptionException : public CVC4::Exception {
+public:
+ OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {}
+};/* class OptionException */
+
+int parseOptions(int argc, char** argv, CVC4::Options*) throw(CVC4::Exception*);
+void cvc4_init() throw();
+
+}/* CVC4::Main namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4_MAIN_H */
--- /dev/null
+#ifndef __CVC4_USAGE_H
+#define __CVC4_USAGE_H
+
+namespace CVC4 {
+namespace Main {
+
+// no more % chars in here without being escaped; it's used as a
+// printf() format string
+const char usage[] = "\
+usage: %s [options] [input-file]\n\
+\n\
+Without an input file, or with `-', CVC4 reads from standard input.\n\
+\n\
+CVC4 options:\n\
+ --lang | -L set input language (--lang help gives a list;\n\
+ `auto' is default)\n\
+ --version | -V identify this CVC4 binary\n\
+ --help | -h this command line reference\n\
+ --verbose | -v increase verbosity (repeatable)\n\
+ --quiet | -q decrease verbosity (repeatable)\n\
+ --debug | -d debugging for something (e.g. --debug arith)\n\
+ --smtcomp competition mode (very quiet)\n\
+ --stats give statistics on exit\n\
+";
+
+}/* CVC4::Main namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4_USAGE_H */
--- /dev/null
+#include <string>
+#include <cstdio>
+#include <cstdlib>
+#include <cerrno>
+#include <string.h>
+#include <signal.h>
+
+#include "util/exception.h"
+#include "config.h"
+
+using CVC4::Exception;
+using namespace std;
+
+namespace CVC4 {
+namespace Main {
+
+void sigint_handler(int sig, siginfo_t* info, void*) {
+ fprintf(stderr, "CVC4 interrupted by user.\n");
+ exit(info->si_signo + 128);
+}
+
+void segv_handler(int sig, siginfo_t* info, void*) {
+ fprintf(stderr, "CVC4 suffered a segfault.\n");
+ exit(info->si_signo + 128);
+}
+
+void cvc4_init() throw() {
+ struct sigaction act1;
+ act1.sa_sigaction = sigint_handler;
+ act1.sa_flags = SA_SIGINFO;
+ sigemptyset(&act1.sa_mask);
+ if(sigaction(SIGINT, &act1, NULL))
+ throw new Exception(string("sigaction(SIGINT) failure: ") + strerror(errno));
+
+ struct sigaction act2;
+ act2.sa_sigaction = segv_handler;
+ act2.sa_flags = SA_SIGINFO;
+ sigemptyset(&act2.sa_mask);
+ if(sigaction(SIGSEGV, &act2, NULL))
+ throw new Exception(string("sigaction(SIGSEGV) failure: ") + strerror(errno));
+}
+
+}/* CVC4::Main namespace */
+}/* CVC4 namespace */
--- /dev/null
+#ifndef __CVC4_OPTIONS_H
+#define __CVC4_OPTIONS_H
+
+namespace CVC4 {
+
+struct Options {
+ std::string binary_name;
+
+ bool smtcomp_mode;
+ bool statistics;
+
+ /* -1 means no output */
+ /* 0 is normal (and default) -- warnings only */
+ /* 1 is warnings + notices so the user doesn't get too bored */
+ /* 2 is chatty, giving statistical things etc. */
+ /* with 3, the solver is slowed down by all the scrolling */
+ int verbosity;
+
+ std::string lang;
+
+ Options() : binary_name(),
+ smtcomp_mode(false),
+ statistics(false),
+ verbosity(0),
+ lang()
+ {}
+};/* struct Options */
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4_OPTIONS_H */
projects / cvc5.git / commitdiff