diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-27 10:23:42 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-27 10:23:42 -0500 |
| commit | a64866663f10db4ffadd2d48500cda05c4831f0e (patch) | |
| tree | 34c95678bf117cda2818a201250354b7601f6545 /src/theory/strings/regexp_operation.h | |
| parent | 27ac2ce712b0bcfdef83e2d44dd210f667ab7959 (diff) | |
Do not require that function sorts are first class internally (#4128)
This PR removes the requirement in the NodeManager that argument types to the function sort are first class.
Notice that the new API does this check (as it should): https://github.com/CVC4/CVC4/blob/master/src/api/cvc4cpp.cpp#L2633
Moreover, SyGuS v2 internally requires constructing function types having arguments that are not first class (e.g. regular expression type). This is required to update the regression https://github.com/CVC4/CVC4/blob/master/test/regress/regress1/sygus/re-concat.sy to SyGuS v2.
FYI @abdoo8080 .
Diffstat (limited to 'src/theory/strings/regexp_operation.h')
0 files changed, 0 insertions, 0 deletions