diff options
Diffstat (limited to 'src')
31 files changed, 1087 insertions, 625 deletions
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index ca09fc3d5..bfc116fd6 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -12,99 +12,139 @@ # LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ +AUTOMAKE_OPTIONS = subdir-objects + AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. AM_CXXFLAGS = -Wall -SUBDIRS = . compat +SUBDIRS = compat + +# any binding-specific flags to pass to swig +java_cpp_SWIGFLAGS = -package edu.nyu.acsys.CVC4 lib_LTLIBRARIES = bin_PROGRAMS = javadatadir = $(datadir)/java +javalibdir = $(datadir)/java ocamldatadir = $(libdir)/ocaml/cvc4 +ocamllibdir = $(libdir)/ocaml/cvc4 +perldatadir = $(datadir)/perl5 +perllibdir = $(libdir)/perl5 +phpdatadir = $(datadir)/php +phplibdir = $(libdir)/php +pythondatadir = $(datadir)/pyshared +pythonlibdir = $(libdir)/pyshared +csharpdatadir = $(datadir)/csharp +csharplibdir = $(libdir)/csharp +rubylibdir = $(libdir)/ruby +tcllibdir = $(libdir)/tcltk javadata_DATA = +javalib_LTLIBRARIES= ocamldata_DATA = +ocamllib_LTLIBRARIES= +perldata_DATA = +perllib_LTLIBRARIES = +phpdata_DATA = +phplib_LTLIBRARIES = +pythondata_DATA = +pythonlib_LTLIBRARIES = +csharpdata_DATA = +csharplib_LTLIBRARIES = +rubylib_LTLIBRARIES = +tcllib_LTLIBRARIES = if CVC4_LANGUAGE_BINDING_JAVA -lib_LTLIBRARIES += libcvc4bindings_java.la +javalib_LTLIBRARIES += java/CVC4.la javadata_DATA += cvc4.jar -libcvc4bindings_java_la_LDFLAGS = \ +java_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_java_la_LIBADD = \ +java_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser endif if CVC4_LANGUAGE_BINDING_CSHARP -lib_LTLIBRARIES += libcvc4bindings_csharp.la -libcvc4bindings_csharp_la_LDFLAGS = \ +csharplib_LTLIBRARIES += csharp/CVC4.la +csharp_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_csharp_la_LIBADD = \ +csharp_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser endif if CVC4_LANGUAGE_BINDING_PERL -lib_LTLIBRARIES += libcvc4bindings_perl.la -libcvc4bindings_perl_la_LDFLAGS = \ +perllib_LTLIBRARIES += perl/CVC4.la +perl_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_perl_la_LIBADD = \ +perl_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser +perldata_DATA += perl/CVC4.pm endif if CVC4_LANGUAGE_BINDING_PHP -lib_LTLIBRARIES += libcvc4bindings_php.la -libcvc4bindings_php_la_LDFLAGS = \ +phplib_LTLIBRARIES += php/CVC4.la +php_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_php_la_LIBADD = \ +php_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser +phpdata_DATA += php/CVC4.php endif if CVC4_LANGUAGE_BINDING_PYTHON -lib_LTLIBRARIES += libcvc4bindings_python.la -libcvc4bindings_python_la_LDFLAGS = \ +pythonlib_LTLIBRARIES += python/CVC4.la +python_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_python_la_LIBADD = \ +python_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser +pythondata_DATA += python/CVC4.py endif if CVC4_LANGUAGE_BINDING_OCAML -lib_LTLIBRARIES += libcvc4bindings_ocaml.la +ocamllib_LTLIBRARIES += ocaml/CVC4.la bin_PROGRAMS += cvc4_ocaml_top # We provide a make rule below, but we have to tell automake to lay off, too, # otherwise it tries (and fails) to package the nonexistent cvc4_ocaml_top.c! cvc4_ocaml_top_SOURCES = ocamldata_DATA += ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/swigp4.cmi ocaml/CVC4.cmo ocaml/CVC4.cmi -libcvc4bindings_ocaml_la_LDFLAGS = \ +ocaml_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_ocaml_la_LIBADD = \ +ocaml_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser endif if CVC4_LANGUAGE_BINDING_RUBY -lib_LTLIBRARIES += libcvc4bindings_ruby.la -libcvc4bindings_ruby_la_LDFLAGS = \ +rubylib_LTLIBRARIES += ruby/CVC4.la +ruby_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_ruby_la_LIBADD = \ +ruby_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser endif if CVC4_LANGUAGE_BINDING_TCL -lib_LTLIBRARIES += libcvc4bindings_tcl.la -libcvc4bindings_tcl_la_LDFLAGS = \ +tcllib_LTLIBRARIES += tcl/CVC4.la +tcl_CVC4_la_LDFLAGS = \ + -module \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_tcl_la_LIBADD = \ +tcl_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser endif -nodist_libcvc4bindings_java_la_SOURCES = java.cpp -libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing -nodist_libcvc4bindings_csharp_la_SOURCES = csharp.cpp -nodist_libcvc4bindings_perl_la_SOURCES = perl.cpp -nodist_libcvc4bindings_php_la_SOURCES = php.cpp -nodist_libcvc4bindings_python_la_SOURCES = python.cpp -nodist_libcvc4bindings_ocaml_la_SOURCES = ocaml.cpp -nodist_libcvc4bindings_ruby_la_SOURCES = ruby.cpp -nodist_libcvc4bindings_tcl_la_SOURCES = tcl.cpp +nodist_java_CVC4_la_SOURCES = java.cpp +java_CVC4_la_CXXFLAGS = -fno-strict-aliasing +nodist_csharp_CVC4_la_SOURCES = csharp.cpp +nodist_perl_CVC4_la_SOURCES = perl.cpp +nodist_php_CVC4_la_SOURCES = php.cpp +nodist_python_CVC4_la_SOURCES = python.cpp +nodist_ocaml_CVC4_la_SOURCES = ocaml.cpp +nodist_ruby_CVC4_la_SOURCES = ruby.cpp +nodist_tcl_CVC4_la_SOURCES = tcl.cpp CLEANFILES = \ java.cpp \ @@ -123,7 +163,7 @@ MOSTLYCLEANFILES = \ $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \ cvc4.jar -libcvc4bindings_java_la-java.lo java.lo: java.cpp +java_CVC4_la-java.lo java.lo: java.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $< cvc4.jar: java.cpp $(AM_V_GEN) \ @@ -133,16 +173,17 @@ cvc4.jar: java.cpp $(JAVAC) -classpath . -d classes `find . -name '*.java'`; \ cd classes); \ $(JAR) cf $@ -C java/classes . -java.cpp:; +#java.cpp:; csharp.lo: csharp.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(CSHARP_CPPFLAGS) -o $@ $< -csharp.cpp:; +#csharp.cpp:; perl.lo: perl.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $< -perl.cpp:; +#perl.cpp:; +perl/CVC4.pm: perl.cpp php.lo: php.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $< -php.cpp:; +#php.cpp:; python.lo: python.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $< ocaml.lo: ocaml.cpp @@ -155,26 +196,18 @@ ocaml/swigp4.cmo: ocaml/swigp4.ml; $(AM_V_GEN)$(OCAMLFIND) ocamlc -package camlp ocaml/swig.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.ml ocaml/swig.mli:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.mli ocaml/swigp4.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swigp4.ml -ocaml.cpp:; -cvc4_ocaml_top: libcvc4bindings_ocaml.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi libcvc4bindings_ocaml.la +#ocaml.cpp:; +cvc4_ocaml_top: ocaml/CVC4.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi $(AM_V_GEN)\ - $(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib -L.libs -cclib -L. -cclib -lcvc4bindings_ocaml -cclib -lstdc++ + $(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib ocaml/.libs/CVC4.so -cclib -lstdc++ ruby.lo: ruby.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $< tcl.lo: tcl.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $< -tcl.cpp:; -java.cpp: @srcdir@/../cvc4.i - $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) - $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $< -# somehow, NULL gets translated to ((void*)0) prematurely, and this causes compiler errors ?! -ruby.cpp python.cpp: @srcdir@/../cvc4.i - $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) - $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $< - $(AM_V_at)mv $@ $@.old && sed 's,((void\*) 0),NULL,g' $@.old > $@ -$(patsubst %,%.cpp,$(filter-out c c++ java,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i +#tcl.cpp:; +$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) - $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $< + $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) $($(subst .,_,$@)_SWIGFLAGS) -o $@ $< $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $< diff --git a/src/cvc4.i b/src/cvc4.i index 7723aee6e..8505d5128 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -25,11 +25,14 @@ namespace std { // caml_invalid_argument and caml_flush, which breaks C++ // standard headers; undo this damage // -// Unfortunately, this doesn't happen early enough. swig puts an -// include <stdexcept> very early, which breaks linking due to a +// Unfortunately, this code isn't inserted early enough. swig puts +// an include <stdexcept> very early, which breaks linking due to a // nonexistent std::caml_invalid_argument symbol.. ridiculous! // #ifdef SWIGOCAML +# if defined(flush) || defined(invalid_argument) +# error "flush" or "invalid_argument" (or both) is defined by the ocaml headers. You must #undef it above before inclusion of <stdexcept>. +# endif /* flush */ # undef flush # undef invalid_argument #endif /* SWIGOCAML */ diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 345d7f956..47c6d1eb5 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -21,6 +21,7 @@ #include <utility> #include <iterator> #include <sstream> +#include <exception> #include "expr/command.h" #include "smt/smt_engine.h" @@ -34,7 +35,10 @@ using namespace std; namespace CVC4 { -std::ostream& operator<<(std::ostream& out, const Command& c) { +const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc(); +const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess(); + +std::ostream& operator<<(std::ostream& out, const Command& c) throw() { c.toStream(out, Node::setdepth::getDepth(out), Node::printtypes::getPrintTypes(out), @@ -42,7 +46,7 @@ std::ostream& operator<<(std::ostream& out, const Command& c) { return out; } -ostream& operator<<(ostream& out, const Command* c) { +ostream& operator<<(ostream& out, const Command* c) throw() { if(c == NULL) { out << "null"; } else { @@ -51,180 +55,259 @@ ostream& operator<<(ostream& out, const Command* c) { return out; } +std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() { + s.toStream(out, Node::setlanguage::getLanguage(out)); + return out; +} + +ostream& operator<<(ostream& out, const CommandStatus* s) throw() { + if(s == NULL) { + out << "null"; + } else { + out << *s; + } + return out; +} + /* class Command */ -void Command::invoke(SmtEngine* smtEngine, std::ostream& out) { +Command::Command() throw() : d_commandStatus(NULL) { +} + +Command::~Command() throw() { + if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) { + delete d_commandStatus; + } +} + +bool Command::ok() const throw() { + // either we haven't run the command yet, or it ran successfully + return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL; +} + +void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { invoke(smtEngine); printResult(out); } -std::string Command::toString() const { +std::string Command::toString() const throw() { std::stringstream ss; toStream(ss); return ss.str(); } void Command::toStream(std::ostream& out, int toDepth, bool types, - OutputLanguage language) const { + OutputLanguage language) const throw() { Printer::getPrinter(language)->toStream(out, this, toDepth, types); } -void Command::printResult(std::ostream& out) const { +void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() { + Printer::getPrinter(language)->toStream(out, this); +} + +void Command::printResult(std::ostream& out) const throw() { + if(d_commandStatus != NULL) { + out << *d_commandStatus; + } } /* class EmptyCommand */ -EmptyCommand::EmptyCommand(std::string name) : +EmptyCommand::EmptyCommand(std::string name) throw() : d_name(name) { } -std::string EmptyCommand::getName() const { +std::string EmptyCommand::getName() const throw() { return d_name; } -void EmptyCommand::invoke(SmtEngine* smtEngine) { +void EmptyCommand::invoke(SmtEngine* smtEngine) throw() { /* empty commands have no implementation */ + d_commandStatus = CommandSuccess::instance(); } /* class AssertCommand */ -AssertCommand::AssertCommand(const BoolExpr& e) : +AssertCommand::AssertCommand(const BoolExpr& e) throw() : d_expr(e) { } -BoolExpr AssertCommand::getExpr() const { +BoolExpr AssertCommand::getExpr() const throw() { return d_expr; } -void AssertCommand::invoke(SmtEngine* smtEngine) { - smtEngine->assertFormula(d_expr); +void AssertCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->assertFormula(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } /* class PushCommand */ -void PushCommand::invoke(SmtEngine* smtEngine) { - smtEngine->push(); +void PushCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->push(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } /* class PopCommand */ -void PopCommand::invoke(SmtEngine* smtEngine) { - smtEngine->pop(); +void PopCommand::invoke(SmtEngine* smtEngine) throw() { + try { + smtEngine->pop(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } /* class CheckSatCommand */ -CheckSatCommand::CheckSatCommand() : +CheckSatCommand::CheckSatCommand() throw() : d_expr() { } -CheckSatCommand::CheckSatCommand(const BoolExpr& expr) : +CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() : d_expr(expr) { } -BoolExpr CheckSatCommand::getExpr() const { +BoolExpr CheckSatCommand::getExpr() const throw() { return d_expr; } -void CheckSatCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->checkSat(d_expr); +void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->checkSat(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -Result CheckSatCommand::getResult() const { +Result CheckSatCommand::getResult() const throw() { return d_result; } -void CheckSatCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void CheckSatCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class QueryCommand */ -QueryCommand::QueryCommand(const BoolExpr& e) : +QueryCommand::QueryCommand(const BoolExpr& e) throw() : d_expr(e) { } -BoolExpr QueryCommand::getExpr() const { +BoolExpr QueryCommand::getExpr() const throw() { return d_expr; } -void QueryCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->query(d_expr); +void QueryCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->query(d_expr); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -Result QueryCommand::getResult() const { +Result QueryCommand::getResult() const throw() { return d_result; } -void QueryCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void QueryCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class QuitCommand */ -QuitCommand::QuitCommand() { +QuitCommand::QuitCommand() throw() { } -void QuitCommand::invoke(SmtEngine* smtEngine) { +void QuitCommand::invoke(SmtEngine* smtEngine) throw() { Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); } /* class CommentCommand */ -CommentCommand::CommentCommand(std::string comment) : d_comment(comment) { +CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) { } -std::string CommentCommand::getComment() const { +std::string CommentCommand::getComment() const throw() { return d_comment; } -void CommentCommand::invoke(SmtEngine* smtEngine) { +void CommentCommand::invoke(SmtEngine* smtEngine) throw() { Dump("benchmark") << *this; + d_commandStatus = CommandSuccess::instance(); } /* class CommandSequence */ -CommandSequence::CommandSequence() : +CommandSequence::CommandSequence() throw() : d_index(0) { } -CommandSequence::~CommandSequence() { +CommandSequence::~CommandSequence() throw() { for(unsigned i = d_index; i < d_commandSequence.size(); ++i) { delete d_commandSequence[i]; } } -void CommandSequence::addCommand(Command* cmd) { +void CommandSequence::addCommand(Command* cmd) throw() { d_commandSequence.push_back(cmd); } -void CommandSequence::invoke(SmtEngine* smtEngine) { +void CommandSequence::invoke(SmtEngine* smtEngine) throw() { for(; d_index < d_commandSequence.size(); ++d_index) { d_commandSequence[d_index]->invoke(smtEngine); + if(! d_commandSequence[d_index]->ok()) { + // abort execution + d_commandStatus = d_commandSequence[d_index]->getCommandStatus(); + return; + } delete d_commandSequence[d_index]; } + + AlwaysAssert(d_commandStatus == NULL); + d_commandStatus = CommandSuccess::instance(); } -void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) { +void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() { for(; d_index < d_commandSequence.size(); ++d_index) { d_commandSequence[d_index]->invoke(smtEngine, out); delete d_commandSequence[d_index]; } } -CommandSequence::const_iterator CommandSequence::begin() const { +CommandSequence::const_iterator CommandSequence::begin() const throw() { return d_commandSequence.begin(); } -CommandSequence::const_iterator CommandSequence::end() const { +CommandSequence::const_iterator CommandSequence::end() const throw() { return d_commandSequence.end(); } -CommandSequence::iterator CommandSequence::begin() { +CommandSequence::iterator CommandSequence::begin() throw() { return d_commandSequence.begin(); } -CommandSequence::iterator CommandSequence::end() { +CommandSequence::iterator CommandSequence::end() throw() { return d_commandSequence.end(); } @@ -232,53 +315,53 @@ CommandSequence::iterator CommandSequence::end() { /* class DeclarationDefinitionCommand */ -DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) : +DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() : d_symbol(id) { } -std::string DeclarationDefinitionCommand::getSymbol() const { +std::string DeclarationDefinitionCommand::getSymbol() const throw() { return d_symbol; } /* class DeclareFunctionCommand */ -DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) : +DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) throw() : DeclarationDefinitionCommand(id), d_type(t) { } -Type DeclareFunctionCommand::getType() const { +Type DeclareFunctionCommand::getType() const throw() { return d_type; } -void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) { +void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } /* class DeclareTypeCommand */ -DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) : +DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() : DeclarationDefinitionCommand(id), d_arity(arity), d_type(t) { } -size_t DeclareTypeCommand::getArity() const { +size_t DeclareTypeCommand::getArity() const throw() { return d_arity; } -Type DeclareTypeCommand::getType() const { +Type DeclareTypeCommand::getType() const throw() { return d_type; } -void DeclareTypeCommand::invoke(SmtEngine* smtEngine) { +void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; } /* class DefineTypeCommand */ DefineTypeCommand::DefineTypeCommand(const std::string& id, - Type t) : + Type t) throw() : DeclarationDefinitionCommand(id), d_params(), d_type(t) { @@ -286,29 +369,30 @@ DefineTypeCommand::DefineTypeCommand(const std::string& id, DefineTypeCommand::DefineTypeCommand(const std::string& id, const std::vector<Type>& params, - Type t) : + Type t) throw() : DeclarationDefinitionCommand(id), d_params(params), d_type(t) { } -const std::vector<Type>& DefineTypeCommand::getParameters() const { +const std::vector<Type>& DefineTypeCommand::getParameters() const throw() { return d_params; } -Type DefineTypeCommand::getType() const { +Type DefineTypeCommand::getType() const throw() { return d_type; } -void DefineTypeCommand::invoke(SmtEngine* smtEngine) { +void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; + d_commandStatus = CommandSuccess::instance(); } /* class DefineFunctionCommand */ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, - Expr formula) : + Expr formula) throw() : DeclarationDefinitionCommand(id), d_func(func), d_formals(), @@ -318,30 +402,31 @@ DefineFunctionCommand::DefineFunctionCommand(const std::string& id, DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) : + Expr formula) throw() : DeclarationDefinitionCommand(id), d_func(func), d_formals(formals), d_formula(formula) { } -Expr DefineFunctionCommand::getFunction() const { +Expr DefineFunctionCommand::getFunction() const throw() { return d_func; } -const std::vector<Expr>& DefineFunctionCommand::getFormals() const { +const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() { return d_formals; } -Expr DefineFunctionCommand::getFormula() const { +Expr DefineFunctionCommand::getFormula() const throw() { return d_formula; } -void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { +void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() { //Dump("declarations") << *this << endl; -- done by SmtEngine if(!d_func.isNull()) { smtEngine->defineFunction(d_func, d_formals, d_formula); } + d_commandStatus = CommandSuccess::instance(); } /* class DefineNamedFunctionCommand */ @@ -349,314 +434,339 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) : + Expr formula) throw() : DefineFunctionCommand(id, func, formals, formula) { } -void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) { +void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() { this->DefineFunctionCommand::invoke(smtEngine); if(!d_func.isNull() && d_func.getType().isBoolean()) { - smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, - d_func)); + smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func)); } + d_commandStatus = CommandSuccess::instance(); } /* class Simplify */ -SimplifyCommand::SimplifyCommand(Expr term) : +SimplifyCommand::SimplifyCommand(Expr term) throw() : d_term(term) { } -Expr SimplifyCommand::getTerm() const { +Expr SimplifyCommand::getTerm() const throw() { return d_term; } -void SimplifyCommand::invoke(SmtEngine* smtEngine) { +void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() { d_result = smtEngine->simplify(d_term); + d_commandStatus = CommandSuccess::instance(); } -Expr SimplifyCommand::getResult() const { +Expr SimplifyCommand::getResult() const throw() { return d_result; } -void SimplifyCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void SimplifyCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class GetValueCommand */ -GetValueCommand::GetValueCommand(Expr term) : +GetValueCommand::GetValueCommand(Expr term) throw() : d_term(term) { } -Expr GetValueCommand::getTerm() const { +Expr GetValueCommand::getTerm() const throw() { return d_term; } -void GetValueCommand::invoke(SmtEngine* smtEngine) { +void GetValueCommand::invoke(SmtEngine* smtEngine) throw() { d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term, smtEngine->getValue(d_term)); + d_commandStatus = CommandSuccess::instance(); } -Expr GetValueCommand::getResult() const { +Expr GetValueCommand::getResult() const throw() { return d_result; } -void GetValueCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void GetValueCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class GetAssignmentCommand */ -GetAssignmentCommand::GetAssignmentCommand() { +GetAssignmentCommand::GetAssignmentCommand() throw() { } -void GetAssignmentCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->getAssignment(); +void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getAssignment(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -SExpr GetAssignmentCommand::getResult() const { +SExpr GetAssignmentCommand::getResult() const throw() { return d_result; } -void GetAssignmentCommand::printResult(std::ostream& out) const { - out << d_result << endl; +void GetAssignmentCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result << endl; + } } /* class GetProofCommand */ -GetProofCommand::GetProofCommand() { +GetProofCommand::GetProofCommand() throw() { } -void GetProofCommand::invoke(SmtEngine* smtEngine) { - d_result = smtEngine->getProof(); +void GetProofCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->getProof(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -Proof* GetProofCommand::getResult() const { +Proof* GetProofCommand::getResult() const throw() { return d_result; } -void GetProofCommand::printResult(std::ostream& out) const { - d_result->toStream(out); +void GetProofCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + d_result->toStream(out); + } } /* class GetAssertionsCommand */ -GetAssertionsCommand::GetAssertionsCommand() { +GetAssertionsCommand::GetAssertionsCommand() throw() { } -void GetAssertionsCommand::invoke(SmtEngine* smtEngine) { - stringstream ss; - const vector<Expr> v = smtEngine->getAssertions(); - copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); - d_result = ss.str(); +void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() { + try { + stringstream ss; + const vector<Expr> v = smtEngine->getAssertions(); + copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") ); + d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } } -std::string GetAssertionsCommand::getResult() const { +std::string GetAssertionsCommand::getResult() const throw() { return d_result; } -void GetAssertionsCommand::printResult(std::ostream& out) const { - out << d_result; +void GetAssertionsCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else { + out << d_result; + } } /* class SetBenchmarkStatusCommand */ -SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) : +SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() : d_status(status) { } -BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const { +BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() { return d_status; } -void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) { - stringstream ss; - ss << d_status; - SExpr status = ss.str(); +void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() { try { + stringstream ss; + ss << d_status; + SExpr status = ss.str(); smtEngine->setInfo(":status", status); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; - } catch(BadOptionException&) { - // should not happen - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class SetBenchmarkLogicCommand */ -SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) : +SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() : d_logic(logic) { } -std::string SetBenchmarkLogicCommand::getLogic() const { +std::string SetBenchmarkLogicCommand::getLogic() const throw() { return d_logic; } -void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) { +void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->setLogic(d_logic); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class SetInfoCommand */ -SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) : +SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() : d_flag(flag), d_sexpr(sexpr) { } -std::string SetInfoCommand::getFlag() const { +std::string SetInfoCommand::getFlag() const throw() { return d_flag; } -SExpr SetInfoCommand::getSExpr() const { +SExpr SetInfoCommand::getSExpr() const throw() { return d_sexpr; } -void SetInfoCommand::invoke(SmtEngine* smtEngine) { +void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->setInfo(d_flag, d_sexpr); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; - } -} - -std::string SetInfoCommand::getResult() const { - return d_result; -} - -void SetInfoCommand::printResult(std::ostream& out) const { - if(d_result != "") { - out << d_result << endl; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class GetInfoCommand */ -GetInfoCommand::GetInfoCommand(std::string flag) : +GetInfoCommand::GetInfoCommand(std::string flag) throw() : d_flag(flag) { } -std::string GetInfoCommand::getFlag() const { +std::string GetInfoCommand::getFlag() const throw() { return d_flag; } -void GetInfoCommand::invoke(SmtEngine* smtEngine) { +void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() { try { stringstream ss; ss << smtEngine->getInfo(d_flag); d_result = ss.str(); + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } -std::string GetInfoCommand::getResult() const { +std::string GetInfoCommand::getResult() const throw() { return d_result; } -void GetInfoCommand::printResult(std::ostream& out) const { - if(d_result != "") { +void GetInfoCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else if(d_result != "") { out << d_result << endl; } } /* class SetOptionCommand */ -SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) : +SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() : d_flag(flag), d_sexpr(sexpr) { } -std::string SetOptionCommand::getFlag() const { +std::string SetOptionCommand::getFlag() const throw() { return d_flag; } -SExpr SetOptionCommand::getSExpr() const { +SExpr SetOptionCommand::getSExpr() const throw() { return d_sexpr; } -void SetOptionCommand::invoke(SmtEngine* smtEngine) { +void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() { try { smtEngine->setOption(d_flag, d_sexpr); - //d_result = "success"; - } catch(ModalException&) { - d_result = "error"; + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; - } -} - -std::string SetOptionCommand::getResult() const { - return d_result; -} - -void SetOptionCommand::printResult(std::ostream& out) const { - if(d_result != "") { - out << d_result << endl; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } /* class GetOptionCommand */ -GetOptionCommand::GetOptionCommand(std::string flag) : +GetOptionCommand::GetOptionCommand(std::string flag) throw() : d_flag(flag) { } -std::string GetOptionCommand::getFlag() const { +std::string GetOptionCommand::getFlag() const throw() { return d_flag; } -void GetOptionCommand::invoke(SmtEngine* smtEngine) { +void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() { try { d_result = smtEngine->getOption(d_flag).getValue(); + d_commandStatus = CommandSuccess::instance(); } catch(BadOptionException&) { - d_result = "unsupported"; + d_commandStatus = new CommandUnsupported(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); } } -std::string GetOptionCommand::getResult() const { +std::string GetOptionCommand::getResult() const throw() { return d_result; } -void GetOptionCommand::printResult(std::ostream& out) const { - if(d_result != "") { +void GetOptionCommand::printResult(std::ostream& out) const throw() { + if(! ok()) { + this->Command::printResult(out); + } else if(d_result != "") { out << d_result << endl; } } /* class DatatypeDeclarationCommand */ -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) : +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() : d_datatypes() { d_datatypes.push_back(datatype); } -DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) : +DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() : d_datatypes(datatypes) { } const std::vector<DatatypeType>& -DatatypeDeclarationCommand::getDatatypes() const { +DatatypeDeclarationCommand::getDatatypes() const throw() { return d_datatypes; } -void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) { +void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { Dump("declarations") << *this << endl; + d_commandStatus = CommandSuccess::instance(); } /* output stream insertion operator for benchmark statuses */ std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) { + BenchmarkStatus status) throw() { switch(status) { case SMT_SATISFIABLE: diff --git a/src/expr/command.h b/src/expr/command.h index b686025fe..cf8c1b615 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -41,9 +41,12 @@ namespace CVC4 { class SmtEngine; class Command; +class CommandStatus; -std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC; -std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC; +std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC; /** The status an SMT benchmark can have */ enum BenchmarkStatus { @@ -56,21 +59,156 @@ enum BenchmarkStatus { }; std::ostream& operator<<(std::ostream& out, - BenchmarkStatus status) CVC4_PUBLIC; + BenchmarkStatus status) throw() CVC4_PUBLIC; + +/** + * IOStream manipulator to print success messages or not. + * + * out << Command::printsuccess(false) << CommandSuccess(); + * + * prints nothing, but + * + * out << Command::printsuccess(true) << CommandSuccess(); + * + * prints a success message (in a manner appropriate for the current + * output language). + */ +class CVC4_PUBLIC CommandPrintSuccess { + /** + * The allocated index in ios_base for our depth setting. + */ + static const int s_iosIndex; + + /** + * The default setting, for ostreams that haven't yet had a + * setdepth() applied to them. + */ + static const int s_defaultPrintSuccess = false; + + /** + * When this manipulator is used, the setting is stored here. + */ + bool d_printSuccess; + +public: + /** + * Construct a CommandPrintSuccess with the given setting. + */ + CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {} + + inline void applyPrintSuccess(std::ostream& out) throw() { + out.iword(s_iosIndex) = d_printSuccess; + } + + static inline bool getPrintSuccess(std::ostream& out) throw() { + return out.iword(s_iosIndex); + } + + static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() { + out.iword(s_iosIndex) = printSuccess; + } + + /** + * Set the print-success state on the output stream for the current + * stack scope. This makes sure the old state is reset on the + * stream after normal OR exceptional exit from the scope, using the + * RAII C++ idiom. + */ + class Scope { + std::ostream& d_out; + bool d_oldPrintSuccess; + + public: + + inline Scope(std::ostream& out, bool printSuccess) throw() : + d_out(out), + d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) { + CommandPrintSuccess::setPrintSuccess(out, printSuccess); + } + + inline ~Scope() throw() { + CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess); + } + + };/* class CommandPrintSuccess::Scope */ + +};/* class CommandPrintSuccess */ + +/** + * Sets the default print-success setting when pretty-printing an Expr + * to an ostream. Use like this: + * + * // let out be an ostream, e an Expr + * out << Expr::setdepth(n) << e << endl; + * + * The depth stays permanently (until set again) with the stream. + */ +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() { + cps.applyPrintSuccess(out); + return out; +} + +class CVC4_PUBLIC CommandStatus { +protected: + // shouldn't construct a CommandStatus (use a derived class) + CommandStatus() throw() {} +public: + virtual ~CommandStatus() throw() {} + void toStream(std::ostream& out, + OutputLanguage language = language::output::LANG_AST) const throw(); +};/* class CommandStatus */ + +class CVC4_PUBLIC CommandSuccess : public CommandStatus { + static const CommandSuccess* s_instance; +public: + static const CommandSuccess* instance() throw() { return s_instance; } +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandUnsupported : public CommandStatus { +};/* class CommandSuccess */ + +class CVC4_PUBLIC CommandFailure : public CommandStatus { + std::string d_message; +public: + CommandFailure(std::string message) throw() : d_message(message) {} + ~CommandFailure() throw() {} + std::string getMessage() const throw() { return d_message; } +};/* class CommandFailure */ class CVC4_PUBLIC Command { +protected: + /** + * This field contains a command status if the command has been + * invoked, or NULL if it has not. This field is either a + * dynamically-allocated pointer, or it's a pointer to the singleton + * CommandSuccess instance. Doing so is somewhat asymmetric, but + * it avoids the need to dynamically allocate memory in the common + * case of a successful command. + */ + const CommandStatus* d_commandStatus; + public: - virtual ~Command() {} + typedef CommandPrintSuccess printsuccess; + + Command() throw(); + virtual ~Command() throw(); - virtual void invoke(SmtEngine* smtEngine) = 0; - virtual void invoke(SmtEngine* smtEngine, std::ostream& out); + virtual void invoke(SmtEngine* smtEngine) throw() = 0; + virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, - OutputLanguage language = language::output::LANG_AST) const; + OutputLanguage language = language::output::LANG_AST) const throw(); + + std::string toString() const throw(); + + /** Either the command hasn't run yet, or it completed successfully. */ + bool ok() const throw(); - std::string toString() const; + /** Get the command status (it's NULL if we haven't run yet). */ + const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; } - virtual void printResult(std::ostream& out) const; + virtual void printResult(std::ostream& out) const throw(); };/* class Command */ @@ -82,45 +220,51 @@ class CVC4_PUBLIC EmptyCommand : public Command { protected: std::string d_name; public: - EmptyCommand(std::string name = ""); - std::string getName() const; - void invoke(SmtEngine* smtEngine); + EmptyCommand(std::string name = "") throw(); + ~EmptyCommand() throw() {} + std::string getName() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class EmptyCommand */ class CVC4_PUBLIC AssertCommand : public Command { protected: BoolExpr d_expr; public: - AssertCommand(const BoolExpr& e); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); + AssertCommand(const BoolExpr& e) throw(); + ~AssertCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class AssertCommand */ class CVC4_PUBLIC PushCommand : public Command { public: - void invoke(SmtEngine* smtEngine); + ~PushCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class PushCommand */ class CVC4_PUBLIC PopCommand : public Command { public: - void invoke(SmtEngine* smtEngine); + ~PopCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class PopCommand */ class CVC4_PUBLIC DeclarationDefinitionCommand : public Command { protected: std::string d_symbol; public: - DeclarationDefinitionCommand(const std::string& id); - std::string getSymbol() const; + DeclarationDefinitionCommand(const std::string& id) throw(); + ~DeclarationDefinitionCommand() throw() {} + std::string getSymbol() const throw(); };/* class DeclarationDefinitionCommand */ class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand { protected: Type d_type; public: - DeclareFunctionCommand(const std::string& id, Type type); - Type getType() const; - void invoke(SmtEngine* smtEngine); + DeclareFunctionCommand(const std::string& id, Type type) throw(); + ~DeclareFunctionCommand() throw() {} + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DeclareFunctionCommand */ class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand { @@ -128,10 +272,11 @@ protected: size_t d_arity; Type d_type; public: - DeclareTypeCommand(const std::string& id, size_t arity, Type t); - size_t getArity() const; - Type getType() const; - void invoke(SmtEngine* smtEngine); + DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw(); + ~DeclareTypeCommand() throw() {} + size_t getArity() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DeclareTypeCommand */ class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand { @@ -139,11 +284,12 @@ protected: std::vector<Type> d_params; Type d_type; public: - DefineTypeCommand(const std::string& id, Type t); - DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t); - const std::vector<Type>& getParameters() const; - Type getType() const; - void invoke(SmtEngine* smtEngine); + DefineTypeCommand(const std::string& id, Type t) throw(); + DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw(); + ~DefineTypeCommand() throw() {} + const std::vector<Type>& getParameters() const throw(); + Type getType() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineTypeCommand */ class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand { @@ -152,13 +298,14 @@ protected: std::vector<Expr> d_formals; Expr d_formula; public: - DefineFunctionCommand(const std::string& id, Expr func, Expr formula); + DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw(); DefineFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula); - Expr getFunction() const; - const std::vector<Expr>& getFormals() const; - Expr getFormula() const; - void invoke(SmtEngine* smtEngine); + const std::vector<Expr>& formals, Expr formula) throw(); + ~DefineFunctionCommand() throw() {} + Expr getFunction() const throw(); + const std::vector<Expr>& getFormals() const throw(); + Expr getFormula() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineFunctionCommand */ /** @@ -169,8 +316,8 @@ public: class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand { public: DefineNamedFunctionCommand(const std::string& id, Expr func, - const std::vector<Expr>& formals, Expr formula); - void invoke(SmtEngine* smtEngine); + const std::vector<Expr>& formals, Expr formula) throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DefineNamedFunctionCommand */ class CVC4_PUBLIC CheckSatCommand : public Command { @@ -178,12 +325,13 @@ protected: BoolExpr d_expr; Result d_result; public: - CheckSatCommand(); - CheckSatCommand(const BoolExpr& expr); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); - Result getResult() const; - void printResult(std::ostream& out) const; + CheckSatCommand() throw(); + CheckSatCommand(const BoolExpr& expr) throw(); + ~CheckSatCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class CheckSatCommand */ class CVC4_PUBLIC QueryCommand : public Command { @@ -191,11 +339,12 @@ protected: BoolExpr d_expr; Result d_result; public: - QueryCommand(const BoolExpr& e); - BoolExpr getExpr() const; - void invoke(SmtEngine* smtEngine); - Result getResult() const; - void printResult(std::ostream& out) const; + QueryCommand(const BoolExpr& e) throw(); + ~QueryCommand() throw() {} + BoolExpr getExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Result getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class QueryCommand */ // this is TRANSFORM in the CVC presentation language @@ -204,11 +353,12 @@ protected: Expr d_term; Expr d_result; public: - SimplifyCommand(Expr term); - Expr getTerm() const; - void invoke(SmtEngine* smtEngine); - Expr getResult() const; - void printResult(std::ostream& out) const; + SimplifyCommand(Expr term) throw(); + ~SimplifyCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class SimplifyCommand */ class CVC4_PUBLIC GetValueCommand : public Command { @@ -216,75 +366,77 @@ protected: Expr d_term; Expr d_result; public: - GetValueCommand(Expr term); - Expr getTerm() const; - void invoke(SmtEngine* smtEngine); - Expr getResult() const; - void printResult(std::ostream& out) const; + GetValueCommand(Expr term) throw(); + ~GetValueCommand() throw() {} + Expr getTerm() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + Expr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetValueCommand */ class CVC4_PUBLIC GetAssignmentCommand : public Command { protected: SExpr d_result; public: - GetAssignmentCommand(); - void invoke(SmtEngine* smtEngine); - SExpr getResult() const; - void printResult(std::ostream& out) const; + GetAssignmentCommand() throw(); + ~GetAssignmentCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + SExpr getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetAssignmentCommand */ class CVC4_PUBLIC GetProofCommand : public Command { protected: Proof* d_result; public: - GetProofCommand(); - void invoke(SmtEngine* smtEngine); - Proof* getResult() const; - void printResult(std::ostream& out) const; + GetProofCommand() throw(); + ~GetProofCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + Proof* getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetProofCommand */ class CVC4_PUBLIC GetAssertionsCommand : public Command { protected: std::string d_result; public: - GetAssertionsCommand(); - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetAssertionsCommand() throw(); + ~GetAssertionsCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetAssertionsCommand */ class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command { protected: - std::string d_result; BenchmarkStatus d_status; public: - SetBenchmarkStatusCommand(BenchmarkStatus status); - BenchmarkStatus getStatus() const; - void invoke(SmtEngine* smtEngine); + SetBenchmarkStatusCommand(BenchmarkStatus status) throw(); + ~SetBenchmarkStatusCommand() throw() {} + BenchmarkStatus getStatus() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetBenchmarkStatusCommand */ class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command { protected: - std::string d_result; std::string d_logic; public: - SetBenchmarkLogicCommand(std::string logic); - std::string getLogic() const; - void invoke(SmtEngine* smtEngine); + SetBenchmarkLogicCommand(std::string logic) throw(); + ~SetBenchmarkLogicCommand() throw() {} + std::string getLogic() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetBenchmarkLogicCommand */ class CVC4_PUBLIC SetInfoCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; - std::string d_result; public: - SetInfoCommand(std::string flag, const SExpr& sexpr); - std::string getFlag() const; - SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + SetInfoCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetInfoCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetInfoCommand */ class CVC4_PUBLIC GetInfoCommand : public Command { @@ -292,25 +444,24 @@ protected: std::string d_flag; std::string d_result; public: - GetInfoCommand(std::string flag); - std::string getFlag() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetInfoCommand(std::string flag) throw(); + ~GetInfoCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetInfoCommand */ class CVC4_PUBLIC SetOptionCommand : public Command { protected: std::string d_flag; SExpr d_sexpr; - std::string d_result; public: - SetOptionCommand(std::string flag, const SExpr& sexpr); - std::string getFlag() const; - SExpr getSExpr() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + SetOptionCommand(std::string flag, const SExpr& sexpr) throw(); + ~SetOptionCommand() throw() {} + std::string getFlag() const throw(); + SExpr getSExpr() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class SetOptionCommand */ class CVC4_PUBLIC GetOptionCommand : public Command { @@ -318,35 +469,39 @@ protected: std::string d_flag; std::string d_result; public: - GetOptionCommand(std::string flag); - std::string getFlag() const; - void invoke(SmtEngine* smtEngine); - std::string getResult() const; - void printResult(std::ostream& out) const; + GetOptionCommand(std::string flag) throw(); + ~GetOptionCommand() throw() {} + std::string getFlag() const throw(); + void invoke(SmtEngine* smtEngine) throw(); + std::string getResult() const throw(); + void printResult(std::ostream& out) const throw(); };/* class GetOptionCommand */ class CVC4_PUBLIC DatatypeDeclarationCommand : public Command { private: std::vector<DatatypeType> d_datatypes; public: - DatatypeDeclarationCommand(const DatatypeType& datatype); - DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes); - const std::vector<DatatypeType>& getDatatypes() const; - void invoke(SmtEngine* smtEngine); + DatatypeDeclarationCommand(const DatatypeType& datatype) throw(); + ~DatatypeDeclarationCommand() throw() {} + DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw(); + const std::vector<DatatypeType>& getDatatypes() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class DatatypeDeclarationCommand */ class CVC4_PUBLIC QuitCommand : public Command { public: - QuitCommand(); - void invoke(SmtEngine* smtEngine); + QuitCommand() throw(); + ~QuitCommand() throw() {} + void invoke(SmtEngine* smtEngine) throw(); };/* class QuitCommand */ class CVC4_PUBLIC CommentCommand : public Command { std::string d_comment; public: - CommentCommand(std::string comment); - std::string getComment() const; - void invoke(SmtEngine* smtEngine); + CommentCommand(std::string comment) throw(); + ~CommentCommand() throw() {} + std::string getComment() const throw(); + void invoke(SmtEngine* smtEngine) throw(); };/* class CommentCommand */ class CVC4_PUBLIC CommandSequence : public Command { @@ -356,27 +511,28 @@ private: /** Next command to be executed */ unsigned int d_index; public: - CommandSequence(); - ~CommandSequence(); + CommandSequence() throw(); + ~CommandSequence() throw(); - void addCommand(Command* cmd); + void addCommand(Command* cmd) throw(); - void invoke(SmtEngine* smtEngine); - void invoke(SmtEngine* smtEngine, std::ostream& out); + void invoke(SmtEngine* smtEngine) throw(); + void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); typedef std::vector<Command*>::iterator iterator; typedef std::vector<Command*>::const_iterator const_iterator; - const_iterator begin() const; - const_iterator end() const; + const_iterator begin() const throw(); + const_iterator end() const throw(); - iterator begin(); - iterator end(); + iterator begin() throw(); + iterator end() throw(); };/* class CommandSequence */ class CVC4_PUBLIC DeclarationSequence : public CommandSequence { public: + ~DeclarationSequence() throw() {} };/* class DeclarationSequence */ }/* CVC4 namespace */ diff --git a/src/expr/command.i b/src/expr/command.i index 3a029b785..a4bf5473e 100644 --- a/src/expr/command.i +++ b/src/expr/command.i @@ -2,11 +2,11 @@ #include "expr/command.h" %} -%ignore CVC4::operator<<(std::ostream&, const Command&); -%ignore CVC4::operator<<(std::ostream&, const Command*); -%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status); +%ignore CVC4::operator<<(std::ostream&, const Command&) throw(); +%ignore CVC4::operator<<(std::ostream&, const Command*) throw(); +%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw(); -%rename(beginConst) CVC4::CommandSequence::begin() const; -%rename(endConst) CVC4::CommandSequence::end() const; +%rename(beginConst) CVC4::CommandSequence::begin() const throw(); +%rename(endConst) CVC4::CommandSequence::end() const throw(); %include "expr/command.h" diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 619fd5280..29aa1a737 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -56,31 +56,28 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) { return out << e.getNode(); } -TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) -: Exception(t.d_msg), d_expr(new Expr(t.getExpression())) - {} - +TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() : + Exception(t.d_msg), d_expr(new Expr(t.getExpression())) { +} -TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) -: Exception(message), d_expr(new Expr(expr)) -{ +TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() : + Exception(message), d_expr(new Expr(expr)) { } TypeCheckingException::TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc) -: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) -{ + const TypeCheckingExceptionPrivate* exc) throw() : + Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) { } -TypeCheckingException::~TypeCheckingException() throw () { +TypeCheckingException::~TypeCheckingException() throw() { delete d_expr; } -void TypeCheckingException::toStream(std::ostream& os) const { +void TypeCheckingException::toStream(std::ostream& os) const throw() { os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr; } -Expr TypeCheckingException::getExpression() const { +Expr TypeCheckingException::getExpression() const throw() { return *d_expr; } diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 616a7c8ff..b54ec20d4 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -81,32 +81,32 @@ private: protected: - TypeCheckingException() : Exception() {} - TypeCheckingException(const Expr& expr, std::string message); + TypeCheckingException() throw() : Exception() {} + TypeCheckingException(const Expr& expr, std::string message) throw(); TypeCheckingException(ExprManager* em, - const TypeCheckingExceptionPrivate* exc); + const TypeCheckingExceptionPrivate* exc) throw(); public: /** Copy constructor */ - TypeCheckingException(const TypeCheckingException& t); + TypeCheckingException(const TypeCheckingException& t) throw(); /** Destructor */ - ~TypeCheckingException() throw (); + ~TypeCheckingException() throw(); /** * Get the Expr that caused the type-checking to fail. * * @return the expr */ - Expr getExpression() const; + Expr getExpression() const throw(); /** * Returns the message corresponding to the type-checking failure. * We prefer toStream() to toString() because that keeps the expr-depth * and expr-language settings present in the stream. */ - void toStream(std::ostream& out) const; + void toStream(std::ostream& out) const throw(); friend class ExprManager; };/* class TypeCheckingException */ @@ -457,9 +457,13 @@ public: * * // let a, b, c, and d be variables of sort U * Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d))) - * out << e; + * out << printtypes(true) << e; * * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but + * + * out << printtypes(false) << [same expr as above] + * + * gives "(OR a b (AND c (NOT d)))" */ typedef expr::ExprPrintTypes printtypes; @@ -824,7 +828,7 @@ public: ${getConst_instantiations} -#line 828 "${template}" +#line 832 "${template}" namespace expr { diff --git a/src/expr/node.cpp b/src/expr/node.cpp index 586d0cb13..695e572ab 100644 --- a/src/expr/node.cpp +++ b/src/expr/node.cpp @@ -26,7 +26,7 @@ using namespace std; namespace CVC4 { TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node, - std::string message) : + std::string message) throw() : Exception(message), d_node(new Node(node)) { } @@ -35,11 +35,11 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () { delete d_node; } -void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const { +void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() { os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node; } -Node TypeCheckingExceptionPrivate::getNode() const { +NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() { return *d_node; } diff --git a/src/expr/node.h b/src/expr/node.h index 2751c96a8..57b02b05b 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -65,7 +65,7 @@ private: protected: - TypeCheckingExceptionPrivate() : Exception() {} + TypeCheckingExceptionPrivate() throw() : Exception() {} public: @@ -74,7 +74,7 @@ public: * @param node the problematic node * @param message the message explaining the failure */ - TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message); + TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw(); /** Destructor */ ~TypeCheckingExceptionPrivate() throw (); @@ -83,14 +83,14 @@ public: * Get the Node that caused the type-checking to fail. * @return the node */ - NodeTemplate<true> getNode() const; + NodeTemplate<true> getNode() const throw(); /** * Returns the message corresponding to the type-checking failure. * We prefer toStream() to toString() because that keeps the expr-depth * and expr-language settings present in the stream. */ - void toStream(std::ostream& out) const; + void toStream(std::ostream& out) const throw(); };/* class TypeCheckingExceptionPrivate */ diff --git a/src/expr/type.i b/src/expr/type.i index 314903342..acde96955 100644 --- a/src/expr/type.i +++ b/src/expr/type.i @@ -18,6 +18,7 @@ %rename(toIntegerType) CVC4::Type::operator IntegerType() const; %rename(toRealType) CVC4::Type::operator RealType() const; %rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const; +%rename(toStringType) CVC4::Type::operator StringType() const; %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const; %rename(toFunctionType) CVC4::Type::operator FunctionType() const; %rename(toTupleType) CVC4::Type::operator TupleType() const; diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h index 6dec72736..398ec57e2 100644 --- a/src/include/cvc4_public.h +++ b/src/include/cvc4_public.h @@ -85,8 +85,4 @@ #define EXPECT_TRUE(x) __builtin_expect( (x), true ) #define EXPECT_FALSE(x) __builtin_expect( (x), false ) -#ifndef NULL -# define NULL ((void*) 0) -#endif - #endif /* __CVC4_PUBLIC_H */ diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp index f2d6f1714..dca554330 100644 --- a/src/main/interactive_shell.cpp +++ b/src/main/interactive_shell.cpp @@ -268,11 +268,11 @@ Command* InteractiveShell::readCommand() { if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) { s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol()); } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol()); + s_declarations.insert(dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol()); } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol()); + s_declarations.insert(dynamic_cast<DeclareTypeCommand*>(cmd)->getSymbol()); } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) { - s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol()); + s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol()); } #endif /* HAVE_LIBREADLINE */ } diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h index d32914d8e..1f2d619ce 100644 --- a/src/parser/parser_exception.h +++ b/src/parser/parser_exception.h @@ -33,20 +33,20 @@ namespace parser { class CVC4_PUBLIC ParserException : public Exception { public: // Constructors - ParserException() : + ParserException() throw() : d_filename(), d_line(0), d_column(0) { } - ParserException(const std::string& msg) : + ParserException(const std::string& msg) throw() : Exception(msg), d_filename(), d_line(0), d_column(0) { } - ParserException(const char* msg) : + ParserException(const char* msg) throw() : Exception(msg), d_filename(), d_line(0), @@ -54,7 +54,7 @@ public: } ParserException(const std::string& msg, const std::string& filename, - unsigned long line, unsigned long column) : + unsigned long line, unsigned long column) throw() : Exception(msg), d_filename(filename), d_line(line), @@ -64,7 +64,7 @@ public: // Destructor virtual ~ParserException() throw() {} - virtual void toStream(std::ostream& os) const { + virtual void toStream(std::ostream& os) const throw() { if( d_line > 0 ) { os << "Parse Error: " << d_filename << ":" << d_line << "." << d_column << ": " << d_msg; @@ -73,15 +73,15 @@ public: } } - std::string getFilename() const { + std::string getFilename() const throw() { return d_filename; } - int getLine() const { + int getLine() const throw() { return d_line; } - int getColumn() const { + int getColumn() const throw() { return d_column; } diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 082765765..b941957c4 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -34,7 +34,7 @@ namespace printer { namespace ast { void AstPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; @@ -95,13 +95,13 @@ void AstPrinter::toStream(std::ostream& out, TNode n, } } out << ')'; -}/* AstPrinter::toStream() */ +}/* AstPrinter::toStream(TNode) */ template <class T> -static bool tryToStream(std::ostream& out, const Command* c); +static bool tryToStream(std::ostream& out, const Command* c) throw(); void AstPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { expr::ExprSetDepth::Scope sdScope(out, toDepth); expr::ExprPrintTypes::Scope ptScope(out, types); @@ -134,27 +134,44 @@ void AstPrinter::toStream(std::ostream& out, const Command* c, return; } - Unhandled("don't know how to print a Command of class: %s", typeid(*c).name()); + out << "ERROR: don't know how to print a Command of class: " + << typeid(*c).name() << endl; -}/* AstPrinter::toStream() */ +}/* AstPrinter::toStream(Command*) */ -static void toStream(std::ostream& out, const EmptyCommand* c) { +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); + +void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { + + if(tryToStream<CommandSuccess>(out, s) || + tryToStream<CommandFailure>(out, s) || + tryToStream<CommandUnsupported>(out, s)) { + return; + } + + out << "ERROR: don't know how to print a CommandStatus of class: " + << typeid(*s).name() << endl; + +}/* AstPrinter::toStream(CommandStatus*) */ + +static void toStream(std::ostream& out, const EmptyCommand* c) throw() { out << "EmptyCommand(" << c->getName() << ")"; } -static void toStream(std::ostream& out, const AssertCommand* c) { +static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "Assert(" << c->getExpr() << ")"; } -static void toStream(std::ostream& out, const PushCommand* c) { +static void toStream(std::ostream& out, const PushCommand* c) throw() { out << "Push()"; } -static void toStream(std::ostream& out, const PopCommand* c) { +static void toStream(std::ostream& out, const PopCommand* c) throw() { out << "Pop()"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) { +static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { BoolExpr e = c->getExpr(); if(e.isNull()) { out << "CheckSat()"; @@ -163,15 +180,15 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { } } -static void toStream(std::ostream& out, const QueryCommand* c) { +static void toStream(std::ostream& out, const QueryCommand* c) throw() { out << "Query(" << c->getExpr() << ')'; } -static void toStream(std::ostream& out, const QuitCommand* c) { +static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "Quit()"; } -static void toStream(std::ostream& out, const DeclarationSequence* c) { +static void toStream(std::ostream& out, const DeclarationSequence* c) throw() { out << "DeclarationSequence[" << endl; for(CommandSequence::const_iterator i = c->begin(); i != c->end(); @@ -181,7 +198,7 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) { out << "]"; } -static void toStream(std::ostream& out, const CommandSequence* c) { +static void toStream(std::ostream& out, const CommandSequence* c) throw() { out << "CommandSequence[" << endl; for(CommandSequence::const_iterator i = c->begin(); i != c->end(); @@ -191,11 +208,11 @@ static void toStream(std::ostream& out, const CommandSequence* c) { out << "]"; } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { out << "Declare(" << c->getSymbol() << "," << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { Expr func = c->getFunction(); const std::vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -208,12 +225,12 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "], << " << formula << " >> )"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) { +static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << "," << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineTypeCommand* c) { +static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { const vector<Type>& params = c->getParameters(); out << "DefineType(" << c->getSymbol() << ",["; if(params.size() > 0) { @@ -224,48 +241,48 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) { out << "]," << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); out << " )"; } -static void toStream(std::ostream& out, const SimplifyCommand* c) { +static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { out << "Simplify( << " << c->getTerm() << " >> )"; } -static void toStream(std::ostream& out, const GetValueCommand* c) { +static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "GetValue( << " << c->getTerm() << " >> )"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) { +static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "GetAssignment()"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) { +static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "GetAssertions()"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "SetBenchmarkStatus(" << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { out << "SetBenchmarkLogic(" << c->getLogic() << ")"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) { +static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) { +static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { out << "GetInfo(" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) { +static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) { +static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "GetOption(" << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); out << "DatatypeDeclarationCommand(["; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), @@ -277,12 +294,12 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { out << "])"; } -static void toStream(std::ostream& out, const CommentCommand* c) { +static void toStream(std::ostream& out, const CommentCommand* c) throw() { out << "CommentCommand([" << c->getComment() << "])"; } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) { +static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { toStream(out, dynamic_cast<const T*>(c)); return true; @@ -290,6 +307,29 @@ static bool tryToStream(std::ostream& out, const Command* c) { return false; } +static void toStream(std::ostream& out, const CommandSuccess* s) throw() { + if(Command::printsuccess::getPrintSuccess(out)) { + out << "OK" << endl; + } +} + +static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { + out << "UNSUPPORTED" << endl; +} + +static void toStream(std::ostream& out, const CommandFailure* s) throw() { + out << s->getMessage() << endl; +} + +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { + if(typeid(*s) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(s)); + return true; + } + return false; +} + }/* CVC4::printer::ast namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h index 69c39915b..2cae4c672 100644 --- a/src/printer/ast/ast_printer.h +++ b/src/printer/ast/ast_printer.h @@ -31,8 +31,9 @@ namespace ast { class AstPrinter : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class AstPrinter */ }/* CVC4::printer::ast namespace */ diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index fa1855ebe..0d47c9c6c 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -37,7 +37,7 @@ namespace printer { namespace cvc { void CvcPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "NULL"; @@ -110,7 +110,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, out << "TYPE"; break; default: - Unhandled(tc); + out << tc; } break; case kind::BUILTIN: @@ -357,15 +357,16 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, return; } + // shouldn't ever happen (unless new metakinds are added) Unhandled(); -}/* CvcPrinter::toStream() */ +}/* CvcPrinter::toStream(TNode) */ template <class T> -static bool tryToStream(std::ostream& out, const Command* c); +static bool tryToStream(std::ostream& out, const Command* c) throw(); void CvcPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { expr::ExprSetDepth::Scope sdScope(out, toDepth); expr::ExprPrintTypes::Scope ptScope(out, types); @@ -398,23 +399,40 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c, return; } - Unhandled("don't know how to print this command in CVC's presentation language: %s", c->toString().c_str()); + out << "ERROR: don't know how to print a Command of class: " + << typeid(*c).name() << endl; -}/* CvcPrinter::toStream() */ +}/* CvcPrinter::toStream(Command*) */ -static void toStream(std::ostream& out, const AssertCommand* c) { +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); + +void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { + + if(tryToStream<CommandSuccess>(out, s) || + tryToStream<CommandFailure>(out, s) || + tryToStream<CommandUnsupported>(out, s)) { + return; + } + + out << "ERROR: don't know how to print a CommandStatus of class: " + << typeid(*s).name() << endl; + +}/* CvcPrinter::toStream(CommandStatus*) */ + +static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "ASSERT " << c->getExpr() << ";"; } -static void toStream(std::ostream& out, const PushCommand* c) { +static void toStream(std::ostream& out, const PushCommand* c) throw() { out << "PUSH;"; } -static void toStream(std::ostream& out, const PopCommand* c) { +static void toStream(std::ostream& out, const PopCommand* c) throw() { out << "POP;"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) { +static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << "CHECKSAT " << e << ";"; @@ -423,7 +441,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { } } -static void toStream(std::ostream& out, const QueryCommand* c) { +static void toStream(std::ostream& out, const QueryCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << "QUERY " << e << ";"; @@ -432,11 +450,11 @@ static void toStream(std::ostream& out, const QueryCommand* c) { } } -static void toStream(std::ostream& out, const QuitCommand* c) { +static void toStream(std::ostream& out, const QuitCommand* c) throw() { //out << "EXIT;"; } -static void toStream(std::ostream& out, const CommandSequence* c) { +static void toStream(std::ostream& out, const CommandSequence* c) throw() { for(CommandSequence::const_iterator i = c->begin(); i != c->end(); ++i) { @@ -444,7 +462,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclarationSequence* c) { +static void toStream(std::ostream& out, const DeclarationSequence* c) throw() { DeclarationSequence::const_iterator i = c->begin(); for(;;) { DeclarationDefinitionCommand* dd = @@ -458,11 +476,11 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) { } } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { out << c->getSymbol() << " : " << c->getType() << ";"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -477,67 +495,69 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << "): " << formula << ";"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) { +static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { if(c->getArity() > 0) { - Unhandled("Don't know how to print parameterized type declaration " - "in CVC language:\n%s", c->toString().c_str()); + out << "ERROR: Don't know how to print parameterized type declaration " + "in CVC language:" << endl << c->toString() << endl; + } else { + out << c->getSymbol() << " : TYPE;"; } - out << c->getSymbol() << " : TYPE;"; } -static void toStream(std::ostream& out, const DefineTypeCommand* c) { +static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { if(c->getParameters().size() > 0) { - Unhandled("Don't know how to print parameterized type definition " - "in CVC language:\n%s", c->toString().c_str()); + out << "ERROR: Don't know how to print parameterized type definition " + "in CVC language:" << endl << c->toString() << endl; + } else { + out << c->getSymbol() << " : TYPE = " << c->getType() << ";"; } - out << c->getSymbol() << " : TYPE = " << c->getType() << ";"; } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { toStream(out, static_cast<const DefineFunctionCommand*>(c)); } -static void toStream(std::ostream& out, const SimplifyCommand* c) { +static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { out << "TRANSFORM " << c->getTerm() << ";"; } -static void toStream(std::ostream& out, const GetValueCommand* c) { +static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "% (get-value " << c->getTerm() << ")"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) { +static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "% (get-assignment)"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) { +static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "% (get-assertions)"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "% (set-info :status " << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { out << "% (set-logic " << c->getLogic() << ")"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) { +static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) { +static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { out << "% (get-info " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) { +static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) { +static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "% (get-option " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); for(vector<DatatypeType>::const_iterator i = datatypes.begin(), i_end = datatypes.end(); @@ -547,15 +567,15 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { } } -static void toStream(std::ostream& out, const CommentCommand* c) { +static void toStream(std::ostream& out, const CommentCommand* c) throw() { out << "% " << c->getComment(); } -static void toStream(std::ostream& out, const EmptyCommand* c) { +static void toStream(std::ostream& out, const EmptyCommand* c) throw() { } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) { +static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { toStream(out, dynamic_cast<const T*>(c)); return true; @@ -563,6 +583,29 @@ static bool tryToStream(std::ostream& out, const Command* c) { return false; } +static void toStream(std::ostream& out, const CommandSuccess* s) throw() { + if(Command::printsuccess::getPrintSuccess(out)) { + out << "OK" << endl; + } +} + +static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { + out << "UNSUPPORTED" << endl; +} + +static void toStream(std::ostream& out, const CommandFailure* s) throw() { + out << s->getMessage() << endl; +} + +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { + if(typeid(*s) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(s)); + return true; + } + return false; +} + }/* CVC4::printer::cvc namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h index fd478dbe5..ba66145fc 100644 --- a/src/printer/cvc/cvc_printer.h +++ b/src/printer/cvc/cvc_printer.h @@ -31,8 +31,9 @@ namespace cvc { class CvcPrinter : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class CvcPrinter */ }/* CVC4::printer::cvc namespace */ diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index 6714d355e..e3b2ed796 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -29,25 +29,26 @@ namespace CVC4 { Printer* Printer::d_printers[language::output::LANG_MAX]; -Printer* Printer::makePrinter(OutputLanguage lang) { +Printer* Printer::makePrinter(OutputLanguage lang) throw() { using namespace CVC4::language::output; switch(lang) { case LANG_SMTLIB: - return new printer::smt::SmtPrinter; + return new printer::smt::SmtPrinter(); case LANG_SMTLIB_V2: - return new printer::smt2::Smt2Printer; + return new printer::smt2::Smt2Printer(); case LANG_CVC4: - return new printer::cvc::CvcPrinter; + return new printer::cvc::CvcPrinter(); case LANG_AST: - return new printer::ast::AstPrinter; + return new printer::ast::AstPrinter(); default: Unhandled(lang); } + }/* Printer::makePrinter() */ }/* CVC4 namespace */ diff --git a/src/printer/printer.h b/src/printer/printer.h index 7294ab231..9bcbba3b0 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -32,11 +32,19 @@ class Printer { static Printer* d_printers[language::output::LANG_MAX]; /** Make a Printer for a given OutputLanguage */ - static Printer* makePrinter(OutputLanguage lang); + static Printer* makePrinter(OutputLanguage lang) throw(); + + // disallow copy, assignment + Printer(const Printer&) CVC4_UNUSED; + Printer& operator=(const Printer&) CVC4_UNUSED; + +protected: + // derived classes can construct, but no one else. + Printer() throw() {} public: /** Get the Printer for a given OutputLanguage */ - static Printer* getPrinter(OutputLanguage lang) { + static Printer* getPrinter(OutputLanguage lang) throw() { if(d_printers[lang] == NULL) { d_printers[lang] = makePrinter(lang); } @@ -45,11 +53,15 @@ public: /** Write a Node out to a stream with this Printer. */ virtual void toStream(std::ostream& out, TNode n, - int toDepth, bool types) const = 0; + int toDepth, bool types) const throw() = 0; /** Write a Command out to a stream with this Printer. */ virtual void toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const = 0; + int toDepth, bool types) const throw() = 0; + + /** Write a CommandStatus out to a stream with this Printer. */ + virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0; + };/* class Printer */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp index ed7f8febf..2ac514988 100644 --- a/src/printer/smt/smt_printer.cpp +++ b/src/printer/smt/smt_printer.cpp @@ -34,15 +34,19 @@ namespace printer { namespace smt { void SmtPrinter::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ void SmtPrinter::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2); }/* SmtPrinter::toStream() */ +void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() { + s->toStream(out, language::output::LANG_SMTLIB_V2); +} + }/* CVC4::printer::smt namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h index 14d6c09e1..370e0908c 100644 --- a/src/printer/smt/smt_printer.h +++ b/src/printer/smt/smt_printer.h @@ -31,8 +31,9 @@ namespace smt { class SmtPrinter : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class SmtPrinter */ }/* CVC4::printer::smt namespace */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 6741d5d2d..0f5fcd73b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -31,12 +31,12 @@ namespace CVC4 { namespace printer { namespace smt2 { -string smtKindString(Kind k); +static string smtKindString(Kind k) throw(); -void printBvParameterizedOp(std::ostream& out, TNode n); +static void printBvParameterizedOp(std::ostream& out, TNode n) throw(); void Smt2Printer::toStream(std::ostream& out, TNode n, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { // null if(n.getKind() == kind::NULL_EXPR) { out << "null"; @@ -247,9 +247,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, } } out << ')'; -}/* Smt2Printer::toStream() */ +}/* Smt2Printer::toStream(TNode) */ -string smtKindString(Kind k) { +static string smtKindString(Kind k) throw() { switch(k) { // builtin theory case kind::APPLY: break; @@ -330,7 +330,7 @@ string smtKindString(Kind k) { return kind::kindToString(k); } -void printBvParameterizedOp(std::ostream& out, TNode n) { +static void printBvParameterizedOp(std::ostream& out, TNode n) throw() { out << "(_ "; switch(n.getKind()) { case kind::BITVECTOR_EXTRACT: { @@ -359,16 +359,16 @@ void printBvParameterizedOp(std::ostream& out, TNode n) { << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount; break; default: - Unhandled(n.getKind()); + out << n.getKind(); } out << ")"; } template <class T> -static bool tryToStream(std::ostream& out, const Command* c); +static bool tryToStream(std::ostream& out, const Command* c) throw(); void Smt2Printer::toStream(std::ostream& out, const Command* c, - int toDepth, bool types) const { + int toDepth, bool types) const throw() { expr::ExprSetDepth::Scope sdScope(out, toDepth); expr::ExprPrintTypes::Scope ptScope(out, types); @@ -400,23 +400,40 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c, return; } - Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str()); + out << "ERROR: don't know how to print a Command of class: " + << typeid(*c).name() << endl; -}/* Smt2Printer::toStream() */ +}/* Smt2Printer::toStream(Command*) */ -static void toStream(std::ostream& out, const AssertCommand* c) { +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw(); + +void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() { + + if(tryToStream<CommandSuccess>(out, s) || + tryToStream<CommandFailure>(out, s) || + tryToStream<CommandUnsupported>(out, s)) { + return; + } + + out << "ERROR: don't know how to print a CommandStatus of class: " + << typeid(*s).name() << endl; + +}/* Smt2Printer::toStream(CommandStatus*) */ + +static void toStream(std::ostream& out, const AssertCommand* c) throw() { out << "(assert " << c->getExpr() << ")"; } -static void toStream(std::ostream& out, const PushCommand* c) { +static void toStream(std::ostream& out, const PushCommand* c) throw() { out << "(push 1)"; } -static void toStream(std::ostream& out, const PopCommand* c) { +static void toStream(std::ostream& out, const PopCommand* c) throw() { out << "(pop 1)"; } -static void toStream(std::ostream& out, const CheckSatCommand* c) { +static void toStream(std::ostream& out, const CheckSatCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << PushCommand() << endl @@ -428,7 +445,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) { } } -static void toStream(std::ostream& out, const QueryCommand* c) { +static void toStream(std::ostream& out, const QueryCommand* c) throw() { BoolExpr e = c->getExpr(); if(!e.isNull()) { out << PushCommand() << endl @@ -440,11 +457,11 @@ static void toStream(std::ostream& out, const QueryCommand* c) { } } -static void toStream(std::ostream& out, const QuitCommand* c) { +static void toStream(std::ostream& out, const QuitCommand* c) throw() { out << "(exit)"; } -static void toStream(std::ostream& out, const CommandSequence* c) { +static void toStream(std::ostream& out, const CommandSequence* c) throw() { for(CommandSequence::const_iterator i = c->begin(); i != c->end(); ++i) { @@ -452,7 +469,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) { } } -static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { +static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() { Type type = c->getType(); out << "(declare-fun " << c->getSymbol() << " ("; if(type.isFunction()) { @@ -469,7 +486,7 @@ static void toStream(std::ostream& out, const DeclareFunctionCommand* c) { out << ") " << type << ")"; } -static void toStream(std::ostream& out, const DefineFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() { Expr func = c->getFunction(); const vector<Expr>& formals = c->getFormals(); Expr formula = c->getFormula(); @@ -487,11 +504,11 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) { out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")"; } -static void toStream(std::ostream& out, const DeclareTypeCommand* c) { +static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() { out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")"; } -static void toStream(std::ostream& out, const DefineTypeCommand* c) { +static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() { const vector<Type>& params = c->getParameters(); out << "(define-sort " << c->getSymbol() << " ("; if(params.size() > 0) { @@ -502,55 +519,57 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) { out << ") " << c->getType() << ")"; } -static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) { +static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() { out << "DefineNamedFunction( "; toStream(out, static_cast<const DefineFunctionCommand*>(c)); out << " )"; - Unhandled("define named function command"); + + out << "ERROR: don't know how to output define-named-function command" << endl; } -static void toStream(std::ostream& out, const SimplifyCommand* c) { +static void toStream(std::ostream& out, const SimplifyCommand* c) throw() { out << "Simplify( << " << c->getTerm() << " >> )"; - Unhandled("simplify command"); + + out << "ERROR: don't know how to output simplify command" << endl; } -static void toStream(std::ostream& out, const GetValueCommand* c) { +static void toStream(std::ostream& out, const GetValueCommand* c) throw() { out << "(get-value " << c->getTerm() << ")"; } -static void toStream(std::ostream& out, const GetAssignmentCommand* c) { +static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() { out << "(get-assignment)"; } -static void toStream(std::ostream& out, const GetAssertionsCommand* c) { +static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() { out << "(get-assertions)"; } -static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() { out << "(set-info :status " << c->getStatus() << ")"; } -static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) { +static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() { out << "(set-logic " << c->getLogic() << ")"; } -static void toStream(std::ostream& out, const SetInfoCommand* c) { +static void toStream(std::ostream& out, const SetInfoCommand* c) throw() { out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetInfoCommand* c) { +static void toStream(std::ostream& out, const GetInfoCommand* c) throw() { out << "(get-info " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const SetOptionCommand* c) { +static void toStream(std::ostream& out, const SetOptionCommand* c) throw() { out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")"; } -static void toStream(std::ostream& out, const GetOptionCommand* c) { +static void toStream(std::ostream& out, const GetOptionCommand* c) throw() { out << "(get-option " << c->getFlag() << ")"; } -static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { +static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() { const vector<DatatypeType>& datatypes = c->getDatatypes(); out << "DatatypeDeclarationCommand(["; for(vector<DatatypeType>::const_iterator i = datatypes.begin(), @@ -560,18 +579,19 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) { out << *i << ";" << endl; } out << "])"; - Unhandled("datatype declaration command"); + + out << "ERROR: don't know how to output datatype declaration command" << endl; } -static void toStream(std::ostream& out, const CommentCommand* c) { +static void toStream(std::ostream& out, const CommentCommand* c) throw() { out << "(set-info :notes \"" << c->getComment() << "\")"; } -static void toStream(std::ostream& out, const EmptyCommand* c) { +static void toStream(std::ostream& out, const EmptyCommand* c) throw() { } template <class T> -static bool tryToStream(std::ostream& out, const Command* c) { +static bool tryToStream(std::ostream& out, const Command* c) throw() { if(typeid(*c) == typeid(T)) { toStream(out, dynamic_cast<const T*>(c)); return true; @@ -579,6 +599,35 @@ static bool tryToStream(std::ostream& out, const Command* c) { return false; } +static void toStream(std::ostream& out, const CommandSuccess* s) throw() { + if(Command::printsuccess::getPrintSuccess(out)) { + out << "success" << endl; + } +} + +static void toStream(std::ostream& out, const CommandUnsupported* s) throw() { + out << "unsupported" << endl; +} + +static void toStream(std::ostream& out, const CommandFailure* s) throw() { + string message = s->getMessage(); + // escape all double-quotes + size_t pos; + while((pos = message.find('"')) != string::npos) { + message = message.replace(pos, 1, "\\\""); + } + out << "(error \"" << message << "\")" << endl; +} + +template <class T> +static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() { + if(typeid(*s) == typeid(T)) { + toStream(out, dynamic_cast<const T*>(s)); + return true; + } + return false; +} + }/* CVC4::printer::smt2 namespace */ }/* CVC4::printer namespace */ }/* CVC4 namespace */ diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h index 2086370ae..a48104e45 100644 --- a/src/printer/smt2/smt2_printer.h +++ b/src/printer/smt2/smt2_printer.h @@ -31,8 +31,9 @@ namespace smt2 { class Smt2Printer : public CVC4::Printer { public: - void toStream(std::ostream& out, TNode n, int toDepth, bool types) const; - void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const; + void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw(); + void toStream(std::ostream& out, const CommandStatus* s) const throw(); };/* class Smt2Printer */ }/* CVC4::printer::smt2 namespace */ diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index b8a79cd9e..8aba4ad41 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -24,9 +24,9 @@ const Integer Cardinality::s_unknownCard(0); const Integer Cardinality::s_intCard(-1); const Integer Cardinality::s_realCard(-2); -const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0)); -const Cardinality Cardinality::REALS(Cardinality::Beth(1)); -const Cardinality Cardinality::UNKNOWN((Cardinality::Unknown())); +const Cardinality Cardinality::INTEGERS(CardinalityBeth(0)); +const Cardinality Cardinality::REALS(CardinalityBeth(1)); +const Cardinality Cardinality::UNKNOWN((CardinalityUnknown())); Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { if(isUnknown()) { @@ -127,7 +127,7 @@ std::string Cardinality::toString() const throw() { } -std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) throw() { +std::ostream& operator<<(std::ostream& out, CardinalityBeth b) throw() { out << "beth[" << b.getNumber() << ']'; return out; @@ -140,7 +140,7 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() { } else if(c.isFinite()) { out << c.getFiniteCardinality(); } else { - out << Cardinality::Beth(c.getBethNumber()); + out << CardinalityBeth(c.getBethNumber()); } return out; diff --git a/src/util/cardinality.h b/src/util/cardinality.h index e08f09bb6..057bb0b0c 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -31,6 +31,35 @@ namespace CVC4 { /** + * Representation for a Beth number, used only to construct + * Cardinality objects. + */ +class CVC4_PUBLIC CardinalityBeth { + Integer d_index; + +public: + CardinalityBeth(const Integer& beth) : d_index(beth) { + CheckArgument(beth >= 0, beth, + "Beth index must be a nonnegative integer, not %s.", + beth.toString().c_str()); + } + + const Integer& getNumber() const throw() { + return d_index; + } + +};/* class CardinalityBeth */ + +/** + * Representation for an unknown cardinality. + */ +class CVC4_PUBLIC CardinalityUnknown { +public: + CardinalityUnknown() throw() {} + ~CardinalityUnknown() throw() {} +};/* class CardinalityUnknown */ + +/** * A simple representation of a cardinality. We store an * arbitrary-precision integer for finite cardinalities, and we * distinguish infinite cardinalities represented as Beth numbers. @@ -65,34 +94,6 @@ public: static const Cardinality UNKNOWN; /** - * Representation for a Beth number, used only to construct - * Cardinality objects. - */ - class CVC4_PUBLIC Beth { - Integer d_index; - - public: - Beth(const Integer& beth) : d_index(beth) { - CheckArgument(beth >= 0, beth, - "Beth index must be a nonnegative integer, not %s.", - beth.toString().c_str()); - } - - const Integer& getNumber() const throw() { - return d_index; - } - };/* class Cardinality::Beth */ - - /** - * Representation for an unknown cardinality. - */ - class CVC4_PUBLIC Unknown { - public: - Unknown() throw() {} - ~Unknown() throw() {} - };/* class Cardinality::Unknown */ - - /** * Construct a finite cardinality equal to the integer argument. * The argument must be nonnegative. If we change this to an * "unsigned" argument to enforce the restriction, we mask some @@ -120,14 +121,14 @@ public: /** * Construct an infinite cardinality equal to the given Beth number. */ - Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) { + Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) { Assert(!isFinite()); } /** * Construct an unknown cardinality. */ - Cardinality(Unknown) : d_card(0) { + Cardinality(CardinalityUnknown) : d_card(0) { } /** Returns true iff this cardinality is unknown. */ @@ -256,7 +257,7 @@ public: /** Print an element of the InfiniteCardinality enumeration. */ -std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) +std::ostream& operator<<(std::ostream& out, CardinalityBeth b) throw() CVC4_PUBLIC; diff --git a/src/util/cardinality.i b/src/util/cardinality.i index 4e1382f87..c88037cfe 100644 --- a/src/util/cardinality.i +++ b/src/util/cardinality.i @@ -2,7 +2,7 @@ #include "util/cardinality.h" %} -%feature("valuewrapper") CVC4::Cardinality::Beth; +%feature("valuewrapper") CVC4::CardinalityBeth; %rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&); %rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&); @@ -18,36 +18,6 @@ %rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const; %ignore CVC4::operator<<(std::ostream&, const Cardinality&); -%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth); - -namespace CVC4 { - class Beth { - Integer d_index; - - public: - Beth(const Integer& beth) : d_index(beth) { - CheckArgument(beth >= 0, beth, - "Beth index must be a nonnegative integer, not %s.", - beth.toString().c_str()); - } - - const Integer& getNumber() const throw() { - return d_index; - } - };/* class Cardinality::Beth */ - - class Unknown { - public: - Unknown() throw() {} - ~Unknown() throw() {} - };/* class Cardinality::Unknown */ -} +%ignore CVC4::operator<<(std::ostream&, CardinalityBeth); %include "util/cardinality.h" - -%{ -namespace CVC4 { - typedef CVC4::Cardinality::Beth Beth; - typedef CVC4::Cardinality::Unknown Unknown; -} -%} diff --git a/src/util/exception.h b/src/util/exception.h index 43a0354ca..fe01eba36 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -24,25 +24,29 @@ #include <iostream> #include <string> #include <sstream> +#include <exception> namespace CVC4 { -class CVC4_PUBLIC Exception { +class CVC4_PUBLIC Exception : public std::exception { protected: std::string d_msg; public: // Constructors - Exception() : d_msg("Unknown exception") {} - Exception(const std::string& msg) : d_msg(msg) {} - Exception(const char* msg) : d_msg(msg) {} + Exception() throw() : d_msg("Unknown exception") {} + Exception(const std::string& msg) throw() : d_msg(msg) {} + Exception(const char* msg) throw() : d_msg(msg) {} // Destructor virtual ~Exception() throw() {} // NON-VIRTUAL METHOD for setting and printing the error message - void setMessage(const std::string& msg) { d_msg = msg; } - std::string getMessage() const { return d_msg; } + void setMessage(const std::string& msg) throw() { d_msg = msg; } + std::string getMessage() const throw() { return d_msg; } + + // overridden from base class std::exception + virtual const char* what() const throw() { return d_msg.c_str(); } /** * Get this exception as a string. Note that @@ -56,7 +60,7 @@ public: * toString(), there is no stream, so the parameters are default * and you'll get exprs and types printed using the AST language. */ - std::string toString() const { + std::string toString() const throw() { std::stringstream ss; toStream(ss); return ss.str(); @@ -67,12 +71,12 @@ public: * a derived class, it's recommended that this method print the * type of exception before the actual message. */ - virtual void toStream(std::ostream& os) const { os << d_msg; } + virtual void toStream(std::ostream& os) const throw() { os << d_msg; } };/* class Exception */ -inline std::ostream& operator<<(std::ostream& os, const Exception& e) CVC4_PUBLIC; -inline std::ostream& operator<<(std::ostream& os, const Exception& e) { +inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC; +inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() { e.toStream(os); return os; } diff --git a/src/util/exception.i b/src/util/exception.i index 52ff28922..ab6284633 100644 --- a/src/util/exception.i +++ b/src/util/exception.i @@ -2,7 +2,7 @@ #include "util/exception.h" %} -%ignore CVC4::operator<<(std::ostream&, const Exception&); -%ignore CVC4::Exception::Exception(const char*); +%ignore CVC4::operator<<(std::ostream&, const Exception&) throw(); +%ignore CVC4::Exception::Exception(const char*) throw(); %include "util/exception.h" diff --git a/src/util/options.cpp b/src/util/options.cpp index 94ddf082f..842bd84b2 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -27,6 +27,7 @@ #include <getopt.h> #include "expr/expr.h" +#include "expr/command.h" #include "util/configuration.h" #include "util/exception.h" #include "util/language.h" @@ -118,6 +119,8 @@ Most commonly-used CVC4 options:\n\ --no-interactive force non-interactive mode\n\ --produce-models | -m support the get-value command\n\ --produce-assignments support the get-assignment command\n\ + --print-success print the \"success\" output required of SMT-LIBv2\n\ + --smtlib2 SMT-LIBv2 conformance mode (implies other options)\n\ --proof turn on proof generation\n\ --incremental | -i enable incremental solving\n\ --tlimit=MS enable time limiting (give milliseconds)\n\ @@ -306,6 +309,8 @@ enum OptionValue { INTERACTIVE, NO_INTERACTIVE, PRODUCE_ASSIGNMENTS, + PRINT_SUCCESS, + SMTLIB2, PROOF, NO_TYPE_CHECKING, LAZY_TYPE_CHECKING, @@ -384,6 +389,8 @@ static struct option cmdlineOptions[] = { { "no-interactive", no_argument , NULL, NO_INTERACTIVE }, { "produce-models", no_argument , NULL, 'm' }, { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS }, + { "print-success", no_argument, NULL, PRINT_SUCCESS }, + { "smtlib2", no_argument, NULL, SMTLIB2 }, { "proof", no_argument, NULL, PROOF }, { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING }, { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING }, @@ -597,14 +604,12 @@ throw(OptionException) { break; case PRINT_EXPR_TYPES: - { - Debug.getStream() << Expr::printtypes(true); - Trace.getStream() << Expr::printtypes(true); - Notice.getStream() << Expr::printtypes(true); - Chat.getStream() << Expr::printtypes(true); - Message.getStream() << Expr::printtypes(true); - Warning.getStream() << Expr::printtypes(true); - } + Debug.getStream() << Expr::printtypes(true); + Trace.getStream() << Expr::printtypes(true); + Notice.getStream() << Expr::printtypes(true); + Chat.getStream() << Expr::printtypes(true); + Message.getStream() << Expr::printtypes(true); + Warning.getStream() << Expr::printtypes(true); break; case LAZY_DEFINITION_EXPANSION: @@ -648,7 +653,27 @@ throw(OptionException) { case PRODUCE_ASSIGNMENTS: produceAssignments = true; break; - + + case SMTLIB2: // smtlib v2 compliance mode + inputLanguage = language::input::LANG_SMTLIB_V2; + outputLanguage = language::output::LANG_SMTLIB_V2; + strictParsing = true; + // make sure entire expressions are printed on all the non-debug, non-trace streams + Notice.getStream() << Expr::setdepth(-1); + Chat.getStream() << Expr::setdepth(-1); + Message.getStream() << Expr::setdepth(-1); + Warning.getStream() << Expr::setdepth(-1); + /* intentionally fall through */ + + case PRINT_SUCCESS: + Debug.getStream() << Command::printsuccess(true); + Trace.getStream() << Command::printsuccess(true); + Notice.getStream() << Command::printsuccess(true); + Chat.getStream() << Command::printsuccess(true); + Message.getStream() << Command::printsuccess(true); + Warning.getStream() << Command::printsuccess(true); + break; + case PROOF: #ifdef CVC4_PROOF proof = true; diff --git a/src/util/stats.h b/src/util/stats.h index e955a7d28..719bbaab6 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -30,6 +30,7 @@ #include <set> #include <ctime> #include <vector> +#include <stdint.h> #include "util/Assert.h" @@ -390,7 +391,6 @@ public: };/* class WrappedStat<T> */ - /** * A backed integer-valued (64-bit signed) statistic. * This doesn't functionally differ from its base class BackedStat<int64_t>, @@ -655,7 +655,7 @@ class CVC4_PUBLIC CodeTimer; * arbitrarily, like a stopwatch; the value of the statistic at the * end is the accumulated time over all (start,stop) pairs. */ -class CVC4_PUBLIC TimerStat : public BackedStat< timespec > { +class CVC4_PUBLIC TimerStat : public BackedStat<timespec> { // strange: timespec isn't placed in 'std' namespace ?! /** The last start time of this timer */ diff --git a/src/util/stats.i b/src/util/stats.i index 5d3b81d4d..6f1ef5367 100644 --- a/src/util/stats.i +++ b/src/util/stats.i @@ -2,6 +2,14 @@ #include "util/stats.h" %} +namespace CVC4 { + template <class T> class CVC4_PUBLIC BackedStat; + + %template(int64_t_BackedStat) BackedStat<int64_t>; + %template(double_BackedStat) BackedStat<double>; + %template(timespec_BackedStat) BackedStat<timespec>; +}/* CVC4 namespace */ + %ignore CVC4::operator<<(std::ostream&, const timespec&); %rename(increment) CVC4::IntStat::operator++(); @@ -19,3 +27,4 @@ %rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&); %include "util/stats.h" + |