diff options
Diffstat (limited to 'src/smt/command.cpp')
-rw-r--r-- | src/smt/command.cpp | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp index d6ec0769a..89d7b5ca2 100644 --- a/src/smt/command.cpp +++ b/src/smt/command.cpp @@ -1233,6 +1233,60 @@ std::string GetSynthSolutionCommand::getCommandName() const throw() { return "get-instantiations"; } +/* class GetQuantifierEliminationCommand */ + +GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() throw() : + d_expr() { +} + +GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(const Expr& expr, bool doFull) throw() : + d_expr(expr), d_doFull(doFull) { +} + +Expr GetQuantifierEliminationCommand::getExpr() const throw() { + return d_expr; +} +bool GetQuantifierEliminationCommand::getDoFull() const throw() { + return d_doFull; +} + +void GetQuantifierEliminationCommand::invoke(SmtEngine* smtEngine) throw() { + try { + d_result = smtEngine->doQuantifierElimination(d_expr, d_doFull); + d_commandStatus = CommandSuccess::instance(); + } catch(exception& e) { + d_commandStatus = new CommandFailure(e.what()); + } +} + +Expr GetQuantifierEliminationCommand::getResult() const throw() { + return d_result; +} + +void GetQuantifierEliminationCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() { + if(! ok()) { + this->Command::printResult(out, verbosity); + } else { + out << d_result << endl; + } +} + +Command* GetQuantifierEliminationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) { + GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr.exportTo(exprManager, variableMap), d_doFull); + c->d_result = d_result; + return c; +} + +Command* GetQuantifierEliminationCommand::clone() const { + GetQuantifierEliminationCommand* c = new GetQuantifierEliminationCommand(d_expr, d_doFull); + c->d_result = d_result; + return c; +} + +std::string GetQuantifierEliminationCommand::getCommandName() const throw() { + return d_doFull ? "get-qe" : "get-qe-disjunct"; +} + /* class GetUnsatCoreCommand */ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() { |