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.

7 files changed, 100 insertions, 77 deletions

diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
index f94fee66b..472dabf68 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
@@ -633,7 +633,7 @@ struct SortBvExtractInterval
 };
 
 void BvInstantiatorPreprocess::registerCounterexampleLemma(
-    std::vector<Node>& lems, std::vector<Node>& ce_vars)
+    Node lem, std::vector<Node>& ceVars, std::vector<Node>& auxLems)
 {
   // new variables
   std::vector<Node> vars;
@@ -647,12 +647,8 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
     // map from terms to bitvector extracts applied to that term
     std::map<Node, std::vector<Node> > extract_map;
     std::unordered_set<TNode, TNodeHashFunction> visited;
-    for (unsigned i = 0, size = lems.size(); i < size; i++)
-    {
-      Trace("cegqi-bv-pp-debug2")
-          << "Register ce lemma # " << i << " : " << lems[i] << std::endl;
-      collectExtracts(lems[i], extract_map, visited);
-    }
+    Trace("cegqi-bv-pp-debug2") << "Register ce lemma " << lem << std::endl;
+    collectExtracts(lem, extract_map, visited);
     for (std::pair<const Node, std::vector<Node> >& es : extract_map)
     {
       // sort based on the extract start position
@@ -721,10 +717,10 @@ void BvInstantiatorPreprocess::registerCounterexampleLemma(
 
     Trace("cegqi-bv-pp") << "Adding " << new_lems.size() << " lemmas..."
                          << std::endl;
-    lems.insert(lems.end(), new_lems.begin(), new_lems.end());
+    auxLems.insert(auxLems.end(), new_lems.begin(), new_lems.end());
     Trace("cegqi-bv-pp") << "Adding " << vars.size() << " variables..."
                          << std::endl;
-    ce_vars.insert(ce_vars.end(), vars.begin(), vars.end());
+    ceVars.insert(ceVars.end(), vars.begin(), vars.end());
   }
 }
 
diff --git a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
index 3ad45d5be..6f6c216f6 100644
--- a/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_bv_instantiator.h
@@ -168,32 +168,32 @@ class BvInstantiatorPreprocess : public InstantiatorPreprocess
   ~BvInstantiatorPreprocess() override {}
   /** register counterexample lemma
    *
-   * This method modifies the contents of lems based on the extract terms
-   * it contains when the option --cbqi-bv-rm-extract is enabled. It introduces
+   * This method adds to auxLems based on the extract terms that lem
+   * contains when the option --cbqi-bv-rm-extract is enabled. It introduces
    * a dummy equality so that segments of terms t under extracts can be solved
    * independently.
    *
-   * For example:
+   * For example, if lem is:
    *   P[ ((extract 7 4) t), ((extract 3 0) t)]
-   *     becomes:
-   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *     then we add:
    *   t = concat( x74, x30 )
-   * where x74 and x30 are fresh variables of type BV_4.
+   * to auxLems, where x74 and x30 are fresh variables of type BV_4, which are
+   * added to ceVars.
    *
-   * Another example:
+   * Another example, for:
    *   P[ ((extract 7 3) t), ((extract 4 0) t)]
-   *     becomes:
-   *   P[((extract 7 4) t), ((extract 3 0) t)] ^
+   *     we add:
    *   t = concat( x75, x44, x30 )
-   * where x75, x44 and x30 are fresh variables of type BV_3, BV_1, and BV_4
-   * respectively.
+   * to auxLems where x75, x44 and x30 are fresh variables of type BV_3, BV_1,
+   * and BV_4 respectively, which are added to ceVars.
    *
-   * Notice we leave the original conjecture alone. This is done for performance
+   * Notice we leave the original lem alone. This is done for performance
    * since the added equalities ensure we are able to construct the proper
    * solved forms for variables in t and for the intermediate variables above.
    */
-  void registerCounterexampleLemma(std::vector<Node>& lems,
-                                   std::vector<Node>& ce_vars) override;
+  void registerCounterexampleLemma(Node lem,
+                                   std::vector<Node>& ceVars,
+                                   std::vector<Node>& auxLems) override;
 
  private:
   /** collect extracts
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 186024219..95a4037fc 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -21,7 +21,6 @@
 
 #include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
-#include "smt/term_formula_removal.h"
 #include "theory/arith/arith_msum.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
 #include "theory/quantifiers/first_order_model.h"
@@ -1571,18 +1570,21 @@ void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited )
   }
 }
 
-void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
+void CegInstantiator::registerCounterexampleLemma(Node lem,
+                                                  std::vector<Node>& ceVars,
+                                                  std::vector<Node>& auxLems)
+{
   Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl;
   d_input_vars.clear();
-  d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
+  d_input_vars.insert(d_input_vars.end(), ceVars.begin(), ceVars.end());
 
   //Assert( d_vars.empty() );
   d_vars.clear();
   registerTheoryId(THEORY_UF);
-  for (unsigned i = 0; i < ce_vars.size(); i++)
+  for (const Node& cv : ceVars)
   {
-    Trace("cegqi-reg") << "  register input variable : " << ce_vars[i] << std::endl;
-    registerVariable(ce_vars[i]);
+    Trace("cegqi-reg") << "  register input variable : " << cv << std::endl;
+    registerVariable(cv);
   }
 
   // preprocess with all relevant instantiator preprocessors
@@ -1592,7 +1594,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
   for (std::pair<const TheoryId, InstantiatorPreprocess*>& p : d_tipp)
   {
-    p.second->registerCounterexampleLemma(lems, pvars);
+    p.second->registerCounterexampleLemma(lem, pvars, auxLems);
   }
   // must register variables generated by preprocessors
   Trace("cegqi-debug") << "Register variables from theory-specific methods "
@@ -1600,28 +1602,43 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
                       << std::endl;
   for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
   {
-    Trace("cegqi-reg") << "  register theory preprocess variable : " << pvars[i]
-                      << std::endl;
+    Trace("cegqi-reg") << "  register inst preprocess variable : " << pvars[i]
+                       << std::endl;
     registerVariable(pvars[i]);
   }
 
-  //remove ITEs
-  IteSkolemMap iteSkolemMap;
-  d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
-  for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
-    Trace("cegqi-reg") << "  register aux variable : " << i->first << std::endl;
-    registerVariable(i->first);
-  }
-  for( unsigned i=0; i<lems.size(); i++ ){
-    Trace("cegqi-debug") << "Counterexample lemma (pre-rewrite)  " << i << " : " << lems[i] << std::endl;
-    Node rlem = lems[i];
-    rlem = Rewriter::rewrite( rlem );
-    // also must preprocess to ensure that the counterexample atoms we
-    // collect below are identical to the atoms that we add to the CNF stream
-    rlem = d_qe->getTheoryEngine()->preprocess(rlem);
-    Trace("cegqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
-    lems[i] = rlem;
+  // register variables that were introduced during TheoryEngine preprocessing
+  std::unordered_set<Node, NodeHashFunction> ceSyms;
+  expr::getSymbols(lem, ceSyms);
+  std::unordered_set<Node, NodeHashFunction> qSyms;
+  expr::getSymbols(d_quant, qSyms);
+  // all variables that are in counterexample lemma but not in quantified
+  // formula
+  for (const Node& ces : ceSyms)
+  {
+    if (qSyms.find(ces) != qSyms.end())
+    {
+      // a free symbol of the quantified formula.
+      continue;
+    }
+    if (std::find(d_vars.begin(), d_vars.end(), ces) != d_vars.end())
+    {
+      // already processed variable
+      continue;
+    }
+    if (ces.getType().isBoolean())
+    {
+      // Boolean variables, including the counterexample literal, don't matter
+      // since they are always assigned a model value.
+      continue;
+    }
+    Trace("cegqi-reg") << "  register theory preprocess variable : " << ces
+                       << std::endl;
+    // register the variable, which was introduced by TheoryEngine's preprocess
+    // method, e.g. an ITE skolem.
+    registerVariable(ces);
   }
+
   // determine variable order: must do Reals before Ints
   Trace("cegqi-debug") << "Determine variable order..." << std::endl;
   if (!d_vars.empty())
@@ -1673,8 +1690,10 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
   // the original body
   d_is_nested_quant = false;
   std::map< Node, bool > visited;
-  for( unsigned i=0; i<lems.size(); i++ ){
-    collectCeAtoms( lems[i], visited );
+  collectCeAtoms(lem, visited);
+  for (const Node& alem : auxLems)
+  {
+    collectCeAtoms(alem, visited);
   }
 }
 
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.h b/src/theory/quantifiers/cegqi/ceg_instantiator.h
index 7351e60f0..08f7a1262 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.h
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.h
@@ -224,21 +224,20 @@ class CegInstantiator {
   void presolve(Node q);
   /** Register the counterexample lemma
    *
-   * lems : contains the conjuncts of the counterexample lemma of the
-   *        quantified formula we are processing. The counterexample
-   *        lemma is the formula { ~phi[e/x] } in Figure 1 of Reynolds
-   *        et al. FMSD 2017.
-   * ce_vars : contains the variables e. Notice these are variables of
-   *           INST_CONSTANT kind, since we do not permit bound
-   *           variables in assertions.
-   *
-   * This method may modify the set of lemmas lems based on:
-   * - ITE removal,
-   * - Theory-specific preprocessing of instantiation lemmas.
-   * It may also introduce new variables to ce_vars if necessary.
-   */
-  void registerCounterexampleLemma(std::vector<Node>& lems,
-                                   std::vector<Node>& ce_vars);
+   * @param lem contains the counterexample lemma of the quantified formula we
+   * are processing. The counterexample lemma is the formula { ~phi[e/x] } in
+   * Figure 1 of Reynolds et al. FMSD 2017.
+   * @param ce_vars contains the variables e. Notice these are variables of
+   * INST_CONSTANT kind, since we do not permit bound variables in assertions.
+   * This method may add additional variables to this vector if it decides there
+   * are additional auxiliary variables to solve for.
+   * @param auxLems : if this method decides that additional lemmas should be
+   * sent on the output channel, they are added to this vector, and sent out by
+   * the caller of this method.
+   */
+  void registerCounterexampleLemma(Node lem,
+                                   std::vector<Node>& ce_vars,
+                                   std::vector<Node>& auxLems);
   //------------------------------interface for instantiators
   /** get quantifiers engine */
   QuantifiersEngine* getQuantifiersEngine() { return d_qe; }
@@ -829,8 +828,9 @@ class InstantiatorPreprocess
    * of counterexample lemmas, with the same contract as
    * CegInstantiation::registerCounterexampleLemma.
    */
-  virtual void registerCounterexampleLemma(std::vector<Node>& lems,
-                                           std::vector<Node>& ce_vars)
+  virtual void registerCounterexampleLemma(Node lem,
+                                           std::vector<Node>& ceVars,
+                                           std::vector<Node>& auxLems)
   {
   }
 };
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 208eb0bf8..8693f97f4 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -593,15 +593,18 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem)
   {
     ce_vars.push_back(tutil->getInstantiationConstant(q, i));
   }
