diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-26 14:59:38 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-26 14:59:38 -0600 |
| commit | 3ef1df6e974ba572a8def512489cd9e47e9d2a2b (patch) | |
| tree | 82ed16f31e9fd3d7a3356c0248b3a7a7a384864c /test | |
| parent | b320aa323923822a7702997bbca05e8512da55a4 (diff) | |
More fixes for printing sygus commands (#3812)
Towards v1 -> v2 sygus conversion.
This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/sygus/sygus-uf.sy | 4 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/constant-bool-si-all.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/constant-dec-tree-bug.sy | 2 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/sygus-uf-ex.sy | 4 | ||||
| -rw-r--r-- | test/regress/regress1/sygus/tester.sy | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy index 1b060637a..d506dd5b2 100644 --- a/test/regress/regress0/sygus/sygus-uf.sy +++ b/test/regress/regress0/sygus/sygus-uf.sy @@ -1,6 +1,6 @@ -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --sygus-out=status --uf-ho ; EXPECT: unsat -(set-logic LIA) +(set-logic UFLIA) (declare-fun uf (Int) Int) diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy index eee7956f4..45d49e75b 100644 --- a/test/regress/regress1/sygus/constant-bool-si-all.sy +++ b/test/regress/regress1/sygus/constant-bool-si-all.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status -(set-logic SAT) +(set-logic LIA) (synth-fun f () Bool) (synth-fun g () Bool) (synth-fun h () Bool) diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy index 7229dea2e..e20520a4a 100644 --- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy +++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete -(set-logic SAT) +(set-logic LIA) (synth-fun u ((x Int)) Int) (synth-fun f () Bool) (synth-fun g () Bool) diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy index b9731de0f..66880eafa 100644 --- a/test/regress/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status -(set-logic LIA) +; COMMAND-LINE: --sygus-out=status --uf-ho +(set-logic UFLIA) (declare-fun uf ( Int ) Int) (synth-fun f ((x Int) (y Int)) Bool ((Start Bool (true false diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy index bf1cd1576..282bc122c 100644 --- a/test/regress/regress1/sygus/tester.sy +++ b/test/regress/regress1/sygus/tester.sy @@ -1,7 +1,7 @@ ; EXPECT: unsat ; COMMAND-LINE: --sygus-out=status -(set-logic SLIA) +(set-logic DTSLIA) (declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool)))) (define-fun isA ((i DT)) Bool ((_ is A) i) ) |