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 /src/parser/cvc | |
| 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 'src/parser/cvc')
| -rw-r--r-- | src/parser/cvc/Cvc.g | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index e604c7769..5d04a8cc0 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -943,7 +943,7 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd] cmd->reset( new DefineFunctionRecCommand(api::termVectorToExprs(funcs), eformals, - api::termVectorToExprs(formulas))); + api::termVectorToExprs(formulas), true)); } | toplevelDeclaration[cmd] ; @@ -1163,7 +1163,7 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::api::Sort& t, ExprManager::VAR_FLAG_GLOBAL | ExprManager::VAR_FLAG_DEFINED); PARSER_STATE->defineVar(*i, f); Command* decl = - new DefineFunctionCommand(*i, func.getExpr(), f.getExpr()); + new DefineFunctionCommand(*i, func.getExpr(), f.getExpr(), true); seq->addCommand(decl); } } |