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 | |
parent | 425bfb52e2a6aca7a968ccf3785356ac469ec046 (diff) |
Implement Hilbert choice operator (#1291)
* Initial support for Hilbert choice operator.
* Clang format.
* Fix
* Minor
Diffstat (limited to 'src/theory/builtin')
-rw-r--r-- | src/theory/builtin/kinds | 3 | ||||
-rw-r--r-- | src/theory/builtin/theory_builtin_type_rules.h | 35 |
2 files changed, 38 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 diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 777f6e57f..a6bd41a0b 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -192,6 +192,41 @@ public: } };/* class LambdaTypeRule */ +class ChoiceTypeRule +{ + public: + inline static TypeNode computeType(NodeManager* nodeManager, + TNode n, + bool check) + { + if (n[0].getType(check) != nodeManager->boundVarListType()) + { + std::stringstream ss; + ss << "expected a bound var list for CHOICE expression, got `" + << n[0].getType().toString() << "'"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (n[0].getNumChildren() != 1) + { + std::stringstream ss; + ss << "expected a bound var list with one argument for CHOICE expression"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + if (check) + { + TypeNode rangeType = n[1].getType(check); + if (!rangeType.isBoolean()) + { + std::stringstream ss; + ss << "expected a body of a CHOICE expression to have Boolean type"; + throw TypeCheckingExceptionPrivate(n, ss.str()); + } + } + // The type of a choice function is the type of its bound variable. + return n[0][0].getType(); + } +}; /* class ChoiceTypeRule */ + class ChainTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { |