diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-28 22:46:09 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-28 22:46:09 +0000 |
commit | 589bf879f00d2d8df4ccdaf3db28674ce3639512 (patch) | |
tree | 467b33e449ff47556388707000ab6b1edfb70411 /src/expr/expr_manager_template.cpp | |
parent | 730ea7d49ae56f8674e63ac9085adf06b6adf6f5 (diff) |
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.)
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 14 |
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]; |