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 /test/regress/regress2 | |
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 'test/regress/regress2')
5 files changed, 5 insertions, 5 deletions
diff --git a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 index c26cde173..72743693a 100644 --- a/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 +++ b/test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --cbqi-all --no-check-models +; COMMAND-LINE: --cegqi-all --no-check-models ; EXPECT: sat ;AJR:BROKEN (set-logic UFBV) diff --git a/test/regress/regress2/sygus/lustre-real.sy b/test/regress/regress2/sygus/lustre-real.sy index 99d682bcc..b7637567f 100644 --- a/test/regress/regress2/sygus/lustre-real.sy +++ b/test/regress/regress2/sygus/lustre-real.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status (set-logic LIRA) (define-fun __node_init_top_0 ( diff --git a/test/regress/regress2/sygus/process-10-vars-2fun.sy b/test/regress/regress2/sygus/process-10-vars-2fun.sy index fe6f5cd0c..00a0099b0 100644 --- a/test/regress/regress2/sygus/process-10-vars-2fun.sy +++ b/test/regress/regress2/sygus/process-10-vars-2fun.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress2/sygus/process-arg-invariance.sy b/test/regress/regress2/sygus/process-arg-invariance.sy index a50cec2d8..15bffb073 100644 --- a/test/regress/regress2/sygus/process-arg-invariance.sy +++ b/test/regress/regress2/sygus/process-arg-invariance.sy @@ -1,4 +1,4 @@ -; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant +; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant ; EXPECT: unsat (set-logic LIA) diff --git a/test/regress/regress2/sygus/real-grammar-neg.sy b/test/regress/regress2/sygus/real-grammar-neg.sy index 0891e57bf..d9a66bcce 100644 --- a/test/regress/regress2/sygus/real-grammar-neg.sy +++ b/test/regress/regress2/sygus/real-grammar-neg.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --no-sygus-pbe +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --no-sygus-pbe (set-logic LRA) |