From: Morgan Deters Date: Thu, 4 Feb 2010 03:31:38 +0000 (+0000) Subject: src/expr/kind.h is now automatically generated. X-Git-Tag: cvc5-1.0.0~9291 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fc14c009e8e9d2274368b54c12f3580a9ec8f718;p=cvc5.git src/expr/kind.h is now automatically generated. 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. --- diff --git a/src/Makefile.am b/src/Makefile.am index fac263152..11173b7e4 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -17,7 +17,7 @@ AM_CPPFLAGS = -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 diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 046281702..3212fc0a0 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -15,11 +15,27 @@ libexpr_la_SOURCES = \ 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 diff --git a/src/expr/command.cpp b/src/expr/command.cpp new file mode 100644 index 000000000..2f8dd789e --- /dev/null +++ b/src/expr/command.cpp @@ -0,0 +1,74 @@ +/********************* -*- 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 */ diff --git a/src/expr/command.h b/src/expr/command.h new file mode 100644 index 000000000..dedefb782 --- /dev/null +++ b/src/expr/command.h @@ -0,0 +1,297 @@ +/********************* -*- 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 +#include +#include +#include + +#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& ids); + void toStream(std::ostream& out) const; +protected: + std::vector 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::iterator iterator; + typedef std::vector::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 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& 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 */ diff --git a/src/expr/kind.h b/src/expr/kind.h deleted file mode 100644 index 575a4790c..000000000 --- a/src/expr/kind.h +++ /dev/null @@ -1,100 +0,0 @@ -/********************* -*- 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 - -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 */ diff --git a/src/expr/kind_epilogue.h b/src/expr/kind_epilogue.h new file mode 100644 index 000000000..0db7038d8 --- /dev/null +++ b/src/expr/kind_epilogue.h @@ -0,0 +1,25 @@ +/********************* -*- 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 */ diff --git a/src/expr/kind_middle.h b/src/expr/kind_middle.h new file mode 100644 index 000000000..6c352c3c9 --- /dev/null +++ b/src/expr/kind_middle.h @@ -0,0 +1,33 @@ +/********************* -*- 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; diff --git a/src/expr/kind_prologue.h b/src/expr/kind_prologue.h new file mode 100644 index 000000000..cf9d2e3be --- /dev/null +++ b/src/expr/kind_prologue.h @@ -0,0 +1,34 @@ +/********************* -*- 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 + +namespace CVC4 { + +enum Kind { + /* undefined */ + UNDEFINED_KIND = -1, + /** Null Kind */ + NULL_EXPR, + + /* built-ins */ + EQUAL, + ITE, + SKOLEM, + VARIABLE, diff --git a/src/expr/mkkind b/src/expr/mkkind new file mode 100755 index 000000000..c8ad61571 --- /dev/null +++ b/src/expr/mkkind @@ -0,0 +1,54 @@ +#!/bin/bash +# +# mkkind +# Morgan Deters 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 <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; @@ -148,6 +159,10 @@ int parseOptions(int argc, char** argv, CVC4::Options* opts) throw(OptionExcepti 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; diff --git a/src/main/main.cpp b/src/main/main.cpp index 02ebe8deb..de179edb8 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -25,7 +25,7 @@ #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" diff --git a/src/main/main.h b/src/main/main.h index 9b2f4fcbe..0c78912ae 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -28,12 +28,31 @@ struct Options; 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 */ diff --git a/src/main/usage.h b/src/main/usage.h index f6c089f1d..6927f0f2f 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -27,8 +27,7 @@ usage: %s [options] [input-file]\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\ + --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\ @@ -36,6 +35,7 @@ CVC4 options:\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 */ diff --git a/src/main/util.cpp b/src/main/util.cpp index df4ab803d..03ae26092 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -10,7 +10,7 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** [[ Add file-specific comments here ]] + ** Utilities for the main driver. **/ #include @@ -22,24 +22,48 @@ #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; diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp index 053eb8a11..58f1babd0 100644 --- a/src/parser/antlr_parser.cpp +++ b/src/parser/antlr_parser.cpp @@ -25,7 +25,7 @@ #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; diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g index 5832847fc..9a77ea178 100644 --- a/src/parser/cvc/cvc_parser.g +++ b/src/parser/cvc/cvc_parser.g @@ -10,13 +10,12 @@ ** 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" { @@ -74,7 +73,7 @@ command returns [CVC4::Command* cmd = 0] : 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 sorts; diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 6a70b5181..71f38e87f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -18,7 +18,7 @@ #include #include "parser.h" -#include "util/command.h" +#include "expr/command.h" #include "util/output.h" #include "util/Assert.h" #include "parser_exception.h" diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g index fe98063cc..8bc557bbd 100644 --- a/src/parser/smt/smt_parser.g +++ b/src/parser/smt/smt_parser.g @@ -15,7 +15,7 @@ header "post_include_hpp" { #include "parser/antlr_parser.h" -#include "util/command.h" +#include "expr/command.h" } header "post_include_cpp" { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 047daace8..f4b10414c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -109,7 +109,7 @@ Result PropEngine::solve() { 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::iterator atomIter = d_atom2lit.begin(); diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2d36da0f1..09790882c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -14,7 +14,7 @@ #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" diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 316c747de..9c3431499 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -10,8 +10,6 @@ libutil_la_SOURCES = \ Assert.cpp \ Makefile.am \ Makefile.in \ - command.cpp \ - command.h \ debug.h \ decision_engine.cpp \ decision_engine.h \ diff --git a/src/util/command.cpp b/src/util/command.cpp deleted file mode 100644 index 58f8b41bb..000000000 --- a/src/util/command.cpp +++ /dev/null @@ -1,74 +0,0 @@ -/********************* -*- 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 */ diff --git a/src/util/command.h b/src/util/command.h deleted file mode 100644 index 81af801d1..000000000 --- a/src/util/command.h +++ /dev/null @@ -1,301 +0,0 @@ -/********************* -*- 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 -#include -#include -#include - -#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& ids); - void toStream(std::ostream& out) const; -protected: - std::vector 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::iterator iterator; - typedef std::vector::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 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& 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 */ diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 1d5de423e..28a38892f 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -20,7 +20,7 @@ #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;