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

1 files changed, 11 insertions, 3 deletions

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];