diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-11-05 15:12:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-11-05 20:12:22 +0000 |
| commit | bc6f79ab1ca703b3507fc43e438f17b4422360b8 (patch) | |
| tree | f4d0d45d36d94bfde765f1e0f497a9a96293aa03 /src/theory/uf/kinds | |
| parent | e187b4c5709fc7b15e3d4c0e751224824208d28b (diff) | |
Move functions and lambdas from builtin to uf (#7570)
This is in preparation for adding better native support for handling lambdas in the higher-order extension of the UF theory.
We require that LAMBDA and function types belong to theory UF so that the theory solver is properly notified.
This also splits the utility methods for computing whether a function is "constant" to its own file.
This PR is code move only.
Diffstat (limited to 'src/theory/uf/kinds')
| -rw-r--r-- | src/theory/uf/kinds | 22 |
1 files changed, 20 insertions, 2 deletions
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds index 0faa5c672..a1db5120f 100644 --- a/src/theory/uf/kinds +++ b/src/theory/uf/kinds @@ -15,10 +15,28 @@ parameterized APPLY_UF VARIABLE 1: "application of an uninterpreted function; fi typerule APPLY_UF ::cvc5::theory::uf::UfTypeRule +operator FUNCTION_TYPE 2: "a function type" +cardinality FUNCTION_TYPE \ + "::cvc5::theory::uf::FunctionProperties::computeCardinality(%TYPE%)" \ + "theory/uf/theory_uf_type_rules.h" +well-founded FUNCTION_TYPE \ + "::cvc5::theory::uf::FunctionProperties::isWellFounded(%TYPE%)" \ + "::cvc5::theory::uf::FunctionProperties::mkGroundTerm(%TYPE%)" \ + "theory/uf/theory_uf_type_rules.h" +enumerator FUNCTION_TYPE \ + ::cvc5::theory::uf::FunctionEnumerator \ + "theory/uf/type_enumerator.h" + +operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body" + +typerule LAMBDA ::cvc5::theory::uf::LambdaTypeRule + variable BOOLEAN_TERM_VARIABLE "Boolean term variable" -parameterized PARTIAL_APPLY_UF APPLY_UF 1: "partial uninterpreted function application" -typerule PARTIAL_APPLY_UF ::cvc5::theory::uf::PartialTypeRule +variable LAMBDA_VARIABLE "Lambda variable, used for lazy lambda lifting" + +# lambda expressions that are isomorphic to array constants can be considered constants +construle LAMBDA ::cvc5::theory::uf::LambdaTypeRule operator HO_APPLY 2 "higher-order (partial) function application" typerule HO_APPLY ::cvc5::theory::uf::HoApplyTypeRule |