From 0ae9a3cfd78bc2d0b8a603a21f2181038fab4880 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 28 Sep 2020 18:33:03 -0500
Subject: [PATCH] Minor fixes to quantifiers proofs (#5151)

Includes minor changes to the proof checker and a fix in the instantiate module.
---
 src/expr/proof_rule.h                    | 14 +++++++-------
 src/theory/quantifiers/instantiate.cpp   |  2 +-
 src/theory/quantifiers/proof_checker.cpp | 22 ++++++++++++++--------
 3 files changed, 22 insertions(+), 16 deletions(-)

diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index c621bffdc..9324f68c2 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -563,7 +563,7 @@ enum class PfRule : uint32_t
   // Conclusion: (= F true)
   TRUE_INTRO,
   // ======== True elim
-  // Children: (P:(= F true)
+  // Children: (P:(= F true))
   // Arguments: none
   // ----------------------------------------
   // Conclusion: F
@@ -575,7 +575,7 @@ enum class PfRule : uint32_t
   // Conclusion: (= F false)
   FALSE_INTRO,
   // ======== False elim
-  // Children: (P:(= F false)
+  // Children: (P:(= F false))
   // Arguments: none
   // ----------------------------------------
   // Conclusion: (not F)
@@ -630,11 +630,11 @@ enum class PfRule : uint32_t
 
   //================================================= Quantifiers rules
   // ======== Witness intro
-  // Children: (P:F[t])
-  // Arguments: (t)
+  // Children: (P:(exists ((x T)) F[x]))
+  // Arguments: none
   // ----------------------------------------
-  // Conclusion: (= t (witness ((x T)) F[x]))
-  // where x is a BOUND_VARIABLE unique to the pair F,t.
+  // Conclusion: (= k (witness ((x T)) F[x]))
+  // where k is the Skolem form of (witness ((x T)) F[x]).
   WITNESS_INTRO,
   // ======== Exists intro
   // Children: (P:F[t])
@@ -650,7 +650,7 @@ enum class PfRule : uint32_t
   // Conclusion: F*sigma
   // sigma maps x1 ... xn to their representative skolems obtained by
   // SkolemManager::mkSkolemize, returned in the skolems argument of that
-  // method.
+  // method. Alternatively, can use negated forall as a premise.
   SKOLEMIZE,
   // ======== Instantiate
   // Children: (P:(forall ((x1 T1) ... (xn Tn)) F))
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 0abcd98cb..f88c2e7a0 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -272,7 +272,7 @@ bool Instantiate::addInstantiation(
                          "Instantiate::getInstantiation:qpreprocess",
                          false,
                          PfRule::THEORY_PREPROCESS);
-      pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {body});
+      pfTmp->addStep(body, PfRule::EQ_RESOLVE, {orig_body, proven}, {});
     }
   }
   Trace("inst-debug") << "...preprocess to " << body << std::endl;
diff --git a/src/theory/quantifiers/proof_checker.cpp b/src/theory/quantifiers/proof_checker.cpp
index 5ba390591..e2a416120 100644
--- a/src/theory/quantifiers/proof_checker.cpp
+++ b/src/theory/quantifiers/proof_checker.cpp
@@ -36,23 +36,30 @@ Node QuantifiersProofRuleChecker::checkInternal(
     PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
 {
   NodeManager* nm = NodeManager::currentNM();
+  SkolemManager* sm = nm->getSkolemManager();
   // compute what was proven
-  if (id == PfRule::WITNESS_INTRO || id == PfRule::EXISTS_INTRO)
+  if (id == PfRule::EXISTS_INTRO)
   {
     Assert(children.size() == 1);
     Assert(args.size() == 1);
-    SkolemManager* sm = nm->getSkolemManager();
     Node p = children[0];
     Node t = args[0];
-    Node exists = sm->mkExistential(t, p);
-    if (id == PfRule::EXISTS_INTRO)
+    return sm->mkExistential(t, p);
+  }
+  else if (id == PfRule::WITNESS_INTRO)
+  {
+    Assert(children.size() == 1);
+    Assert(args.empty());
+    if (children[0].getKind() != EXISTS || children[0][0].getNumChildren() != 1)
     {
-      return exists;
+      return Node::null();
     }
     std::vector<Node> skolems;
-    sm->mkSkolemize(exists, skolems, "k");
+    sm->mkSkolemize(children[0], skolems, "k");
     Assert(skolems.size() == 1);
-    return skolems[0];
+    Node witness = SkolemManager::getWitnessForm(skolems[0]);
+    Assert(witness.getKind() == WITNESS && witness[0] == children[0][0]);
+    return skolems[0].eqNode(witness);
   }
   else if (id == PfRule::SKOLEMIZE)
   {
@@ -64,7 +71,6 @@ Node QuantifiersProofRuleChecker::checkInternal(
     {
       return Node::null();
     }
-    SkolemManager* sm = nm->getSkolemManager();
     Node exists;
     if (children[0].getKind() == EXISTS)
     {
-- 
2.30.2