diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-06 01:24:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-06 01:24:17 -0700 |
commit | fd60da4a22f02f6f5b82cef3585240c1b33595e9 (patch) | |
tree | 137d45e65f204c2f604fed65d47a7d7b4f716c78 /test/unit/memory.h | |
parent | 6a61c1a75b08867c7c06623b8c03084056b6bed7 (diff) |
Keep definitions when global-declarations enabled (#4572)
Fixes #4552. Fixes #4555. The SMT-LIB standard mandates that definitions
are kept when `:global-declarations` are enabled. Until now, CVC4 was
keeping track of the symbols of a definition correctly but lost the body
of the definition when the user context was popped. This commit fixes
the issue by adding a `global` parameter to
`SmtEngine::defineFunction()` and `SmtEngine::defineFunctionRec()`. If
that parameter is set, the definitions of functions are added at level 0
to `d_definedFunctions` and the lemmas for recursive function
definitions are kept in an additional list and asserted during each
`checkSat` call. The commit also updates new API, the commands, and the
parsers to reflect this change.
Diffstat (limited to 'test/unit/memory.h')
0 files changed, 0 insertions, 0 deletions