diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-06-17 15:58:04 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
| commit | 552bc5f8045d773f36523e3d5a95506b83c819ab (patch) | |
| tree | 6c0fb9a53695eb39c76d1dd3fdde6fe6b1e96758 /src | |
| parent | 5401e0f9c1e88af588466bc437e1beef53fa4d2e (diff) | |
New translator features: expand define-funs and combine assertions.
Diffstat (limited to 'src')
| -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(); |