diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-12-06 20:57:44 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-12-06 20:57:44 -0600 |
commit | 691abe521ea8a7e87db51e22880cf101d59bf3e7 (patch) | |
tree | a3e7e336a64597a03b3142bd6cd39c7d42322bec /src/smt/command.cpp | |
parent | a97411d90188fc3ceda419faf7be4b3508e305a5 (diff) |
Add command for define-fun-rec and add to API (#1412)
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 88 |
1 files changed, 88 insertions, 0 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index aea6365b7..ad7fd9af0 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -890,6 +890,94 @@ Command* DefineNamedFunctionCommand::clone() const { return new DefineNamedFunctionCommand(d_symbol, d_func, d_formals, d_formula); } +/* class DefineFunctionRecCommand */ + +DefineFunctionRecCommand::DefineFunctionRecCommand( + Expr func, const std::vector<Expr>& formals, Expr formula) throw() +{ + d_funcs.push_back(func); + d_formals.push_back(formals); + d_formulas.push_back(formula); +} + +DefineFunctionRecCommand::DefineFunctionRecCommand( + const std::vector<Expr>& funcs, + const std::vector<std::vector<Expr> >& formals, + const std::vector<Expr>& formulas) throw() +{ + 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 throw() +{ + return d_funcs; +} + +const std::vector<std::vector<Expr> >& DefineFunctionRecCommand::getFormals() + const throw() +{ + return d_formals; +} + +const std::vector<Expr>& DefineFunctionRecCommand::getFormulas() const throw() +{ + return d_formulas; +} + +void DefineFunctionRecCommand::invoke(SmtEngine* smtEngine) +{ + try + { + smtEngine->defineFunctionsRec(d_funcs, d_formals, d_formulas); + d_commandStatus = CommandSuccess::instance(); + } + catch (exception& e) + { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Command* DefineFunctionRecCommand::exportTo( + ExprManager* exprManager, ExprManagerMapCollection& variableMap) +{ + std::vector<Expr> funcs; + for (unsigned i = 0, size = d_funcs.size(); i < size; i++) + { + Expr func = d_funcs[i].exportTo( + exprManager, variableMap, /* flags = */ ExprManager::VAR_FLAG_DEFINED); + funcs.push_back(func); + } + std::vector<std::vector<Expr> > formals; + for (unsigned i = 0, size = d_formals.size(); i < size; i++) + { + std::vector<Expr> formals_c; + transform(d_formals[i].begin(), + d_formals[i].end(), + back_inserter(formals_c), + ExportTransformer(exprManager, variableMap)); + formals.push_back(formals_c); + } + std::vector<Expr> formulas; + for (unsigned i = 0, size = d_formulas.size(); i < size; i++) + { + Expr formula = d_formulas[i].exportTo(exprManager, variableMap); + formulas.push_back(formula); + } + return new DefineFunctionRecCommand(funcs, formals, formulas); +} + +Command* DefineFunctionRecCommand::clone() const +{ + return new DefineFunctionRecCommand(d_funcs, d_formals, d_formulas); +} + +std::string DefineFunctionRecCommand::getCommandName() const throw() +{ + return "define-fun-rec"; +} + /* class SetUserAttribute */ SetUserAttributeCommand::SetUserAttributeCommand( |