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/smt/command.cpp | |
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/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 47 |
1 files changed, 28 insertions, 19 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index 20f2dcff9..9fd0122fc 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1266,22 +1266,27 @@ std::string DefineTypeCommand::getCommandName() const { return "define-sort"; } DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, - Expr formula) + Expr formula, + bool global) : DeclarationDefinitionCommand(id), d_func(func), d_formals(), - d_formula(formula) + d_formula(formula), + d_global(global) { } DefineFunctionCommand::DefineFunctionCommand(const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) + Expr formula, + bool global) : DeclarationDefinitionCommand(id), d_func(func), d_formals(formals), - d_formula(formula) + d_formula(formula), + d_global(global) + { } @@ -1298,7 +1303,7 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { if (!d_func.isNull()) { - smtEngine->defineFunction(d_func, d_formals, d_formula); + smtEngine->defineFunction(d_func, d_formals, d_formula, d_global); } d_commandStatus = CommandSuccess::instance(); } @@ -1319,12 +1324,13 @@ Command* DefineFunctionCommand::exportTo(ExprManager* exprManager, back_inserter(formals), ExportTransformer(exprManager, variableMap)); Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineFunctionCommand(d_symbol, func, formals, formula); + return new DefineFunctionCommand(d_symbol, func, formals, formula, d_global); } Command* DefineFunctionCommand::clone() const { - return new DefineFunctionCommand(d_symbol, d_func, d_formals, d_formula); + return new DefineFunctionCommand( + d_symbol, d_func, d_formals, d_formula, d_global); } std::string DefineFunctionCommand::getCommandName() const @@ -1340,8 +1346,9 @@ DefineNamedFunctionCommand::DefineNamedFunctionCommand( const std::string& id, Expr func, const std::vector<Expr>& formals, - Expr formula) - : DefineFunctionCommand(id, func, formals, formula) + Expr formula, + bool global) + : DefineFunctionCommand(id, func, formals, formula, global) { } @@ -1365,12 +1372,14 @@ Command* DefineNamedFunctionCommand::exportTo( back_inserter(formals), ExportTransformer(exprManager, variableMap)); Expr formula = d_formula.exportTo(exprManager, variableMap); - return new DefineNamedFunctionCommand(d_symbol, func, formals, formula); + return new DefineNamedFunctionCommand( + d_symbol, func, formals, formula, d_global); } Command* DefineNamedFunctionCommand::clone() const { - return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); + return new DefineNamedFunctionCommand( + d_symbol, d_func, d_formals, d_formula, d_global); } /* -------------------------------------------------------------------------- */ @@ -1378,7 +1387,8 @@ Command* DefineNamedFunctionCommand::clone() const /* -------------------------------------------------------------------------- */ DefineFunctionRecCommand::DefineFunctionRecCommand( - Expr func, const std::vector<Expr>& formals, Expr formula) + Expr func, const std::vector<Expr>& formals, Expr formula, bool global) + : d_global(global) { d_funcs.push_back(func); d_formals.push_back(formals); @@ -1388,11 +1398,10 @@ DefineFunctionRecCommand::DefineFunctionRecCommand( DefineFunctionRecCommand::DefineFunctionRecCommand( const std::vector<Expr>& funcs, const std::vector<std::vector<Expr>>& formals, - const std::vector<Expr>& formulas) + const std::vector<Expr>& formulas, + bool global) + : d_funcs(funcs), d_formals(formals), d_formulas(formulas), d_global(global) { - d_funcs.insert(d_funcs.end(), funcs.begin(), funcs.end()); - d_formals.insert(d_formals.end(), formals.begin(), formals.end()); - d_formulas.insert(d_formulas.end(), formulas.begin(), formulas.end()); } const std::vector<Expr>& DefineFunctionRecCommand::getFunctions() const @@ -1415,7 +1424,7 @@ void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine) { try { - smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas); + smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas, d_global); d_commandStatus = CommandSuccess::instance(); } catch (exception& e) @@ -1450,12 +1459,12 @@ Command* DefineFunctionRecCommand::exportTo( Expr formula = d_formulas[i].exportTo(exprManager, variableMap); formulas.push_back(formula); } - return new DefineFunctionRecCommand(funcs, formals, formulas); + return new DefineFunctionRecCommand(funcs, formals, formulas, d_global); } Command* DefineFunctionRecCommand::clone() const { - return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas); + return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas, d_global); } std::string DefineFunctionRecCommand::getCommandName() const |