diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-13 19:26:35 -0500 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2017-09-13 17:26:35 -0700 |
commit | c4306288347e043091628b63797f9f54b0359a7c (patch) | |
tree | 6140c164ae44519d4828cbd161938e69321667da /src/expr/node_manager.h | |
parent | 1f11ea2b651aa6627f90d5be2afa225d07f56089 (diff) |
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.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index b1b0bc974..d5d296579 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -491,6 +491,9 @@ public: Node mkBoundVar(const TypeNode& type); Node* mkBoundVarPtr(const TypeNode& type); + /** get the canonical bound variable list for function type tn */ + static Node getBoundVarListForFunctionType( TypeNode tn ); + /** * Optional flags used to control behavior of NodeManager::mkSkolem(). * They should be composed with a bitwise OR (e.g., |