diff options
Diffstat (limited to 'src/prop/skolem_def_manager.cpp')
| -rw-r--r-- | src/prop/skolem_def_manager.cpp | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index 9b4011557..873a748ae 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -44,12 +44,13 @@ void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def) TNode SkolemDefManager::getDefinitionForSkolem(TNode skolem) const { NodeNodeMap::const_iterator it = d_skDefs.find(skolem); - AlwaysAssert(it != d_skDefs.end()) << "No skolem def for " << skolem; + Assert(it != d_skDefs.end()) << "No skolem def for " << skolem; return it->second; } void SkolemDefManager::notifyAsserted(TNode literal, - std::vector<TNode>& activatedSkolems) + std::vector<TNode>& activatedSkolems, + bool useDefs) { std::unordered_set<Node, NodeHashFunction> skolems; getSkolems(literal, skolems); @@ -61,8 +62,18 @@ void SkolemDefManager::notifyAsserted(TNode literal, continue; } d_skActive.insert(k); - // add to the activated list - activatedSkolems.push_back(k); + if (useDefs) + { + // add its definition to the activated list + NodeNodeMap::const_iterator it = d_skDefs.find(k); + Assert(it != d_skDefs.end()); + activatedSkolems.push_back(it->second); + } + else + { + // add to the activated list + activatedSkolems.push_back(k); + } } } |