diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-01 22:11:26 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-10-01 22:11:26 +0000 |
commit | 35ac65b0034eacf2766d9e94be1c7fe9c116bb75 (patch) | |
tree | de4a0848b08485fa2d9fa60738e0a47b5c876dc5 | |
parent | 2ee52cf8ccaa2e4514cd0e2023ee71a2b8b8d467 (diff) |
"Fix" (disable) portfolio when using quantifiers
Other changes:
* fix compile error in smt_engine in debug builds
* add getLogicInfo in smt_engine
* remove "empty-channel" and "disable-lemma-sharing" debug tags
(this commit was certified error- and warning-free by the test-and-commit script.)
-rw-r--r-- | src/main/command_executor_portfolio.cpp | 18 | ||||
-rw-r--r-- | src/main/portfolio_util.h | 18 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 6 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 5 |
4 files changed, 17 insertions, 30 deletions
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp index b9bf39002..4867082e6 100644 --- a/src/main/command_executor_portfolio.cpp +++ b/src/main/command_executor_portfolio.cpp @@ -104,13 +104,6 @@ void CommandExecutorPortfolio::lemmaSharingInit() const unsigned int sharingChannelSize = 1000000; for(unsigned i = 0; i < d_numThreads; ++i){ - if(Debug.isOn("channel-empty")) { - d_channelsOut.push_back - (new EmptySharedChannel<ChannelFormat>(sharingChannelSize)); - d_channelsIn.push_back - (new EmptySharedChannel<ChannelFormat>(sharingChannelSize)); - continue; - } d_channelsOut.push_back (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize)); d_channelsIn.push_back @@ -199,6 +192,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_seq->addCommand(cmd->clone()); return CommandExecutor::doCommandSingleton(cmd); } else if(mode == 1) { // portfolio + + // If quantified, stay sequential + if(d_smts[0]->getLogicInfo().isQuantified()) { + return CommandExecutor::doCommandSingleton(cmd); + } + d_seq->addCommand(cmd->clone()); // We currently don't support changing number of threads for each @@ -271,11 +270,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd) d_lastWinner = portfolioReturn.first; - // *d_options[options::out] - // << "Winner = " - // << portfolioReturn.first - // << std::endl; - if(d_ostringstreams.size() != 0) { assert(d_numThreads == d_options[options::threads]); assert(portfolioReturn.first >= 0); diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h index 416b9f44a..a3e7763fb 100644 --- a/src/main/portfolio_util.h +++ b/src/main/portfolio_util.h @@ -29,16 +29,6 @@ namespace CVC4 { typedef expr::pickle::Pickle ChannelFormat; -template <typename T> -class EmptySharedChannel: public SharedChannel<T> { -public: - EmptySharedChannel(int) {} - bool push(const T&) { return true; } - T pop() { return T(); } - bool empty() { return true; } - bool full() { return false; } -};/* class EmptySharedChannel */ - class PortfolioLemmaOutputChannel : public LemmaOutputChannel { private: std::string d_tag; @@ -59,15 +49,9 @@ public: {} void notifyNewLemma(Expr lemma) { - if(Debug.isOn("disable-lemma-sharing")) { + if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { return; } - if(options::sharingFilterByLength() >= 0) { - // 0 would mean no-sharing effectively - if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) { - return; - } - } ++cnt; Trace("sharing") << d_tag << ": " << lemma << std::endl; expr::pickle::Pickle pkl; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 069e5473e..08fdbec95 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -576,6 +576,10 @@ void SmtEngine::setLogic(const std::string& s) throw(ModalException) { setLogic(LogicInfo(s)); } +LogicInfo SmtEngine::getLogicInfo() const { + return d_logic; +} + // This function is called when d_logic has just been changed. // The LogicInfo isn't passed in explicitly, because that might // tempt people in the code to use the (potentially unlocked) @@ -1094,7 +1098,7 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect } return preSkolemizeQuantifiers( nn, polarity, fvs ); }else{ - Assert( n.getKind()==AND || n.getKind()==OR ); + Assert( n.getKind() == kind::AND || n.getKind() == kind::OR ); std::vector< Node > children; for( int i=0; i<(int)n.getNumChildren(); i++ ){ children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) ); diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index e906863ad..fb456a4a4 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -318,6 +318,11 @@ public: void setLogic(const LogicInfo& logic) throw(ModalException); /** + * Get the logic information currently set + */ + LogicInfo getLogicInfo() const; + + /** * Set information about the script executing. */ void setInfo(const std::string& key, const CVC4::SExpr& value) |