Some fixes to portfolio

* respect output lang
* fix export variable for BOUND_VARIABLE
* support export of SUBRANGE_TYPE
* statistic for lastWinner, other minor stat changes
* fix running of multiple threads on checsat/query
* changes of Assert -> assert which became private
* fix some destruction time order issues
* fix Pickler with AssertionException going private

Fixed by not fixing:
* portfolio+datatypes does not work
  - added ExportUnsupportedException to more places, switches
    to sequential
   (still TODO / decide : not switch silently, but print error)
   > note: this exception now needs to be (and is) defined in expr.h

Known issues:
* problems in portfolio+quantifiers
   - at least some problems appear to be because of static variables
   (will be later "fixed" like the datatypes)

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 938f286352b3d86c9a0961b6eba8c86db984e904..a62a9421faf7fb81019bdce55545fb610cae3c28 100644 (file)
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -1273,12 +1273,8 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  throw ExportToUnsupportedException();
-  // vector<DatatypeType> params;
-  // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params),
-  //           ExportTransformer(exprManager, variableMap));
-  // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params);
-  // return c;
+  throw ExportUnsupportedException
+          ("export of DatatypeDeclarationCommand unsupported");
 }
 
 Command* DatatypeDeclarationCommand::clone() const {

diff --git a/src/expr/command.h b/src/expr/command.h
index 5786f4e71373f54c1ec010628f1fa1be5ab4df90..e120deed62910bf90c63cc7793aeb8cc072783d8 100644 (file)
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -50,13 +50,6 @@ 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 CVC4_PUBLIC ExportToUnsupportedException : public Exception {
-public:
-  ExportToUnsupportedException() throw() :
-    Exception("exportTo unsupported for command") {
-  }
-};/* class ExportToUnsupportedException */
-
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
   /** Benchmark is satisfiable */

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index be2804fd5c0f787ba190c0a406e7b7f89cffe762..457491445818d7268bda96e9a98f0f0308222081 100644 (file)
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -928,13 +928,21 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
 
 TypeNode exportTypeInternal(TypeNode n, NodeManager* from, NodeManager* to, ExprManagerMapCollection& vmap) {
   Debug("export") << "type: " << n << std::endl;
-  Assert(n.getKind() == kind::SORT_TYPE ||
-         n.getMetaKind() != kind::metakind::PARAMETERIZED,
-         "PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+  if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+    throw ExportUnsupportedException
+      ("export of types belonging to theory of DATATYPES kinds unsupported");
+  }
+  if(n.getMetaKind() == kind::metakind::PARAMETERIZED &&
+     n.getKind() != kind::SORT_TYPE) { 
+    throw ExportUnsupportedException
+      ("export of PARAMETERIZED-kinded types (other than SORT_KIND) not supported");
+  }
   if(n.getKind() == kind::TYPE_CONSTANT) {
     return to->mkTypeConst(n.getConst<TypeConstant>());
   } else if(n.getKind() == kind::BITVECTOR_TYPE) {
     return to->mkBitVectorType(n.getConst<BitVectorSize>());
+  } else if(n.getKind() == kind::SUBRANGE_TYPE) {
+    return to->mkSubrangeType(n.getSubrangeBounds());
   }
   Type from_t = from->toType(n);
   Type& to_t = vmap.d_typeMap[from_t];

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index f39c0e7eadcc714c53f89c9be98373ad923bf84f..2f9e27c0c0309981a32eebb0e21cbeba27e0226f 100644 (file)
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -114,7 +114,12 @@ namespace expr {
 static Node exportConstant(TNode n, NodeManager* to);
 
 Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapCollection& vmap) {
-  if(n.isConst()) {
+  if(theory::kindToTheoryId(n.getKind()) == theory::THEORY_DATATYPES) {
+    throw ExportUnsupportedException
+       ("export of node belonging to theory of DATATYPES kinds unsupported");
+  }
+
+  if(n.getMetaKind() == metakind::CONSTANT) {
     return exportConstant(n, NodeManager::fromExprManager(to));
   } else if(n.isVar()) {
     Expr from_e(from, new Node(n));
@@ -132,7 +137,7 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
         // a check that mkVar isn't called internally
         NodeManagerScope nullScope(NULL);
 
-        if(n.getKind() == kind::BOUND_VAR_LIST) {
+        if(n.getKind() == kind::BOUND_VAR_LIST || n.getKind() == kind::BOUND_VARIABLE) {
           to_e = to->mkBoundVar(name, type);// FIXME thread safety
         } else if(n.getKind() == kind::VARIABLE) {
           to_e = to->mkVar(name, type);// FIXME thread safety

diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 96c7cfadfb67a5f72f6de96700d9621bc034a9b0..4255e34546844b7e1c118b8d4245f59434b3f4d3 100644 (file)
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -132,6 +132,19 @@ public:
   friend class ExprManager;
 };/* class TypeCheckingException */
 
+/**
+ * Exception thrown in case of failure to export
+ */
+class CVC4_PUBLIC ExportUnsupportedException : public Exception {
+public:
+  ExportUnsupportedException() throw():
+    Exception("export unsupported") {
+  }
+  ExportUnsupportedException(const char* msg) throw():
+    Exception(msg) {
+  }
+};/* class DatatypeExportUnsupportedException */
+
 std::ostream& operator<<(std::ostream& out,
                          const TypeCheckingException& e) CVC4_PUBLIC;
 

diff --git a/src/expr/pickler.cpp b/src/expr/pickler.cpp
index a41db794db536e32133c0ebd09aa1f9aa9c0a817..6548cf98af3c6cea2ccf3b946f6e02f4c6dc1a7a 100644 (file)
--- a/src/expr/pickler.cpp
+++ b/src/expr/pickler.cpp
@@ -129,7 +129,7 @@ Pickler::~Pickler() {
 }
 
 void Pickler::toPickle(Expr e, Pickle& p)
-  throw(AssertionException, PicklingException) {
+  throw(PicklingException) {
   Assert(NodeManager::fromExprManager(e.getExprManager()) == d_private->d_nm);
   Assert(d_private->atDefaultState());
 
@@ -471,6 +471,13 @@ Pickle::~Pickle() {
   delete d_data;
 }
 
+uint64_t MapPickler::variableFromMap(uint64_t x) const 
+{
+  VarMap::const_iterator i = d_fromMap.find(x);
+  Assert(i != d_fromMap.end());
+  return i->second;
+}
+
 }/* CVC4::expr::pickle namespace */
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */

diff --git a/src/expr/pickler.h b/src/expr/pickler.h
index a6427ad47654537f754252096096ff86b9502e80..dee4f06e6886743a8bc35e7f9c2b3380a6cb0ecc 100644 (file)
--- a/src/expr/pickler.h
+++ b/src/expr/pickler.h
@@ -67,7 +67,7 @@ class CVC4_PUBLIC Pickler {
 
 protected:
   virtual uint64_t variableToMap(uint64_t x) const
-    throw(AssertionException, PicklingException) {
+    throw(PicklingException) {
     return x;
   }
   virtual uint64_t variableFromMap(uint64_t x) const {
@@ -87,7 +87,7 @@ public:
    *
    * @return the pickle, which should be dispose()'d when you're done with it
    */
-  void toPickle(Expr e, Pickle& p) throw(AssertionException, PicklingException);
+  void toPickle(Expr e, Pickle& p) throw(PicklingException);
 
   /**
    * Constructs a node from a Pickle.
@@ -116,7 +116,7 @@ public:
 protected:
 
   virtual uint64_t variableToMap(uint64_t x) const
-    throw(AssertionException, PicklingException) {
+    throw(PicklingException) {
     VarMap::const_iterator i = d_toMap.find(x);
     if(i != d_toMap.end()) {
       return i->second;
@@ -125,11 +125,7 @@ protected:
     }
   }
 
-  virtual uint64_t variableFromMap(uint64_t x) const {
-    VarMap::const_iterator i = d_fromMap.find(x);
-    Assert(i != d_fromMap.end());
-    return i->second;
-  }
+  virtual uint64_t variableFromMap(uint64_t x) const; 
 };/* class MapPickler */
 
 }/* CVC4::expr::pickle namespace */

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 435299ce32a89f8083b116ac49b66a191942208d..a5bd78abe53bad717b8e6fc0f168b47f4c081676 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -38,14 +38,8 @@ protected:
   StatisticsRegistry d_stats;
 
 public:
-  // Note: though the options are not cached (instead a reference is
-  // used), the portfolio command executer currently parses them
-  // during initalization, creating thread-specific options and
-  // storing them
   CommandExecutor(ExprManager &exprMgr, Options &options);
 
-  ~CommandExecutor() {}
-
   /**
    * Executes a command. Recursively handles if cmd is a command
    * sequence.  Eventually uses doCommandSingleton (which can be

diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 32a507d78a4e562a2c8c5c7d2e5fd5e03513951e..b9bf390026ab86040703f7b9efc72a1728dab76d 100644 (file)
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -48,9 +48,13 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
   d_lastWinner(0),
   d_channelsOut(),
   d_channelsIn(),
-  d_ostringstreams()
+  d_ostringstreams(),
+  d_statLastWinner("portfolio::lastWinner")
 {
-  Assert(d_threadOptions.size() == d_numThreads);
+  assert(d_threadOptions.size() == d_numThreads);
+
+  d_statLastWinner.setData(d_lastWinner);
+  d_stats.registerStat_(&d_statLastWinner);
 
   /* Duplication, Individualisation */
   d_exprMgrs.push_back(&d_exprMgr);
@@ -64,7 +68,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
     d_smts.push_back(new SmtEngine(d_exprMgrs[i]));
   }
 
-  Assert(d_vmaps.size() == 0);
+  assert(d_vmaps.size() == 0);
   for(unsigned i = 0; i < d_numThreads; ++i) {
     d_vmaps.push_back(new ExprManagerMapCollection());
   }
@@ -72,15 +76,15 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
 
 CommandExecutorPortfolio::~CommandExecutorPortfolio()
 {
-  Assert(d_seq != NULL);
+  assert(d_seq != NULL);
   delete d_seq;
 
-  Assert(d_smts.size() == d_numThreads);
+  assert(d_smts.size() == d_numThreads);
   for(unsigned i = 1; i < d_numThreads; ++i) {
     // the 0-th one is responsibility of parent class
 
-    delete d_exprMgrs[i];
     delete d_smts[i];
+    delete d_exprMgrs[i];
   }
   d_exprMgrs.clear();
   d_smts.clear();
@@ -89,8 +93,8 @@ CommandExecutorPortfolio::~CommandExecutorPortfolio()
 void CommandExecutorPortfolio::lemmaSharingInit()
 {
   /* Sharing channels */
-  Assert(d_channelsIn.size() == 0);
-  Assert(d_channelsOut.size() == 0);
+  assert(d_channelsIn.size() == 0);
+  assert(d_channelsOut.size() == 0);
 
   if(d_numThreads == 1) {
     // Disable sharing
@@ -130,10 +134,14 @@ void CommandExecutorPortfolio::lemmaSharingInit()
     /* Output to string stream  */
     if(d_options[options::verbosity] == 0
        || d_options[options::separateOutput]) {
-      Assert(d_ostringstreams.size() == 0);
+      assert(d_ostringstreams.size() == 0);
       for(unsigned i = 0; i < d_numThreads; ++i) {
         d_ostringstreams.push_back(new ostringstream);
         d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+
+        // important even for muzzled builds (to get result output right)
+        *d_threadOptions[i][options::out]
+          << Expr::setlanguage(d_threadOptions[i][options::outputLanguage]);
       }
     }
   }
@@ -141,11 +149,11 @@ void CommandExecutorPortfolio::lemmaSharingInit()
 
 void CommandExecutorPortfolio::lemmaSharingCleanup()
 {
-  Assert(d_numThreads == d_options[options::threads]);
+  assert(d_numThreads == d_options[options::threads]);
 
   // Channel cleanup
-  Assert(d_channelsIn.size() == d_numThreads);
-  Assert(d_channelsOut.size() == d_numThreads);
+  assert(d_channelsIn.size() == d_numThreads);
+  assert(d_channelsOut.size() == d_numThreads);
   for(unsigned i = 0; i < d_numThreads; ++i) {
     delete d_channelsIn[i];
     delete d_channelsOut[i];
@@ -157,7 +165,7 @@ void CommandExecutorPortfolio::lemmaSharingCleanup()
 
   // sstreams cleanup (if used)
   if(d_ostringstreams.size() != 0) {
-    Assert(d_ostringstreams.size() == d_numThreads);
+    assert(d_ostringstreams.size() == d_numThreads);
     for(unsigned i = 0; i < d_numThreads; ++i) {
       d_threadOptions[i].set(options::out, d_options[options::out]);
       delete d_ostringstreams[i];
@@ -180,12 +188,12 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
   // mode = 1 : run a porfolio
   // mode = 2 : run the last winner
 
-  // if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
-  //    dynamic_cast<QueryCommand*>(cmd) != NULL) {
-  //   mode = 1;
-  // } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) {
-  //   mode = 2;
-  // }
+  if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
+    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+    mode = 1;
+  } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) {
+    mode = 2;
+  }
 
   if(mode == 0) {
     d_seq->addCommand(cmd->clone());
@@ -213,7 +221,7 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
        */
       try {
         seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
-      }catch(ExportToUnsupportedException& e){
+      }catch(ExportUnsupportedException& e){
         return CommandExecutor::doCommandSingleton(cmd);
       }
     }
@@ -244,9 +252,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                            );
     }
 
-    Assert(d_channelsIn.size() == d_numThreads);
-    Assert(d_channelsOut.size() == d_numThreads);
-    Assert(d_smts.size() == d_numThreads);
+    assert(d_channelsIn.size() == d_numThreads);
+    assert(d_channelsOut.size() == d_numThreads);
+    assert(d_smts.size() == d_numThreads);
     boost::function<void()>
       smFn = boost::bind(sharingManager<ChannelFormat>,
                          d_numThreads,
@@ -269,9 +277,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     //   << std::endl;
 
     if(d_ostringstreams.size() != 0) {
-      Assert(d_numThreads == d_options[options::threads]);
-      Assert(portfolioReturn.first >= 0);
-      Assert(unsigned(portfolioReturn.first) < d_numThreads);
+      assert(d_numThreads == d_options[options::threads]);
+      assert(portfolioReturn.first >= 0);
+      assert(unsigned(portfolioReturn.first) < d_numThreads);
 
       *d_options[options::out]
         << d_ostringstreams[portfolioReturn.first]->str();
@@ -286,7 +294,8 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                            cmd,
                            d_threadOptions[d_lastWinner][options::out]);
   } else {
-    Unreachable();
+    // Unreachable();
+    assert(false);
   }
 
 }/* CommandExecutorPortfolio::doCommandSingleton() */
@@ -297,15 +306,15 @@ std::string CommandExecutorPortfolio::getSmtEngineStatus()
 }
 
 void CommandExecutorPortfolio::flushStatistics(std::ostream& out) const {
-  Assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
+  assert(d_numThreads == d_exprMgrs.size() && d_exprMgrs.size() == d_smts.size());
   for(size_t i = 0; i < d_numThreads; ++i) {
-    string emTag = "ExprManager thread #"
+    string emTag = "thread#"
       + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
     Statistics stats = d_exprMgrs[i]->getStatistics();
     stats.setPrefix(emTag);
     stats.flushInformation(out);
 
-    string smtTag = "SmtEngine thread #"
+    string smtTag = "thread#"
       + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
     stats = d_smts[i]->getStatistics();
     stats.setPrefix(smtTag);

diff --git a/src/main/command_executor_portfolio.h b/src/main/command_executor_portfolio.h
index 72a677789b29bad08069026ab8d5067729016993..867b62d31ea59f82dbe7cfafae555046378e3c87 100644 (file)
--- a/src/main/command_executor_portfolio.h
+++ b/src/main/command_executor_portfolio.h
@@ -52,6 +52,9 @@ class CommandExecutorPortfolio : public CommandExecutor {
   std::vector< SharedChannel<ChannelFormat>* > d_channelsIn;
   std::vector<std::ostringstream*> d_ostringstreams;
 
+  // Stats
+  ReferenceStat<int> d_statLastWinner;
+
 public:
   CommandExecutorPortfolio(ExprManager &exprMgr,
                            Options &options,

diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
index b208b2479ada5c0aa69a9ea2d10f378c5b1c8566..b16ac2d341eaa337a59164218b2934b127cdf98d 100644 (file)
--- a/src/main/portfolio_util.cpp
+++ b/src/main/portfolio_util.cpp
@@ -14,6 +14,7 @@
  ** \brief Code relevant only for portfolio builds
  **/
 
+#include <cassert>
 #include <vector>
 #include <unistd.h>
 #include "options/options.h"
@@ -97,7 +98,7 @@ vector<Options> parseThreadSpecificOptions(Options opts)
     }
   }
 
-  Assert(numThreads >= 1);      //do we need this?
+  assert(numThreads >= 1);      //do we need this?
 
   return threadOptions;
 }

diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
index 1955a29a73f4bacca748215692b558296250bcf4..416b9f44acb448351ed80047cdfb1c849c21f678 100644 (file)
--- a/src/main/portfolio_util.h
+++ b/src/main/portfolio_util.h
@@ -155,7 +155,7 @@ void sharingManager(unsigned numThreads,
 
       /* Alert if channel full, so that we increase sharingChannelSize
          or decrease sharingBroadcastInterval */
-      Assert(not channelsOut[t]->full());
+      assert(not channelsOut[t]->full());
 
       T data = channelsOut[t]->pop();
 
@@ -177,7 +177,7 @@ void sharingManager(unsigned numThreads,
     for(unsigned t = 0; t < numThreads; ++t){
       /* Alert if channel full, so that we increase sharingChannelSize
          or decrease sharingBroadcastInterval */
-      Assert(not channelsIn[t]->full());
+      assert(not channelsIn[t]->full());
 
       while(!queues[t].empty() && !channelsIn[t]->full()){
         Trace("sharing") << "sharing: pushing on channel " << t << std::endl;