Make option names related to CEGQI consistent (#4316)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 21 Apr 2020 00:47:35 +0000 (19:47 -0500)
committerGitHub <noreply@github.com>
Tue, 21 Apr 2020 00:47:35 +0000 (19:47 -0500)
commitad7907adff119a6e25fe3c229663afecb15db7c4
tree0cf0c1931db8d4529127806eca03cd014fcb6a42
parent6255c0356bd78140a9cf075491c1d4608ac27704
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.
133 files changed:
contrib/competitions/smt-comp/run-script-smtcomp-current
contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
src/options/didyoumean_test.cpp
src/options/quantifiers_options.toml
src/preprocessing/passes/global_negate.cpp
src/smt/set_defaults.cpp
src/theory/datatypes/sygus_extension.cpp
src/theory/quantifiers/bv_inverter.cpp
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp
src/theory/quantifiers/cegqi/ceg_instantiator.cpp
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
src/theory/quantifiers/ematching/candidate_generator.cpp
src/theory/quantifiers/ematching/inst_match_generator.cpp
src/theory/quantifiers/equality_query.cpp
src/theory/quantifiers/inst_strategy_enumerative.cpp
src/theory/quantifiers/instantiate.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp
src/theory/quantifiers/sygus/cegis.cpp
src/theory/quantifiers/sygus/sygus_enumerator.cpp
src/theory/quantifiers/sygus/sygus_repair_const.cpp
src/theory/quantifiers/sygus/synth_conjecture.cpp
src/theory/quantifiers/sygus/synth_engine.cpp
src/theory/quantifiers_engine.cpp
test/regress/regress0/expect/scrub.08.sy
test/regress/regress0/quantifiers/ari056.smt2
test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2
test/regress/regress0/quantifiers/issue4086-infs.smt2
test/regress/regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
test/regress/regress0/quantifiers/mix-complete-strat.smt2
test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
test/regress/regress0/quantifiers/qbv-inequality2.smt2
test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
test/regress/regress0/quantifiers/qbv-simp.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
test/regress/regress0/sygus/General_plus10.sy
test/regress/regress0/sygus/aig-si.sy
test/regress/regress0/sygus/c100.sy
test/regress/regress0/sygus/check-generic-red.sy
test/regress/regress0/sygus/const-var-test.sy
test/regress/regress0/sygus/hd-05-d1-prog-nogrammar.sy
test/regress/regress0/sygus/let-ringer.sy
test/regress/regress0/sygus/let-simp.sy
test/regress/regress0/sygus/parity-AIG-d0.sy
test/regress/regress0/sygus/pbe-pred-contra.sy
test/regress/regress1/bug519.smt2
test/regress/regress1/quantifiers/NUM878.smt2
test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
test/regress/regress1/quantifiers/anti-sk-simp.smt2
test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2
test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
test/regress/regress1/quantifiers/extract-nproc.smt2
test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
test/regress/regress1/quantifiers/issue4243-prereg-inc.smt2
test/regress/regress1/quantifiers/lra-vts-inf.smt2
test/regress/regress1/quantifiers/model_6_1_bv.smt2
test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
test/regress/regress1/quantifiers/nl-pow-trick.smt2
test/regress/regress1/quantifiers/nra-interleave-inst.smt2
test/regress/regress1/quantifiers/psyco-107-bv.smt2
test/regress/regress1/quantifiers/qbv-disequality3.smt2
test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2
test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2
test/regress/regress1/sygus/Base16_1.sy
test/regress/regress1/sygus/array_search_2.sy
test/regress/regress1/sygus/array_search_5-Q-easy.sy
test/regress/regress1/sygus/array_sum_2_5.sy
test/regress/regress1/sygus/clock-inc-tuple.sy
test/regress/regress1/sygus/crcy-si-rcons.sy
test/regress/regress1/sygus/dt-test-ns.sy
test/regress/regress1/sygus/dup-op.sy
test/regress/regress1/sygus/enum-test.sy
test/regress/regress1/sygus/error1-dt.sy
test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy
test/regress/regress1/sygus/hd-sdiv.sy
test/regress/regress1/sygus/int-any-const.sy
test/regress/regress1/sygus/large-const-simp.sy
test/regress/regress1/sygus/list-head-x.sy
test/regress/regress1/sygus/max.sy
test/regress/regress1/sygus/nia-max-square-ns.sy
test/regress/regress1/sygus/parity-si-rcons.sy
test/regress/regress1/sygus/phone-1-long.sy
test/regress/regress1/sygus/process-10-vars.sy
test/regress/regress1/sygus/qe.sy
test/regress/regress1/sygus/real-any-const.sy
test/regress/regress1/sygus/real-grammar.sy
test/regress/regress1/sygus/repair-const-rl.sy
test/regress/regress1/sygus/strings-any-term1.sy
test/regress/regress1/sygus/tl-type-0.sy
test/regress/regress1/sygus/tl-type-4x.sy
test/regress/regress1/sygus/tl-type.sy
test/regress/regress1/sygus/twolets1.sy
test/regress/regress1/sygus/twolets2-orig.sy
test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2
test/regress/regress2/sygus/lustre-real.sy
test/regress/regress2/sygus/process-10-vars-2fun.sy
test/regress/regress2/sygus/process-arg-invariance.sy
test/regress/regress2/sygus/real-grammar-neg.sy
test/regress/regress3/strings-any-term.sy
test/unit/theory/theory_quantifiers_bv_inverter_white.h