diff options
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/Assert.h | 8 | ||||
| -rw-r--r-- | src/util/Makefile.am | 2 | ||||
| -rw-r--r-- | src/util/options.h | 136 | ||||
| -rw-r--r-- | src/util/result.cpp | 210 | ||||
| -rw-r--r-- | src/util/result.h | 161 | ||||
| -rw-r--r-- | src/util/sexpr.h | 6 |
6 files changed, 290 insertions, 233 deletions
diff --git a/src/util/Assert.h b/src/util/Assert.h index dbbdfe9b7..5bb2e830f 100644 --- a/src/util/Assert.h +++ b/src/util/Assert.h @@ -163,7 +163,7 @@ public: va_list args; va_start(args, fmt); construct("Illegal argument detected", - ( std::string(argDesc) + " invalid" ).c_str(), + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), function, file, line, fmt, args); va_end(args); } @@ -172,7 +172,7 @@ public: const char* file, unsigned line) : AssertionException() { construct("Illegal argument detected", - ( std::string(argDesc) + " invalid" ).c_str(), + ( std::string("`") + argDesc + "' is a bad argument" ).c_str(), function, file, line); } @@ -183,7 +183,7 @@ public: va_list args; va_start(args, fmt); construct("Illegal argument detected", - ( std::string(argDesc) + " invalid; expected " + + ( std::string("`") + argDesc + "' is a bad argument; expected " + condStr + " to hold" ).c_str(), function, file, line, fmt, args); va_end(args); @@ -194,7 +194,7 @@ public: unsigned line) : AssertionException() { construct("Illegal argument detected", - ( std::string(argDesc) + " invalid; expected " + + ( std::string("`") + argDesc + "' is a bad argument; expected " + condStr + " to hold" ).c_str(), function, file, line); } diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 02315143d..61c0bf885 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -18,10 +18,10 @@ libutil_la_SOURCES = \ hash.h \ bool.h \ model.h \ - options.h \ output.cpp \ output.h \ result.h \ + result.cpp \ unique_id.h \ configuration.h \ configuration_private.h \ diff --git a/src/util/options.h b/src/util/options.h deleted file mode 100644 index af254dabf..000000000 --- a/src/util/options.h +++ /dev/null @@ -1,136 +0,0 @@ -/********************* */ -/*! \file options.h - ** \verbatim - ** Original author: mdeters - ** Major contributors: cconway - ** Minor contributors (to current version): dejan - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) - ** Courant Institute of Mathematical Sciences - ** New York University - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief Global (command-line or equivalent) tuning parameters. - ** - ** Global (command-line or equivalent) tuning parameters. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__OPTIONS_H -#define __CVC4__OPTIONS_H - -#ifdef CVC4_DEBUG -# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT true -#else /* CVC4_DEBUG */ -# define USE_EARLY_TYPE_CHECKING_BY_DEFAULT false -#endif /* CVC4_DEBUG */ - -#include <iostream> -#include <string> - -#include "util/language.h" - -namespace CVC4 { - -struct CVC4_PUBLIC Options { - - std::string binary_name; - - bool statistics; - - std::ostream *out; - std::ostream *err; - - /* -1 means no output */ - /* 0 is normal (and default) -- warnings only */ - /* 1 is warnings + notices so the user doesn't get too bored */ - /* 2 is chatty, giving statistical things etc. */ - /* with 3, the solver is slowed down by all the scrolling */ - int verbosity; - - /** The input language */ - InputLanguage inputLanguage; - - /** Enumeration of UF implementation choices */ - typedef enum { TIM, MORGAN } UfImplementation; - - /** Which implementation of uninterpreted function theory to use */ - UfImplementation uf_implementation; - - /** Should we exit after parsing? */ - bool parseOnly; - - /** Should the parser do semantic checks? */ - bool semanticChecks; - - /** Should the parser memory-map file input? */ - bool memoryMap; - - /** Should we strictly enforce the language standard while parsing? */ - bool strictParsing; - - /** Should we expand function definitions lazily? */ - bool lazyDefinitionExpansion; - - /** Whether we're in interactive mode or not */ - bool interactive; - - /** - * Whether we're in interactive mode (or not) due to explicit user - * setting (if false, we inferred the proper default setting). - */ - bool interactiveSetByUser; - - /** Whether we support SmtEngine::getValue() for this run. */ - bool produceModels; - - /** Whether we support SmtEngine::getAssignment() for this run. */ - bool produceAssignments; - - /** Whether we support SmtEngine::getAssignment() for this run. */ - bool earlyTypeChecking; - - Options() : - binary_name(), - statistics(false), - out(0), - err(0), - verbosity(0), - inputLanguage(language::input::LANG_AUTO), - uf_implementation(MORGAN), - parseOnly(false), - semanticChecks(true), - memoryMap(false), - strictParsing(false), - lazyDefinitionExpansion(false), - interactive(false), - interactiveSetByUser(false), - produceModels(false), - produceAssignments(false), - earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) { - } -};/* struct Options */ - -inline std::ostream& operator<<(std::ostream& out, - Options::UfImplementation uf) { - switch(uf) { - case Options::TIM: - out << "TIM"; - break; - case Options::MORGAN: - out << "MORGAN"; - break; - default: - out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]"; - } - - return out; -} - -}/* CVC4 namespace */ - -#undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT - -#endif /* __CVC4__OPTIONS_H */ diff --git a/src/util/result.cpp b/src/util/result.cpp new file mode 100644 index 000000000..b8f34f47f --- /dev/null +++ b/src/util/result.cpp @@ -0,0 +1,210 @@ +/********************* */ +/*! \file result.h + ** \verbatim + ** Original author: mdeters + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Encapsulation of the result of a query. + ** + ** Encapsulation of the result of a query. + **/ + +#include <iostream> +#include <algorithm> +#include <string> +#include <cctype> + +#include "util/result.h" +#include "util/Assert.h" + +using namespace std; + +namespace CVC4 { + +Result::Result(const string& instr) : + d_sat(SAT_UNKNOWN), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON) { + string s = instr; + transform(s.begin(), s.end(), s.begin(), ::tolower); + if(s == "sat" || s == "satisfiable") { + d_which = TYPE_SAT; + d_sat = SAT; + } else if(s == "unsat" || s == "unsatisfiable") { + d_which = TYPE_SAT; + d_sat = UNSAT; + } else if(s == "valid") { + d_which = TYPE_VALIDITY; + d_validity = VALID; + } else if(s == "invalid") { + d_which = TYPE_VALIDITY; + d_validity = INVALID; + } else if(s == "unknown") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + } else if(s == "incomplete") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = INCOMPLETE; + } else if(s == "timeout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = TIMEOUT; + } else if(s == "memout") { + d_which = TYPE_SAT; + d_sat = SAT_UNKNOWN; + d_unknownExplanation = MEMOUT; + } else { + IllegalArgument(s, "expected satisfiability/validity result, " + "instead got `%s'", s.c_str()); + } +} + +bool Result::operator==(const Result& r) const { + if(d_which != r.d_which) { + return false; + } + if(d_which == TYPE_SAT) { + return d_sat == r.d_sat && + ( d_sat != SAT_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + if(d_which == TYPE_VALIDITY) { + return d_validity == r.d_validity && + ( d_validity != VALIDITY_UNKNOWN || + d_unknownExplanation == r.d_unknownExplanation ); + } + return false; +} + +Result Result::asSatisfiabilityResult() const { + if(d_which == TYPE_SAT) { + return *this; + } + + Assert(d_which == TYPE_VALIDITY); + + switch(d_validity) { + + case INVALID: + return Result(SAT); + + case VALID: + return Result(UNSAT); + + case VALIDITY_UNKNOWN: + return Result(SAT_UNKNOWN, d_unknownExplanation); + + default: + Unhandled(d_validity); + } +} + +Result Result::asValidityResult() const { + if(d_which == TYPE_VALIDITY) { + return *this; + } + + Assert(d_which == TYPE_SAT); + + switch(d_sat) { + + case SAT: + return Result(INVALID); + + case UNSAT: + return Result(VALID); + + case SAT_UNKNOWN: + return Result(VALIDITY_UNKNOWN, d_unknownExplanation); + + default: + Unhandled(d_sat); + } +} + +string Result::toString() const { + stringstream ss; + ss << *this; + return ss.str(); +} + +ostream& operator<<(ostream& out, enum Result::Sat s) { + switch(s) { + case Result::UNSAT: out << "UNSAT"; break; + case Result::SAT: out << "SAT"; break; + case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; + default: Unhandled(s); + } + return out; +} + +ostream& operator<<(ostream& out, enum Result::Validity v) { + switch(v) { + case Result::INVALID: out << "INVALID"; break; + case Result::VALID: out << "VALID"; break; + case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; + default: Unhandled(v); + } + return out; +} + +ostream& operator<<(ostream& out, + enum Result::UnknownExplanation e) { + switch(e) { + case Result::REQUIRES_FULL_CHECK: out << "REQUIRES_FULL_CHECK"; break; + case Result::INCOMPLETE: out << "INCOMPLETE"; break; + case Result::TIMEOUT: out << "TIMEOUT"; break; + case Result::MEMOUT: out << "MEMOUT"; break; + case Result::OTHER: out << "OTHER"; break; + case Result::UNKNOWN_REASON: out << "UNKNOWN_REASON"; break; + default: Unhandled(e); + } + return out; +} + +ostream& operator<<(ostream& out, const Result& r) { + if(r.d_which == Result::TYPE_SAT) { + switch(r.d_sat) { + case Result::UNSAT: + out << "unsat"; + break; + case Result::SAT: + out << "sat"; + break; + case Result::SAT_UNKNOWN: + out << "unknown"; + if(r.whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << r.whyUnknown() << ")"; + } + break; + } + } else { + switch(r.d_validity) { + case Result::INVALID: + out << "invalid"; + break; + case Result::VALID: + out << "valid"; + break; + case Result::VALIDITY_UNKNOWN: + out << "unknown"; + if(r.whyUnknown() != Result::UNKNOWN_REASON) { + out << " (" << r.whyUnknown() << ")"; + } + break; + } + } + + return out; +}/* operator<<(ostream&, const Result&) */ + +}/* CVC4 namespace */ diff --git a/src/util/result.h b/src/util/result.h index f1f6ae1c2..fc2fa4522 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -21,20 +21,29 @@ #ifndef __CVC4__RESULT_H #define __CVC4__RESULT_H +#include <iostream> +#include <string> + +#include "util/Assert.h" + namespace CVC4 { -// TODO: perhaps best to templatize Result on its Kind (SAT/Validity), -// but this requires doing the same for Prover and needs discussion. +// TODO: either templatize Result on its Kind (Sat/Validity) or subclass. +// TODO: INVALID/SAT provide models, etc?---perhaps just by linking back +// into the SmtEngine that produced the Result? +// TODO: make unconstructible except by SmtEngine? That would ensure that +// any Result in the system is bona fide. -// TODO: subclass to provide models, etc. This is really just -// intended as a three-valued response code. +class Result; + +std::ostream& operator<<(std::ostream& out, const Result& r) CVC4_PUBLIC; /** - * Three-valued, immutable SMT result, with optional explanation. + * Three-valued SMT result, with optional explanation. */ class CVC4_PUBLIC Result { public: - enum SAT { + enum Sat { UNSAT = 0, SAT = 1, SAT_UNKNOWN = 2 @@ -50,121 +59,95 @@ public: REQUIRES_FULL_CHECK, INCOMPLETE, TIMEOUT, - BAIL, - OTHER + MEMOUT, + OTHER, + UNKNOWN_REASON }; private: - enum SAT d_sat; + enum Sat d_sat; enum Validity d_validity; enum { TYPE_SAT, TYPE_VALIDITY, TYPE_NONE } d_which; + enum UnknownExplanation d_unknownExplanation; - friend std::ostream& CVC4::operator<<(std::ostream& out, Result r); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Result& r); public: Result() : d_sat(SAT_UNKNOWN), d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_NONE) { + d_which(TYPE_NONE), + d_unknownExplanation(UNKNOWN_REASON) { } - Result(enum SAT s) : + Result(enum Sat s) : d_sat(s), d_validity(VALIDITY_UNKNOWN), - d_which(TYPE_SAT) { + d_which(TYPE_SAT), + d_unknownExplanation(UNKNOWN_REASON) { + CheckArgument(s != SAT_UNKNOWN, + "Must provide a reason for satisfiability being unknown"); } Result(enum Validity v) : d_sat(SAT_UNKNOWN), d_validity(v), - d_which(TYPE_VALIDITY) { + d_which(TYPE_VALIDITY), + d_unknownExplanation(UNKNOWN_REASON) { + CheckArgument(v != VALIDITY_UNKNOWN, + "Must provide a reason for validity being unknown"); + } + Result(enum Sat s, enum UnknownExplanation unknownExplanation) : + d_sat(s), + d_validity(VALIDITY_UNKNOWN), + d_which(TYPE_SAT), + d_unknownExplanation(unknownExplanation) { + CheckArgument(s == SAT_UNKNOWN, + "improper use of unknown-result constructor"); + } + Result(enum Validity v, enum UnknownExplanation unknownExplanation) : + d_sat(SAT_UNKNOWN), + d_validity(v), + d_which(TYPE_VALIDITY), + d_unknownExplanation(unknownExplanation) { + CheckArgument(v == VALIDITY_UNKNOWN, + "improper use of unknown-result constructor"); } + Result(const std::string& s); - enum SAT isSAT() { + enum Sat isSat() const { return d_which == TYPE_SAT ? d_sat : SAT_UNKNOWN; } - enum Validity isValid() { + enum Validity isValid() const { return d_which == TYPE_VALIDITY ? d_validity : VALIDITY_UNKNOWN; } - enum UnknownExplanation whyUnknown(); - - inline bool operator==(Result r) { - if(d_which != r.d_which) { - return false; - } - if(d_which == TYPE_SAT) { - return d_sat == r.d_sat; - } - if(d_which == TYPE_VALIDITY) { - return d_validity == r.d_validity; - } - return false; - } - inline bool operator!=(Result r) { - return !(*this == r); - } - inline Result asSatisfiabilityResult() const; - inline Result asValidityResult() const; - -};/* class Result */ - -inline Result Result::asSatisfiabilityResult() const { - if(d_which == TYPE_SAT) { - return *this; - } - - switch(d_validity) { - - case INVALID: - return Result(SAT); - - case VALID: - return Result(UNSAT); - - case VALIDITY_UNKNOWN: - return Result(SAT_UNKNOWN); - - default: - Unhandled(d_validity); + bool isUnknown() const { + return isSat() == SAT_UNKNOWN && isValid() == VALIDITY_UNKNOWN; } -} - -inline Result Result::asValidityResult() const { - if(d_which == TYPE_VALIDITY) { - return *this; + enum UnknownExplanation whyUnknown() const { + AlwaysAssert( isUnknown(), + "This result is not unknown, so the reason for " + "being unknown cannot be inquired of it" ); + return d_unknownExplanation; } - switch(d_sat) { - - case SAT: - return Result(INVALID); + bool operator==(const Result& r) const; + inline bool operator!=(const Result& r) const; + Result asSatisfiabilityResult() const; + Result asValidityResult() const; - case UNSAT: - return Result(VALID); + std::string toString() const; - case SAT_UNKNOWN: - return Result(VALIDITY_UNKNOWN); +};/* class Result */ - default: - Unhandled(d_sat); - } +inline bool Result::operator!=(const Result& r) const { + return !(*this == r); } -inline std::ostream& operator<<(std::ostream& out, Result r) { - if(r.d_which == Result::TYPE_SAT) { - switch(r.d_sat) { - case Result::UNSAT: out << "UNSAT"; break; - case Result::SAT: out << "SAT"; break; - case Result::SAT_UNKNOWN: out << "SAT_UNKNOWN"; break; - } - } else { - switch(r.d_validity) { - case Result::INVALID: out << "INVALID"; break; - case Result::VALID: out << "VALID"; break; - case Result::VALIDITY_UNKNOWN: out << "VALIDITY_UNKNOWN"; break; - } - } - - return out; -} +std::ostream& operator<<(std::ostream& out, + enum Result::Sat s) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + enum Result::Validity v) CVC4_PUBLIC; +std::ostream& operator<<(std::ostream& out, + enum Result::UnknownExplanation e) CVC4_PUBLIC; }/* CVC4 namespace */ diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 9821664bd..376a8a224 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -38,7 +38,7 @@ class CVC4_PUBLIC SExpr { bool d_isAtom; /** The value of an atomic S-expression. */ - std::string d_value; + std::string d_stringValue; /** The children of a list S-expression. */ std::vector<SExpr> d_children; @@ -50,7 +50,7 @@ public: SExpr(const std::string& value) : d_isAtom(true), - d_value(value) { + d_stringValue(value) { } SExpr(const std::vector<SExpr> children) : @@ -80,7 +80,7 @@ inline bool SExpr::isAtom() const { inline const std::string SExpr::getValue() const { AlwaysAssert( d_isAtom ); - return d_value; + return d_stringValue; } inline const std::vector<SExpr> SExpr::getChildren() const { |