diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-20 19:47:35 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-20 19:47:35 -0500 |
commit | ad7907adff119a6e25fe3c229663afecb15db7c4 (patch) | |
tree | 0cf0c1931db8d4529127806eca03cd014fcb6a42 /contrib/competitions/smt-comp/run-script-smtcomp-current | |
parent | 6255c0356bd78140a9cf075491c1d4608ac27704 (diff) |
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.
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current')
-rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 20 |
1 files changed, 10 insertions, 10 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 |