Make option names related to CEGQI consistent (#4316)

This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.

Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.

The changes were done by these commands in the given directories:

src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done

And a few minor fixes afterwards.

This should be merged close to the time of the next stable release.

1 files changed, 5 insertions, 5 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index dfef0bad4..0c11baecc 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -138,7 +138,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
   // constructors.
   if (!d_usingSymCons)
   {
-    Trace("cegqi-engine") << "  *** Do refinement lemma evaluation"
+    Trace("sygus-engine") << "  *** Do refinement lemma evaluation"
                           << (doGen ? " with conjecture-specific refinement"
                                     : "")
                           << "..." << std::endl;
@@ -168,7 +168,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
       // just check whether the refinement lemmas are satisfied, fail if not
       if (checkRefinementEvalLemmas(candidates, candidate_values))
       {
-        Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
+        Trace("sygus-engine") << "...(actively enumerated) candidate failed "
                                  "refinement lemma evaluation."
                               << std::endl;
         return true;
@@ -179,7 +179,7 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
   bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
   if (doEvalUnfold)
   {
-    Trace("cegqi-engine") << "  *** Do evaluation unfolding..." << std::endl;
+    Trace("sygus-engine") << "  *** Do evaluation unfolding..." << std::endl;
     std::vector<Node> eager_terms, eager_vals, eager_exps;
     for (unsigned i = 0, size = candidates.size(); i < size; ++i)
     {
@@ -627,7 +627,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
                                      const std::vector<Node>& vals,
                                      std::vector<Node>& lems)
 {
-  Trace("cegqi-engine") << "  *** Do sample add refinement..." << std::endl;
+  Trace("sygus-engine") << "  *** Do sample add refinement..." << std::endl;
   if (Trace.isOn("cegis-sample"))
   {
     Trace("cegis-sample") << "Check sampling for candidate solution"
@@ -681,7 +681,7 @@ bool Cegis::sampleAddRefinementLemma(const std::vector<Node>& candidates,
             }
             Trace("cegis-sample") << std::endl;
           }
-          Trace("cegqi-engine") << "  *** Refine by sampling" << std::endl;
+          Trace("sygus-engine") << "  *** Refine by sampling" << std::endl;
           addRefinementLemma(rlem);
           // if trust, we are not interested in sending out refinement lemmas
           if (options::cegisSample() != options::CegisSampleMode::TRUST)