Add notions of evaluated kinds in TheoryModel (#1947)

15 files changed, 289 insertions, 137 deletions

diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index 2b1f75072..3509f408d 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -23,3 +23,20 @@ header = "options/theory_options.h"
   notifies   = ["notifyUseTheoryList"]
   read_only  = true
   help       = "use alternate theory implementation NAME (--use-theory=help for a list). This option may be repeated or a comma separated list."
+
+[[option]]
+  name       = "assignFunctionValues"
+  category   = "regular"
+  long       = "assign-function-values"
+  type       = "bool"
+  default    = "true"
+  help       = "assign values for uninterpreted functions in models"
+
+[[option]]
+  name       = "condenseFunctionValues"
+  category   = "regular"
+  long       = "condense-function-values"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "condense values for functions in models rather than explicitly representing them"
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index 791b6e0bb..73a2be9ff 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -12,15 +12,6 @@ header = "options/uf_options.h"
   help       = "use UF symmetry breaker (Deharbe et al., CADE 2011)"
 
 [[option]]
-  name       = "condenseFunctionValues"
-  category   = "regular"
-  long       = "condense-function-values"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "condense models for functions rather than explicitly representing them"
-
-[[option]]
   name       = "ufssRegions"
   category   = "regular"
   long       = "uf-ss-regions"
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 114527334..9d4462210 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1313,6 +1313,11 @@ void SmtEngine::setDefaults() {
     {
       options::cbqiMidpoint.set(true);
     }
+    // do not assign function values (optimization)
+    if (!options::assignFunctionValues.wasSetByUser())
+    {
+      options::assignFunctionValues.set(false);
+    }
   }
   else
   {
@@ -5189,6 +5194,13 @@ Model* SmtEngine::getModel() {
     Dump("benchmark") << GetModelCommand();
   }
 
+  if (!options::assignFunctionValues())
+  {
+    const char* msg =
+        "Cannot get the model when --assign-function-values is false.";
+    throw RecoverableModalException(msg);
+  }
+
   if(d_status.isNull() ||
      d_status.asSatisfiabilityResult() == Result::UNSAT ||
      d_problemExtended) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 2041b0805..107cb9672 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -187,6 +187,16 @@ Node TheoryBV::getBVDivByZero(Kind k, unsigned width) {
   Unreachable();
 }
 
+void TheoryBV::finishInit()
+{
+  // these kinds are semi-evaluated in getModelValue (applications of this
+  // kind are treated as variables)
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UDIV);
+  tm->setSemiEvaluatedKind(kind::BITVECTOR_ACKERMANNIZE_UREM);
+}
+
 Node TheoryBV::expandDefinition(LogicRequest &logicRequest, Node node) {
   Debug("bitvector-expandDefinition") << "TheoryBV::expandDefinition(" << node << ")" << std::endl;
 
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 13469d562..603823ff0 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -66,6 +66,8 @@ public:
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
 
+  void finishInit() override;
+
   Node expandDefinition(LogicRequest& logicRequest, Node node) override;
 
   void preRegisterTerm(TNode n) override;
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.cpp b/src/theory/quantifiers/fmf/ambqi_builder.cpp
index cedd2a2ed..52ce4407a 100644
--- a/src/theory/quantifiers/fmf/ambqi_builder.cpp
+++ b/src/theory/quantifiers/fmf/ambqi_builder.cpp
@@ -744,6 +744,11 @@ QModelBuilder( c, qe ){
 //------------------------model construction----------------------------
 
 bool AbsMbqiBuilder::processBuildModel(TheoryModel* m) {
+  if (!m->areFunctionValuesEnabled())
+  {
+    // nothing to do if no functions
+    return true;
+  }
   Trace("ambqi-debug") << "process build model " << std::endl;
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 0ec8b00b2..e97f716cb 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/fmf/full_model_check.h"
 #include "options/quantifiers_options.h"
+#include "options/theory_options.h"
 #include "options/uf_options.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/instantiate.h"
@@ -370,6 +371,11 @@ bool FullModelChecker::preProcessBuildModel(TheoryModel* m) {
 }
 
 bool FullModelChecker::processBuildModel(TheoryModel* m){
+  if (!m->areFunctionValuesEnabled())
+  {
+    // nothing to do if no functions
+    return true;
+  }
   FirstOrderModelFmc * fm = ((FirstOrderModelFmc*)m)->asFirstOrderModelFmc();
   Trace("fmc") << "---Full Model Check reset() " << std::endl;
   d_quant_models.clear();
diff --git a/src/theory/quantifiers/fmf/model_builder.cpp b/src/theory/quantifiers/fmf/model_builder.cpp
index 9e7961172..055bee231 100644
--- a/src/theory/quantifiers/fmf/model_builder.cpp
+++ b/src/theory/quantifiers/fmf/model_builder.cpp
@@ -183,6 +183,11 @@ Node QModelBuilderIG::getCurrentUfModelValue( FirstOrderModel* fm, Node n, std::
 */
 
 bool QModelBuilderIG::processBuildModel( TheoryModel* m ) {
+  if (!m->areFunctionValuesEnabled())
+  {
+    // nothing to do if no functions
+    return true;
+  }
   FirstOrderModel* f = (FirstOrderModel*)m;
   FirstOrderModelIG* fm = f->asFirstOrderModelIG();
   Trace("model-engine-debug") << "Process build model " << optUseModel() << std::endl;
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 74d8269f9..5016bd87f 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -73,6 +73,15 @@ void TheoryQuantifiers::notifyEq(TNode lhs, TNode rhs) {
 
 }
 
+void TheoryQuantifiers::finishInit()
+{
+  // quantifiers are not evaluated in getModelValue
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  tm->setUnevaluatedKind(EXISTS);
+  tm->setUnevaluatedKind(FORALL);
+}
+
 void TheoryQuantifiers::preRegisterTerm(TNode n) {
   Debug("quantifiers-prereg") << "TheoryQuantifiers::preRegisterTerm() " << n << endl;
   if( n.getKind()==FORALL ){
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 4bb28fe79..4f0302bf3 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -42,6 +42,8 @@ class TheoryQuantifiers : public Theory {
   void setMasterEqualityEngine(eq::EqualityEngine* eq) override;
   void addSharedTerm(TNode t) override;
   void notifyEq(TNode lhs, TNode rhs);
+  /** finish initialization */
+  void finishInit() override;
   void preRegisterTerm(TNode n) override;
   void presolve() override;
   void ppNotifyAssertions(const std::vector<Node>& assertions) override;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 08d33fe6c..4d78482c5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -232,7 +232,8 @@ void TheoryEngine::finishInit() {
     d_curr_model_builder = d_quantEngine->getModelBuilder();
     d_curr_model = d_quantEngine->getModel();
   } else {
-    d_curr_model = new theory::TheoryModel(d_userContext, "DefaultModel", true);
+    d_curr_model = new theory::TheoryModel(
+        d_userContext, "DefaultModel", options::assignFunctionValues());
     d_aloc_curr_model = true;
   }
   //make the default builder, e.g. in the case that the quantifiers engine does not have a model builder
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 35ada798c..0258e65cc 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -48,6 +48,12 @@ TheoryModel::TheoryModel(context::Context* c,
   d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_eeContext->push();
+  // do not interpret APPLY_UF if we are not assigning function values
+  if (!enableFuncModels)
+  {
+    setSemiEvaluatedKind(kind::APPLY_UF);
+  }
+  setUnevaluatedKind(kind::BOUND_VARIABLE);
 }
 
 TheoryModel::~TheoryModel()
@@ -160,148 +166,157 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c
   }
   Debug("model-getvalue-debug") << "Get model value " << n << " ... ";
   Debug("model-getvalue-debug") << d_equalityEngine->hasTerm(n) << std::endl;
+  if (n.isConst())
+  {
+    d_modelCache[n] = n;
+    return n;
+  }
+
   Node ret = n;
-  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ) {
-    // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
-    // However, if the Decision Engine stops us early, there might be a
-    // quantifier that isn't assigned.  In conjunction with miniscoping, this
-    // might lead to a perfectly good model.  Think of
-    //     ASSERT FORALL(x) : p OR x=5
-    // The p is pulled out by miniscoping, and set to TRUE by the decision
-    // engine, then the quantifier's value in the model doesn't matter, so the
-    // Decision Engine stops.  So even though the top-level quantifier was
-    // asserted, it can't be checked directly: first, it doesn't "exist" in
-    // non-miniscoped form, and second, no quantifiers have been asserted, so
-    // none is in the model.  We used to fail an assertion here, but that's
-    // no good.  Instead, return the quantifier itself.  If we're in
-    // checkModel(), and the quantifier actually matters, we'll get an
-    // assert-fail since the quantifier isn't a constant.
-    Node nr = Rewriter::rewrite(n);
-    if(!d_equalityEngine->hasTerm(nr)) {
-      d_modelCache[n] = ret;
-      return ret;
-    } else {
-      ret = nr;
+  Kind nk = n.getKind();
+  NodeManager* nm = NodeManager::currentNM();
+
+  // if it is an evaluated kind, compute model values for children and evaluate
+  if (n.getNumChildren() > 0
+      && d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end())
+  {
+    Debug("model-getvalue-debug")
+        << "Get model value children " << n << std::endl;
+    std::vector<Node> children;
+    if (n.getKind() == APPLY_UF)
+    {
+      Node op = getModelValue(n.getOperator(), hasBoundVars);
+      Debug("model-getvalue-debug") << "  operator : " << op << std::endl;
+      children.push_back(op);
     }
-  } else {
-    // FIXME : special case not necessary? (also address BV_ACKERMANNIZE
-    // functions below), github issue #1116
-    if(n.getKind() == kind::LAMBDA) {
-      NodeManager* nm = NodeManager::currentNM();
-      Node body = getModelValue(n[1], true);
-      body = Rewriter::rewrite(body);
-      ret = nm->mkNode(kind::LAMBDA, n[0], body);
-      ret = Rewriter::rewrite( ret );
-      d_modelCache[n] = ret;
-      return ret;
+    else if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+    {
+      children.push_back(n.getOperator());
+    }
+    // evaluate the children
+    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
+    {
+      ret = getModelValue(n[i], hasBoundVars);
+      Debug("model-getvalue-debug")
+          << "  " << n << "[" << i << "] is " << ret << std::endl;
+      children.push_back(ret);
     }
-    if(n.isConst() || (hasBoundVars && n.getKind() == kind::BOUND_VARIABLE)) {
+    ret = nm->mkNode(n.getKind(), children);
+    Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
+    ret = Rewriter::rewrite(ret);
+    Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
+    // special cases
+    if (ret.getKind() == kind::CARDINALITY_CONSTRAINT)
+    {
+      Debug("model-getvalue-debug")
+          << "get cardinality constraint " << ret[0].getType() << std::endl;
+      ret = nm->mkConst(
+          getCardinality(ret[0].getType().toType()).getFiniteCardinality()
+          <= ret[1].getConst<Rational>().getNumerator());
+    }
+    else if (ret.getKind() == kind::CARDINALITY_VALUE)
+    {
+      Debug("model-getvalue-debug")
+          << "get cardinality value " << ret[0].getType() << std::endl;
+      ret = nm->mkConst(Rational(
+          getCardinality(ret[0].getType().toType()).getFiniteCardinality()));
+    }
+    d_modelCache[n] = ret;
+    return ret;
+  }
+  // must rewrite the term at this point
+  ret = Rewriter::rewrite(n);
+  // return the representative of the term in the equality engine, if it exists
+  TypeNode t = ret.getType();
+  bool eeHasTerm;
+  if (!options::ufHo() && (t.isFunction() || t.isPredicate()))
+  {
+    // functions are in the equality engine, but *not* as first-class members
+    // when higher-order is disabled. In this case, we cannot query
+    // representatives for functions since they are "internal" nodes according
+    // to the equality engine despite hasTerm returning true. However, they are
+    // first class members when higher-order is enabled. Hence, the special
+    // case here.
+    eeHasTerm = false;
+  }
+  else
+  {
+    eeHasTerm = d_equalityEngine->hasTerm(ret);
+  }
+  if (eeHasTerm)
+  {
+    Debug("model-getvalue-debug")
+        << "get value from representative " << ret << "..." << std::endl;
+    ret = d_equalityEngine->getRepresentative(ret);
+    Assert(d_reps.find(ret) != d_reps.end());
+    std::map<Node, Node>::const_iterator it2 = d_reps.find(ret);
+    if (it2 != d_reps.end())
+    {
+      ret = it2->second;
       d_modelCache[n] = ret;
       return ret;
     }
+  }
 
-    if (n.getNumChildren() > 0
-        && n.getKind() != kind::BITVECTOR_ACKERMANNIZE_UDIV
-        && n.getKind() != kind::BITVECTOR_ACKERMANNIZE_UREM)
+  // if we are a evaluated or semi-evaluated kind, return an arbitrary value
+  // if we are not in the d_not_evaluated_kinds map, we are evaluated
+  // if we are in the d_semi_evaluated_kinds, we are semi-evaluated
+  if (d_not_evaluated_kinds.find(nk) == d_not_evaluated_kinds.end()
+      || d_semi_evaluated_kinds.find(nk) != d_semi_evaluated_kinds.end())
+  {
+    if (t.isFunction() || t.isPredicate())
     {
-      Debug("model-getvalue-debug") << "Get model value children " << n << std::endl;
-      std::vector<Node> children;
-      if (n.getKind() == APPLY_UF) {
-        Node op = getModelValue(n.getOperator(), hasBoundVars);
-        Debug("model-getvalue-debug") << "  operator : " << op << std::endl;
-        children.push_back(op);
-      }
-      else if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
-        children.push_back(n.getOperator());
-      }
-      //evaluate the children
-      for (unsigned i = 0; i < n.getNumChildren(); ++i) {
-        ret = getModelValue(n[i], hasBoundVars);
-        Debug("model-getvalue-debug") << "  " << n << "[" << i << "] is " << ret << std::endl;
-        children.push_back(ret);
+      if (d_enableFuncModels)
+      {
+        std::map<Node, Node>::const_iterator it = d_uf_models.find(n);
+        if (it != d_uf_models.end())
+        {
+          // Existing function
+          ret = it->second;
+          d_modelCache[n] = ret;
+          return ret;
+        }
+        // Unknown function symbol: return LAMBDA x. c, where c is the first
+        // constant in the enumeration of the range type
+        vector<TypeNode> argTypes = t.getArgTypes();
+        vector<Node> args;
+        NodeManager* nm = NodeManager::currentNM();
+        for (unsigned i = 0, size = argTypes.size(); i < size; ++i)
+        {
+          args.push_back(nm->mkBoundVar(argTypes[i]));
+        }
+        Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
+        TypeEnumerator te(t.getRangeType());
+        ret = nm->mkNode(kind::LAMBDA, boundVarList, *te);
       }
-      ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
-      Debug("model-getvalue-debug") << "ret (pre-rewrite): " << ret << std::endl;
-      ret = Rewriter::rewrite(ret);
-      Debug("model-getvalue-debug") << "ret (post-rewrite): " << ret << std::endl;
-      if(ret.getKind() == kind::CARDINALITY_CONSTRAINT) {
-        Debug("model-getvalue-debug") << "get cardinality constraint " << ret[0].getType() << std::endl;
-        ret = NodeManager::currentNM()->mkConst(getCardinality(ret[0].getType().toType()).getFiniteCardinality() <= ret[1].getConst<Rational>().getNumerator());
-      }else if(ret.getKind() == kind::CARDINALITY_VALUE) {
-        Debug("model-getvalue-debug") << "get cardinality value " << ret[0].getType() << std::endl;
-        ret = NodeManager::currentNM()->mkConst(Rational(getCardinality(ret[0].getType().toType()).getFiniteCardinality()));
+      else
+      {
+        // if func models not enabled, throw an error
+        Unreachable();
       }
-      d_modelCache[n] = ret;
-      return ret;
     }
-  
-    Debug("model-getvalue-debug") << "Handling special cases for types..." << std::endl;
-    TypeNode t = n.getType();
-    bool eeHasTerm;
-    if( !options::ufHo() && (t.isFunction() || t.isPredicate()) ){
-      // functions are in the equality engine, but *not* as first-class members
-      // when higher-order is disabled. In this case, we cannot query representatives for functions
-      // since they are "internal" nodes according to the equality engine despite hasTerm returning true. 
-      // However, they are first class members when higher-order is enabled. Hence, the special
-      // case here.
-      eeHasTerm = false;
-    }else{
-      eeHasTerm = d_equalityEngine->hasTerm(n);
+    else if (!t.isFirstClass())
+    {
+      // this is the class for regular expressions
+      // we simply invoke the rewriter on them
+      ret = Rewriter::rewrite(ret);
     }
-    // if the term does not exist in the equality engine, return an arbitrary value
-    if (!eeHasTerm) {
-      if (t.isFunction() || t.isPredicate()) {
-        if (d_enableFuncModels) {
-          std::map< Node, Node >::const_iterator it = d_uf_models.find(n);
-          if (it != d_uf_models.end()) {
-            // Existing function
-            ret = it->second;
-            d_modelCache[n] = ret;
-            return ret;
-          }
-          // Unknown function symbol: return LAMBDA x. c, where c is the first constant in the enumeration of the range type
-          vector<TypeNode> argTypes = t.getArgTypes();
-          vector<Node> args;
-          NodeManager* nm = NodeManager::currentNM();
-          for (unsigned i = 0; i < argTypes.size(); ++i) {
-            args.push_back(nm->mkBoundVar(argTypes[i]));
-          }
-          Node boundVarList = nm->mkNode(kind::BOUND_VAR_LIST, args);
-          TypeEnumerator te(t.getRangeType());
-          ret = nm->mkNode(kind::LAMBDA, boundVarList, *te);
-        }else{
-          // TODO: if func models not enabled, throw an error?
-          Unreachable();
-        }
-      }
-      else if (!t.isFirstClass())
+    else
+    {
+      if (options::omitDontCares() && useDontCares)
       {
-        // this is the class for regular expressions
-        // we simply invoke the rewriter on them
-        ret = Rewriter::rewrite(ret);
-      } else {
-        if (options::omitDontCares() && useDontCares) {
-          return Node();
-        }
-        // Unknown term - return first enumerated value for this type
-        TypeEnumerator te(n.getType());
-        ret = *te;
+        return Node();
       }
-      d_modelCache[n] = ret;
-      return ret;
+      // Unknown term - return first enumerated value for this type
+      TypeEnumerator te(n.getType());
+      ret = *te;
     }
+    d_modelCache[n] = ret;
+    return ret;
   }
-  Debug("model-getvalue-debug") << "get value from representative " << ret << "..." << std::endl;
-  ret = d_equalityEngine->getRepresentative(ret);
-  Assert(d_reps.find(ret) != d_reps.end());
-  std::map< Node, Node >::const_iterator it2 = d_reps.find( ret );
-  if (it2 != d_reps.end()) {
-    ret = it2->second;
-  } else {
-    ret = Node::null();
-  }
-  d_modelCache[n] = ret;
-  return ret;
+
+  d_modelCache[n] = n;
+  return n;
 }
 
 /** add substitution */
@@ -477,6 +492,17 @@ void TheoryModel::recordApproximation(TNode n, TNode pred)
   d_approx_list.push_back(std::pair<Node, Node>(n, pred));
 }
 
+void TheoryModel::setUnevaluatedKind(Kind k)
+{
+  d_not_evaluated_kinds.insert(k);
+}
+
+void TheoryModel::setSemiEvaluatedKind(Kind k)
+{
+  d_not_evaluated_kinds.insert(k);
+  d_semi_evaluated_kinds.insert(k);
+}
+
 bool TheoryModel::hasTerm(TNode a)
 {
   return d_equalityEngine->hasTerm( a );
@@ -546,6 +572,11 @@ void TheoryModel::printRepresentative( std::ostream& out, Node r ){
   }
 }
 
+bool TheoryModel::areFunctionValuesEnabled() const
+{
+  return d_enableFuncModels;
+}
+
 void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) {
   Assert( d_uf_models.find( f )==d_uf_models.end() );
   Trace("model-builder") << "  Assigning function (" << f << ") to (" << f_def << ")" << endl;
diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index b6d1288ae..cee39b542 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -161,6 +161,50 @@ public:
    * construction process.
    */
   void recordApproximation(TNode n, TNode pred);
+  /** set unevaluate/semi-evaluated kind
+   *
+   * This informs this model how it should interpret applications of terms with
+   * kind k in getModelValue. We distinguish four categories of kinds:
+   *
+   * [1] "Evaluated"
+   * This includes (standard) interpreted symbols like NOT, PLUS, UNION, etc.
+   * These operators can be characterized by the invariant that they are
+   * "evaluatable". That is, if they are applied to only constants, the rewriter
+   * is guaranteed to rewrite the application to a constant. When getting
+   * the model value of <k>( t1...tn ) where k is a kind of this category, we
+   * compute the (constant) value of t1...tn, say this returns c1...cn, we
+   * return the (constant) result of rewriting <k>( c1...cn ).
+   *
+   * [2] "Unevaluated"
+   * This includes interpreted symbols like FORALL, EXISTS,
+   * CARDINALITY_CONSTRAINT, that are not evaluatable. When getting a model
+   * value for a term <k>( t1...tn ) where k is a kind of this category, we
+   * check whether <k>( t1...tn ) exists in the equality engine of this model.
+   * If it does, we return its representative, otherwise we return the term
+   * itself.
+   *
+   * [3] "Semi-evaluated"
+   * This includes kinds like BITVECTOR_ACKERMANNIZE_UDIV and others, typically
+   * those that correspond to abstractions. Like unevaluated kinds, these
+   * kinds do not have an evaluator. In contrast to unevaluated kinds, we
+   * interpret a term <k>( t1...tn ) not appearing in the equality engine as an
+   * arbitrary value instead of the term itself.
+   *
+   * [4] APPLY_UF, where getting the model value depends on an internally
+   * constructed representation of a lambda model value (d_uf_models).
+   * It is optional whether this kind is "evaluated" or "semi-evaluated".
+   * In the case that it is "evaluated", get model rewrites the application
+   * of the lambda model value of its operator to its evaluated arguments.
+   *
+   * By default, all kinds are considered "evaluated". The following methods
+   * change the interpretation of various (non-APPLY_UF) kinds to one of the
+   * above categories and should be called by the theories that own the kind
+   * during Theory::finishInit. We set APPLY_UF to be semi-interpreted when
+   * this model does not enabled function values (this is the case for the model
+   * of TheoryEngine when the option assignFunctionValues is set to false).
+   */
+  void setUnevaluatedKind(Kind k);
+  void setSemiEvaluatedKind(Kind k);
   //---------------------------- end building the model
 
   // ------------------- general equality queries
@@ -217,6 +261,8 @@ public:
   std::map< Node, std::vector< Node > > d_uf_terms;
   /** a map from functions f to a list of all HO_APPLY terms with first argument f */
   std::map< Node, std::vector< Node > > d_ho_uf_terms;
+  /** are function values enabled? */
+  bool areFunctionValuesEnabled() const;
   /** assign function value f to definition f_def */
   void assignFunctionDefinition( Node f, Node f_def );
   /** have we assigned function f? */
@@ -245,6 +291,10 @@ public:
   std::map<Node, Node> d_approximations;
   /** list of all approximations */
   std::vector<std::pair<Node, Node> > d_approx_list;
+  /** a set of kinds that are not evaluated */
+  std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds;
+  /** a set of kinds that are semi-evaluated */
+  std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
   /** map of representatives of equality engine to used representatives in
    * representative set */
   std::map<Node, Node> d_reps;
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index e88d1e3be..f91a413e3 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -930,7 +930,10 @@ bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
 
 bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
 {
-  assignFunctions(m);
+  if (m->areFunctionValuesEnabled())
+  {
+    assignFunctions(m);
+  }
   return true;
 }
 
@@ -1098,6 +1101,10 @@ struct sortTypeSize
 
 void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
 {
+  if (!options::assignFunctionValues())
+  {
+    return;
+  }
   Trace("model-builder") << "Assigning function values..." << std::endl;
   std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
 
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index f5748549e..851f43582 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -75,6 +75,10 @@ void TheoryUF::setMasterEqualityEngine(eq::EqualityEngine* eq) {
 }
 
 void TheoryUF::finishInit() {
+  // combined cardinality constraints are not evaluated in getModelValue
+  TheoryModel* tm = d_valuation.getModel();
+  Assert(tm != nullptr);
+  tm->setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
   // initialize the strong solver
   if (options::finiteModelFind() && options::ufssMode()!=UF_SS_NONE) {
     d_thss = new StrongSolverTheoryUF(getSatContext(), getUserContext(), *d_out, this);