Reorganizing use of skolem definition manager in prop engine (#6415)

Towards setting up the proper callbacks into the new justification heuristic.

Moves ownership of skolem definition manager from TheoryProxy to PropEngine.

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);
+    }
   }
 }