From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Jun 2021 23:26:58 +0000 (-0500)
Subject: Avoid full normalization of lambdas in getValue (#6787)
X-Git-Tag: cvc5-1.0.0~1568
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=21ee0f18c288d430d08c133f601173be25411187;p=cvc5.git

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 8eec7f911..3e902463c 100644
--- 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 c6ca206fc..8f197cd04 100644
--- 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)