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 /src/main/portfolio_util.h | |
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.)
Diffstat (limited to 'src/main/portfolio_util.h')
-rw-r--r-- | src/main/portfolio_util.h | 18 |
1 files changed, 1 insertions, 17 deletions
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; |