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, 8 insertions, 1 deletions

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 */