diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-07 07:16:49 +0000 |
commit | 2d7ff62cd52c5c56f29b6567489310cc45767236 (patch) | |
tree | afb975f93b219e7b7a670a4dfc2897e425fd9bf7 /src/expr/command.cpp | |
parent | ce4a5fe6a2529f11eaff66b6cdcdb32ef5309323 (diff) |
SMT-LIBv2 (define-fun...) command now functional; does eager expansion at preprocessing time
Diffstat (limited to 'src/expr/command.cpp')
-rw-r--r-- | src/expr/command.cpp | 35 |
1 files changed, 18 insertions, 17 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp index a1486fcab..8c90f337e 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -23,6 +23,7 @@ #include "expr/command.h" #include "smt/smt_engine.h" +#include "smt/bad_option_exception.h" #include "util/output.h" using namespace std; @@ -217,26 +218,26 @@ void DeclarationCommand::toStream(std::ostream& out) const { /* class DefineFunctionCommand */ -DefineFunctionCommand::DefineFunctionCommand(const std::string& name, - const std::vector<std::pair<std::string, Type> >& args, - Type type, - Expr formula) : - d_name(name), - d_args(args), - d_type(type), +DefineFunctionCommand::DefineFunctionCommand(Expr func, + const std::vector<Expr>& formals, + Expr formula) : + d_func(func), + d_formals(formals), d_formula(formula) { } void DefineFunctionCommand::invoke(SmtEngine* smtEngine) { - smtEngine->defineFunction(d_name, d_args, d_type, d_formula); + smtEngine->defineFunction(d_func, d_formals, d_formula); } void DefineFunctionCommand::toStream(std::ostream& out) const { - out << "DefineFunction( \"" << d_name << "\", ["; - copy( d_args.begin(), d_args.end() - 1, - ostream_iterator<std::pair<std::string, Type> >(out, ", ") ); - out << d_args.back(); - out << "], << " << d_type << " >>, << " << d_formula << " >> )"; + out << "DefineFunction( \"" << d_func << "\", ["; + if(d_formals.size() > 0) { + copy( d_formals.begin(), d_formals.end() - 1, + ostream_iterator<Expr>(out, ", ") ); + out << d_formals.back(); + } + out << "], << " << d_formula << " >> )"; } /* class GetValueCommand */ @@ -324,7 +325,7 @@ void SetInfoCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setInfo(d_flag, d_sexpr); //d_result = "success"; - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -352,7 +353,7 @@ GetInfoCommand::GetInfoCommand(std::string flag) : void GetInfoCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getInfo(d_flag).getValue(); - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -382,7 +383,7 @@ void SetOptionCommand::invoke(SmtEngine* smtEngine) { try { smtEngine->setOption(d_flag, d_sexpr); //d_result = "success"; - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } @@ -410,7 +411,7 @@ GetOptionCommand::GetOptionCommand(std::string flag) : void GetOptionCommand::invoke(SmtEngine* smtEngine) { try { d_result = smtEngine->getOption(d_flag).getValue(); - } catch(BadOption& bo) { + } catch(BadOptionException& bo) { d_result = "unsupported"; } } |