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 /NEWS | |
| 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 'NEWS')
| -rw-r--r-- | NEWS | 4 |
1 files changed, 4 insertions, 0 deletions
@@ -3,6 +3,10 @@ This file contains a summary of important user-visible changes. Changes since 1.7 ================= +Improvements: +* API: Function definitions can now be requested to be global. If the `global` + parameter is set to true, they persist after popping the user context. + Changes: * API change: `SmtEngine::query()` has been renamed to `SmtEngine::checkEntailed()` and `Result::Validity` has been renamed to |