(proof-new) Rename ProofSkolemCache to SkolemManager (#4556)

This PR changes the design of ProofSkolemCache so that it has facilities for tracking proofs. This is required so that the term formula removal pass can be made proof-producing.

This makes it so that ProofSkolemCache is renamed to SkolemManager, which lives in NodeManager. Creating (most) skolems must be accompanied by a corresponding ProofGenerator that can provide the proof for the existential corresponding to their witness form.

Further updates will include refactoring the mkSkolemExists method of SkolemManager so that its contract wrt proofs is simpler.

Once all calls to mkSkolem go through the standard interface, then NodeManager::mkSkolem will be moved to SkolemManager::mkSkolemInternal.

1 files changed, 264 insertions, 0 deletions

diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
new file mode 100644
index 000000000..0570af687
--- /dev/null
+++ b/src/expr/skolem_manager.cpp
@@ -0,0 +1,264 @@
+/*********************                                                        */
+/*! \file skolem_manager.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Implementation of skolem manager class
+ **/
+
+#include "expr/skolem_manager.h"
+
+#include "expr/attribute.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+
+struct WitnessFormAttributeId
+{
+};
+typedef expr::Attribute<WitnessFormAttributeId, Node> WitnessFormAttribute;
+
+struct SkolemFormAttributeId
+{
+};
+typedef expr::Attribute<SkolemFormAttributeId, Node> SkolemFormAttribute;
+
+struct PurifySkolemAttributeId
+{
+};
+typedef expr::Attribute<PurifySkolemAttributeId, Node> PurifySkolemAttribute;
+
+Node SkolemManager::mkSkolem(Node v,
+                             Node pred,
+                             const std::string& prefix,
+                             const std::string& comment,
+                             int flags,
+                             ProofGenerator* pg)
+{
+  Assert(v.getKind() == BOUND_VARIABLE);
+  // make the witness term
+  NodeManager* nm = NodeManager::currentNM();
+  Node bvl = nm->mkNode(BOUND_VAR_LIST, v);
+  // translate pred to witness form, since pred itself may contain skolem
+  Node predw = getWitnessForm(pred);
+  // make the witness term, which should not contain any skolem
+  Node w = nm->mkNode(WITNESS, bvl, predw);
+  // store the mapping to proof generator
+  d_gens[w] = pg;
+  return getOrMakeSkolem(w, prefix, comment, flags);
+}
+
+Node SkolemManager::mkSkolemExists(Node v,
+                                   Node q,
+                                   const std::string& prefix,
+                                   const std::string& comment,
+                                   int flags,
+                                   ProofGenerator* pg)
+{
+  Assert(q.getKind() == EXISTS);
+  bool foundVar = false;
+  std::vector<Node> ovars;
+  for (const Node& av : q[0])
+  {
+    if (av == v)
+    {
+      foundVar = true;
+      continue;
+    }
+    ovars.push_back(av);
+  }
+  if (!foundVar)
+  {
+    Assert(false);
+    return Node::null();
+  }
+  Node pred = q[1];
+  if (!ovars.empty())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    Node bvl = nm->mkNode(BOUND_VAR_LIST, ovars);
+    pred = nm->mkNode(EXISTS, bvl, pred);
+  }
+  return mkSkolem(v, pred, prefix, comment, flags, pg);
+}
+
+Node SkolemManager::mkPurifySkolem(Node t,
+                                   const std::string& prefix,
+                                   const std::string& comment,
+                                   int flags)
+{
+  PurifySkolemAttribute psa;
+  if (t.hasAttribute(psa))
+  {
+    return t.getAttribute(psa);
+  }
+  // The case where t is a witness term is special: we set its Skolem attribute
+  // directly.
+  if (t.getKind() == WITNESS)
+  {
+    return getOrMakeSkolem(t, prefix, comment, flags);
+  }
+  Node v = NodeManager::currentNM()->mkBoundVar(t.getType());
+  Node k = mkSkolem(v, v.eqNode(t), prefix, comment, flags);
+  t.setAttribute(psa, k);
+  return k;
+}
+
+ProofGenerator* SkolemManager::getProofGenerator(Node t)
+{
+  std::map<Node, ProofGenerator*>::iterator it = d_gens.find(t);
+  if (it != d_gens.end())
+  {
+    return it->second;
+  }
+  return nullptr;
+}
+
+Node SkolemManager::getWitnessForm(Node n) { return convertInternal(n, true); }
+
+Node SkolemManager::getSkolemForm(Node n) { return convertInternal(n, false); }
+
+Node SkolemManager::convertInternal(Node n, bool toWitness)
+{
+  if (n.isNull())
+  {
+    return n;
+  }
+  Trace("pf-skolem-debug") << "SkolemManager::convertInternal: " << toWitness
+                           << " " << n << std::endl;
+  WitnessFormAttribute wfa;
+  SkolemFormAttribute sfa;
+  NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
+  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  visit.push_back(n);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = visited.find(cur);
+
+    if (it == visited.end())
+    {
+      if (toWitness && cur.hasAttribute(wfa))
+      {
+        visited[cur] = cur.getAttribute(wfa);
+      }
+      else if (!toWitness && cur.hasAttribute(sfa))
+      {
+        visited[cur] = cur.getAttribute(sfa);
+      }
+      else
+      {
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        if (cur.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          visit.push_back(cur.getOperator());
+        }
+        for (const Node& cn : cur)
+        {
+          visit.push_back(cn);
+        }
+      }
+    }
+    else if (it->second.isNull())
+    {
+      Node ret = cur;
+      bool childChanged = false;
+      std::vector<Node> children;
+      if (cur.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        it = visited.find(cur.getOperator());
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cur.getOperator() != it->second;
+        children.push_back(it->second);
+      }
+      for (const Node& cn : cur)
+      {
+        it = visited.find(cn);
+        Assert(it != visited.end());
+        Assert(!it->second.isNull());
+        childChanged = childChanged || cn != it->second;
+        children.push_back(it->second);
+      }
+      if (childChanged)
+      {
+        ret = nm->mkNode(cur.getKind(), children);
+      }
+      if (toWitness)
+      {
+        cur.setAttribute(wfa, ret);
+      }
+      else
+      {
+        // notice that WITNESS terms t may be assigned a skolem form that is
+        // of kind WITNESS here, if t contains a free variable. This is due to
+        // the fact that witness terms in the bodies of quantified formulas are
+        // not eliminated and thus may appear in places where getSkolemForm is
+        // called on them. Regardless, witness terms with free variables
+        // should never be themselves assigned skolems (otherwise we would have
+        // assertions with free variables), and thus they can be treated like
+        // ordinary terms here.
+        cur.setAttribute(sfa, ret);
+      }
+      visited[cur] = ret;
+    }
+  } while (!visit.empty());
+  Assert(visited.find(n) != visited.end());
+  Assert(!visited.find(n)->second.isNull());
+  Trace("pf-skolem-debug") << "..return " << visited[n] << std::endl;
+  return visited[n];
+}
+
+void SkolemManager::convertToWitnessFormVec(std::vector<Node>& vec)
+{
+  for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
+  {
+    vec[i] = getWitnessForm(vec[i]);
+  }
+}
+void SkolemManager::convertToSkolemFormVec(std::vector<Node>& vec)
+{
+  for (unsigned i = 0, nvec = vec.size(); i < nvec; i++)
+  {
+    vec[i] = getSkolemForm(vec[i]);
+  }
+}
+
+Node SkolemManager::getOrMakeSkolem(Node w,
+                                    const std::string& prefix,
+                                    const std::string& comment,
+                                    int flags)
+{
+  Assert(w.getKind() == WITNESS);
+  SkolemFormAttribute sfa;
+  // could already have a skolem if we used w already
+  if (w.hasAttribute(sfa))
+  {
+    return w.getAttribute(sfa);
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  // make the new skolem
+  Node k = nm->mkSkolem(prefix, w.getType(), comment, flags);
+  // set witness form attribute for k
+  WitnessFormAttribute wfa;
+  k.setAttribute(wfa, w);
+  // set skolem form attribute for w
+  w.setAttribute(sfa, k);
+  Trace("pf-skolem") << "SkolemManager::mkSkolem: " << k << " : " << w
+                     << std::endl;
+  return k;
+}
+
+}  // namespace CVC4