diff options
-rw-r--r-- | src/expr/command.cpp | 4 | ||||
-rwxr-xr-x | src/expr/mkmetakind | 16 | ||||
-rw-r--r-- | src/parser/parser.cpp | 66 | ||||
-rw-r--r-- | src/parser/parser.h | 19 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 46 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 115 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 8 | ||||
-rw-r--r-- | src/theory/builtin/kinds | 2 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 28 | ||||
-rw-r--r-- | src/util/configuration.cpp | 7 | ||||
-rw-r--r-- | src/util/configuration.h | 2 | ||||
-rw-r--r-- | src/util/stats.h | 74 |
12 files changed, 278 insertions, 109 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 8c90f337e..15fea22da 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -352,7 +352,9 @@ GetInfoCommand::GetInfoCommand(std::string flag) : void GetInfoCommand::invoke(SmtEngine* smtEngine) { try { - d_result = smtEngine->getInfo(d_flag).getValue(); + stringstream ss; + ss << smtEngine->getInfo(d_flag); + d_result = ss.str(); } catch(BadOptionException& bo) { d_result = "unsupported"; } diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind index c4968af26..351893feb 100755 --- a/src/expr/mkmetakind +++ b/src/expr/mkmetakind @@ -195,9 +195,9 @@ struct ConstantMapReverse< ::CVC4::kind::$1 > { } function registerOperatorToKind { - operatorKind=$1 - applyKind=$2 - metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind; + operatorKind=$1 + applyKind=$2 + metakind_operatorKinds="${metakind_operatorKinds} case kind::$applyKind: return kind::$operatorKind; "; } @@ -227,8 +227,14 @@ function register_metakind { exit 1 fi - if [ $mk = OPERATOR ] || [ $mk = PARAMETERIZED -a "$k" != SORT_TYPE ]; then - if [ $lb = 0 ]; then + if [ $mk = OPERATOR -o $mk = PARAMETERIZED ]; then + if [ $mk = PARAMETERIZED -a "$k" = SORT_TYPE ]; then + # exception: zero-ary SORT_TYPE is permitted for sort constructors + : + elif [ $mk = PARAMETERIZED -a "$k" = APPLY ]; then + # exception: zero-ary APPLY is permitted for defined zero-ary functions + : + elif [ $lb = 0 ]; then echo "$kf:$lineno: error in range \`$nc' for \`$k': $mk-kinded kinds must always take at least one child" >&2 exit 1 fi diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 297a2d804..09e65526d 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -103,7 +103,9 @@ bool Parser::isFunction(const std::string& name) { /* Returns true if name is bound to a defined function. */ bool Parser::isDefinedFunction(const std::string& name) { - return isFunction(name) && d_declScope.isBoundDefinedFunction(name); + // more permissive in type than isFunction(), because defined + // functions can be zero-ary and declared functions cannot. + return d_declScope.isBoundDefinedFunction(name); } /* Returns true if name is bound to a function returning boolean. */ @@ -286,50 +288,42 @@ void Parser::addOperator(Kind kind) { d_logicOperators.insert(kind); } +void Parser::preemptCommand(Command* cmd) { + d_commandQueue.push_back(cmd); +} + Command* Parser::nextCommand() throw(ParserException) { Debug("parser") << "nextCommand()" << std::endl; Command* cmd = NULL; - if(!done()) { - try { - cmd = d_input->parseCommand(); - if(cmd == NULL) { - setDone(); - } - } catch(ParserException& e) { + if(!d_commandQueue.empty()) { + cmd = d_commandQueue.front(); + d_commandQueue.pop_front(); + if(cmd == NULL) { setDone(); - throw; - } catch(Exception& e) { - setDone(); - stringstream ss; - ss << e; - parseError( ss.str() ); } - } - Debug("parser") << "nextCommand() => " << cmd << std::endl; - return cmd; -} - -Expr Parser::nextExpression() throw(ParserException) { - Debug("parser") << "nextExpression()" << std::endl; - Expr result; - if(!done()) { - try { - result = d_input->parseExpr(); - if(result.isNull()) { + } else { + if(!done()) { + try { + cmd = d_input->parseCommand(); + d_commandQueue.push_back(cmd); + cmd = d_commandQueue.front(); + d_commandQueue.pop_front(); + if(cmd == NULL) { + setDone(); + } + } catch(ParserException& e) { setDone(); + throw; + } catch(Exception& e) { + setDone(); + stringstream ss; + ss << e; + parseError( ss.str() ); } - } catch(ParserException& e) { - setDone(); - throw; - } catch(Exception& e) { - setDone(); - stringstream ss; - ss << e; - parseError( ss.str() ); } } - Debug("parser") << "nextExpression() => " << result << std::endl; - return result; + Debug("parser") << "nextCommand() => " << cmd << std::endl; + return cmd; } diff --git a/src/parser/parser.h b/src/parser/parser.h index 1c492c843..bc0142089 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -23,6 +23,7 @@ #include <string> #include <set> +#include <list> #include "input.h" #include "parser_exception.h" @@ -124,6 +125,13 @@ class CVC4_PUBLIC Parser { /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; + /** + * "Preemption commands": extra commands implied by subterms that + * should be issued before the currently-being-parsed command is + * issued. Used to support SMT-LIBv2 ":named" attribute on terms. + */ + std::list<Command*> d_commandQueue; + /** Lookup a symbol in the given namespace. */ Expr getSymbol(const std::string& var_name, SymbolType type); @@ -315,12 +323,20 @@ public: const std::vector<Type> mkSorts(const std::vector<std::string>& names); - /** Add an operator to the current legal set. + /** + * Add an operator to the current legal set. * * @param kind the built-in operator to add */ void addOperator(Kind kind); + /** + * Preempt the next returned command with other ones; used to + * support the :named attribute in SMT-LIBv2, which implicitly + * inserts a new command before the current one. + */ + void preemptCommand(Command* cmd); + /** Is the symbol bound to a boolean variable? */ bool isBoolean(const std::string& name); @@ -334,7 +350,6 @@ public: bool isPredicate(const std::string& name); Command* nextCommand() throw(ParserException); - Expr nextExpression() throw(ParserException); inline void parseError(const std::string& msg) throw (ParserException) { d_input->parseError(msg); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 4c447f9c1..ddfd1804e 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -196,7 +196,7 @@ command returns [CVC4::Command* cmd] sortSymbol[t] { Debug("parser") << "declare fun: '" << name << "'" << std::endl; if( sorts.size() > 0 ) { - t = EXPR_MANAGER->mkFunctionType(sorts,t); + t = EXPR_MANAGER->mkFunctionType(sorts, t); } PARSER_STATE->mkVar(name, t); $cmd = new DeclarationCommand(name,t); } @@ -215,7 +215,7 @@ command returns [CVC4::Command* cmd] ++i) { sorts.push_back((*i).second); } - t = EXPR_MANAGER->mkFunctionType(sorts,t); + t = EXPR_MANAGER->mkFunctionType(sorts, t); } PARSER_STATE->pushScope(); for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i = @@ -320,6 +320,7 @@ term[CVC4::Expr& expr] Kind kind; std::string name; std::vector<Expr> args; + SExpr sexpr; } : /* a built-in operator application */ LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK @@ -361,8 +362,9 @@ term[CVC4::Expr& expr] PARSER_STATE->getFunction(name) : PARSER_STATE->getVariable(name); args[0] = expr; - // TODO: check arity - expr = MK_EXPR(isDefinedFunction ? CVC4::kind::APPLY : CVC4::kind::APPLY_UF, args); } + expr = MK_EXPR(isDefinedFunction ? + CVC4::kind::APPLY : + CVC4::kind::APPLY_UF, args); } | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK @@ -374,9 +376,38 @@ term[CVC4::Expr& expr] RPAREN_TOK { PARSER_STATE->popScope(); } - | /* a variable */ - symbol[name,CHECK_DECLARED,SYM_VARIABLE] - { expr = PARSER_STATE->getVariable(name); } + /* a variable */ + | symbol[name,CHECK_DECLARED,SYM_VARIABLE] + { const bool isDefinedFunction = + PARSER_STATE->isDefinedFunction(name); + if(isDefinedFunction) { + expr = MK_EXPR(CVC4::kind::APPLY, + PARSER_STATE->getFunction(name)); + } else { + expr = PARSER_STATE->getVariable(name); + } + } + + /* attributed expressions */ + | LPAREN_TOK ATTRIBUTE_TOK term[expr] KEYWORD symbolicExpr[sexpr] RPAREN_TOK + { std::string attr = AntlrInput::tokenText($KEYWORD); + if(attr == ":named") { + name = sexpr.getValue(); + // FIXME ensure expr is a closed subterm + // check that sexpr is a fresh function symbol + PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + // define it + Expr func = PARSER_STATE->mkFunction(name, expr.getType()); + // bind name to expr with define-fun + Command* c = + new DefineFunctionCommand(func, std::vector<Expr>(), expr); + PARSER_STATE->preemptCommand(c); + } else { + std::stringstream ss; + ss << "Attribute `" << attr << "' not supported"; + PARSER_STATE->parseError(ss.str()); + } + } /* constants */ | INTEGER_LITERAL @@ -558,6 +589,7 @@ GET_ASSERTIONS_TOK : 'get-assertions'; EXIT_TOK : 'exit'; ITE_TOK : 'ite'; LET_TOK : 'let'; +ATTRIBUTE_TOK : '!'; LPAREN_TOK : '('; RPAREN_TOK : ')'; SET_LOGIC_TOK : 'set-logic'; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5de1cd0b1..edf49c7ac 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -31,6 +31,7 @@ #include "util/output.h" #include "util/exception.h" #include "util/options.h" +#include "util/configuration.h" #include "prop/prop_engine.h" #include "theory/theory_engine.h" @@ -121,7 +122,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw() : d_propEngine(NULL), d_assertionList(NULL), d_haveAdditions(false), - d_lastResult() { + d_status() { NodeManagerScope nms(d_nodeManager); @@ -166,7 +167,6 @@ void SmtEngine::setInfo(const string& key, const SExpr& value) throw(BadOptionException) { Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl; if(key == ":name" || - key == ":status" || key == ":source" || key == ":category" || key == ":difficulty" || @@ -174,15 +174,68 @@ void SmtEngine::setInfo(const string& key, const SExpr& value) key == ":notes") { // ignore these return; + } else if(key == ":status") { + string s; + if(value.isAtom()) { + s = value.getValue(); + } + if(s != "sat" && s != "unsat" && s != "unknown") { + throw BadOptionException("argument to (set-info :status ..) must be " + "`sat' or `unsat' or `unknown'"); + } + if(s == "sat") { + d_status = Result::SAT; + } else if(s == "unsat") { + d_status = Result::UNSAT; + } else if(s == "unknown") { + d_status = Result::SAT_UNKNOWN; + } else { + Unreachable(); + } + return; } throw BadOptionException(); } -const SExpr& SmtEngine::getInfo(const string& key) const +SExpr SmtEngine::getInfo(const string& key) const throw(BadOptionException) { Debug("smt") << "SMT getInfo(" << key << ")" << endl; - // FIXME implement me - throw BadOptionException(); + if(key == ":all-statistics") { + vector<SExpr> stats; + for(StatisticsRegistry::const_iterator i = StatisticsRegistry::begin(); + i != StatisticsRegistry::end(); + ++i) { + vector<SExpr> v; + v.push_back((*i)->getName()); + v.push_back((*i)->getValue()); + stats.push_back(v); + } + return stats; + } else if(key == ":error-behavior") { + return SExpr("immediate-exit"); + } else if(key == ":name") { + return Configuration::getName(); + } else if(key == ":version") { + return Configuration::getVersionString(); + } else if(key == ":authors") { + return Configuration::about(); + } else if(key == ":status") { + enum Result::SAT status = d_status.asSatisfiabilityResult().isSAT(); + switch(status) { + case Result::SAT: + return SExpr("sat"); + case Result::UNSAT: + return SExpr("unsat"); + case Result::SAT_UNKNOWN: + return SExpr("unknown"); + default: + Unhandled(status); + } + } else if(key == ":reason-unknown") { + throw BadOptionException(); + } else { + throw BadOptionException(); + } } void SmtEngine::setOption(const string& key, const SExpr& value) @@ -192,11 +245,34 @@ void SmtEngine::setOption(const string& key, const SExpr& value) throw BadOptionException(); } -const SExpr& SmtEngine::getOption(const string& key) const +SExpr SmtEngine::getOption(const string& key) const throw(BadOptionException) { Debug("smt") << "SMT getOption(" << key << ")" << endl; - // FIXME implement me - throw BadOptionException(); + if(key == ":print-success") { + return SExpr("true"); + } else if(key == ":expand-definitions") { + throw BadOptionException(); + } else if(key == ":interactive-mode") { + throw BadOptionException(); + } else if(key == ":produce-proofs") { + throw BadOptionException(); + } else if(key == ":produce-unsat-cores") { + throw BadOptionException(); + } else if(key == ":produce-models") { + throw BadOptionException(); + } else if(key == ":produce-assignments") { + throw BadOptionException(); + } else if(key == ":regular-output-channel") { + return SExpr("stdout"); + } else if(key == ":diagnostic-output-channel") { + return SExpr("stderr"); + } else if(key == ":random-seed") { + throw BadOptionException(); + } else if(key == ":verbosity") { + throw BadOptionException(); + } else { + throw BadOptionException(); + } } void SmtEngine::defineFunction(Expr func, @@ -205,12 +281,14 @@ void SmtEngine::defineFunction(Expr func, Debug("smt") << "SMT defineFunction(" << func << ")" << endl; NodeManagerScope nms(d_nodeManager); Type formulaType = formula.getType(true);// type check body - if(formulaType != FunctionType(func.getType()).getRangeType()) { + Type funcType = func.getType(); + Type rangeType = funcType.isFunction() ? + FunctionType(funcType).getRangeType() : funcType; + if(formulaType != rangeType) { stringstream ss; ss << "Defined function's declared type does not match that of body\n" << "The function : " << func << "\n" - << "Its range type: " - << FunctionType(func.getType()).getRangeType() << "\n" + << "Its range type: " << rangeType << "\n" << "The body : " << formula << "\n" << "Body type : " << formulaType; throw TypeCheckingException(func, ss.str()); @@ -225,7 +303,9 @@ void SmtEngine::defineFunction(Expr func, } TNode formulaNode = formula.getTNode(); DefinedFunction def(funcNode, formalsNodes, formulaNode); - d_haveAdditions = true; + // Permit (check-sat) (define-fun ...) (get-value ...) sequences. + // Otherwise, (check-sat) (get-value ((! foo :named bar))) breaks + // d_haveAdditions = true; d_definedFunctions->insert(funcNode, def); } @@ -335,7 +415,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) { ensureBoolean(e);// ensure expr is type-checked at this point SmtEnginePrivate::addFormula(*this, e.getNode()); Result r = check().asSatisfiabilityResult(); - d_lastResult = r; + d_status = r; d_haveAdditions = false; Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl; return r; @@ -348,7 +428,7 @@ Result SmtEngine::query(const BoolExpr& e) { ensureBoolean(e);// ensure expr is type-checked at this point SmtEnginePrivate::addFormula(*this, e.getNode().notNode()); Result r = check().asValidityResult(); - d_lastResult = r; + d_status = r; d_haveAdditions = false; Debug("smt") << "SMT query(" << e << ") ==> " << r << endl; return r; @@ -389,7 +469,7 @@ Expr SmtEngine::getValue(Expr e) "Cannot get value when produce-models options is off."; throw ModalException(msg); } - if(d_lastResult.asSatisfiabilityResult() != Result::SAT || + if(d_status.asSatisfiabilityResult() != Result::SAT || d_haveAdditions) { const char* msg = "Cannot get value unless immediately proceded by SAT/INVALID response."; @@ -457,9 +537,8 @@ void SmtEngine::pop() { d_context->pop(); Debug("userpushpop") << "SmtEngine: popped to level " << d_context->getLevel() << endl; - // clear out last result: get-value/get-assignment no longer - // available here - d_lastResult = Result(); + // FIXME: should we reset d_status here? + // SMT-LIBv2 spec seems to imply no, but it would make sense to.. } }/* CVC4 namespace */ diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index efa48e517..7272762d8 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -119,9 +119,9 @@ class CVC4_PUBLIC SmtEngine { bool d_haveAdditions; /** - * Result of last checkSat/query. + * Most recent result of last checkSat/query or (set-info :status). */ - Result d_lastResult; + Result d_status; /** * This is called by the destructor, just before destroying the @@ -173,7 +173,7 @@ public: /** * Query information about the SMT environment. */ - const SExpr& getInfo(const std::string& key) const + SExpr getInfo(const std::string& key) const throw(BadOptionException); /** @@ -185,7 +185,7 @@ public: /** * Get an aspect of the current SMT execution environment. */ - const SExpr& getOption(const std::string& key) const + SExpr getOption(const std::string& key) const throw(BadOptionException); /** diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 47ee8cbfc..ad442fc2f 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -119,7 +119,7 @@ constant BUILTIN \ "The kind of nodes representing built-in operators" variable FUNCTION "function" -parameterized APPLY FUNCTION 1: "defined function application" +parameterized APPLY FUNCTION 0: "defined function application" operator EQUAL 2 "equality" operator DISTINCT 2: "disequality" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index aee147eff..ec98e61d2 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -37,23 +37,29 @@ class ApplyTypeRule { throw (TypeCheckingExceptionPrivate) { TNode f = n.getOperator(); TypeNode fType = f.getType(check); - if( !fType.isFunction() ) { + if( !fType.isFunction() && n.getNumChildren() > 0 ) { throw TypeCheckingExceptionPrivate(n, "operator does not have function type"); } if( check ) { - if (n.getNumChildren() != fType.getNumChildren() - 1) { - throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); - } - TNode::iterator argument_it = n.begin(); - TNode::iterator argument_it_end = n.end(); - TypeNode::iterator argument_type_it = fType.begin(); - for(; argument_it != argument_it_end; ++argument_it) { - if((*argument_it).getType() != *argument_type_it) { - throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + if(fType.isFunction()) { + if(n.getNumChildren() != fType.getNumChildren() - 1) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); + } + TNode::iterator argument_it = n.begin(); + TNode::iterator argument_it_end = n.end(); + TypeNode::iterator argument_type_it = fType.begin(); + for(; argument_it != argument_it_end; ++argument_it) { + if((*argument_it).getType() != *argument_type_it) { + throw TypeCheckingExceptionPrivate(n, "argument types do not match the function type"); + } + } + } else { + if( n.getNumChildren() > 0 ) { + throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type"); } } } - return fType.getRangeType(); + return fType.isFunction() ? fType.getRangeType() : fType; } };/* class ApplyTypeRule */ diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 403f6f84b..9b463f797 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -18,13 +18,20 @@ ** configuration information about the CVC4 library. **/ +#include <string> + #include "util/configuration.h" #include "util/configuration_private.h" +#include "cvc4autoconfig.h" using namespace std; namespace CVC4 { +string Configuration::getName() { + return PACKAGE_NAME; +} + bool Configuration::isDebugBuild() { return IS_DEBUG_BUILD; } diff --git a/src/util/configuration.h b/src/util/configuration.h index 907cd1d31..33c0a7407 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -37,6 +37,8 @@ class CVC4_PUBLIC Configuration { public: + static std::string getName(); + static bool isDebugBuild(); static bool isTracingBuild(); diff --git a/src/util/stats.h b/src/util/stats.h index 43b48140e..d6b463e65 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -24,6 +24,7 @@ #include <string> #include <ostream> +#include <sstream> #include <iomanip> #include <set> #include <ctime> @@ -44,16 +45,28 @@ class CVC4_PUBLIC Stat; class CVC4_PUBLIC StatisticsRegistry { private: - struct StatCmp; + struct StatCmp { + inline bool operator()(const Stat* s1, const Stat* s2) const; + };/* class StatisticsRegistry::StatCmp */ typedef std::set< Stat*, StatCmp > StatSet; static StatSet d_registeredStats; public: + + typedef StatSet::const_iterator const_iterator; + static void flushStatistics(std::ostream& out); static inline void registerStat(Stat* s) throw(AssertionException); static inline void unregisterStat(Stat* s) throw(AssertionException); + + static inline const_iterator begin() { + return d_registeredStats.begin(); + } + static inline const_iterator end() { + return d_registeredStats.end(); + } };/* class StatisticsRegistry */ @@ -65,8 +78,8 @@ private: public: - Stat(const std::string& s) throw(CVC4::AssertionException) : d_name(s) - { + Stat(const std::string& s) throw(CVC4::AssertionException) : + d_name(s) { if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_name.find(s_delim) == std::string::npos); } @@ -85,18 +98,17 @@ public: const std::string& getName() const { return d_name; } -};/* class Stat */ - -struct StatisticsRegistry::StatCmp { - bool operator()(const Stat* s1, const Stat* s2) const - { - return (s1->getName()) < (s2->getName()); - } -};/* class StatCmp */ + virtual std::string getValue() const = 0; +};/* class Stat */ +inline bool StatisticsRegistry::StatCmp::operator()(const Stat* s1, + const Stat* s2) const { + return s1->getName() < s2->getName(); +} -inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) { +inline void StatisticsRegistry::registerStat(Stat* s) + throw(AssertionException) { if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end()); d_registeredStats.insert(s); @@ -104,7 +116,8 @@ inline void StatisticsRegistry::registerStat(Stat* s) throw(AssertionException) }/* StatisticsRegistry::registerStat */ -inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException) { +inline void StatisticsRegistry::unregisterStat(Stat* s) + throw(AssertionException) { if(__CVC4_USE_STATISTICS) { AlwaysAssert(d_registeredStats.find(s) != d_registeredStats.end()); d_registeredStats.erase(s); @@ -120,7 +133,9 @@ inline void StatisticsRegistry::unregisterStat(Stat* s) throw(AssertionException template <class T> class DataStat : public Stat { public: - DataStat(const std::string& s) : Stat(s) {} + DataStat(const std::string& s) : + Stat(s) { + } virtual const T& getData() const = 0; virtual void setData(const T&) = 0; @@ -130,6 +145,12 @@ public: out << getData(); } } + + std::string getValue() const { + std::stringstream ss; + ss << getData(); + return ss.str(); + } };/* class DataStat */ @@ -140,13 +161,14 @@ private: const T* d_data; public: - ReferenceStat(const std::string& s): - DataStat<T>(s), d_data(NULL) - {} + ReferenceStat(const std::string& s) : + DataStat<T>(s), + d_data(NULL) { + } - ReferenceStat(const std::string& s, const T& data): - DataStat<T>(s), d_data(NULL) - { + ReferenceStat(const std::string& s, const T& data) : + DataStat<T>(s), + d_data(NULL) { setData(data); } @@ -155,6 +177,7 @@ public: d_data = &t; } } + const T& getData() const { if(__CVC4_USE_STATISTICS) { return *d_data; @@ -173,8 +196,10 @@ protected: public: - BackedStat(const std::string& s, const T& init): DataStat<T>(s), d_data(init) - {} + BackedStat(const std::string& s, const T& init) : + DataStat<T>(s), + d_data(init) { + } void setData(const T& t) { if(__CVC4_USE_STATISTICS) { @@ -202,8 +227,9 @@ public: class IntStat : public BackedStat<int64_t> { public: - IntStat(const std::string& s, int64_t init): BackedStat<int64_t>(s, init) - {} + IntStat(const std::string& s, int64_t init) : + BackedStat<int64_t>(s, init) { + } IntStat& operator++() { if(__CVC4_USE_STATISTICS) { |