From ad7907adff119a6e25fe3c229663afecb15db7c4 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 20 Apr 2020 19:47:35 -0500 Subject: 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. --- .../competitions/smt-comp/run-script-smtcomp-current | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current') 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 -- cgit v1.2.3