diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-22 12:45:19 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-22 12:45:19 -0500 |
| commit | 519cdc2d4b44a9785ee68d181e2682d74890e89a (patch) | |
| tree | 573fe58b8aa3db82dab1678916ebccb7e4d74ea4 /src/api | |
| parent | 64abc6827ec78183605db53e5dd8e2a7a0db59ed (diff) | |
Function types are always first-class (#6167)
This eliminates one of the dependencies of TypeNode on options. In particular, this makes it so that function types are always considered first-class.
This change makes it so that higher-order types can always be constructed; logic exceptions should occur if they are used in constraints.
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/checks.h | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/src/api/checks.h b/src/api/checks.h index c2869f463..d5408d312 100644 --- a/src/api/checks.h +++ b/src/api/checks.h @@ -429,16 +429,18 @@ namespace api { /** * Codomain sort check for member functions of class Solver. * Check if codomain sort is not null, associated with this solver, and a - * first-class sort. + * first-class, non-function sort. */ -#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ - do \ - { \ - CVC4_API_ARG_CHECK_NOT_NULL(sort); \ - CVC4_API_CHECK(this == sort.d_solver) \ - << "Given sort is not associated with this solver"; \ - CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ - << "first-class sort as codomain sort"; \ +#define CVC4_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \ + do \ + { \ + CVC4_API_ARG_CHECK_NOT_NULL(sort); \ + CVC4_API_CHECK(this == sort.d_solver) \ + << "Given sort is not associated with this solver"; \ + CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort) \ + << "first-class sort as codomain sort"; \ + CVC4_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \ + << "function sort as codomain sort"; \ } while (0) /* Term checks. ------------------------------------------------------------- */ |