"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.)

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;