Avoid full normalization of lambdas in getValue (#6787)

This ensures that we don't apply lambda rewriting, which involves array value normalization, to lambda terms returned by TheoryModel::getValue.

This can significantly speed up our time to return function terms for getValue.

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 8eec7f911ffd7931301277216893cb9f37b246a2..3e902463cc2513daf5d63916d0d1da14d05a5bf9 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -142,8 +142,22 @@ Node TheoryModel::getValue(TNode n) const
   Debug("model-getvalue-debug") << "[model-getvalue] getValue : substitute " << n << " to " << nn << std::endl;
   //get value in model
   nn = getModelValue(nn);
-  if (nn.isNull()) return nn;
-  if(options::condenseFunctionValues() || nn.getKind() != kind::LAMBDA) {
+  if (nn.isNull())
+  {
+    return nn;
+  }
+  else if (nn.getKind() == kind::LAMBDA)
+  {
+    if (options::condenseFunctionValues())
+    {
+      // normalize the body. Do not normalize the entire node, which
+      // involves array normalization.
+      NodeManager* nm = NodeManager::currentNM();
+      nn = nm->mkNode(kind::LAMBDA, nn[0], Rewriter::rewrite(nn[1]));
+    }
+  }
+  else
+  {
     //normalize
     nn = Rewriter::rewrite(nn);
   }

diff --git a/test/regress/regress0/define-fun-model.smt2 b/test/regress/regress0/define-fun-model.smt2
index c6ca206fc74bc3ad14726141c401b09bc5e902dd..8f197cd04decd09c4e880c2a5046cfcd0c7a8403 100644 (file)
--- a/test/regress/regress0/define-fun-model.smt2
+++ b/test/regress/regress0/define-fun-model.smt2
@@ -1,8 +1,8 @@
-; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/BOUND_VARIABLE/'
+; SCRUBBER: sed -e 's/BOUND_VARIABLE_[0-9]*/V/; s/_arg_[0-9]*/V/'
 ; EXPECT: sat
 ; EXPECT: (((f 4) 7))
-; EXPECT: ((g (lambda ((BOUND_VARIABLE Int)) 7)))
-; EXPECT: ((f (lambda ((BOUND_VARIABLE Int)) 7)))
+; EXPECT: ((g (lambda ((V Int)) 7)))
+; EXPECT: ((f (lambda ((V Int)) 7)))
 (set-logic UFLIA)
 (set-option :produce-models true)
 (define-fun f ((x Int)) Int 7)