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

4 files changed, 50 insertions, 22 deletions

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,