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/regress | |
| 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/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/smtlib/issue4552.smt2 | 27 |
2 files changed, 28 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 4bc9d2705..e0ce456bc 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -921,6 +921,7 @@ set(regress_0_tests regress0/smtlib/issue4028.smt2 regress0/smtlib/issue4077.smt2 regress0/smtlib/issue4151.smt2 + regress0/smtlib/issue4552.smt2 regress0/smtlib/reason-unknown.smt2 regress0/smtlib/reset.smt2 regress0/smtlib/reset-assertions1.smt2 diff --git a/test/regress/regress0/smtlib/issue4552.smt2 b/test/regress/regress0/smtlib/issue4552.smt2 new file mode 100644 index 000000000..af8e0b948 --- /dev/null +++ b/test/regress/regress0/smtlib/issue4552.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --incremental +; EXPECT: unsat +; EXPECT: unsat +; EXPECT: unsat +(set-logic UF) +(set-option :global-declarations true) + +(push) +(define a true) +(define (f (b Bool)) b) +(define-const a2 Bool true) + +(define-fun a3 () Bool true) + +(define-fun-rec b () Bool true) +(define-funs-rec ((g ((b Bool)) Bool)) (b)) +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) +(pop) + +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) + +(reset-assertions) + +(assert (or (not a) (not a2) (not a3) (not b) (g false))) +(check-sat) |