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

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index b9bf390026ab86040703f7b9efc72a1728dab76d..4867082e69192c105b279b86c3d6013e7ac17c03 100644 (file)
--- 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 416b9f44acb448351ed80047cdfb1c849c21f678..a3e7763fb07f8beb734915f02456e5f6d711ff1b 100644 (file)
--- 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 069e5473e904f5f4ad64b1d1be7feaab66b87cf0..08fdbec95b1fa17241cca655fc5db133c3dde996 100644 (file)
--- 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 e906863ada35d356c2f5a444098de83b091bd2c8..fb456a4a4b3fa452bf51844ce94607e780270eff 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -317,6 +317,11 @@ public:
    */
   void setLogic(const LogicInfo& logic) throw(ModalException);
 
+  /**
+   * Get the logic information currently set
+   */
+  LogicInfo getLogicInfo() const;
+
   /**
    * Set information about the script executing.
    */