(proof-new) Clean up uses of witness with skolem lemmas (#6109)

This ensures we do not return WITNESS terms in response to ppRewrite. This makes standard utility methods in SkolemLemma to help make this easy.

It also removes TheorySetsPrivate::expandDefinitions, which was returning WITNESS in response to expandDefinitions, which is no longer permitted.

8 files changed, 83 insertions, 47 deletions

diff --git a/src/theory/arith/operator_elim.cpp b/src/theory/arith/operator_elim.cpp
index 100116fd7..ab01960dd 100644
--- a/src/theory/arith/operator_elim.cpp
+++ b/src/theory/arith/operator_elim.cpp
@@ -481,18 +481,16 @@ Node OperatorElim::mkWitnessTerm(Node v,
   // we mark that we should send a lemma
   Node k =
       sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this);
-  TNode tv = v;
-  TNode tk = k;
-  Node lem = pred.substitute(tv, tk);
   if (d_pnm != nullptr)
   {
+    Node lem = SkolemLemma::getSkolemLemmaFor(k);
     TrustNode tlem =
         mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
     lems.push_back(SkolemLemma(tlem, k));
   }
   else
   {
-    lems.push_back(SkolemLemma(TrustNode::mkTrustLemma(lem), k));
+    lems.push_back(SkolemLemma(k, nullptr));
   }
   return k;
 }
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index ee23aae49..f3ad57535 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -132,7 +132,8 @@ void TheorySets::preRegisterTerm(TNode node)
 
 TrustNode TheorySets::expandDefinition(Node n)
 {
-  return d_internal->expandDefinition(n);
+  // we currently do not expand any set operators
+  return TrustNode::null();
 }
 
 TrustNode TheorySets::ppRewrite(TNode n, std::vector<SkolemLemma>& lems)
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index c15ea6f65..da2958c5c 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -20,6 +20,7 @@
 
 #include "expr/emptyset.h"
 #include "expr/node_algorithm.h"
+#include "expr/skolem_manager.h"
 #include "options/sets_options.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/sets/normal_form.h"
@@ -1265,17 +1266,6 @@ void TheorySetsPrivate::preRegisterTerm(TNode node)
   }
 }
 
-TrustNode TheorySetsPrivate::expandDefinition(Node node)
-{
-  Debug("sets-proc") << "expandDefinition : " << node << std::endl;
-
-  if (node.getKind()==kind::CHOOSE)
-  {
-    return expandChooseOperator(node);
-  }
-  return TrustNode::null();
-}
-
 TrustNode TheorySetsPrivate::ppRewrite(Node node,
                                        std::vector<SkolemLemma>& lems)
 {
@@ -1283,24 +1273,17 @@ TrustNode TheorySetsPrivate::ppRewrite(Node node,
 
   switch (node.getKind())
   {
-    case kind::CHOOSE: return expandChooseOperator(node);
+    case kind::CHOOSE: return expandChooseOperator(node, lems);
     case kind::IS_SINGLETON: return expandIsSingletonOperator(node);
     default: return TrustNode::null();
   }
 }
 
-TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node)
+TrustNode TheorySetsPrivate::expandChooseOperator(
+    const Node& node, std::vector<SkolemLemma>& lems)
 {
   Assert(node.getKind() == CHOOSE);
 
-  // we call the rewriter here to handle the pattern (choose (singleton x))
-  // because the rewriter is called after expansion
-  Node rewritten = Rewriter::rewrite(node);
-  if (rewritten.getKind() != CHOOSE)
-  {
-    return TrustNode::mkTrustRewrite(node, rewritten, nullptr);
-  }
-
   // (choose A) is expanded as
   // (witness ((x elementType))
   //    (ite
@@ -1309,7 +1292,7 @@ TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node)
   //      (and (member x A) (= x chooseUf(A)))
 
   NodeManager* nm = NodeManager::currentNM();
-  Node set = rewritten[0];
+  Node set = node[0];
   TypeNode setType = set.getType();
   Node chooseSkolem = getChooseFunction(setType);
   Node apply = NodeManager::currentNM()->mkNode(APPLY_UF, chooseSkolem, set);
@@ -1322,9 +1305,10 @@ TrustNode TheorySetsPrivate::expandChooseOperator(const Node& node)
   Node member = nm->mkNode(MEMBER, witnessVariable, set);
   Node memberAndEqual = member.andNode(equal);
   Node ite = nm->mkNode(ITE, isEmpty, equal, memberAndEqual);
