diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-22 18:26:58 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-22 23:26:58 +0000 |
commit | 21ee0f18c288d430d08c133f601173be25411187 (patch) | |
tree | 6fdfc41ca511f19e80e6e5bb37c7be7a8fede581 | |
parent | 39f90ff035a5e5024fe0cd11b965f1103d83e88d (diff) |
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.
-rw-r--r-- | src/theory/theory_model.cpp | 18 | ||||
-rw-r--r-- | test/regress/regress0/define-fun-model.smt2 | 6 |
2 files changed, 19 insertions, 5 deletions
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) |