Add isConst check for lambda expressions. (#1084)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 14 Sep 2017 00:26:35 +0000 (19:26 -0500)
committerAina Niemetz <aina.niemetz@gmail.com>
Thu, 14 Sep 2017 00:26:35 +0000 (17:26 -0700)
commitc4306288347e043091628b63797f9f54b0359a7c
tree6140c164ae44519d4828cbd161938e69321667da
parent1f11ea2b651aa6627f90d5be2afa225d07f56089
Add isConst check for lambda expressions. (#1084)

Add isConst check for lambda expressions by conversions to and from an Array representation where isConst is implemented. This enables check-model to succeed on higher-order benchmarks. Change the builtin rewriter for lambda to attempt to put lambdas into constant form. Update regression.
src/expr/node_manager.cpp
src/expr/node_manager.h
src/theory/builtin/kinds
src/theory/builtin/theory_builtin_rewriter.cpp
src/theory/builtin/theory_builtin_rewriter.h
src/theory/builtin/theory_builtin_type_rules.h
test/regress/regress0/print_lambda.cvc