Implement Hilbert choice operator (#1291)

* Initial support for Hilbert choice operator.

* Clang format.

* Fix

* Minor

4 files changed, 75 insertions, 10 deletions

diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp
index 0cd166c87..01cf59c15 100644
--- a/src/smt/term_formula_removal.cpp
+++ b/src/smt/term_formula_removal.cpp
@@ -116,7 +116,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
   }
   //if a lambda, do lambda-lifting
   if( node.getKind() == kind::LAMBDA && !inQuant ){
-    // Make the skolem to represent the ITE
+    // Make the skolem to represent the lambda
     skolem = nodeManager->mkSkolem("lambdaF", nodeType, "a function introduced due to term-level lambda removal");
 
     // The new assertion
@@ -134,6 +134,25 @@ Node RemoveTermFormulas::run(TNode node, std::vector<Node>& output,
     // axiom defining skolem
     newAssertion = nodeManager->mkNode( kind::FORALL, children );
   }
+
+  // If a Hilbert choice function, witness the choice.
+  //   For details on this operator, see
+  //   http://planetmath.org/hilbertsvarepsilonoperator.
+  if (node.getKind() == kind::CHOICE && !inQuant)
+  {
+    // Make the skolem to witness the choice
+    skolem = nodeManager->mkSkolem(
+        "choiceK",
+        nodeType,
+        "a skolem introduced due to term-level Hilbert choice removal");
+
+    Assert(node[0].getNumChildren() == 1);
+
+    // The new assertion is the assumption that the body
+    // of the choice operator holds for the Skolem
+    newAssertion = node[1].substitute(node[0], skolem);
+  }
+
   //if a non-variable Boolean term, replace it
   if(node.getKind()!=kind::BOOLEAN_TERM_VARIABLE && nodeType.isBoolean() && inTerm && !inQuant ){//(!inQuant || !node.hasBoundVar())){
 
diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h
index 48b1c36c5..f84f9dc37 100644
--- a/src/smt/term_formula_removal.h
+++ b/src/smt/term_formula_removal.h
@@ -50,30 +50,38 @@ public:
 
   /**
    * By introducing skolem variables, this function removes all occurrences of:
-   * (1) term ITEs 
-   * (2) terms of type Boolean that are not Boolean term variables, and
-   * (3) lambdas
+   * (1) term ITEs
+   * (2) terms of type Boolean that are not Boolean term variables,
+   * (3) lambdas, and
+   * (4) Hilbert choice expressions.
    * from assertions.
    * All additional assertions are pushed into assertions. iteSkolemMap
    * contains a map from introduced skolem variables to the index in
    * assertions containing the new definition created in conjunction
    * with that skolem variable.
    *
-   * As an example of (1): 
+   * As an example of (1):
    *   f( (ite C 0 1)) = 2
-   *   becomes
+   * becomes
    *   f( k ) = 2 ^ ite( C, k=0, k=1 )
    *
    * As an example of (2):
    *   g( (and C1 C2) ) = 3
-   *   becomes
+   * becomes
    *   g( k ) = 3 ^ ( k <=> (and C1 C2) )
    *
-   * As an example of (3): 
+   * As an example of (3):
    *   (lambda x. t[x]) = f
-   *   becomes
+   * becomes
    *   (forall x. k(x) = t[x]) ^ k = f
-   * where k is a fresh skolem. This is sometimes called "lambda lifting"
+   * where k is a fresh skolem function.
+   * This is sometimes called "lambda lifting"
+   *
+   * As an example of (4):
+   *   (choice x. P( x ) ) = t
+   * becomes
+   *   P( k ) ^ k = t
+   * where k is a fresh skolem constant.
    *
    * With reportDeps true, report reasoning dependences to the proof
    * manager (for unsat cores).
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) {