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_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_template.cpp')
| -rw-r--r-- | src/expr/expr_template.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
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 |