Do not require that function sorts are first class internally (#4128)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 27 Mar 2020 15:23:42 +0000 (10:23 -0500)
committerGitHub <noreply@github.com>
Fri, 27 Mar 2020 15:23:42 +0000 (10:23 -0500)
commita64866663f10db4ffadd2d48500cda05c4831f0e
tree34c95678bf117cda2818a201250354b7601f6545
parent27ac2ce712b0bcfdef83e2d44dd210f667ab7959
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 .
src/expr/node_manager.cpp
src/expr/node_manager.h