diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/cardinality.cpp | 10 | ||||
-rw-r--r-- | src/util/cardinality.h | 63 | ||||
-rw-r--r-- | src/util/cardinality.i | 34 | ||||
-rw-r--r-- | src/util/exception.h | 24 | ||||
-rw-r--r-- | src/util/exception.i | 4 | ||||
-rw-r--r-- | src/util/options.cpp | 43 | ||||
-rw-r--r-- | src/util/stats.h | 4 | ||||
-rw-r--r-- | src/util/stats.i | 9 |
8 files changed, 100 insertions, 91 deletions
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" + |