diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 09:03:07 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-27 09:03:07 -0500 |
| commit | 03cc40cc070df0bc11c1556cef3016f784a95d23 (patch) | |
| tree | 6360b66292cfd6a1f46a4970c8f8e3cfc9e2e853 /src/theory/builtin/kinds | |
| parent | 425bfb52e2a6aca7a968ccf3785356ac469ec046 (diff) | |
Implement Hilbert choice operator (#1291)
* Initial support for Hilbert choice operator.
* Clang format.
* Fix
* Minor
Diffstat (limited to 'src/theory/builtin/kinds')
| -rw-r--r-- | src/theory/builtin/kinds | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 6b7b952e2..c1edd81cb 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -302,6 +302,8 @@ operator SEXPR 0: "a symbolic expression (any arity)" operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body" +operator CHOICE 2 "a Hilbert choice (epsilon) expression; first parameter is a BOUND_VAR_LIST, second is the Hilbert choice body" + parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator" constant CHAIN_OP \ ::CVC4::Chain \ @@ -333,6 +335,7 @@ typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule +typerule CHOICE ::CVC4::theory::builtin::ChoiceTypeRule typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule |