From 480d440174c565bec9aba412c0d35221c9169ff6 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 8 Sep 2012 22:31:44 +0000 Subject: [PATCH] Some minor changes after reviewing the portfolio "unified driver" commit. (this commit was certified error- and warning-free by the test-and-commit script.) --- src/expr/command.h | 5 ++-- src/expr/expr_template.cpp | 8 +++-- src/main/Makefile.am | 8 +++-- ...mand_executer.cpp => command_executor.cpp} | 16 +++++----- ...{command_executer.h => command_executor.h} | 30 +++++++++---------- ...lio.cpp => command_executor_portfolio.cpp} | 28 ++++++++--------- ...rtfolio.h => command_executor_portfolio.h} | 28 ++++++++--------- src/main/driver_unified.cpp | 16 +++++----- src/main/portfolio_util.cpp | 1 + src/main/portfolio_util.h | 12 ++++---- src/prop/prop_engine.cpp | 2 -- src/util/channel.h | 9 ++++-- 12 files changed, 83 insertions(+), 80 deletions(-) rename src/main/{command_executer.cpp => command_executor.cpp} (82%) rename src/main/{command_executer.h => command_executor.h} (71%) rename src/main/{command_executer_portfolio.cpp => command_executor_portfolio.cpp} (92%) rename src/main/{command_executer_portfolio.h => command_executor_portfolio.h} (71%) diff --git a/src/expr/command.h b/src/expr/command.h index 3c919c374..70e71a111 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -50,13 +50,12 @@ 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 ExportToUnsupportedException : public Exception { +class CVC4_PUBLIC ExportToUnsupportedException : public Exception { public: ExportToUnsupportedException() throw() : Exception("exportTo unsupported for command") { } -};/* class NoMoreValuesException */ - +};/* class ExportToUnsupportedException */ /** The status an SMT benchmark can have */ enum BenchmarkStatus { diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 4009bc610..08c3a2b1e 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -137,9 +137,11 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC } else if(n.getKind() == kind::VARIABLE) { to_e = to->mkVar(name, type);// FIXME thread safety } else if(n.getKind() == kind::SKOLEM) { - Assert(false, "Skolem exporting not yet supported properly."); - // to fix this, get the node manager and do the appropriate - to_e = to->mkVar(name, type);// FIXME thread safety + // skolems are only available at the Node level (not the Expr level) + TypeNode typeNode = TypeNode::fromType(type); + NodeManager* to_nm = NodeManager::fromExprManager(to); + Node n = to_nm->mkSkolem(name, typeNode);// FIXME thread safety + to_e = n.toExpr(); } else { Unhandled(); } diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 9b0200231..2a1ce0d55 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -20,8 +20,10 @@ pcvc4_SOURCES = \ portfolio.cpp \ portfolio.h \ portfolio_util.cpp \ - command_executer.cpp \ - command_executer_portfolio.cpp \ + command_executor.cpp \ + command_executor_portfolio.cpp \ + command_executor.h \ + command_executor_portfolio.h \ driver_unified.cpp pcvc4_LDADD = \ libmain.a \ @@ -42,7 +44,7 @@ endif cvc4_SOURCES = \ main.cpp \ - command_executer.cpp \ + command_executor.cpp \ driver_unified.cpp cvc4_LDADD = \ libmain.a \ diff --git a/src/main/command_executer.cpp b/src/main/command_executor.cpp similarity index 82% rename from src/main/command_executer.cpp rename to src/main/command_executor.cpp index 039ab664c..1bffd5e35 100644 --- a/src/main/command_executer.cpp +++ b/src/main/command_executor.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file command_executer.cpp +/*! \file command_executor.cpp ** \verbatim ** Original author: kshitij ** Major contributors: none - ** Minor contributors (to current version): + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 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 @@ -16,7 +16,7 @@ #include -#include "main/command_executer.h" +#include "main/command_executor.h" #include "expr/command.h" #include "main/main.h" @@ -25,7 +25,7 @@ namespace CVC4 { namespace main { -CommandExecuter::CommandExecuter(ExprManager &exprMgr, Options &options): +CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options): d_exprMgr(exprMgr), d_smtEngine(SmtEngine(&exprMgr)), d_options(options) { @@ -36,7 +36,7 @@ CommandExecuter::CommandExecuter(ExprManager &exprMgr, Options &options): main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry()); } -bool CommandExecuter::doCommand(Command* cmd) +bool CommandExecutor::doCommand(Command* cmd) { if( d_options[options::parseOnly] ) { return true; @@ -63,7 +63,7 @@ bool CommandExecuter::doCommand(Command* cmd) } } -bool CommandExecuter::doCommandSingleton(Command *cmd) +bool CommandExecutor::doCommandSingleton(Command *cmd) { bool status = true; if(d_options[options::verbosity] >= 0) { @@ -74,7 +74,7 @@ bool CommandExecuter::doCommandSingleton(Command *cmd) return status; } -std::string CommandExecuter::getSmtEngineStatus() +std::string CommandExecutor::getSmtEngineStatus() { return d_smtEngine.getInfo("status").getValue(); } diff --git a/src/main/command_executer.h b/src/main/command_executor.h similarity index 71% rename from src/main/command_executer.h rename to src/main/command_executor.h index 245857c04..273225e69 100644 --- a/src/main/command_executer.h +++ b/src/main/command_executor.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file command_executer.cpp +/*! \file command_executor.h ** \verbatim ** Original author: kshitij - ** Major contributors: mdeters - ** Minor contributors (to current version): + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 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 @@ -14,17 +14,16 @@ ** \brief An additional layer between commands and invoking them. **/ -#ifndef __CVC4__COMMAND_EXECUTER_H -#define __CVC4__COMMAND_EXECUTER_H +#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_H +#define __CVC4__MAIN__COMMAND_EXECUTOR_H #include "expr/expr_manager.h" #include "smt/smt_engine.h" namespace CVC4 { - namespace main { -class CommandExecuter { +class CommandExecutor { protected: ExprManager& d_exprMgr; @@ -36,9 +35,9 @@ public: // used), the portfolio command executer currently parses them // during initalization, creating thread-specific options and // storing them - CommandExecuter(ExprManager &exprMgr, Options &options); + CommandExecutor(ExprManager &exprMgr, Options &options); - ~CommandExecuter() {} + ~CommandExecutor() {} /** * Executes a command. Recursively handles if cmd is a command @@ -54,16 +53,15 @@ protected: virtual bool doCommandSingleton(CVC4::Command* cmd); private: - CommandExecuter(); + CommandExecutor(); -}; +};/* class CommandExecutor */ bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out); +}/* CVC4::main namespace */ +}/* CVC4 namespace */ -}/*main namespace*/ -}/*CVC4 namespace*/ - -#endif /* __CVC4__COMMAND_EXECUTER_H */ +#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_H */ diff --git a/src/main/command_executer_portfolio.cpp b/src/main/command_executor_portfolio.cpp similarity index 92% rename from src/main/command_executer_portfolio.cpp rename to src/main/command_executor_portfolio.cpp index 85180c9a9..045cac8f1 100644 --- a/src/main/command_executer_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -1,11 +1,11 @@ /********************* */ -/*! \file command_executer_portfolio.cpp +/*! \file command_executor_portfolio.cpp ** \verbatim ** Original author: kshitij - ** Major contributors: mdeters, taking - ** Minor contributors (to current version): + ** Major contributors: none + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 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 @@ -24,7 +24,7 @@ #include "expr/command.h" #include "expr/pickler.h" -#include "main/command_executer_portfolio.h" +#include "main/command_executor_portfolio.h" #include "main/main.h" #include "main/options.h" #include "main/portfolio.h" @@ -36,9 +36,9 @@ using namespace std; namespace CVC4 { namespace main { -CommandExecuterPortfolio::CommandExecuterPortfolio +CommandExecutorPortfolio::CommandExecutorPortfolio (ExprManager &exprMgr, Options &options, vector& tOpts): - CommandExecuter(exprMgr, options), + CommandExecutor(exprMgr, options), d_numThreads(options[options::threads]), d_smts(), d_seq(new CommandSequence()), @@ -85,7 +85,7 @@ CommandExecuterPortfolio::CommandExecuterPortfolio } -CommandExecuterPortfolio::~CommandExecuterPortfolio() +CommandExecutorPortfolio::~CommandExecutorPortfolio() { Assert(d_seq != NULL); delete d_seq; @@ -101,7 +101,7 @@ CommandExecuterPortfolio::~CommandExecuterPortfolio() d_smts.clear(); } -void CommandExecuterPortfolio::lemmaSharingInit() +void CommandExecutorPortfolio::lemmaSharingInit() { /* Sharing channels */ Assert(d_channelsIn.size() == 0); @@ -154,7 +154,7 @@ void CommandExecuterPortfolio::lemmaSharingInit() } } -void CommandExecuterPortfolio::lemmaSharingCleanup() +void CommandExecutorPortfolio::lemmaSharingCleanup() { Assert(d_numThreads == d_options[options::threads]); @@ -182,7 +182,7 @@ void CommandExecuterPortfolio::lemmaSharingCleanup() } -bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd) +bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) { /** * save the command and if check sat or query command, run a @@ -203,7 +203,7 @@ bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd) if(mode == 0) { d_seq->addCommand(cmd->clone()); - return CommandExecuter::doCommandSingleton(cmd); + return CommandExecutor::doCommandSingleton(cmd); } else if(mode == 1) { // portfolio d_seq->addCommand(cmd->clone()); @@ -228,7 +228,7 @@ bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd) try { seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) ); }catch(ExportToUnsupportedException& e){ - return CommandExecuter::doCommandSingleton(cmd); + return CommandExecutor::doCommandSingleton(cmd); } } @@ -305,7 +305,7 @@ bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd) } -std::string CommandExecuterPortfolio::getSmtEngineStatus() +std::string CommandExecutorPortfolio::getSmtEngineStatus() { return d_smts[d_lastWinner]->getInfo("status").getValue(); } diff --git a/src/main/command_executer_portfolio.h b/src/main/command_executor_portfolio.h similarity index 71% rename from src/main/command_executer_portfolio.h rename to src/main/command_executor_portfolio.h index db9db6509..cc0a77698 100644 --- a/src/main/command_executer_portfolio.h +++ b/src/main/command_executor_portfolio.h @@ -1,11 +1,11 @@ /********************* */ -/*! \file command_executer_portfolio.h +/*! \file command_executor_portfolio.h ** \verbatim ** Original author: kshitij ** Major contributors: none - ** Minor contributors (to current version): + ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 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 @@ -17,10 +17,10 @@ ** threads. **/ -#ifndef __CVC4__COMMAND_EXECUTER_PORTFOLIO_H -#define __CVC4__COMMAND_EXECUTER_PORTFOLIO_H +#ifndef __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H +#define __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H -#include "main/command_executer.h" +#include "main/command_executor.h" #include "main/portfolio_util.h" namespace CVC4 { @@ -29,7 +29,7 @@ class CommandSequence; namespace main { -class CommandExecuterPortfolio : public CommandExecuter { +class CommandExecutorPortfolio : public CommandExecutor { // These shall be created/deleted during initalization std::vector d_exprMgrs; @@ -48,22 +48,22 @@ class CommandExecuterPortfolio : public CommandExecuter { std::vector d_ostringstreams; public: - CommandExecuterPortfolio(ExprManager &exprMgr, + CommandExecutorPortfolio(ExprManager &exprMgr, Options &options, std::vector& tOpts); - ~CommandExecuterPortfolio(); + ~CommandExecutorPortfolio(); std::string getSmtEngineStatus(); protected: bool doCommandSingleton(Command* cmd); private: - CommandExecuterPortfolio(); + CommandExecutorPortfolio(); void lemmaSharingInit(); void lemmaSharingCleanup(); -}; +};/* class CommandExecutorPortfolio */ -}/*main namespace*/ -}/*CVC4 namespace*/ +}/* CVC4::main namespace */ +}/* CVC4 namespace */ -#endif /* __CVC4__COMMAND_EXECUTER_PORTFOLIO_H */ +#endif /* __CVC4__MAIN__COMMAND_EXECUTOR_PORTFOLIO_H */ diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 061e34223..f91f951c6 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -35,9 +35,9 @@ #include "util/Assert.h" #include "util/configuration.h" #include "options/options.h" -#include "main/command_executer.h" +#include "main/command_executor.h" # ifdef PORTFOLIO_BUILD -# include "main/command_executer_portfolio.h" +# include "main/command_executor_portfolio.h" # endif #include "main/options.h" #include "smt/options.h" @@ -226,11 +226,11 @@ int runCvc4(int argc, char* argv[], Options& opts) { ExprManager exprMgr(threadOpts[0]); # endif - CommandExecuter* cmdExecuter = + CommandExecutor* cmdExecutor = # ifndef PORTFOLIO_BUILD - new CommandExecuter(exprMgr, opts); + new CommandExecutor(exprMgr, opts); # else - new CommandExecuterPortfolio(exprMgr, opts, threadOpts); + new CommandExecutorPortfolio(exprMgr, opts, threadOpts); #endif // Create the SmtEngine @@ -280,7 +280,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { replayParser->useDeclarationsFrom(shell.getParser()); } while((cmd = shell.readCommand())) { - status = cmdExecuter->doCommand(cmd) && status; + status = cmdExecutor->doCommand(cmd) && status; delete cmd; } } else { @@ -304,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { delete cmd; break; } - status = cmdExecuter->doCommand(cmd); + status = cmdExecutor->doCommand(cmd); delete cmd; } // Remove the parser @@ -320,7 +320,7 @@ int runCvc4(int argc, char* argv[], Options& opts) { int returnValue; string result = "unknown"; if(status) { - result = cmdExecuter->getSmtEngineStatus(); + result = cmdExecutor->getSmtEngineStatus(); if(result == "sat") { returnValue = 10; diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp index bad532d30..b208b2479 100644 --- a/src/main/portfolio_util.cpp +++ b/src/main/portfolio_util.cpp @@ -15,6 +15,7 @@ **/ #include +#include #include "options/options.h" #include "main/options.h" #include "prop/options.h" diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index eed993b9f..1955a29a7 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -14,8 +14,8 @@ ** \brief Code relevant only for portfolio builds **/ -#ifndef __CVC4_PORTFOLIO_UTIL_H -#define __CVC4_PORTFOLIO_UTIL_H +#ifndef __CVC4__PORTFOLIO_UTIL_H +#define __CVC4__PORTFOLIO_UTIL_H #include @@ -37,7 +37,7 @@ public: T pop() { return T(); } bool empty() { return true; } bool full() { return false; } -}; +};/* class EmptySharedChannel */ class PortfolioLemmaOutputChannel : public LemmaOutputChannel { private: @@ -202,8 +202,8 @@ void sharingManager(unsigned numThreads, } Trace("sharing") << "sharing: Interrupted, exiting." << std::endl; -} +}/* sharingManager() */ -}/*CVC4 namespace*/ +}/* CVC4 namespace */ -#endif /* __CVC4_PORTFOLIO_UTIL_H */ +#endif /* __CVC4__PORTFOLIO_UTIL_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 281645317..a82e1b735 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -272,8 +272,6 @@ bool PropEngine::isRunning() const { void PropEngine::interrupt() throw(ModalException) { if(! d_inCheckSat) { return; - throw ModalException("SAT solver is not currently solving anything; " - "cannot interrupt it"); } d_interrupted = true; diff --git a/src/util/channel.h b/src/util/channel.h index eae7a4f11..4a07f265d 100644 --- a/src/util/channel.h +++ b/src/util/channel.h @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_public.h" + #ifndef __CVC4__CHANNEL_H #define __CVC4__CHANNEL_H @@ -31,12 +33,13 @@ namespace CVC4 { template -class SharedChannel { +class CVC4_PUBLIC SharedChannel { private: int d_maxsize; // just call it size? public: SharedChannel() {} SharedChannel(int maxsize) : d_maxsize(maxsize) {} + virtual ~SharedChannel() {} /* Tries to add element and returns true if successful */ virtual bool push(const T&) = 0; @@ -59,7 +62,7 @@ http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.h and is covered by the Boost Software License, version 1.0. */ template -class SynchronizedSharedChannel : public SharedChannel { +class CVC4_PUBLIC SynchronizedSharedChannel : public SharedChannel { public: typedef boost::circular_buffer container_type; typedef typename container_type::size_type size_type; @@ -108,6 +111,6 @@ private: boost::condition m_not_full; };/* class SynchronizedSharedChannel */ -} +}/* CVC4 namespace */ #endif /* __CVC4__CHANNEL_H */ -- 2.30.2