-  Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable);
-  Node witness = nm->mkNode(WITNESS, witnessVariables, ite);
-  return TrustNode::mkTrustRewrite(node, witness, nullptr);
+  SkolemManager* sm = nm->getSkolemManager();
+  Node ret = sm->mkSkolem(witnessVariable, ite, "kSetChoose");
+  lems.push_back(SkolemLemma(ret, nullptr));
+  return TrustNode::mkTrustRewrite(node, ret, nullptr);
 }
 
 TrustNode TheorySetsPrivate::expandIsSingletonOperator(const Node& node)
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 262a4c572..329fbfc17 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -167,8 +167,6 @@ class TheorySetsPrivate {
 
   void preRegisterTerm(TNode node);
 
-  /** ppRewrite, which expands choose.  */
-  TrustNode expandDefinition(Node n);
   /** ppRewrite, which expands choose and is_singleton.  */
   TrustNode ppRewrite(Node n, std::vector<SkolemLemma>& lems);
 
@@ -204,7 +202,8 @@ class TheorySetsPrivate {
    */
   Node getChooseFunction(const TypeNode& setType);
   /** expand the definition of the choose operator */
-  TrustNode expandChooseOperator(const Node& node);
+  TrustNode expandChooseOperator(const Node& node,
+                                 std::vector<SkolemLemma>& lems);
   /** expand the definition of is_singleton operator */
   TrustNode expandIsSingletonOperator(const Node& node);
   /** subtheory solver for the theory of relations */
diff --git a/src/theory/skolem_lemma.cpp b/src/theory/skolem_lemma.cpp
new file mode 100644
index 000000000..7c8f00dd7
--- /dev/null
+++ b/src/theory/skolem_lemma.cpp
@@ -0,0 +1,43 @@
+/*********************                                                        */
+/*! \file skolem_lemma.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 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 skolem lemma utility
+ **/
+
+#include "theory/skolem_lemma.h"
+
+#include "expr/skolem_manager.h"
+
+namespace CVC4 {
+namespace theory {
+
+SkolemLemma::SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k)
+{
+  Assert(lem.getKind() == TrustNodeKind::LEMMA);
+}
+
+SkolemLemma::SkolemLemma(Node k, ProofGenerator* pg) : d_lemma(), d_skolem(k)
+{
+  Node lem = getSkolemLemmaFor(k);
+  d_lemma = TrustNode::mkTrustLemma(lem, pg);
+}
+
+Node SkolemLemma::getSkolemLemmaFor(Node k)
+{
+  Node w = SkolemManager::getWitnessForm(k);
+  Assert(w.getKind() == kind::WITNESS);
+  TNode tx = w[0][0];
+  TNode tk = k;
+  return w[1].substitute(tx, tk);
+}
+
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/skolem_lemma.h b/src/theory/skolem_lemma.h
index a44d5a30d..c669b527d 100644
--- a/src/theory/skolem_lemma.h
+++ b/src/theory/skolem_lemma.h
@@ -36,14 +36,26 @@ namespace theory {
 class SkolemLemma
 {
  public:
-  SkolemLemma(TrustNode lem, Node k) : d_lemma(lem), d_skolem(k)
-  {
-    Assert(lem.getKind() == TrustNodeKind::LEMMA);
-  }
+  /**
+   * Make skolem from trust node lem of kind LEMMA and skolem k.
+   */
+  SkolemLemma(TrustNode lem, Node k);
+  /**
+   * Make skolem lemma from witness form of skolem k. If non-null, pg is
+   * proof generator that can generator a proof for getSkolemLemmaFor(k).
+   */
+  SkolemLemma(Node k, ProofGenerator* pg);
+
   /** The lemma, a trust node of kind LEMMA */
   TrustNode d_lemma;
   /** The skolem associated with that lemma */
   Node d_skolem;
+
+  /**
+   * Get the lemma for skolem k based on its witness form. If k has witness
+   * form (witness ((x T)) (P x)), this is the formula (P k).
+   */
+  static Node getSkolemLemmaFor(Node k);
 };
 
 }  // namespace theory
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 7f838e411..fbede89f0 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -998,15 +998,13 @@ TrustNode TheoryStrings::ppRewrite(TNode atom, std::vector<SkolemLemma>& lems)
     Node card = nm->mkConst(Rational(utils::getAlphabetCardinality()));
     Node cond =
         nm->mkNode(AND, nm->mkNode(LEQ, d_zero, t), nm->mkNode(LT, t, card));
-    Node k = nm->mkBoundVar(nm->stringType());
-    Node bvl = nm->mkNode(BOUND_VAR_LIST, k);
+    Node v = nm->mkBoundVar(nm->stringType());
     Node emp = Word::mkEmptyWord(atom.getType());
-    // TODO: use skolem manager
-    Node ret = nm->mkNode(
-        WITNESS,
-        bvl,
-        nm->mkNode(
-            ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, k)), k.eqNode(emp)));
+    Node pred = nm->mkNode(
+        ITE, cond, t.eqNode(nm->mkNode(STRING_TO_CODE, v)), v.eqNode(emp));
+    SkolemManager* sm = nm->getSkolemManager();
+    Node ret = sm->mkSkolem(v, pred, "kFromCode");
+    lems.push_back(SkolemLemma(ret, nullptr));
     return TrustNode::mkTrustRewrite(atom, ret, nullptr);
   }
   TrustNode ret;
diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index ea4b0f82f..a9e16f48f 100644
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -204,13 +204,14 @@ TrustNode TheoryPreprocessor::preprocessLemmaInternal(
   {
     Assert(d_lp != nullptr);
     // add the original proof to the lazy proof
-    d_lp->addLazyStep(node.getProven(), node.getGenerator());
+    d_lp->addLazyStep(
+        node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA);
     // only need to do anything if lemmap changed in a non-trivial way
     if (!CDProof::isSame(lemmap, lemma))
     {
       d_lp->addLazyStep(tplemma.getProven(),
                         tplemma.getGenerator(),
-                        PfRule::PREPROCESS_LEMMA,
+                        PfRule::THEORY_PREPROCESS,
                         true,
                         "TheoryEngine::lemma_pp");
       // ---------- from node -------------- from theory preprocess