diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-21 12:15:28 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-21 17:15:28 +0000 |
commit | 624292d7fb5bd27b10bdce285441540d6931fa57 (patch) | |
tree | 73169808ce6106ba4ab18f515bb1752e1227ff3e /test | |
parent | bb39d534c89dc2569aa048bb053196bfa5bbb3a1 (diff) |
Update to sygus standard output for check-synth responses (#6521)
This PR does two things:
(1) It eliminates the ad-hoc implementation of printSynthSolutions and removes it from the API. Now, printing response to a check-synth command is done in a more standard way, using the API + symbol manager. This is analogous to recent refactoring to get-model.
(2) It updates cvc5's output in response to check-synth to be compliant with the upcoming sygus 2.1 standard. The standard has changed slightly: responses to check-synth are now closed in parentheses, mirroring the smt2 response to get-model.
It also removes the unused command GetSynthSolutionCommand.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/sygus/print-debug.sy | 3 | ||||
-rw-r--r-- | test/regress/regress0/sygus/print-define-fun.sy | 3 | ||||
-rw-r--r-- | test/regress/regress1/sygus/no-var-in-sol.sy | 3 |
3 files changed, 6 insertions, 3 deletions
diff --git a/test/regress/regress0/sygus/print-debug.sy b/test/regress/regress0/sygus/print-debug.sy index 0de431294..aba9c715f 100644 --- a/test/regress/regress0/sygus/print-debug.sy +++ b/test/regress/regress0/sygus/print-debug.sy @@ -3,8 +3,9 @@ ; EXPECT: (sygus-candidate (f 0)) ; EXPECT: (sygus-enum 1) ; EXPECT: (sygus-candidate (f 1)) -; EXPECT: unsat +; EXPECT: ( ; EXPECT: (define-fun f () Int 1) +; EXPECT: ) (set-logic LIA) (synth-fun f () Int ((Start Int)) ((Start Int (0 1)))) diff --git a/test/regress/regress0/sygus/print-define-fun.sy b/test/regress/regress0/sygus/print-define-fun.sy index e6c7e4748..520a03d2a 100644 --- a/test/regress/regress0/sygus/print-define-fun.sy +++ b/test/regress/regress0/sygus/print-define-fun.sy @@ -1,6 +1,7 @@ ; COMMAND-LINE: --lang=sygus2 -; EXPECT: unsat +; EXPECT: ( ; EXPECT: (define-fun g ((x Int)) Int (f 0)) +; EXPECT: ) (set-logic LIA) (define-fun f ((x Int)) Int (+ x 1)) (synth-fun g ((x Int)) Int ((Start Int)) ((Start Int ((f 0))))) diff --git a/test/regress/regress1/sygus/no-var-in-sol.sy b/test/regress/regress1/sygus/no-var-in-sol.sy index 333e29d6e..ff2be7b22 100644 --- a/test/regress/regress1/sygus/no-var-in-sol.sy +++ b/test/regress/regress1/sygus/no-var-in-sol.sy @@ -1,7 +1,8 @@ ; COMMAND-LINE: --sygus-si=all --dag-thresh=0 -; EXPECT: unsat +; EXPECT: ( ; EXPECT: (define-fun f1 ((x Bool) (y Bool)) Bool (ite true true false)) ; EXPECT: (define-fun f2 ((x Bool) (y Bool)) Bool (ite x (ite y false (not false)) (not (ite false false (not false))))) +; EXPECT: ) ; Test ensures that the solution does not contain a random variable |