diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 15:58:04 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 18:43:59 -0400 |
commit | 40f3b400173c637185eb9ad20e649bd92030c82b (patch) | |
tree | 6c0fb9a53695eb39c76d1dd3fdde6fe6b1e96758 /src/smt/smt_engine.cpp | |
parent | d93f5f6164b04ae2e82dbaf3af517ba206659547 (diff) |
New translator features: expand define-funs and combine assertions.
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 28a45206f..f82fc86ed 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -528,7 +528,7 @@ public: /** * Expand definitions in n. */ - Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache) + Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly = false) throw(TypeCheckingException, LogicException); /** @@ -1501,10 +1501,7 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } - - - -Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache) +Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) throw(TypeCheckingException, LogicException) { stack< triple<Node, Node, bool> > worklist; @@ -1586,12 +1583,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF n.begin(), n.end()); Debug("expand") << "made : " << instance << endl; - Node expanded = expandDefinitions(instance, cache); + Node expanded = expandDefinitions(instance, cache, expandOnly); cache[n] = (n == expanded ? Node::null() : expanded); result.push(expanded); continue; - } else { + } else if(! expandOnly) { + // do not do any theory stuff if expandOnly is true + theory::Theory* t = d_smt.d_theoryEngine->theoryOf(node); Assert(t != NULL); @@ -3478,7 +3477,7 @@ Expr SmtEngine::expandDefinitions(const Expr& ex) throw(TypeCheckingException, L Dump("benchmark") << ExpandDefinitionsCommand(e); } hash_map<Node, Node, NodeHashFunction> cache; - Node n = d_private->expandDefinitions(Node::fromExpr(e), cache); + Node n = d_private->expandDefinitions(Node::fromExpr(e), cache, /* expandOnly = */ true); n = postprocess(n, TypeNode::fromType(e.getType())); return n.toExpr(); |