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 /src/expr | |
| 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 'src/expr')
| -rw-r--r-- | src/expr/dtype_cons.h | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h index d5d0013de..ca4806316 100644 --- a/src/expr/dtype_cons.h +++ b/src/expr/dtype_cons.h @@ -87,12 +87,9 @@ class DTypeConstructor void setSygus(Node op); /** get sygus op * - * This method returns the operator or - * term that this constructor represents - * in the sygus encoding. This may be a - * builtin operator, defined function, variable, - * or constant that this constructor encodes in this - * deep embedding. + * This method returns the operator or term that this constructor represents + * in the sygus encoding. This may be a builtin operator, defined function, + * variable, or constant that this constructor encodes in this deep embedding. */ Node getSygusOp() const; /** is this a sygus identity function? |