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

7 files changed, 45 insertions, 27 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 938f28635..a62a9421f 100644
--- 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 5786f4e71..e120deed6 100644
--- 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 be2804fd5..457491445 100644
--- 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 f39c0e7ea..2f9e27c0c 100644
--- 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 96c7cfadf..4255e3454 100644
--- 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 a41db794d..6548cf98a 100644
--- 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 a6427ad47..dee4f06e6 100644
--- 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 */