Frontend support for the choice operator (#4175)

Added the operator choice to Smt2.g and Cvc.g.
Removed the unused parameter hasBoundVars from TheoryModel::getModelValue

9 files changed, 78 insertions, 24 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 033389610..8b3b96cfd 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -114,6 +114,7 @@ tokens {
 
   FORALL_TOK = 'FORALL';
   EXISTS_TOK = 'EXISTS';
+  CHOICE_TOK = 'CHOICE';
   PATTERN_TOK = 'PATTERN';
 
   LAMBDA_TOK = 'LAMBDA';
@@ -343,7 +344,8 @@ int getOperatorPrecedence(int type) {
   case IMPLIES_TOK: return 30;// right-to-left
   case IFF_TOK: return 31;
   case FORALL_TOK:
-  case EXISTS_TOK: return 32;
+  case EXISTS_TOK:
+  case CHOICE_TOK: return 32;
   case ASSIGN_TOK:
   case IN_TOK: return 33;
 
@@ -1465,7 +1467,7 @@ prefixFormula[CVC4::api::Term& f]
   api::Term ipl;
 }
     /* quantifiers */
-  : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } )
+  : ( FORALL_TOK { k = api::FORALL; } | EXISTS_TOK { k = api::EXISTS; } | CHOICE_TOK { k = api::CHOICE; } )
     { PARSER_STATE->pushScope(); } LPAREN
     boundVarDecl[ids,t]
     { for(std::vector<std::string>::const_iterator i = ids.begin(); i != ids.end(); ++i) {
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 0c42678aa..d0a73ce6a 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2312,6 +2312,7 @@ quantOp[CVC4::api::Kind& kind]
 }
   : EXISTS_TOK    { $kind = api::EXISTS; }
   | FORALL_TOK    { $kind = api::FORALL; }
+  | CHOICE_TOK    { $kind = api::CHOICE; }
   ;
 
 /**
@@ -2682,6 +2683,7 @@ ATTRIBUTE_INST_LEVEL : ':quant-inst-max-level';
 // operators (NOTE: theory symbols go here)
 EXISTS_TOK        : 'exists';
 FORALL_TOK        : 'forall';
+CHOICE_TOK        : { !PARSER_STATE->strictModeEnabled() }? 'choice';
 
 EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index b819b883d..505aa503f 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -15,9 +15,10 @@
  **/
 
 #include "theory/builtin/theory_builtin.h"
-#include "theory/valuation.h"
+
 #include "expr/kind.h"
 #include "theory/theory_model.h"
+#include "theory/valuation.h"
 
 using namespace std;
 
@@ -25,6 +26,28 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory */
-}/* CVC4 namespace */
+TheoryBuiltin::TheoryBuiltin(context::Context* c,
+                             context::UserContext* u,
+                             OutputChannel& out,
+                             Valuation valuation,
+                             const LogicInfo& logicInfo)
+    : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo)
+{
+}
+
+std::string TheoryBuiltin::identify() const
+{
+  return std::string("TheoryBuiltin");
+}
+
+void TheoryBuiltin::finishInit()
+{
+  // choice nodes are not evaluated in getModelValue
+  TheoryModel* theoryModel = d_valuation.getModel();
+  Assert(theoryModel != nullptr);
+  theoryModel->setUnevaluatedKind(kind::CHOICE);
+}
+
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 8a7d1bf7b..6e99ef040 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -25,17 +25,23 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-class TheoryBuiltin : public Theory {
-public:
-  TheoryBuiltin(context::Context* c, context::UserContext* u,
-                OutputChannel& out, Valuation valuation,
-                const LogicInfo& logicInfo)
-      : Theory(THEORY_BUILTIN, c, u, out, valuation, logicInfo) {}
-  std::string identify() const override { return std::string("TheoryBuiltin"); }
-};/* class TheoryBuiltin */
-
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+class TheoryBuiltin : public Theory
+{
+ public:
+  TheoryBuiltin(context::Context* c,
+                context::UserContext* u,
+                OutputChannel& out,
+                Valuation valuation,
+                const LogicInfo& logicInfo);
+
+  std::string identify() const override;
+
+  /** finish initialization */
+  void finishInit() override;
+}; /* class TheoryBuiltin */
+
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 7bfb0e8f3..dae7261e5 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -147,7 +147,7 @@ Node TheoryModel::getValue(TNode n) const
   Node nn = d_substitutions.apply(n);
   Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
   //get value in model
-  nn = getModelValue(nn, false);
+  nn = getModelValue(nn);
   if (nn.isNull()) return nn;
   if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
     //normalize
@@ -193,7 +193,7 @@ Cardinality TheoryModel::getCardinality( Type t ) const{
   }
 }
 
-Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
+Node TheoryModel::getModelValue(TNode n) const
 {
   std::unordered_map<Node, Node, NodeHashFunction>::iterator it = d_modelCache.find(n);
   if (it != d_modelCache.end()) {
@@ -220,7 +220,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     std::vector<Node> children;
     if (n.getKind() == APPLY_UF)
     {
-      Node op = getModelValue(n.getOperator(), hasBoundVars);
+      Node op = getModelValue(n.getOperator());
       Debug("model-getvalue-debug") << "  operator : " << op << std::endl;
       children.push_back(op);
     }
@@ -231,7 +231,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars) const
     // evaluate the children
     for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
     {
-      ret = getModelValue(n[i], hasBoundVars);
+      ret = getModelValue(n[i]);
       Debug("model-getvalue-debug")
           << "  " << n << "[" << i << "] is " << ret << std::endl;
       children.push_back(ret);
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index d2ce63ac5..d984fbc6b 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -390,9 +390,8 @@ public:
   /** Get model value function.
    *
    * This function is a helper function for getValue.
-   *   hasBoundVars is whether n may contain bound variables
    */
-  Node getModelValue(TNode n, bool hasBoundVars = false) const;
+  Node getModelValue(TNode n) const;
   /** add term internal
    *
    * This will do any model-specific processing necessary for n,
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a5acd62fb..d843eb5ed 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -610,6 +610,8 @@ set(regress_0_tests
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
   regress0/parser/bv_nat.smt2
+  regress0/parser/choice.cvc
+  regress0/parser/choice.smt2
   regress0/parser/constraint.smt2
   regress0/parser/declarefun-emptyset-uf.smt2
   regress0/parser/force_logic_set_logic.smt2
diff --git a/test/regress/regress0/parser/choice.cvc b/test/regress/regress0/parser/choice.cvc
new file mode 100644
index 000000000..e0ebac051
--- /dev/null
+++ b/test/regress/regress0/parser/choice.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+
+a : INT;
+b : INT;
+c : INT;
+
+ASSERT (CHOICE(x: INT): x = a) = 1;
+ASSERT (CHOICE(x: INT): x = b) = 2;
+
+CHECKSAT;
\ No newline at end of file
diff --git a/test/regress/regress0/parser/choice.smt2 b/test/regress/regress0/parser/choice.smt2
new file mode 100644
index 000000000..19763e222
--- /dev/null
+++ b/test/regress/regress0/parser/choice.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(assert (= (choice ((x Int)) (= x a)) 1))
+(assert (= (choice ((x Int)) (= x b)) 2))
+;(assert (let ((x (choice ((x Int)) true))) (and (distinct a b x)(= x c))))
+(check-sat)
+