projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 55fd458) | patch
Optionally permit creation of non-flat function types (#6010)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 26 Feb 2021 17:44:23 +0000 (11:44 -0600)
committerGitHub <noreply@github.com>
Fri, 26 Feb 2021 17:44:23 +0000 (14:44 -0300)
commitcc052e096323a193b52a05c2400c0c4639ada5de
tree7df1a434c075a4359bca3b1378447017791982e4tree
parent55fd45841d2f51c5194b710d8d99ad43c2315c08commit | diff
Optionally permit creation of non-flat function types (#6010)

This is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
src/expr/node_manager.cpp diff | blob | history
src/expr/node_manager.h diff | blob | history