From 589bf879f00d2d8df4ccdaf3db28674ce3639512 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Fri, 28 Sep 2012 22:46:09 +0000 Subject: [PATCH] Some fixes to portfolio * respect output lang * fix export variable for BOUND_VARIABLE * support export of SUBRANGE_TYPE * statistic for lastWinner, other minor stat changes * fix running of multiple threads on checsat/query * changes of Assert -> assert which became private * fix some destruction time order issues * fix Pickler with AssertionException going private Fixed by not fixing: * portfolio+datatypes does not work - added ExportUnsupportedException to more places, switches to sequential (still TODO / decide : not switch silently, but print error) > note: this exception now needs to be (and is) defined in expr.h Known issues: * problems in portfolio+quantifiers - at least some problems appear to be because of static variables (will be later "fixed" like the datatypes) (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/command.cpp | 8 +-- src/expr/command.h | 7 --- src/expr/expr_manager_template.cpp | 14 +++-- src/expr/expr_template.cpp | 9 +++- src/expr/expr_template.h | 13 +++++ src/expr/pickler.cpp | 9 +++- src/expr/pickler.h | 12 ++--- src/main/command_executor.h | 6 --- src/main/command_executor_portfolio.cpp | 69 ++++++++++++++----------- src/main/command_executor_portfolio.h | 3 ++ src/main/portfolio_util.cpp | 3 +- src/main/portfolio_util.h | 4 +- 12 files changed, 91 insertions(+), 66 deletions(-) diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 938f28635..a62a9421f 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -1273,12 +1273,8 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() { } Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { - throw ExportToUnsupportedException(); - // vector params; - // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params), - // ExportTransformer(exprManager, variableMap)); - // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params); - // return c; + throw ExportUnsupportedException + ("export of DatatypeDeclarationCommand unsupported"); } Command* DatatypeDeclarationCommand::clone() const { diff --git a/src/expr/command.h b/src/expr/command.h index 5786f4e71..e120deed6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -50,13 +50,6 @@ 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; -class CVC4_PUBLIC ExportToUnsupportedException : public Exception { -public: - ExportToUnsupportedException() throw() : - Exception("exportTo unsupported for command") { - } -};/* class ExportToUnsupportedException */ - /** The status an SMT benchmark can have */ enum BenchmarkStatus { /** Benchmark is satisfiable */ diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index be2804fd5..457491445 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -928,13 +928,21 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) { Debug("export") << "type: " << n << std::endl; - Assert(n.getKind() == kind::SORT_TYPE || - n.getMetaKind() != kind::metakind::PARAMETERIZED, - "PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { + throw ExportUnsupportedException + ("export of types belonging to theory of DATATYPES kinds unsupported"); + } + if(n.getMetaKind() == kind::metakind::PARAMETERIZED && + n.getKind() != kind::SORT_TYPE) { + throw ExportUnsupportedException + ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported"); + } if(n.getKind() == kind::TYPE_CONSTANT) { return to->mkTypeConst(n.getConst()); } else if(n.getKind() == kind::BITVECTOR_TYPE) { return to->mkBitVectorType(n.getConst()); + } else if(n.getKind() == kind::SUBRANGE_TYPE) { + return to->mkSubrangeType(n.getSubrangeBounds()); } Type from_t = from->toType(n); Type& to_t = vmap.d_typeMap[from_t]; diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index f39c0e7ea..2f9e27c0c 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -114,7 +114,12 @@ namespace expr { static Node exportConstant(TNode n, NodeManager* to); Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) { - if(n.isConst()) { + if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) { + throw ExportUnsupportedException + ("export of node belonging to theory of DATATYPES kinds unsupported"); + } + + if(n.getMetaKind() == metakind::CONSTANT) { return exportConstant(n, NodeManager::fromExprManager(to)); } else if(n.isVar()) { Expr from_e(from, new Node(n)); @@ -132,7 +137,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC // a check that mkVar isn't called internally NodeManagerScope nullScope(NULL); - if(n.getKind() == kind::BOUND_VAR_LIST) { + if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) { to_e = to->mkBoundVar(name, type);// FIXME thread safety } else if(n.getKind() == kind::VARIABLE) { to_e = to->mkVar(name, type);// FIXME thread safety diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 96c7cfadf..4255e3454 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -132,6 +132,19 @@ public: friend class ExprManager; };/* class TypeCheckingException */ +/** + * Exception thrown in case of failure to export + */ +class CVC4_PUBLIC ExportUnsupportedException : public Exception { +public: + ExportUnsupportedException() throw(): + Exception("export unsupported") { + } + ExportUnsupportedException(const char* msg) throw(): + Exception(msg) { + } +};/* class DatatypeExportUnsupportedException */ + std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) CVC4_PUBLIC; diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp index a41db794d..6548cf98a 100644 --- a/src/expr/pickler.cpp +++ b/src/expr/pickler.cpp @@ -129,7 +129,7 @@ Pickler::~Pickler() { } void Pickler::toPickle(Expr e, Pickle& p) - throw(AssertionException, PicklingException) { + throw(PicklingException) { Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm); Assert(d_private->atDefaultState()); @@ -471,6 +471,13 @@ Pickle::~Pickle() { delete d_data; } +uint64_t MapPickler::variableFromMap(uint64_t x) const +{ + VarMap::const_iterator i = d_fromMap.find(x); + Assert(i != d_fromMap.end()); + return i->second; +} + }/* CVC4::expr::pickle namespace */ }/* CVC4::expr namespace */ }/* CVC4 namespace */ diff --git a/src/expr/pickler.h b/src/expr/pickler.h index a6427ad47..dee4f06e6 100644 --- a/src/expr/pickler.h +++ b/src/expr/pickler.h @@ -67,7 +67,7 @@ class CVC4_PUBLIC Pickler { protected: virtual uint64_t variableToMap(uint64_t x) const - throw(AssertionException, PicklingException) { + throw(PicklingException) { return x; } virtual uint64_t variableFromMap(uint64_t x) const { @@ -87,7 +87,7 @@ public: * * @return the pickle, which should be dispose()'d when you're done with it */ - void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException); + void toPickle(Expr e, Pickle& p) throw(PicklingException); /** * Constructs a node from a Pickle. @@ -116,7 +116,7 @@ public: protected: virtual uint64_t variableToMap(uint64_t x) const - throw(AssertionException, PicklingException) { + throw(PicklingException) { VarMap::const_iterator i = d_toMap.find(x); if(i != d_toMap.end()) { return i->second; @@ -125,11 +125,7 @@ protected: } } - virtual uint64_t variableFromMap(uint64_t x) const { - VarMap::const_iterator i = d_fromMap.find(x); - Assert(i != d_fromMap.end()); - return i->second; - } + virtual uint64_t variableFromMap(uint64_t x) const; };/* class MapPickler */ }/* CVC4::expr::pickle namespace */ diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 435299ce3..a5bd78abe 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -38,14 +38,8 @@ protected: StatisticsRegistry d_stats; public: - // Note: though the options are not cached (instead a reference is - // used), the portfolio command executer currently parses them - // during initalization, creating thread-specific options and - // storing them CommandExecutor(ExprManager &exprMgr, Options &options); - ~CommandExecutor() {} - /** * Executes a command. Recursively handles if cmd is a command * sequence. Eventually uses doCommandSingleton (which can be diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index 32a507d78..b9bf39002 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -48,9 +48,13 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_lastWinner(0), d_channelsOut(), d_channelsIn(), - d_ostringstreams() + d_ostringstreams(), + d_statLastWinner("portfolio::lastWinner") { - Assert(d_threadOptions.size() == d_numThreads); + assert(d_threadOptions.size() == d_numThreads); + + d_statLastWinner.setData(d_lastWinner); + d_stats.registerStat_(&d_statLastWinner); /* Duplication, Individualisation */ d_exprMgrs.push_back(&d_exprMgr); @@ -64,7 +68,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio d_smts.push_back(new SmtEngine(d_exprMgrs[i])); } - Assert(d_vmaps.size() == 0); + assert(d_vmaps.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { d_vmaps.push_back(new ExprManagerMapCollection()); } @@ -72,15 +76,15 @@ CommandExecutorPortfolio::CommandExecutorPortfolio CommandExecutorPortfolio::~CommandExecutorPortfolio() { - Assert(d_seq != NULL); + assert(d_seq != NULL); delete d_seq; - Assert(d_smts.size() == d_numThreads); + assert(d_smts.size() == d_numThreads); for(unsigned i = 1; i < d_numThreads; ++i) { // the 0-th one is responsibility of parent class - delete d_exprMgrs[i]; delete d_smts[i]; + delete d_exprMgrs[i]; } d_exprMgrs.clear(); d_smts.clear(); @@ -89,8 +93,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio() void CommandExecutorPortfolio::lemmaSharingInit() { /* Sharing channels */ - Assert(d_channelsIn.size() == 0); - Assert(d_channelsOut.size() == 0); + assert(d_channelsIn.size() == 0); + assert(d_channelsOut.size() == 0); if(d_numThreads == 1) { // Disable sharing @@ -130,10 +134,14 @@ void CommandExecutorPortfolio::lemmaSharingInit() /* Output to string stream */ if(d_options[options::verbosity] == 0 || d_options[options::separateOutput]) { - Assert(d_ostringstreams.size() == 0); + assert(d_ostringstreams.size() == 0); for(unsigned i = 0; i < d_numThreads; ++i) { d_ostringstreams.push_back(new ostringstream); d_threadOptions[i].set(options::out, d_ostringstreams[i]); + + // important even for muzzled builds (to get result output right) + *d_threadOptions[i][options::out] + << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]); } } } @@ -141,11 +149,11 @@ void CommandExecutorPortfolio::lemmaSharingInit() void CommandExecutorPortfolio::lemmaSharingCleanup() { - Assert(d_numThreads == d_options[options::threads]); + assert(d_numThreads == d_options[options::threads]); // Channel cleanup - Assert(d_channelsIn.size() == d_numThreads); - Assert(d_channelsOut.size() == d_numThreads); + assert(d_channelsIn.size() == d_numThreads); + assert(d_channelsOut.size() == d_numThreads); for(unsigned i = 0; i < d_numThreads; ++i) { delete d_channelsIn[i]; delete d_channelsOut[i]; @@ -157,7 +165,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup() // sstreams cleanup (if used) if(d_ostringstreams.size() != 0) { - Assert(d_ostringstreams.size() == d_numThreads); + assert(d_ostringstreams.size() == d_numThreads); for(unsigned i = 0; i < d_numThreads; ++i) { d_threadOptions[i].set(options::out, d_options[options::out]); delete d_ostringstreams[i]; @@ -180,12 +188,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // mode = 1 : run a porfolio // mode = 2 : run the last winner - // if(dynamic_cast(cmd) != NULL || - // dynamic_cast(cmd) != NULL) { - // mode = 1; - // } else if(dynamic_cast(cmd) != NULL) { - // mode = 2; - // } + if(dynamic_cast(cmd) != NULL || + dynamic_cast(cmd) != NULL) { + mode = 1; + } else if(dynamic_cast(cmd) != NULL) { + mode = 2; + } if(mode == 0) { d_seq->addCommand(cmd->clone()); @@ -213,7 +221,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) */ try { seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); - }catch(ExportToUnsupportedException& e){ + }catch(ExportUnsupportedException& e){ return CommandExecutor::doCommandSingleton(cmd); } } @@ -244,9 +252,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) ); } - Assert(d_channelsIn.size() == d_numThreads); - Assert(d_channelsOut.size() == d_numThreads); - Assert(d_smts.size() == d_numThreads); + assert(d_channelsIn.size() == d_numThreads); + assert(d_channelsOut.size() == d_numThreads); + assert(d_smts.size() == d_numThreads); boost::function smFn = boost::bind(sharingManager, d_numThreads, @@ -269,9 +277,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) // << std::endl; if(d_ostringstreams.size() != 0) { - Assert(d_numThreads == d_options[options::threads]); - Assert(portfolioReturn.first >= 0); - Assert(unsigned(portfolioReturn.first) < d_numThreads); + assert(d_numThreads == d_options[options::threads]); + assert(portfolioReturn.first >= 0); + assert(unsigned(portfolioReturn.first) < d_numThreads); *d_options[options::out] << d_ostringstreams[portfolioReturn.first]->str(); @@ -286,7 +294,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) cmd, d_threadOptions[d_lastWinner][options::out]); } else { - Unreachable(); + // Unreachable(); + assert(false); } }/* CommandExecutorPortfolio::doCommandSingleton() */ @@ -297,15 +306,15 @@ std::string CommandExecutorPortfolio::getSmtEngineStatus() } void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const { - Assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size()); + assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size()); for(size_t i = 0; i < d_numThreads; ++i) { - string emTag = "ExprManager thread #" + string emTag = "thread#" + boost::lexical_cast(d_threadOptions[i][options::thread_id]); Statistics stats = d_exprMgrs[i]->getStatistics(); stats.setPrefix(emTag); stats.flushInformation(out); - string smtTag = "SmtEngine thread #" + string smtTag = "thread#" + boost::lexical_cast(d_threadOptions[i][options::thread_id]); stats = d_smts[i]->getStatistics(); stats.setPrefix(smtTag); diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h index 72a677789..867b62d31 100644 --- a/src/main/command_executor_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -52,6 +52,9 @@ class CommandExecutorPortfolio : public CommandExecutor { std::vector< SharedChannel* > d_channelsIn; std::vector d_ostringstreams; + // Stats + ReferenceStat d_statLastWinner; + public: CommandExecutorPortfolio(ExprManager &exprMgr, Options &options, diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index b208b2479..b16ac2d34 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -14,6 +14,7 @@ ** \brief Code relevant only for portfolio builds **/ +#include #include #include #include "options/options.h" @@ -97,7 +98,7 @@ vector parseThreadSpecificOptions(Options opts) } } - Assert(numThreads >= 1); //do we need this? + assert(numThreads >= 1); //do we need this? return threadOptions; } diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 1955a29a7..416b9f44a 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -155,7 +155,7 @@ void sharingManager(unsigned numThreads, /* Alert if channel full, so that we increase sharingChannelSize or decrease sharingBroadcastInterval */ - Assert(not channelsOut[t]->full()); + assert(not channelsOut[t]->full()); T data = channelsOut[t]->pop(); @@ -177,7 +177,7 @@ void sharingManager(unsigned numThreads, for(unsigned t = 0; t < numThreads; ++t){ /* Alert if channel full, so that we increase sharingChannelSize or decrease sharingBroadcastInterval */ - Assert(not channelsIn[t]->full()); + assert(not channelsIn[t]->full()); while(!queues[t].empty() && !channelsIn[t]->full()){ Trace("sharing") << "sharing: pushing on channel " << t << std::endl; -- 2.30.2