diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index fa145813c..ce8f68c09 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1787,6 +1787,12 @@ void SmtEngine::defineFunction(Expr func, d_definedFunctions->insert(funcNode, def); } +bool SmtEngine::isDefinedFunction( Expr func ){ + Node nf = Node::fromExpr( func ); + Debug("smt") << "isDefined function " << nf << "?" << std::endl; + return d_definedFunctions->find(nf) != d_definedFunctions->end(); +} + Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache, bool expandOnly) throw(TypeCheckingException, LogicException, UnsafeInterruptException) { |