Implement Hilbert choice operator (#1291)

* Initial support for Hilbert choice operator.

* Clang format.

* Fix

* Minor

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) {