summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/cardinality.cpp10
-rw-r--r--src/util/cardinality.h63
-rw-r--r--src/util/cardinality.i34
-rw-r--r--src/util/exception.h24
-rw-r--r--src/util/exception.i4
-rw-r--r--src/util/options.cpp43
-rw-r--r--src/util/stats.h4
-rw-r--r--src/util/stats.i9
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"
+
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback