Simplify lemma interface (#5819)

This makes it so that TheoryEngine::lemma returns void not LemmaStatus.

Currently, there was only one use of LemmaStatus by theory solvers, which was CEGQI using it as a way of getting the preprocessed form of a lemma. This makes it so that there is an explicit method in Valuation for getting the preprocessed form of a term + its skolems and their definition assertions.

It also simplifies a few things, e.g. Valuation calls are forwarded to PropEngine instead of going through TheoryEngine. It fixes a few issues in TermFormulaRemoval related to getSkolems.

4 files changed, 76 insertions, 17 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index fb43ebe73..28159c229 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -36,6 +36,7 @@
 #include "prop/theory_proxy.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/output_channel.h"
+#include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
@@ -206,7 +207,7 @@ void PropEngine::assertFormula(TNode node) {
   }
 }
 
-Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
+void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
 {
   bool removable = isLemmaPropertyRemovable(p);
 
@@ -261,20 +262,6 @@ Node PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
     }
     d_decisionEngine->addAssertions(assertions, ppLemmasF, ppSkolems);
   }
-
-  // make the return lemma, which the theory engine will use
-  Node retLemma = tplemma.getProven();
-  if (!ppLemmas.empty())
-  {
-    std::vector<Node> lemmas{retLemma};
-    for (const theory::TrustNode& tnl : ppLemmas)
-    {
-      lemmas.push_back(tnl.getProven());
-    }
-    // the returned lemma is the conjunction of all additional lemmas.
-    retLemma = NodeManager::currentNM()->mkNode(kind::AND, lemmas);
-  }
-  return retLemma;
 }
 
 void PropEngine::assertLemmaInternal(theory::TrustNode trn, bool removable)
@@ -441,6 +428,7 @@ Node PropEngine::ensureLiteral(TNode n)
 
 Node PropEngine::getPreprocessedTerm(TNode n)
 {
+  Node rewritten = theory::Rewriter::rewrite(n);
   // must preprocess
   std::vector<theory::TrustNode> newLemmas;
   std::vector<Node> newSkolems;
@@ -453,6 +441,39 @@ Node PropEngine::getPreprocessedTerm(TNode n)
   return tpn.isNull() ? Node(n) : tpn.getNode();
 }
 
+Node PropEngine::getPreprocessedTerm(TNode n,
+                                     std::vector<Node>& skAsserts,
+                                     std::vector<Node>& sks)
+{
+  // get the preprocessed form of the term
+  Node pn = getPreprocessedTerm(n);
+  // initialize the set of skolems and assertions to process
+  std::vector<theory::TrustNode> toProcessAsserts;
+  std::vector<Node> toProcess;
+  d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess);
+  size_t index = 0;
+  // until fixed point is reached
+  while (index < toProcess.size())
+  {
+    theory::TrustNode ka = toProcessAsserts[index];
+    Node k = toProcess[index];
+    index++;
+    if (std::find(sks.begin(), sks.end(), k) != sks.end())
+    {
+      // already added the skolem to the list
+      continue;
+    }
+    // must preprocess lemmas as well
+    Node kap = getPreprocessedTerm(ka.getProven());
+    skAsserts.push_back(kap);
+    sks.push_back(k);
+    // get the skolems in the preprocessed form of the lemma ka
+    d_theoryProxy->getSkolems(kap, toProcessAsserts, toProcess);
+  }
+  // return the preprocessed term
+  return pn;
+}
+
 void PropEngine::push()
 {
   Assert(!d_inCheckSat) << "Sat solver in solve()!";
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 493dbfe01..f7561d945 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -145,9 +145,8 @@ class PropEngine
    *
    * @param trn the trust node storing the formula to assert
    * @param p the properties of the lemma
-   * @return the (preprocessed) lemma
    */
-  Node assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
+  void assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p);
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
@@ -209,6 +208,20 @@ class PropEngine
    * if preprocessing n involves introducing new skolems.
    */
   Node getPreprocessedTerm(TNode n);
+  /**
+   * Same as above, but also compute the skolems in n and in the lemmas
+   * corresponding to their definition.
+   *
+   * Note this will include skolems that occur in the definition lemma
+   * for all skolems in sks. This is run until a fixed point is reached.
+   * For example, if k1 has definition (ite A (= k1 k2) (= k1 x)) where k2 is
+   * another skolem introduced by term formula removal, then calling this
+   * method on (P k1) will include both k1 and k2 in sks, and their definitions
+   * in skAsserts.
+   */
+  Node getPreprocessedTerm(TNode n,
+                           std::vector<Node>& skAsserts,
+                           std::vector<Node>& sks);
 
   /**
    * Push the context level.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index c604c47f7..a6d570bc2 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -194,6 +194,20 @@ theory::TrustNode TheoryProxy::removeItes(
   return rtf.run(node, newLemmas, newSkolems, true);
 }
 
+void TheoryProxy::getSkolems(TNode node,
+                             std::vector<theory::TrustNode>& skAsserts,
+                             std::vector<Node>& sks)
+{
+  RemoveTermFormulas& rtf = d_tpp.getRemoveTermFormulas();
+  std::unordered_set<Node, NodeHashFunction> skolems;
+  rtf.getSkolems(node, skolems);
+  for (const Node& k : skolems)
+  {
+    sks.push_back(k);
+    skAsserts.push_back(rtf.getLemmaForSkolem(k));
+  }
+}
+
 void TheoryProxy::preRegister(Node n) { d_theoryEngine->preRegister(n); }
 
 }/* CVC4::prop namespace */
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 57115d660..ac79cf967 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -118,6 +118,17 @@ class TheoryProxy : public Registrar
   theory::TrustNode removeItes(TNode node,
                                std::vector<theory::TrustNode>& newLemmas,
                                std::vector<Node>& newSkolems);
+  /**
+   * Get the skolems within node and their corresponding definitions, store
+   * them in sks and skAsserts respectively. Note that this method does not
+   * necessary include all of the skolems in skAsserts. In other words, it
+   * collects from node only. To compute all skolems that node depends on
+   * requires calling this method again on each lemma in skAsserts until a
+   * fixed point is reached.
+   */
+  void getSkolems(TNode node,
+                  std::vector<theory::TrustNode>& skAsserts,
+                  std::vector<Node>& sks);
   /** Preregister term */
   void preRegister(Node n) override;