-  std::vector<Node> lems;
-  lems.push_back(lem);
   CegInstantiator* cinst = getInstantiator(q);
-  cinst->registerCounterexampleLemma(lems, ce_vars);
-  for (unsigned i = 0, size = lems.size(); i < size; i++)
+  LemmaStatus status = d_quantEngine->getOutputChannel().lemma(lem);
+  Node ppLem = status.getRewrittenLemma();
+  Trace("cegqi-debug") << "Counterexample lemma (post-preprocess): " << ppLem
+                       << std::endl;
+  std::vector<Node> auxLems;
+  cinst->registerCounterexampleLemma(ppLem, ce_vars, auxLems);
+  for (unsigned i = 0, size = auxLems.size(); i < size; i++)
   {
-    Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
-                        << std::endl;
-    d_quantEngine->addLemma(lems[i], false);
+    Trace("cegqi-debug") << "Auxiliary CE lemma " << i << " : " << auxLems[i]
+                         << std::endl;
+    d_quantEngine->addLemma(auxLems[i], false);
   }
 }
 
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) {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 9c631ca60..233047321 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -890,8 +890,6 @@ public:
 
   theory::eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; }
 
-  RemoveTermFormulas* getTermFormulaRemover() { return &d_tform_remover; }
-
   SortInference* getSortInference() { return &d_sortInfer; }
 
   /** Prints the assertions to the debug stream */