diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-09-08 14:25:25 +0000 |
| commit | cfa9e2cbbdf77a325791b5548b41093a0781311c (patch) | |
| tree | e843d38afe4b197a2dd81316998477cedac26c52 /src/expr/expr_template.cpp | |
| parent | 6935324f45bd7f2c735ca4120a9e800ef8903442 (diff) | |
Single driver for both sequential and portfolio
A "command executer" layer between parsing commands and invoking them.
New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.
Diffstat (limited to 'src/expr/expr_template.cpp')
| -rw-r--r-- | src/expr/expr_template.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index a6f9f2cf6..4009bc610 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -131,7 +131,19 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC // temporarily set the node manager to NULL; this gets around // a check that mkVar isn't called internally NodeManagerScope nullScope(NULL); - to_e = to->mkVar(name, type);// FIXME thread safety + + if(n.getKind() == kind::BOUND_VAR_LIST) { + to_e = to->mkBoundVar(name, type);// FIXME thread safety + } else if(n.getKind() == kind::VARIABLE) { + to_e = to->mkVar(name, type);// FIXME thread safety + } else if(n.getKind() == kind::SKOLEM) { + Assert(false, "Skolem exporting not yet supported properly."); + // to fix this, get the node manager and do the appropriate + to_e = to->mkVar(name, type);// FIXME thread safety + } else { + Unhandled(); + } + Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl; } else { // temporarily set the node manager to NULL; this gets around |