Build src/expr before src/util.
Moved CVC4::Command to the expr package.
Re-quieted the "result is sat/invalid" etc. from PropEngine (this is
now done at the main driver level).
Added file-level documentation to Antlr sources
When built for debug, spin on SEGV instead of aborting. Really useful
for debugging problems that crop up only on long runs. Added
'--segv-nospin' to override this spinning so that "make check,"
nightly regressions, etc. don't hang when built with debug.
Updated src/main/about.h for 2010.
-I@srcdir@/include -I@srcdir@
AM_CXXFLAGS = -Wall -fvisibility=hidden
-SUBDIRS = util expr context prop smt theory . parser main
+SUBDIRS = expr util context prop smt theory . parser main
lib_LTLIBRARIES = libcvc4.la
node_manager.h \
expr_manager.h \
node_attribute.h \
- kind.h \
+ @srcdir@/kind.h \
node.cpp \
node_builder.cpp \
node_manager.cpp \
expr_manager.cpp \
node_value.cpp \
- expr.cpp
+ expr.cpp \
+ command.h \
+ command.cpp
+EXTRA_DIST = @srcdir@/kind.h kind_prologue.h kind_middle.h kind_epilogue.h
+
+@srcdir@/kind.h: @srcdir@/mkkind kind_prologue.h kind_middle.h kind_epilogue.h @top_srcdir@/src/theory/Makefile.in @top_srcdir@/src/theory/*/kinds
+ chmod +x @srcdir@/mkkind
+ (@srcdir@/mkkind \
+ @srcdir@/kind_prologue.h \
+ @srcdir@/kind_middle.h \
+ @srcdir@/kind_epilogue.h \
+ `grep '^SUBDIRS = ' @top_srcdir@/src/theory/Makefile.in | cut -d' ' -f3- | tr ' ' "\n" | xargs -i__D__ echo @top_srcdir@/src/theory/__D__/kinds` \
+ > @srcdir@/kind.h) || (rm -f @srcdir@/kind.h && exit 1)
+
+BUILT_SOURCES = @srcdir@/kind.h
+dist-hook: @srcdir@/kind.h
+MAINTAINERCLEANFILES = @srcdir@/kind.h
--- /dev/null
+/********************* -*- C++ -*- */
+/** command.cpp
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Implementation of command objects.
+ **/
+
+#include "expr/command.h"
+#include "smt/smt_engine.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+ostream& operator<<(ostream& out, const Command* c) {
+ if (c == NULL) {
+ out << "null";
+ } else {
+ c->toStream(out);
+ }
+ return out;
+}
+
+CommandSequence::~CommandSequence() {
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ delete d_commandSequence[i];
+ }
+}
+
+void CommandSequence::invoke(SmtEngine* smtEngine) {
+ for(; d_index < d_commandSequence.size(); ++d_index) {
+ d_commandSequence[d_index]->invoke(smtEngine);
+ delete d_commandSequence[d_index];
+ }
+}
+
+void CheckSatCommand::toStream(ostream& out) const {
+ if(d_expr.isNull()) {
+ out << "CheckSat()";
+ } else {
+ out << "CheckSat(" << d_expr << ")";
+ }
+}
+
+void CommandSequence::toStream(ostream& out) const {
+ out << "CommandSequence[" << endl;
+ for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
+ out << *d_commandSequence[i] << endl;
+ }
+ out << "]";
+}
+
+void DeclarationCommand::toStream(std::ostream& out) const {
+ out << "Declare(";
+ bool first = true;
+ for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
+ if(!first) {
+ out << ", ";
+ }
+ out << d_declaredSymbols[i];
+ first = false;
+ }
+ out << ")";
+}
+
+}/* CVC4 namespace */
--- /dev/null
+/********************* -*- C++ -*- */
+/** command.h
+ ** Original author: mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Implementation of the command pattern on SmtEngines. Command
+ ** objects are generated by the parser (typically) to implement the
+ ** commands in parsed input (see Parser::parseNextCommand()), or by
+ ** client code.
+ **/
+
+#ifndef __CVC4__COMMAND_H
+#define __CVC4__COMMAND_H
+
+#include <iostream>
+#include <sstream>
+#include <string>
+#include <vector>
+
+#include "cvc4_config.h"
+#include "expr/expr.h"
+#include "util/result.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+class Command;
+
+inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+
+class CVC4_PUBLIC Command {
+public:
+ virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
+ virtual ~Command() {};
+ virtual void toStream(std::ostream&) const = 0;
+ std::string toString() const;
+};/* class Command */
+
+class CVC4_PUBLIC EmptyCommand : public Command {
+public:
+ EmptyCommand(std::string name = "");
+ void invoke(CVC4::SmtEngine* smt_engine);
+ void toStream(std::ostream& out) const;
+private:
+ std::string d_name;
+};/* class EmptyCommand */
+
+class CVC4_PUBLIC AssertCommand : public Command {
+public:
+ AssertCommand(const BoolExpr& e);
+ void invoke(CVC4::SmtEngine* smt_engine);
+ void toStream(std::ostream& out) const;
+protected:
+ BoolExpr d_expr;
+};/* class AssertCommand */
+
+class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
+public:
+ DeclarationCommand(const std::vector<std::string>& ids);
+ void toStream(std::ostream& out) const;
+protected:
+ std::vector<std::string> d_declaredSymbols;
+};
+
+class CVC4_PUBLIC CheckSatCommand : public Command {
+public:
+ CheckSatCommand(const BoolExpr& e);
+ void invoke(SmtEngine* smt);
+ Result getResult();
+ void toStream(std::ostream& out) const;
+protected:
+ BoolExpr d_expr;
+ Result d_result;
+};/* class CheckSatCommand */
+
+class CVC4_PUBLIC QueryCommand : public Command {
+public:
+ QueryCommand(const BoolExpr& e);
+ void invoke(SmtEngine* smt);
+ Result getResult();
+ void toStream(std::ostream& out) const;
+protected:
+ BoolExpr d_expr;
+ Result d_result;
+};/* class QueryCommand */
+
+class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
+public:
+ /** The status an SMT benchmark can have */
+ enum BenchmarkStatus {
+ /** Benchmark is satisfiable */
+ SMT_SATISFIABLE,
+ /** Benchmark is unsatisfiable */
+ SMT_UNSATISFIABLE,
+ /** The status of the benchmark is unknown */
+ SMT_UNKNOWN
+ };
+ SetBenchmarkStatusCommand(BenchmarkStatus status);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ BenchmarkStatus d_status;
+};/* class SetBenchmarkStatusCommand */
+
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs)
+ CVC4_PUBLIC;
+
+class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
+public:
+ SetBenchmarkLogicCommand(std::string logic);
+ void invoke(SmtEngine* smt);
+ void toStream(std::ostream& out) const;
+protected:
+ std::string d_logic;
+};/* class SetBenchmarkLogicCommand */
+
+class CVC4_PUBLIC CommandSequence : public Command {
+public:
+ CommandSequence();
+ ~CommandSequence();
+ void invoke(SmtEngine* smt);
+ void addCommand(Command* cmd);
+ void toStream(std::ostream& out) const;
+
+ typedef std::vector<Command*>::iterator iterator;
+ typedef std::vector<Command*>::const_iterator const_iterator;
+
+ const_iterator begin() const { return d_commandSequence.begin(); }
+ const_iterator end() const { return d_commandSequence.end(); }
+
+ iterator begin() { return d_commandSequence.begin(); }
+ iterator end() { return d_commandSequence.end(); }
+
+private:
+ /** All the commands to be executed (in sequence) */
+ std::vector<Command*> d_commandSequence;
+ /** Next command to be executed */
+ unsigned int d_index;
+};/* class CommandSequence */
+
+}/* CVC4 namespace */
+
+/* =========== inline function definitions =========== */
+
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+inline std::ostream& operator<<(std::ostream& out, const Command& c) {
+ c.toStream(out);
+ return out;
+}
+
+/* class Command */
+
+inline std::string Command::toString() const {
+ std::stringstream ss;
+ toStream(ss);
+ return ss.str();
+}
+
+/* class EmptyCommand */
+
+inline EmptyCommand::EmptyCommand(std::string name) :
+ d_name(name) {
+}
+
+inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
+}
+
+inline void EmptyCommand::toStream(std::ostream& out) const {
+ out << "EmptyCommand(" << d_name << ")";
+}
+
+/* class AssertCommand */
+
+inline AssertCommand::AssertCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void AssertCommand::invoke(SmtEngine* smt_engine) {
+ smt_engine->assertFormula(d_expr);
+}
+
+inline void AssertCommand::toStream(std::ostream& out) const {
+ out << "Assert(" << d_expr << ")";
+}
+
+/* class CheckSatCommand */
+
+inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
+ d_result = smt_engine->checkSat(d_expr);
+}
+
+inline Result CheckSatCommand::getResult() {
+ return d_result;
+}
+
+/* class QueryCommand */
+
+inline QueryCommand::QueryCommand(const BoolExpr& e) :
+ d_expr(e) {
+}
+
+inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
+ d_result = smt_engine->query(d_expr);
+}
+
+inline Result QueryCommand::getResult() {
+ return d_result;
+}
+
+inline void QueryCommand::toStream(std::ostream& out) const {
+ out << "Query(";
+ d_expr.printAst(out, 0);
+ out << ")";
+}
+
+/* class CommandSequence */
+
+inline CommandSequence::CommandSequence() :
+ d_index(0) {
+}
+
+inline void CommandSequence::addCommand(Command* cmd) {
+ d_commandSequence.push_back(cmd);
+}
+
+/* class DeclarationCommand */
+
+inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
+ d_declaredSymbols(ids) {
+}
+
+/* class SetBenchmarkStatusCommand */
+
+inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
+ d_status(s) {
+}
+
+inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the status
+}
+
+inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkStatus(" << d_status << ")";
+}
+
+/* class SetBenchmarkLogicCommand */
+
+inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
+ d_logic(l) {
+}
+
+inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
+ // FIXME: TODO: something to be done with the logic
+}
+
+inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
+ out << "SetBenchmarkLogic(" << d_logic << ")";
+}
+
+/* output stream insertion operator for benchmark statuses */
+inline std::ostream& operator<<(std::ostream& out,
+ SetBenchmarkStatusCommand::BenchmarkStatus bs) {
+ switch(bs) {
+
+ case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
+ return out << "sat";
+
+ case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
+ return out << "unsat";
+
+ case SetBenchmarkStatusCommand::SMT_UNKNOWN:
+ return out << "unknown";
+
+ default:
+ return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
+ }
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__COMMAND_H */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** kind.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): cconway, dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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.
- **
- ** Kinds of Nodes.
- **/
-
-#ifndef __CVC4__KIND_H
-#define __CVC4__KIND_H
-
-#include "cvc4_config.h"
-#include <iostream>
-
-namespace CVC4 {
-
-// TODO: create this file (?) from theory solver headers so that we
-// have a collection of kinds from all. This file is mainly a
-// placeholder for design & development work.
-
-enum Kind {
- /* undefined */
- UNDEFINED_KIND = -1,
- /** Null Kind */
- NULL_EXPR,
-
- /* built-ins */
- EQUAL,
- ITE,
- SKOLEM,
- VARIABLE,
- APPLY,
-
- /* propositional connectives */
- FALSE,
- TRUE,
-
- NOT,
-
- AND,
- IFF,
- IMPLIES,
- OR,
- XOR,
-
- /* from arith */
- PLUS,
- MINUS,
- MULT
-};/* enum Kind */
-
-inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
- using namespace CVC4;
-
- switch(k) {
-
- /* special cases */
- case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
- case NULL_EXPR: out << "NULL"; break;
-
- case EQUAL: out << "EQUAL"; break;
- case ITE: out << "ITE"; break;
- case SKOLEM: out << "SKOLEM"; break;
- case VARIABLE: out << "VARIABLE"; break;
- case APPLY: out << "APPLY"; break;
-
- /* propositional connectives */
- case FALSE: out << "FALSE"; break;
- case TRUE: out << "TRUE"; break;
-
- case NOT: out << "NOT"; break;
-
- case AND: out << "AND"; break;
- case IFF: out << "IFF"; break;
- case IMPLIES: out << "IMPLIES"; break;
- case OR: out << "OR"; break;
- case XOR: out << "XOR"; break;
-
- /* from arith */
- case PLUS: out << "PLUS"; break;
- case MINUS: out << "MINUS"; break;
- case MULT: out << "MULT"; break;
-
- default: out << "UNKNOWNKIND!" << int(k); break;
- }
-
- return out;
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__KIND_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** kind_epilogue.h
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Kinds of Nodes.
+ **/
+
+ case LAST_KIND: out << "LAST_KIND"; break;
+ default: out << "UNKNOWNKIND!" << int(k); break;
+ }
+
+ return out;
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__KIND_H */
--- /dev/null
+/********************* -*- C++ -*- */
+/** kind_middle.h
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Kinds of Nodes.
+ **/
+
+ LAST_KIND
+
+};/* enum Kind */
+
+inline std::ostream& operator<<(std::ostream&, CVC4::Kind) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CVC4::Kind k) {
+ using namespace CVC4;
+
+ switch(k) {
+
+ /* special cases */
+ case UNDEFINED_KIND: out << "UNDEFINED_KIND"; break;
+ case NULL_EXPR: out << "NULL"; break;
+
+ case EQUAL: out << "EQUAL"; break;
+ case ITE: out << "ITE"; break;
+ case SKOLEM: out << "SKOLEM"; break;
+ case VARIABLE: out << "VARIABLE"; break;
--- /dev/null
+/********************* -*- C++ -*- */
+/** kind_prologue.h
+ ** Original author:
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 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.
+ **
+ ** Kinds of Nodes.
+ **/
+
+#ifndef __CVC4__KIND_H
+#define __CVC4__KIND_H
+
+#include "cvc4_config.h"
+#include <iostream>
+
+namespace CVC4 {
+
+enum Kind {
+ /* undefined */
+ UNDEFINED_KIND = -1,
+ /** Null Kind */
+ NULL_EXPR,
+
+ /* built-ins */
+ EQUAL,
+ ITE,
+ SKOLEM,
+ VARIABLE,
--- /dev/null
+#!/bin/bash
+#
+# mkkind
+# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
+#
+# The purpose of this script is to create kind.h from a prologue,
+# middle, epilogue, and a list of theory kinds.
+#
+# Invocation:
+#
+# mkkind prologue-file middle-file epilogue-file theory-kind-files...
+#
+# Output is to standard out.
+#
+
+cat <<EOF
+/********************* -*- C++ -*- */
+/** kind.h
+ **
+ ** Copyright 2009, 2010 The AcSys Group, New York University, and as below.
+ **
+ ** This header file automatically generated by:
+ **
+ ** $0 $@
+ **
+ ** for the CVC4 project.
+ **
+ **/
+
+EOF
+
+prologue=$1; shift
+middle=$1; shift
+epilogue=$1; shift
+
+cases=
+cat "$prologue"
+while [ $# -gt 0 ]; do
+ b=$(basename $(dirname "$1"))
+ echo
+ echo " /* from $b */"
+ cases="$cases
+ /* from $b */
+"
+ for r in `cat "$1"`; do
+ echo " $r,"
+ cases="$cases case $r: out << \"$r\"; break;
+"
+ done
+ shift
+done
+cat "$middle"
+echo "$cases"
+cat "$epilogue"
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\
+Copyright (C) 2009, 2010\n\
+ The ACSys Group\n\
+ Courant Institute of Mathematical Sciences,\n\
+ New York University\n\
+ New York, NY 10012 USA\n\
";
}/* CVC4::main namespace */
enum OptionValue {
CNF = 256, /* no clash with char options */
SMTCOMP,
- STATS
+ STATS,
+ SEGV_NOSPIN
};/* enum OptionValue */
// FIXME add a comment here describing the option array
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' },
- { "cnf" , required_argument, NULL, CNF },
- { "smtcomp", no_argument , NULL, SMTCOMP },
- { "stats" , no_argument , NULL, STATS }
+ { "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' },
+ { "cnf" , required_argument, NULL, CNF },
+ { "smtcomp" , no_argument , NULL, SMTCOMP },
+ { "stats" , no_argument , NULL, STATS },
+ { "segv-nospin", no_argument , NULL, SEGV_NOSPIN }
};/* if you add things to the above, please remember to update usage.h! */
-int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionException) {
- const char *progName = argv[0];
+/** Full argv[0] */
+const char *progPath;
+
+/** Just the basename component of argv[0] */
+const char *progName;
+
+/** Parse argc/argv and put the result into a CVC4::Options struct. */
+int parseOptions(int argc, char** argv, CVC4::Options* opts)
+throw(OptionException) {
+ progPath = progName = argv[0];
int c;
// find the base name of the program
opts->binary_name = string(progName);
// FIXME add a comment here describing the option string
- while((c = getopt_long(argc, argv, "+:hVvqL:d:", cmdlineOptions, NULL)) != -1) {
+ while((c = getopt_long(argc, argv,
+ "+:hVvqL:d:",
+ cmdlineOptions, NULL)) != -1) {
switch(c) {
case 'h':
printf(usage, opts->binary_name.c_str());
exit(1);
- break;
case 'V':
fputs(about, stdout);
- break;
+ exit(0);
case 'v':
++opts->verbosity;
opts->statistics = true;
break;
+ case SEGV_NOSPIN:
+ segvNoSpin = true;
+ break;
+
case SMTCOMP:
// silences CVC4 (except "sat" or "unsat" or "unknown", forces smtlib input)
opts->smtcomp_mode = true;
#include "parser/parser.h"
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"
-#include "util/command.h"
+#include "expr/command.h"
#include "util/result.h"
#include "util/Assert.h"
#include "util/output.h"
namespace main {
+/** Class representing an option-parsing exception. */
class OptionException : public CVC4::Exception {
public:
- OptionException(const std::string& s) throw() : CVC4::Exception("Error in option parsing: " + s) {}
+ OptionException(const std::string& s) throw() :
+ CVC4::Exception("Error in option parsing: " + s) {
+ }
};/* class OptionException */
+/** Full argv[0] */
+extern const char *progPath;
+
+/** Just the basename component of argv[0] */
+extern const char *progName;
+
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc. See util.cpp.
+ */
+extern bool segvNoSpin;
+
+/** Parse argc/argv and put the result into a CVC4::Options struct. */
int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException);
+
+/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */
void cvc4_init() throw();
}/* CVC4::main namespace */
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\
+ --lang | -L force input language (default is `auto'; see --lang help)\n\
--version | -V identify this CVC4 binary\n\
--help | -h this command line reference\n\
--verbose | -v increase 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\
+ --segv-nospin (debug builds only) don't spin on segfault waiting for gdb\n\
";
}/* CVC4::main namespace */
** See the file COPYING in the top-level source directory for licensing
** information.
**
- ** [[ Add file-specific comments here ]]
+ ** Utilities for the main driver.
**/
#include <cstdio>
#include "util/exception.h"
#include "config.h"
+#include "main.h"
+
using CVC4::Exception;
using namespace std;
namespace CVC4 {
namespace main {
-// FIXME add comments to functions
+/**
+ * If true, will not spin on segfault even when CVC4_DEBUG is on.
+ * Useful for nightly regressions, noninteractive performance runs
+ * etc.
+ */
+bool segvNoSpin = false;
+/** Handler for SIGINT, i.e., when the user hits control C. */
void sigint_handler(int sig, siginfo_t* info, void*) {
fprintf(stderr, "CVC4 interrupted by user.\n");
abort();
}
+/** Handler for SIGSEGV (segfault). */
void segv_handler(int sig, siginfo_t* info, void*) {
+#ifdef CVC4_DEBUG
+ fprintf(stderr, "CVC4 suffered a segfault in DEBUG mode.\n");
+ if(segvNoSpin) {
+ fprintf(stderr, "No-spin requested, aborting...\n");
+ abort();
+ } else {
+ fprintf(stderr, "Spinning so that a debugger can be connected.\n");
+ fprintf(stderr, "Try: gdb %s %u\n", progName, getpid());
+ for(;;) {
+ sleep(60);
+ }
+ }
+#else /* CVC4_DEBUG */
fprintf(stderr, "CVC4 suffered a segfault.\n");
abort();
+#endif /* CVC4_DEBUG */
}
+/** Initialize the driver. Sets signal handlers for SIGINT and SIGSEGV. */
void cvc4_init() throw() {
struct sigaction act1;
act1.sa_sigaction = sigint_handler;
#include "antlr_parser.h"
#include "util/output.h"
#include "util/Assert.h"
-#include "util/command.h"
+#include "expr/command.h"
using namespace std;
using namespace CVC4;
** See the file COPYING in the top-level source directory for licensing
** information.
**
- **
** Parser for CVC presentation language.
**/
header "post_include_hpp" {
#include "parser/antlr_parser.h"
-#include "util/command.h"
+#include "expr/command.h"
}
header "post_include_cpp" {
: ASSERT f = formula SEMICOLON { cmd = new AssertCommand(f); }
| QUERY f = formula SEMICOLON { cmd = new QueryCommand(f); }
| CHECKSAT f = formula SEMICOLON { cmd = new CheckSatCommand(f); }
- | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(); }
+ | CHECKSAT SEMICOLON { cmd = new CheckSatCommand(getTrueExpr()); }
| identifierList[ids, CHECK_UNDECLARED] COLON type {
// FIXME: switch on type (may not be predicates)
vector<string> sorts;
#include <antlr/CharScanner.hpp>
#include "parser.h"
-#include "util/command.h"
+#include "expr/command.h"
#include "util/output.h"
#include "util/Assert.h"
#include "parser_exception.h"
header "post_include_hpp" {
#include "parser/antlr_parser.h"
-#include "util/command.h"
+#include "expr/command.h"
}
header "post_include_cpp" {
d_restartMayBeNeeded = true;
}
- Message() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
+ Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
if(result){
for(map<Node,Lit>::iterator atomIter = d_atom2lit.begin();
#include "smt/smt_engine.h"
#include "util/exception.h"
-#include "util/command.h"
+#include "expr/command.h"
#include "util/output.h"
#include "expr/node_builder.h"
#include "util/options.h"
Assert.cpp \
Makefile.am \
Makefile.in \
- command.cpp \
- command.h \
debug.h \
decision_engine.cpp \
decision_engine.h \
+++ /dev/null
-/********************* -*- C++ -*- */
-/** command.cpp
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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.
- **
- ** Implementation of command objects.
- **/
-
-#include "util/command.h"
-#include "smt/smt_engine.h"
-
-using namespace std;
-
-namespace CVC4 {
-
-ostream& operator<<(ostream& out, const Command* c) {
- if (c == NULL) {
- out << "null";
- } else {
- c->toStream(out);
- }
- return out;
-}
-
-CommandSequence::~CommandSequence() {
- for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
- delete d_commandSequence[i];
- }
-}
-
-void CommandSequence::invoke(SmtEngine* smtEngine) {
- for(; d_index < d_commandSequence.size(); ++d_index) {
- d_commandSequence[d_index]->invoke(smtEngine);
- delete d_commandSequence[d_index];
- }
-}
-
-void CheckSatCommand::toStream(ostream& out) const {
- if(d_expr.isNull()) {
- out << "CheckSat()";
- } else {
- out << "CheckSat(" << d_expr << ")";
- }
-}
-
-void CommandSequence::toStream(ostream& out) const {
- out << "CommandSequence[" << endl;
- for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
- out << *d_commandSequence[i] << endl;
- }
- out << "]";
-}
-
-void DeclarationCommand::toStream(std::ostream& out) const {
- out << "Declare(";
- bool first = true;
- for(unsigned i = 0; i < d_declaredSymbols.size(); ++i) {
- if(!first) {
- out << ", ";
- }
- out << d_declaredSymbols[i];
- first = false;
- }
- out << ")";
-}
-
-}/* CVC4 namespace */
+++ /dev/null
-/********************* -*- C++ -*- */
-/** command.h
- ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 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.
- **
- ** Implementation of the command pattern on SmtEngines. Command
- ** objects are generated by the parser (typically) to implement the
- ** commands in parsed input (see Parser::parseNextCommand()), or by
- ** client code.
- **/
-
-#ifndef __CVC4__COMMAND_H
-#define __CVC4__COMMAND_H
-
-#include <iostream>
-#include <sstream>
-#include <string>
-#include <vector>
-
-#include "cvc4_config.h"
-#include "expr/expr.h"
-#include "util/result.h"
-
-namespace CVC4 {
-
-class SmtEngine;
-class Command;
-
-inline std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
-
-class CVC4_PUBLIC Command {
-public:
- virtual void invoke(CVC4::SmtEngine* smt_engine) = 0;
- virtual ~Command() {};
- virtual void toStream(std::ostream&) const = 0;
- std::string toString() const;
-};/* class Command */
-
-class CVC4_PUBLIC EmptyCommand : public Command {
-public:
- EmptyCommand(std::string name = "");
- void invoke(CVC4::SmtEngine* smt_engine);
- void toStream(std::ostream& out) const;
-private:
- std::string d_name;
-};/* class EmptyCommand */
-
-class CVC4_PUBLIC AssertCommand : public Command {
-public:
- AssertCommand(const BoolExpr& e);
- void invoke(CVC4::SmtEngine* smt_engine);
- void toStream(std::ostream& out) const;
-protected:
- BoolExpr d_expr;
-};/* class AssertCommand */
-
-class CVC4_PUBLIC DeclarationCommand : public EmptyCommand {
-public:
- DeclarationCommand(const std::vector<std::string>& ids);
- void toStream(std::ostream& out) const;
-protected:
- std::vector<std::string> d_declaredSymbols;
-};
-
-class CVC4_PUBLIC CheckSatCommand : public Command {
-public:
- CheckSatCommand();
- CheckSatCommand(const BoolExpr& e);
- void invoke(SmtEngine* smt);
- Result getResult();
- void toStream(std::ostream& out) const;
-protected:
- BoolExpr d_expr;
- Result d_result;
-};/* class CheckSatCommand */
-
-class CVC4_PUBLIC QueryCommand : public Command {
-public:
- QueryCommand(const BoolExpr& e);
- void invoke(SmtEngine* smt);
- Result getResult();
- void toStream(std::ostream& out) const;
-protected:
- BoolExpr d_expr;
- Result d_result;
-};/* class QueryCommand */
-
-class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
-public:
- /** The status an SMT benchmark can have */
- enum BenchmarkStatus {
- /** Benchmark is satisfiable */
- SMT_SATISFIABLE,
- /** Benchmark is unsatisfiable */
- SMT_UNSATISFIABLE,
- /** The status of the benchmark is unknown */
- SMT_UNKNOWN
- };
- SetBenchmarkStatusCommand(BenchmarkStatus status);
- void invoke(SmtEngine* smt);
- void toStream(std::ostream& out) const;
-protected:
- BenchmarkStatus d_status;
-};/* class SetBenchmarkStatusCommand */
-
-inline std::ostream& operator<<(std::ostream& out,
- SetBenchmarkStatusCommand::BenchmarkStatus bs)
- CVC4_PUBLIC;
-
-class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
-public:
- SetBenchmarkLogicCommand(std::string logic);
- void invoke(SmtEngine* smt);
- void toStream(std::ostream& out) const;
-protected:
- std::string d_logic;
-};/* class SetBenchmarkLogicCommand */
-
-class CVC4_PUBLIC CommandSequence : public Command {
-public:
- CommandSequence();
- ~CommandSequence();
- void invoke(SmtEngine* smt);
- void addCommand(Command* cmd);
- void toStream(std::ostream& out) const;
-
- typedef std::vector<Command*>::iterator iterator;
- typedef std::vector<Command*>::const_iterator const_iterator;
-
- const_iterator begin() const { return d_commandSequence.begin(); }
- const_iterator end() const { return d_commandSequence.end(); }
-
- iterator begin() { return d_commandSequence.begin(); }
- iterator end() { return d_commandSequence.end(); }
-
-private:
- /** All the commands to be executed (in sequence) */
- std::vector<Command*> d_commandSequence;
- /** Next command to be executed */
- unsigned int d_index;
-};/* class CommandSequence */
-
-}/* CVC4 namespace */
-
-/* =========== inline function definitions =========== */
-
-#include "smt/smt_engine.h"
-
-namespace CVC4 {
-
-inline std::ostream& operator<<(std::ostream& out, const Command& c) {
- c.toStream(out);
- return out;
-}
-
-/* class Command */
-
-inline std::string Command::toString() const {
- std::stringstream ss;
- toStream(ss);
- return ss.str();
-}
-
-/* class EmptyCommand */
-
-inline EmptyCommand::EmptyCommand(std::string name) :
- d_name(name) {
-}
-
-inline void EmptyCommand::invoke(SmtEngine* smt_engine) {
-}
-
-inline void EmptyCommand::toStream(std::ostream& out) const {
- out << "EmptyCommand(" << d_name << ")";
-}
-
-/* class AssertCommand */
-
-inline AssertCommand::AssertCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-inline void AssertCommand::invoke(SmtEngine* smt_engine) {
- smt_engine->assertFormula(d_expr);
-}
-
-inline void AssertCommand::toStream(std::ostream& out) const {
- out << "Assert(" << d_expr << ")";
-}
-
-/* class CheckSatCommand */
-
-inline CheckSatCommand::CheckSatCommand() {
-}
-
-inline CheckSatCommand::CheckSatCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-inline void CheckSatCommand::invoke(SmtEngine* smt_engine) {
- d_result = smt_engine->checkSat(d_expr);
-}
-
-inline Result CheckSatCommand::getResult() {
- return d_result;
-}
-
-/* class QueryCommand */
-
-inline QueryCommand::QueryCommand(const BoolExpr& e) :
- d_expr(e) {
-}
-
-inline void QueryCommand::invoke(CVC4::SmtEngine* smt_engine) {
- d_result = smt_engine->query(d_expr);
-}
-
-inline Result QueryCommand::getResult() {
- return d_result;
-}
-
-inline void QueryCommand::toStream(std::ostream& out) const {
- out << "Query(";
- d_expr.printAst(out, 0);
- out << ")";
-}
-
-/* class CommandSequence */
-
-inline CommandSequence::CommandSequence() :
- d_index(0) {
-}
-
-inline void CommandSequence::addCommand(Command* cmd) {
- d_commandSequence.push_back(cmd);
-}
-
-/* class DeclarationCommand */
-
-inline DeclarationCommand::DeclarationCommand(const std::vector<std::string>& ids) :
- d_declaredSymbols(ids) {
-}
-
-/* class SetBenchmarkStatusCommand */
-
-inline SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus s) :
- d_status(s) {
-}
-
-inline void SetBenchmarkStatusCommand::invoke(SmtEngine* smt) {
- // FIXME: TODO: something to be done with the status
-}
-
-inline void SetBenchmarkStatusCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkStatus(" << d_status << ")";
-}
-
-/* class SetBenchmarkLogicCommand */
-
-inline SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string l) :
- d_logic(l) {
-}
-
-inline void SetBenchmarkLogicCommand::invoke(SmtEngine* smt) {
- // FIXME: TODO: something to be done with the logic
-}
-
-inline void SetBenchmarkLogicCommand::toStream(std::ostream& out) const {
- out << "SetBenchmarkLogic(" << d_logic << ")";
-}
-
-/* output stream insertion operator for benchmark statuses */
-inline std::ostream& operator<<(std::ostream& out,
- SetBenchmarkStatusCommand::BenchmarkStatus bs) {
- switch(bs) {
-
- case SetBenchmarkStatusCommand::SMT_SATISFIABLE:
- return out << "sat";
-
- case SetBenchmarkStatusCommand::SMT_UNSATISFIABLE:
- return out << "unsat";
-
- case SetBenchmarkStatusCommand::SMT_UNKNOWN:
- return out << "unknown";
-
- default:
- return out << "SetBenchmarkStatusCommand::[UNKNOWNSTATUS!]";
- }
-}
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__COMMAND_H */
#include "expr/expr.h"
#include "expr/expr_manager.h"
#include "parser/parser.h"
-#include "util/command.h"
+#include "expr/command.h"
using namespace CVC4;
using namespace CVC4::parser;
projects / cvc5.git / commitdiff