Update CEGQI to use lemma status instead of forcing preprocess (#4551)

This PR removes a hack in counterexample-guided quantifier instantiation.

The issue is the CEGQI needs to know the form of certain lemmas, after theory preprocessing. CEGQI needs to know this since it must construct solutions (e.g. solved form of equalities) for free variables in these lemmas, which includes fresh variables in the lemma after postprocess like ITE skolems.

Previously, CEGQI was hacked so that it applied the preprocessing eagerly so that it had full knowledge of the postprocessed lemma. This PR updates CEGQI so that it uses the returned LemmaStatus as the way of getting the lemma after postprocess. It also fixes the lemma status returned by TheoryEngine so that all lemmas not just the "main lemma" are returned as a conjunction.

This PR is in preparation for major refactoring to theory preprocessing for the sake of proofs.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2c27c6054..71c144daa 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1931,7 +1931,14 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
 
   // Lemma analysis isn't online yet; this lemma may only live for this
   // user level.
-  return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
+  Node retLemma = additionalLemmas[0];
+  if (additionalLemmas.size() > 1)
+  {
+    // the returned lemma is the conjunction of all additional lemmas.
+    retLemma =
+        NodeManager::currentNM()->mkNode(kind::AND, additionalLemmas.ref());
+  }
+  return theory::LemmaStatus(retLemma, d_userContext->getLevel());
 }
 
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {