projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 39f90ff) | patch
Avoid full normalization of lambdas in getValue (#6787)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 22 Jun 2021 23:26:58 +0000 (18:26 -0500)
committerGitHub <noreply@github.com>
Tue, 22 Jun 2021 23:26:58 +0000 (23:26 +0000)
commit21ee0f18c288d430d08c133f601173be25411187
tree6fdfc41ca511f19e80e6e5bb37c7be7a8fede581tree
parent39f90ff035a5e5024fe0cd11b965f1103d83e88dcommit | 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.
src/theory/theory_model.cpp diff | blob | history
test/regress/regress0/define-fun-model.smt2 diff | blob | history