1 files changed, 128 insertions, 0 deletions
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
new file mode 100644
index 000000000..891c0f731
--- /dev/null
+++ b/src/smt/witness_form.cpp
@@ -0,0 +1,128 @@
+/*********************                                                        */
+/*! \file witness_form.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 The module for managing witness form conversion in proofs
+ **/
+
+#include "smt/witness_form.h"
+
+#include "expr/skolem_manager.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace smt {
+
+WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
+    : d_tcpg(pnm), d_wintroPf(pnm)
+{
+}
+
+std::shared_ptr<ProofNode> WitnessFormGenerator::getProofFor(Node eq)
+{
+  if (eq.getKind() != kind::EQUAL)
+  {
+    // expecting an equality
+    return nullptr;
+  }
+  Node lhs = eq[0];
+  Node rhs = convertToWitnessForm(eq[0]);
+  if (rhs != eq[1])
+  {
+    // expecting witness form
+    return nullptr;
+  }
+  std::shared_ptr<ProofNode> pn = d_tcpg.getProofFor(eq);
+  Assert(pn != nullptr);
+  return pn;
+}
+
+std::string WitnessFormGenerator::identify() const
+{
+  return "WitnessFormGenerator";
+}
+
+Node WitnessFormGenerator::convertToWitnessForm(Node t)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* skm = nm->getSkolemManager();
+  Node tw = SkolemManager::getWitnessForm(t);
+  if (t == tw)
+  {
+    // trivial case
+    return tw;
+  }
+  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
+  std::vector<TNode> visit;
+  TNode cur;
+  TNode curw;
+  visit.push_back(t);
+  do
+  {
+    cur = visit.back();
+    visit.pop_back();
+    it = d_visited.find(cur);
+    if (it == d_visited.end())
+    {
+      d_visited.insert(cur);
+      curw = SkolemManager::getWitnessForm(cur);
+      // if its witness form is different
+      if (cur != curw)
+      {
+        if (cur.isVar())
+        {
+          Node eq = cur.eqNode(curw);
+          // equality between a variable and its witness form
+          d_eqs.insert(eq);
+          Assert(curw.getKind() == kind::WITNESS);
+          Node skBody = SkolemManager::getSkolemForm(curw[1]);
+          Node exists = nm->mkNode(kind::EXISTS, curw[0], skBody);
+          ProofGenerator* pg = skm->getProofGenerator(exists);
+          // --------------------------- from pg
+          // (exists ((x T)) (P x))
+          // --------------------------- WITNESS_INTRO
+          // k = (witness ((x T)) (P x))
+          d_wintroPf.addLazyStep(exists, pg, false, PfRule::WITNESS_AXIOM);
+          d_wintroPf.addStep(eq, PfRule::WITNESS_INTRO, {exists}, {});
+          d_tcpg.addRewriteStep(cur, curw, &d_wintroPf);
+        }
+        else
+        {
+          // A term whose witness form is different from itself, recurse.
+          // It should be the case that cur has children, since the witness
+          // form of constants are themselves.
+          Assert(cur.getNumChildren() > 0);
+          visit.insert(visit.end(), cur.begin(), cur.end());
+        }
+      }
+    }
+  } while (!visit.empty());
+  return tw;
+}
+
+bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const
+{
+  return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s);
+}
+
+bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
+{
+  Node tr = theory::Rewriter::rewrite(t);
+  return !tr.isConst() || !tr.getConst<bool>();
+}
+
+const std::unordered_set<Node, NodeHashFunction>&
+WitnessFormGenerator::getWitnessFormEqs() const
+{
+  return d_eqs;
+}
+
+}  // namespace smt
+}  // namespace CVC4