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.

2 files changed, 12 insertions, 12 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index b46253851..b0bc70cd7 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -90,24 +90,24 @@ ABVFP|BVFP|FP)
 UFBV)
   # most problems in UFBV are essentially BV
   trywith 600 --full-saturate-quant --decision=internal
-  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
+  trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
 BV)
   trywith 240 --full-saturate-quant
-  trywith 240 --full-saturate-quant --no-cbqi-innermost
-  trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
-  trywith 60 --full-saturate-quant --no-cbqi-bv
-  trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
+  trywith 240 --full-saturate-quant --no-cegqi-innermost
+  trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal
+  trywith 60 --full-saturate-quant --no-cegqi-bv
+  trywith 60 --full-saturate-quant --cegqi-bv-ineq=eq-slack
   # finish 10min
-  finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
+  finishwith --full-saturate-quant --no-cegqi-innermost --global-negate
   ;;
 LIA|LRA|NIA|NRA)
   trywith 60 --full-saturate-quant --nl-ext-tplanes
-  trywith 600 --full-saturate-quant --no-cbqi-innermost
-  trywith 600 --full-saturate-quant --cbqi-nested-qe
-  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  trywith 600 --full-saturate-quant --no-cegqi-innermost
+  trywith 600 --full-saturate-quant --cegqi-nested-qe
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
   trywith 1200 --ite-simp
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 0371d8b42..5e827128e 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -36,10 +36,10 @@ BV)
   finishwith --full-saturate-quant --decision=internal
   ;;
 LIA|LRA)
-  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 NIA|NRA)
-  finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+  finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
   finishwith --decision=justification-stoponly --ite-simp