diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-10 23:37:43 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-04-10 23:37:43 -0500 |
| commit | 4e310461b2e41f9ccf1426797b5d8b58e27bc1c7 (patch) | |
| tree | f6b6861a47d42b12b3cf776488038358db09a50a /test/regress/CMakeLists.txt | |
| parent | 04a8bf833bad57329a4e83b3c5aafb7537de885d (diff) | |
Ensure exported sygus solutions match grammar (#4270)
Previously we were doing rewriting/expand definitions during grammar normalization, which overwrote the original sygus operators. The connection to the original grammar was maintained via the SygusPrintCallback utility, which ensured that a sygus term printed in a way that matched the grammar.
We now have several use cases where solutions from SyGuS will be directly exported to the user, including the current use of get-abduct. This means that the terms must match the grammar, and we cannot simply rely on the print callback.
This moves the code to normalize sygus operators to datatypes utils, where the conversion between sygus and builtin terms takes place. This allows a version of this function where isExternal = true, which constructs terms matching the original grammar.
This PR enables the SyGuS API to have an accurate getSynthSolution method. It also will eliminate the need for SygusPrintCallback altogether, once the v1 parser is deleted.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 8aae1890d..06dc2d87c 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1951,6 +1951,7 @@ set(regress_1_tests regress1/sygus/unbdd_inv_gen_ex7.sy regress1/sygus/unbdd_inv_gen_winf1.sy regress1/sygus/univ_2-long-repeat.sy + regress1/sygus/yoni-true-sol.smt2 regress1/sym/q-constant.smt2 regress1/sym/q-function.smt2 regress1/sym/qf-function.smt2 |