Add skolem definition manager (#6187)

This creates a central utility for managing "skolem definitions", e.g. mapping between skolems and the lemmas that define their behavior.

This utility is taken from the satRlv branch. It will also be used for the new implementation of the justification decision heuristic.

Note that this PR takes some helper functions out of term formula removal (e.g. hasSkolems) Prior to this PR, these helper functions were incorrect since term formula removal does not account for all introduced skolems. For instance, Theory::ppRewrite may introduce skolems directly. This PR consolidates these cases into the new class, which is called from PropEngine when lemmas and assertions are added. At the moment, the only use of this method is for CEGQI, which needs to do its own tracking of skolems in certain literals.

It also makes some minor reorganization to prop engine.

1 files changed, 173 insertions, 0 deletions

diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp
new file mode 100644
index 000000000..c2a6a8462
--- /dev/null
+++ b/src/prop/skolem_def_manager.cpp
@@ -0,0 +1,173 @@
+/*********************                                                        */
+/*! \file skolem_def_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Skolem definition manager
+ **/
+
+#include "prop/skolem_def_manager.h"
+
+#include "expr/attribute.h"
+
+namespace CVC4 {
+namespace prop {
+
+SkolemDefManager::SkolemDefManager(context::Context* context,
+                                   context::UserContext* userContext)
+    : d_skDefs(userContext), d_skActive(context)
+{
+}
+
+SkolemDefManager::~SkolemDefManager() {}
+
+void SkolemDefManager::notifySkolemDefinition(TNode skolem, Node def)
+{
+  // Notice that skolem may have kind SKOLEM or BOOLEAN_TERM_VARIABLE
+  Trace("sk-defs") << "notifySkolemDefinition: " << def << " for " << skolem
+                   << std::endl;
+  // in very rare cases, a skolem may be generated twice for terms that are
+  // equivalent up to purification
+  if (d_skDefs.find(skolem) == d_skDefs.end())
+  {
+    d_skDefs.insert(skolem, 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;
+  return it->second;
+}
+
+void SkolemDefManager::notifyAsserted(TNode literal,
+                                      std::vector<TNode>& activatedSkolems)
+{
+  std::unordered_set<Node, NodeHashFunction> skolems;
+  getSkolems(literal, skolems);
+  for (const Node& k : skolems)
+  {
+    if (d_skActive.find(k) != d_skActive.end())
+    {
+      // already active
+      continue;
+    }
+    d_skActive.insert(k);
+    // add to the activated list
+    activatedSkolems.push_back(k);
+  }
+}
+
+struct HasSkolemTag
+{
+};
+struct HasSkolemComputedTag
+{
+};
+/** Attribute true for nodes with skolems in them */
+typedef expr::Attribute<HasSkolemTag, bool> HasSkolemAttr;
+/** Attribute true for nodes where we have computed the above attribute */
+typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr;
+
+bool SkolemDefManager::hasSkolems(TNode n) const
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    if (cur.getAttribute(HasSkolemComputedAttr()))
+    {
+      visit.pop_back();
+      // already computed
+      continue;
+    }
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.getNumChildren() == 0)
+      {
+        visit.pop_back();
+        bool hasSkolem = false;
+        if (cur.isVar())
+        {
+          hasSkolem = (d_skDefs.find(cur) != d_skDefs.end());
+        }
+        cur.setAttribute(HasSkolemAttr(), hasSkolem);
+        cur.setAttribute(HasSkolemComputedAttr(), true);
+      }
+      else
+      {
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+    else
+    {
+      visit.pop_back();
+      bool hasSkolem = false;
+      for (TNode i : cur)
+      {
+        Assert(i.getAttribute(HasSkolemComputedAttr()));
+        if (i.getAttribute(HasSkolemAttr()))
+        {
+          hasSkolem = true;
+          break;
+        }
+      }
+      cur.setAttribute(HasSkolemAttr(), hasSkolem);
+      cur.setAttribute(HasSkolemComputedAttr(), true);
+    }
+  } while (!visit.empty());
+  Assert(n.getAttribute(HasSkolemComputedAttr()));
+  return n.getAttribute(HasSkolemAttr());
+}
+
+void SkolemDefManager::getSkolems(
+    TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const
+{
+  std::unordered_set<TNode, TNodeHashFunction> visited;
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    if (!hasSkolems(cur))
+    {
+      // does not have skolems, continue
+      continue;
+    }
+    it = visited.find(cur);
+    if (it == visited.end())
+    {
+      visited.insert(cur);
+      if (cur.isVar())
+      {
+        if (d_skDefs.find(cur) != d_skDefs.end())
+        {
+          skolems.insert(cur);
+        }
+      }
+      else
+      {
+        visit.insert(visit.end(), cur.begin(), cur.end());
+      }
+    }
+  } while (!visit.empty());
+}
+
+}  // namespace prop
+}  // namespace CVC4