1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Morgan Deters, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Implementation of command objects.
14 ** Implementation of command objects.
17 #include "smt/command.h"
26 #include "base/cvc4_assert.h"
27 #include "base/output.h"
28 #include "expr/expr_iomanip.h"
29 #include "expr/node.h"
30 #include "options/options.h"
31 #include "options/smt_options.h"
32 #include "printer/printer.h"
34 #include "smt/model.h"
35 #include "smt/smt_engine.h"
36 #include "smt/smt_engine_scope.h"
37 #include "util/sexpr.h"
38 #include "util/utility.h"
46 std::vector
<Expr
> ExportTo(ExprManager
* exprManager
,
47 ExprManagerMapCollection
& variableMap
,
48 const std::vector
<Expr
>& exprs
)
50 std::vector
<Expr
> exported
;
51 exported
.reserve(exprs
.size());
52 for (const Expr
& expr
: exprs
)
54 exported
.push_back(expr
.exportTo(exprManager
, variableMap
));
61 const int CommandPrintSuccess::s_iosIndex
= std::ios_base::xalloc();
62 const CommandSuccess
* CommandSuccess::s_instance
= new CommandSuccess();
63 const CommandInterrupted
* CommandInterrupted::s_instance
=
64 new CommandInterrupted();
66 std::ostream
& operator<<(std::ostream
& out
, const Command
& c
)
69 Node::setdepth::getDepth(out
),
70 Node::printtypes::getPrintTypes(out
),
71 Node::dag::getDag(out
),
72 Node::setlanguage::getLanguage(out
));
76 ostream
& operator<<(ostream
& out
, const Command
* c
)
89 std::ostream
& operator<<(std::ostream
& out
, const CommandStatus
& s
)
91 s
.toStream(out
, Node::setlanguage::getLanguage(out
));
95 ostream
& operator<<(ostream
& out
, const CommandStatus
* s
)
109 /* output stream insertion operator for benchmark statuses */
110 std::ostream
& operator<<(std::ostream
& out
, BenchmarkStatus status
)
114 case SMT_SATISFIABLE
: return out
<< "sat";
116 case SMT_UNSATISFIABLE
: return out
<< "unsat";
118 case SMT_UNKNOWN
: return out
<< "unknown";
120 default: return out
<< "BenchmarkStatus::[UNKNOWNSTATUS!]";
124 /* -------------------------------------------------------------------------- */
125 /* class CommandPrintSuccess */
126 /* -------------------------------------------------------------------------- */
128 void CommandPrintSuccess::applyPrintSuccess(std::ostream
& out
)
130 out
.iword(s_iosIndex
) = d_printSuccess
;
133 bool CommandPrintSuccess::getPrintSuccess(std::ostream
& out
)
135 return out
.iword(s_iosIndex
);
138 void CommandPrintSuccess::setPrintSuccess(std::ostream
& out
, bool printSuccess
)
140 out
.iword(s_iosIndex
) = printSuccess
;
143 std::ostream
& operator<<(std::ostream
& out
, CommandPrintSuccess cps
)
145 cps
.applyPrintSuccess(out
);
149 /* -------------------------------------------------------------------------- */
151 /* -------------------------------------------------------------------------- */
153 Command::Command() : d_commandStatus(NULL
), d_muted(false) {}
154 Command::Command(const Command
& cmd
)
157 (cmd
.d_commandStatus
== NULL
) ? NULL
: &cmd
.d_commandStatus
->clone();
158 d_muted
= cmd
.d_muted
;
163 if (d_commandStatus
!= NULL
&& d_commandStatus
!= CommandSuccess::instance())
165 delete d_commandStatus
;
169 bool Command::ok() const
171 // either we haven't run the command yet, or it ran successfully
172 return d_commandStatus
== NULL
173 || dynamic_cast<const CommandSuccess
*>(d_commandStatus
) != NULL
;
176 bool Command::fail() const
178 return d_commandStatus
!= NULL
179 && dynamic_cast<const CommandFailure
*>(d_commandStatus
) != NULL
;
182 bool Command::interrupted() const
184 return d_commandStatus
!= NULL
185 && dynamic_cast<const CommandInterrupted
*>(d_commandStatus
) != NULL
;
188 void Command::invoke(SmtEngine
* smtEngine
, std::ostream
& out
)
191 if (!(isMuted() && ok()))
194 smtEngine
->getOption("command-verbosity:" + getCommandName())
200 std::string
Command::toString() const
202 std::stringstream ss
;
207 void Command::toStream(std::ostream
& out
,
211 OutputLanguage language
) const
213 Printer::getPrinter(language
)->toStream(out
, this, toDepth
, types
, dag
);
216 void CommandStatus::toStream(std::ostream
& out
, OutputLanguage language
) const
218 Printer::getPrinter(language
)->toStream(out
, this);
221 void Command::printResult(std::ostream
& out
, uint32_t verbosity
) const
223 if (d_commandStatus
!= NULL
)
225 if ((!ok() && verbosity
>= 1) || verbosity
>= 2)
227 out
<< *d_commandStatus
;
232 /* -------------------------------------------------------------------------- */
233 /* class EmptyCommand */
234 /* -------------------------------------------------------------------------- */
236 EmptyCommand::EmptyCommand(std::string name
) : d_name(name
) {}
237 std::string
EmptyCommand::getName() const { return d_name
; }
238 void EmptyCommand::invoke(SmtEngine
* smtEngine
)
240 /* empty commands have no implementation */
241 d_commandStatus
= CommandSuccess::instance();
244 Command
* EmptyCommand::exportTo(ExprManager
* exprManager
,
245 ExprManagerMapCollection
& variableMap
)
247 return new EmptyCommand(d_name
);
250 Command
* EmptyCommand::clone() const { return new EmptyCommand(d_name
); }
251 std::string
EmptyCommand::getCommandName() const { return "empty"; }
253 /* -------------------------------------------------------------------------- */
254 /* class EchoCommand */
255 /* -------------------------------------------------------------------------- */
257 EchoCommand::EchoCommand(std::string output
) : d_output(output
) {}
258 std::string
EchoCommand::getOutput() const { return d_output
; }
259 void EchoCommand::invoke(SmtEngine
* smtEngine
)
261 /* we don't have an output stream here, nothing to do */
262 d_commandStatus
= CommandSuccess::instance();
265 void EchoCommand::invoke(SmtEngine
* smtEngine
, std::ostream
& out
)
267 out
<< d_output
<< std::endl
;
268 d_commandStatus
= CommandSuccess::instance();
270 smtEngine
->getOption("command-verbosity:" + getCommandName())
275 Command
* EchoCommand::exportTo(ExprManager
* exprManager
,
276 ExprManagerMapCollection
& variableMap
)
278 return new EchoCommand(d_output
);
281 Command
* EchoCommand::clone() const { return new EchoCommand(d_output
); }
282 std::string
EchoCommand::getCommandName() const { return "echo"; }
284 /* -------------------------------------------------------------------------- */
285 /* class AssertCommand */
286 /* -------------------------------------------------------------------------- */
288 AssertCommand::AssertCommand(const Expr
& e
, bool inUnsatCore
)
289 : d_expr(e
), d_inUnsatCore(inUnsatCore
)
293 Expr
AssertCommand::getExpr() const { return d_expr
; }
294 void AssertCommand::invoke(SmtEngine
* smtEngine
)
298 smtEngine
->assertFormula(d_expr
, d_inUnsatCore
);
299 d_commandStatus
= CommandSuccess::instance();
301 catch (UnsafeInterruptException
& e
)
303 d_commandStatus
= new CommandInterrupted();
307 d_commandStatus
= new CommandFailure(e
.what());
311 Command
* AssertCommand::exportTo(ExprManager
* exprManager
,
312 ExprManagerMapCollection
& variableMap
)
314 return new AssertCommand(d_expr
.exportTo(exprManager
, variableMap
),
318 Command
* AssertCommand::clone() const
320 return new AssertCommand(d_expr
, d_inUnsatCore
);
323 std::string
AssertCommand::getCommandName() const { return "assert"; }
325 /* -------------------------------------------------------------------------- */
326 /* class PushCommand */
327 /* -------------------------------------------------------------------------- */
329 void PushCommand::invoke(SmtEngine
* smtEngine
)
334 d_commandStatus
= CommandSuccess::instance();
336 catch (UnsafeInterruptException
& e
)
338 d_commandStatus
= new CommandInterrupted();
342 d_commandStatus
= new CommandFailure(e
.what());
346 Command
* PushCommand::exportTo(ExprManager
* exprManager
,
347 ExprManagerMapCollection
& variableMap
)
349 return new PushCommand();
352 Command
* PushCommand::clone() const { return new PushCommand(); }
353 std::string
PushCommand::getCommandName() const { return "push"; }
355 /* -------------------------------------------------------------------------- */
356 /* class PopCommand */
357 /* -------------------------------------------------------------------------- */
359 void PopCommand::invoke(SmtEngine
* smtEngine
)
364 d_commandStatus
= CommandSuccess::instance();
366 catch (UnsafeInterruptException
& e
)
368 d_commandStatus
= new CommandInterrupted();
372 d_commandStatus
= new CommandFailure(e
.what());
376 Command
* PopCommand::exportTo(ExprManager
* exprManager
,
377 ExprManagerMapCollection
& variableMap
)
379 return new PopCommand();
382 Command
* PopCommand::clone() const { return new PopCommand(); }
383 std::string
PopCommand::getCommandName() const { return "pop"; }
385 /* -------------------------------------------------------------------------- */
386 /* class CheckSatCommand */
387 /* -------------------------------------------------------------------------- */
389 CheckSatCommand::CheckSatCommand() : d_expr() {}
390 CheckSatCommand::CheckSatCommand(const Expr
& expr
, bool inUnsatCore
)
391 : d_expr(expr
), d_inUnsatCore(inUnsatCore
)
395 Expr
CheckSatCommand::getExpr() const { return d_expr
; }
396 void CheckSatCommand::invoke(SmtEngine
* smtEngine
)
400 d_result
= smtEngine
->checkSat(d_expr
);
401 d_commandStatus
= CommandSuccess::instance();
405 d_commandStatus
= new CommandFailure(e
.what());
409 Result
CheckSatCommand::getResult() const { return d_result
; }
410 void CheckSatCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
414 this->Command::printResult(out
, verbosity
);
418 out
<< d_result
<< endl
;
422 Command
* CheckSatCommand::exportTo(ExprManager
* exprManager
,
423 ExprManagerMapCollection
& variableMap
)
425 CheckSatCommand
* c
= new CheckSatCommand(
426 d_expr
.exportTo(exprManager
, variableMap
), d_inUnsatCore
);
427 c
->d_result
= d_result
;
431 Command
* CheckSatCommand::clone() const
433 CheckSatCommand
* c
= new CheckSatCommand(d_expr
, d_inUnsatCore
);
434 c
->d_result
= d_result
;
438 std::string
CheckSatCommand::getCommandName() const { return "check-sat"; }
440 /* -------------------------------------------------------------------------- */
441 /* class CheckSatAssumingCommand */
442 /* -------------------------------------------------------------------------- */
444 CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term
) : d_terms()
446 d_terms
.push_back(term
);
449 CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector
<Expr
>& terms
,
451 : d_terms(terms
), d_inUnsatCore(inUnsatCore
)
455 const std::vector
<Expr
>& CheckSatAssumingCommand::getTerms() const
460 void CheckSatAssumingCommand::invoke(SmtEngine
* smtEngine
)
464 d_result
= smtEngine
->checkSat(d_terms
);
465 d_commandStatus
= CommandSuccess::instance();
469 d_commandStatus
= new CommandFailure(e
.what());
473 Result
CheckSatAssumingCommand::getResult() const
478 void CheckSatAssumingCommand::printResult(std::ostream
& out
,
479 uint32_t verbosity
) const
483 this->Command::printResult(out
, verbosity
);
487 out
<< d_result
<< endl
;
491 Command
* CheckSatAssumingCommand::exportTo(
492 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
494 vector
<Expr
> exportedTerms
;
495 for (const Expr
& e
: d_terms
)
497 exportedTerms
.push_back(e
.exportTo(exprManager
, variableMap
));
499 CheckSatAssumingCommand
* c
=
500 new CheckSatAssumingCommand(exportedTerms
, d_inUnsatCore
);
501 c
->d_result
= d_result
;
505 Command
* CheckSatAssumingCommand::clone() const
507 CheckSatAssumingCommand
* c
=
508 new CheckSatAssumingCommand(d_terms
, d_inUnsatCore
);
509 c
->d_result
= d_result
;
513 std::string
CheckSatAssumingCommand::getCommandName() const
515 return "check-sat-assuming";
518 /* -------------------------------------------------------------------------- */
519 /* class QueryCommand */
520 /* -------------------------------------------------------------------------- */
522 QueryCommand::QueryCommand(const Expr
& e
, bool inUnsatCore
)
523 : d_expr(e
), d_inUnsatCore(inUnsatCore
)
527 Expr
QueryCommand::getExpr() const { return d_expr
; }
528 void QueryCommand::invoke(SmtEngine
* smtEngine
)
532 d_result
= smtEngine
->query(d_expr
);
533 d_commandStatus
= CommandSuccess::instance();
537 d_commandStatus
= new CommandFailure(e
.what());
541 Result
QueryCommand::getResult() const { return d_result
; }
542 void QueryCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
546 this->Command::printResult(out
, verbosity
);
550 out
<< d_result
<< endl
;
554 Command
* QueryCommand::exportTo(ExprManager
* exprManager
,
555 ExprManagerMapCollection
& variableMap
)
557 QueryCommand
* c
= new QueryCommand(d_expr
.exportTo(exprManager
, variableMap
),
559 c
->d_result
= d_result
;
563 Command
* QueryCommand::clone() const
565 QueryCommand
* c
= new QueryCommand(d_expr
, d_inUnsatCore
);
566 c
->d_result
= d_result
;
570 std::string
QueryCommand::getCommandName() const { return "query"; }
572 /* -------------------------------------------------------------------------- */
573 /* class CheckSynthCommand */
574 /* -------------------------------------------------------------------------- */
576 CheckSynthCommand::CheckSynthCommand() : d_expr() {}
577 CheckSynthCommand::CheckSynthCommand(const Expr
& expr
) : d_expr(expr
) {}
578 Expr
CheckSynthCommand::getExpr() const { return d_expr
; }
579 void CheckSynthCommand::invoke(SmtEngine
* smtEngine
)
583 d_result
= smtEngine
->checkSynth(d_expr
);
584 d_commandStatus
= CommandSuccess::instance();
585 smt::SmtScope
scope(smtEngine
);
587 // check whether we should print the status
588 if (d_result
.asSatisfiabilityResult() != Result::UNSAT
589 || options::sygusOut() == SYGUS_SOL_OUT_STATUS_AND_DEF
590 || options::sygusOut() == SYGUS_SOL_OUT_STATUS
)
592 if (options::sygusOut() == SYGUS_SOL_OUT_STANDARD
)
594 d_solution
<< "(fail)" << endl
;
598 d_solution
<< d_result
<< endl
;
601 // check whether we should print the solution
602 if (d_result
.asSatisfiabilityResult() == Result::UNSAT
603 && options::sygusOut() != SYGUS_SOL_OUT_STATUS
)
605 // printing a synthesis solution is a non-constant
606 // method, since it invokes a sophisticated algorithm
607 // (Figure 5 of Reynolds et al. CAV 2015).
608 // Hence, we must call here print solution here,
609 // instead of during printResult.
610 smtEngine
->printSynthSolution(d_solution
);
615 d_commandStatus
= new CommandFailure(e
.what());
619 Result
CheckSynthCommand::getResult() const { return d_result
; }
620 void CheckSynthCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
624 this->Command::printResult(out
, verbosity
);
628 out
<< d_solution
.str();
632 Command
* CheckSynthCommand::exportTo(ExprManager
* exprManager
,
633 ExprManagerMapCollection
& variableMap
)
635 CheckSynthCommand
* c
=
636 new CheckSynthCommand(d_expr
.exportTo(exprManager
, variableMap
));
637 c
->d_result
= d_result
;
641 Command
* CheckSynthCommand::clone() const
643 CheckSynthCommand
* c
= new CheckSynthCommand(d_expr
);
644 c
->d_result
= d_result
;
648 std::string
CheckSynthCommand::getCommandName() const { return "check-synth"; }
650 /* -------------------------------------------------------------------------- */
651 /* class ResetCommand */
652 /* -------------------------------------------------------------------------- */
654 void ResetCommand::invoke(SmtEngine
* smtEngine
)
659 d_commandStatus
= CommandSuccess::instance();
663 d_commandStatus
= new CommandFailure(e
.what());
667 Command
* ResetCommand::exportTo(ExprManager
* exprManager
,
668 ExprManagerMapCollection
& variableMap
)
670 return new ResetCommand();
673 Command
* ResetCommand::clone() const { return new ResetCommand(); }
674 std::string
ResetCommand::getCommandName() const { return "reset"; }
676 /* -------------------------------------------------------------------------- */
677 /* class ResetAssertionsCommand */
678 /* -------------------------------------------------------------------------- */
680 void ResetAssertionsCommand::invoke(SmtEngine
* smtEngine
)
684 smtEngine
->resetAssertions();
685 d_commandStatus
= CommandSuccess::instance();
689 d_commandStatus
= new CommandFailure(e
.what());
693 Command
* ResetAssertionsCommand::exportTo(ExprManager
* exprManager
,
694 ExprManagerMapCollection
& variableMap
)
696 return new ResetAssertionsCommand();
699 Command
* ResetAssertionsCommand::clone() const
701 return new ResetAssertionsCommand();
704 std::string
ResetAssertionsCommand::getCommandName() const
706 return "reset-assertions";
709 /* -------------------------------------------------------------------------- */
710 /* class QuitCommand */
711 /* -------------------------------------------------------------------------- */
713 void QuitCommand::invoke(SmtEngine
* smtEngine
)
715 Dump("benchmark") << *this;
716 d_commandStatus
= CommandSuccess::instance();
719 Command
* QuitCommand::exportTo(ExprManager
* exprManager
,
720 ExprManagerMapCollection
& variableMap
)
722 return new QuitCommand();
725 Command
* QuitCommand::clone() const { return new QuitCommand(); }
726 std::string
QuitCommand::getCommandName() const { return "exit"; }
728 /* -------------------------------------------------------------------------- */
729 /* class CommentCommand */
730 /* -------------------------------------------------------------------------- */
732 CommentCommand::CommentCommand(std::string comment
) : d_comment(comment
) {}
733 std::string
CommentCommand::getComment() const { return d_comment
; }
734 void CommentCommand::invoke(SmtEngine
* smtEngine
)
736 Dump("benchmark") << *this;
737 d_commandStatus
= CommandSuccess::instance();
740 Command
* CommentCommand::exportTo(ExprManager
* exprManager
,
741 ExprManagerMapCollection
& variableMap
)
743 return new CommentCommand(d_comment
);
746 Command
* CommentCommand::clone() const { return new CommentCommand(d_comment
); }
747 std::string
CommentCommand::getCommandName() const { return "comment"; }
749 /* -------------------------------------------------------------------------- */
750 /* class CommandSequence */
751 /* -------------------------------------------------------------------------- */
753 CommandSequence::CommandSequence() : d_index(0) {}
754 CommandSequence::~CommandSequence()
756 for (unsigned i
= d_index
; i
< d_commandSequence
.size(); ++i
)
758 delete d_commandSequence
[i
];
762 void CommandSequence::addCommand(Command
* cmd
)
764 d_commandSequence
.push_back(cmd
);
767 void CommandSequence::clear() { d_commandSequence
.clear(); }
768 void CommandSequence::invoke(SmtEngine
* smtEngine
)
770 for (; d_index
< d_commandSequence
.size(); ++d_index
)
772 d_commandSequence
[d_index
]->invoke(smtEngine
);
773 if (!d_commandSequence
[d_index
]->ok())
776 d_commandStatus
= d_commandSequence
[d_index
]->getCommandStatus();
779 delete d_commandSequence
[d_index
];
782 AlwaysAssert(d_commandStatus
== NULL
);
783 d_commandStatus
= CommandSuccess::instance();
786 void CommandSequence::invoke(SmtEngine
* smtEngine
, std::ostream
& out
)
788 for (; d_index
< d_commandSequence
.size(); ++d_index
)
790 d_commandSequence
[d_index
]->invoke(smtEngine
, out
);
791 if (!d_commandSequence
[d_index
]->ok())
794 d_commandStatus
= d_commandSequence
[d_index
]->getCommandStatus();
797 delete d_commandSequence
[d_index
];
800 AlwaysAssert(d_commandStatus
== NULL
);
801 d_commandStatus
= CommandSuccess::instance();
804 Command
* CommandSequence::exportTo(ExprManager
* exprManager
,
805 ExprManagerMapCollection
& variableMap
)
807 CommandSequence
* seq
= new CommandSequence();
808 for (iterator i
= begin(); i
!= end(); ++i
)
810 Command
* cmd_to_export
= *i
;
811 Command
* cmd
= cmd_to_export
->exportTo(exprManager
, variableMap
);
812 seq
->addCommand(cmd
);
813 Debug("export") << "[export] so far converted: " << seq
<< endl
;
815 seq
->d_index
= d_index
;
819 Command
* CommandSequence::clone() const
821 CommandSequence
* seq
= new CommandSequence();
822 for (const_iterator i
= begin(); i
!= end(); ++i
)
824 seq
->addCommand((*i
)->clone());
826 seq
->d_index
= d_index
;
830 CommandSequence::const_iterator
CommandSequence::begin() const
832 return d_commandSequence
.begin();
835 CommandSequence::const_iterator
CommandSequence::end() const
837 return d_commandSequence
.end();
840 CommandSequence::iterator
CommandSequence::begin()
842 return d_commandSequence
.begin();
845 CommandSequence::iterator
CommandSequence::end()
847 return d_commandSequence
.end();
850 std::string
CommandSequence::getCommandName() const { return "sequence"; }
852 /* -------------------------------------------------------------------------- */
853 /* class DeclarationDefinitionCommand */
854 /* -------------------------------------------------------------------------- */
856 DeclarationDefinitionCommand::DeclarationDefinitionCommand(
857 const std::string
& id
)
862 std::string
DeclarationDefinitionCommand::getSymbol() const { return d_symbol
; }
864 /* -------------------------------------------------------------------------- */
865 /* class DeclareFunctionCommand */
866 /* -------------------------------------------------------------------------- */
868 DeclareFunctionCommand::DeclareFunctionCommand(const std::string
& id
,
871 : DeclarationDefinitionCommand(id
),
874 d_printInModel(true),
875 d_printInModelSetByUser(false)
879 Expr
DeclareFunctionCommand::getFunction() const { return d_func
; }
880 Type
DeclareFunctionCommand::getType() const { return d_type
; }
881 bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel
; }
882 bool DeclareFunctionCommand::getPrintInModelSetByUser() const
884 return d_printInModelSetByUser
;
887 void DeclareFunctionCommand::setPrintInModel(bool p
)
890 d_printInModelSetByUser
= true;
893 void DeclareFunctionCommand::invoke(SmtEngine
* smtEngine
)
895 d_commandStatus
= CommandSuccess::instance();
898 Command
* DeclareFunctionCommand::exportTo(ExprManager
* exprManager
,
899 ExprManagerMapCollection
& variableMap
)
901 DeclareFunctionCommand
* dfc
=
902 new DeclareFunctionCommand(d_symbol
,
903 d_func
.exportTo(exprManager
, variableMap
),
904 d_type
.exportTo(exprManager
, variableMap
));
905 dfc
->d_printInModel
= d_printInModel
;
906 dfc
->d_printInModelSetByUser
= d_printInModelSetByUser
;
910 Command
* DeclareFunctionCommand::clone() const
912 DeclareFunctionCommand
* dfc
=
913 new DeclareFunctionCommand(d_symbol
, d_func
, d_type
);
914 dfc
->d_printInModel
= d_printInModel
;
915 dfc
->d_printInModelSetByUser
= d_printInModelSetByUser
;
919 std::string
DeclareFunctionCommand::getCommandName() const
921 return "declare-fun";
924 /* -------------------------------------------------------------------------- */
925 /* class DeclareTypeCommand */
926 /* -------------------------------------------------------------------------- */
928 DeclareTypeCommand::DeclareTypeCommand(const std::string
& id
,
931 : DeclarationDefinitionCommand(id
), d_arity(arity
), d_type(t
)
935 size_t DeclareTypeCommand::getArity() const { return d_arity
; }
936 Type
DeclareTypeCommand::getType() const { return d_type
; }
937 void DeclareTypeCommand::invoke(SmtEngine
* smtEngine
)
939 d_commandStatus
= CommandSuccess::instance();
942 Command
* DeclareTypeCommand::exportTo(ExprManager
* exprManager
,
943 ExprManagerMapCollection
& variableMap
)
945 return new DeclareTypeCommand(
946 d_symbol
, d_arity
, d_type
.exportTo(exprManager
, variableMap
));
949 Command
* DeclareTypeCommand::clone() const
951 return new DeclareTypeCommand(d_symbol
, d_arity
, d_type
);
954 std::string
DeclareTypeCommand::getCommandName() const
956 return "declare-sort";
959 /* -------------------------------------------------------------------------- */
960 /* class DefineTypeCommand */
961 /* -------------------------------------------------------------------------- */
963 DefineTypeCommand::DefineTypeCommand(const std::string
& id
, Type t
)
964 : DeclarationDefinitionCommand(id
), d_params(), d_type(t
)
968 DefineTypeCommand::DefineTypeCommand(const std::string
& id
,
969 const std::vector
<Type
>& params
,
971 : DeclarationDefinitionCommand(id
), d_params(params
), d_type(t
)
975 const std::vector
<Type
>& DefineTypeCommand::getParameters() const
980 Type
DefineTypeCommand::getType() const { return d_type
; }
981 void DefineTypeCommand::invoke(SmtEngine
* smtEngine
)
983 d_commandStatus
= CommandSuccess::instance();
986 Command
* DefineTypeCommand::exportTo(ExprManager
* exprManager
,
987 ExprManagerMapCollection
& variableMap
)
990 transform(d_params
.begin(),
992 back_inserter(params
),
993 ExportTransformer(exprManager
, variableMap
));
994 Type type
= d_type
.exportTo(exprManager
, variableMap
);
995 return new DefineTypeCommand(d_symbol
, params
, type
);
998 Command
* DefineTypeCommand::clone() const
1000 return new DefineTypeCommand(d_symbol
, d_params
, d_type
);
1003 std::string
DefineTypeCommand::getCommandName() const { return "define-sort"; }
1005 /* -------------------------------------------------------------------------- */
1006 /* class DefineFunctionCommand */
1007 /* -------------------------------------------------------------------------- */
1009 DefineFunctionCommand::DefineFunctionCommand(const std::string
& id
,
1012 : DeclarationDefinitionCommand(id
),
1019 DefineFunctionCommand::DefineFunctionCommand(const std::string
& id
,
1021 const std::vector
<Expr
>& formals
,
1023 : DeclarationDefinitionCommand(id
),
1030 Expr
DefineFunctionCommand::getFunction() const { return d_func
; }
1031 const std::vector
<Expr
>& DefineFunctionCommand::getFormals() const
1036 Expr
DefineFunctionCommand::getFormula() const { return d_formula
; }
1037 void DefineFunctionCommand::invoke(SmtEngine
* smtEngine
)
1041 if (!d_func
.isNull())
1043 smtEngine
->defineFunction(d_func
, d_formals
, d_formula
);
1045 d_commandStatus
= CommandSuccess::instance();
1047 catch (exception
& e
)
1049 d_commandStatus
= new CommandFailure(e
.what());
1053 Command
* DefineFunctionCommand::exportTo(ExprManager
* exprManager
,
1054 ExprManagerMapCollection
& variableMap
)
1056 Expr func
= d_func
.exportTo(
1057 exprManager
, variableMap
, /* flags = */ ExprManager::VAR_FLAG_DEFINED
);
1058 vector
<Expr
> formals
;
1059 transform(d_formals
.begin(),
1061 back_inserter(formals
),
1062 ExportTransformer(exprManager
, variableMap
));
1063 Expr formula
= d_formula
.exportTo(exprManager
, variableMap
);
1064 return new DefineFunctionCommand(d_symbol
, func
, formals
, formula
);
1067 Command
* DefineFunctionCommand::clone() const
1069 return new DefineFunctionCommand(d_symbol
, d_func
, d_formals
, d_formula
);
1072 std::string
DefineFunctionCommand::getCommandName() const
1074 return "define-fun";
1077 /* -------------------------------------------------------------------------- */
1078 /* class DefineNamedFunctionCommand */
1079 /* -------------------------------------------------------------------------- */
1081 DefineNamedFunctionCommand::DefineNamedFunctionCommand(
1082 const std::string
& id
,
1084 const std::vector
<Expr
>& formals
,
1086 : DefineFunctionCommand(id
, func
, formals
, formula
)
1090 void DefineNamedFunctionCommand::invoke(SmtEngine
* smtEngine
)
1092 this->DefineFunctionCommand::invoke(smtEngine
);
1093 if (!d_func
.isNull() && d_func
.getType().isBoolean())
1095 smtEngine
->addToAssignment(
1096 d_func
.getExprManager()->mkExpr(kind::APPLY
, d_func
));
1098 d_commandStatus
= CommandSuccess::instance();
1101 Command
* DefineNamedFunctionCommand::exportTo(
1102 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1104 Expr func
= d_func
.exportTo(exprManager
, variableMap
);
1105 vector
<Expr
> formals
;
1106 transform(d_formals
.begin(),
1108 back_inserter(formals
),
1109 ExportTransformer(exprManager
, variableMap
));
1110 Expr formula
= d_formula
.exportTo(exprManager
, variableMap
);
1111 return new DefineNamedFunctionCommand(d_symbol
, func
, formals
, formula
);
1114 Command
* DefineNamedFunctionCommand::clone() const
1116 return new DefineNamedFunctionCommand(d_symbol
, d_func
, d_formals
, d_formula
);
1119 /* -------------------------------------------------------------------------- */
1120 /* class DefineFunctionRecCommand */
1121 /* -------------------------------------------------------------------------- */
1123 DefineFunctionRecCommand::DefineFunctionRecCommand(
1124 Expr func
, const std::vector
<Expr
>& formals
, Expr formula
)
1126 d_funcs
.push_back(func
);
1127 d_formals
.push_back(formals
);
1128 d_formulas
.push_back(formula
);
1131 DefineFunctionRecCommand::DefineFunctionRecCommand(
1132 const std::vector
<Expr
>& funcs
,
1133 const std::vector
<std::vector
<Expr
>>& formals
,
1134 const std::vector
<Expr
>& formulas
)
1136 d_funcs
.insert(d_funcs
.end(), funcs
.begin(), funcs
.end());
1137 d_formals
.insert(d_formals
.end(), formals
.begin(), formals
.end());
1138 d_formulas
.insert(d_formulas
.end(), formulas
.begin(), formulas
.end());
1141 const std::vector
<Expr
>& DefineFunctionRecCommand::getFunctions() const
1146 const std::vector
<std::vector
<Expr
>>& DefineFunctionRecCommand::getFormals()
1152 const std::vector
<Expr
>& DefineFunctionRecCommand::getFormulas() const
1157 void DefineFunctionRecCommand::invoke(SmtEngine
* smtEngine
)
1161 smtEngine
->defineFunctionsRec(d_funcs
, d_formals
, d_formulas
);
1162 d_commandStatus
= CommandSuccess::instance();
1164 catch (exception
& e
)
1166 d_commandStatus
= new CommandFailure(e
.what());
1170 Command
* DefineFunctionRecCommand::exportTo(
1171 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1173 std::vector
<Expr
> funcs
;
1174 for (unsigned i
= 0, size
= d_funcs
.size(); i
< size
; i
++)
1176 Expr func
= d_funcs
[i
].exportTo(
1177 exprManager
, variableMap
, /* flags = */ ExprManager::VAR_FLAG_DEFINED
);
1178 funcs
.push_back(func
);
1180 std::vector
<std::vector
<Expr
>> formals
;
1181 for (unsigned i
= 0, size
= d_formals
.size(); i
< size
; i
++)
1183 std::vector
<Expr
> formals_c
;
1184 transform(d_formals
[i
].begin(),
1186 back_inserter(formals_c
),
1187 ExportTransformer(exprManager
, variableMap
));
1188 formals
.push_back(formals_c
);
1190 std::vector
<Expr
> formulas
;
1191 for (unsigned i
= 0, size
= d_formulas
.size(); i
< size
; i
++)
1193 Expr formula
= d_formulas
[i
].exportTo(exprManager
, variableMap
);
1194 formulas
.push_back(formula
);
1196 return new DefineFunctionRecCommand(funcs
, formals
, formulas
);
1199 Command
* DefineFunctionRecCommand::clone() const
1201 return new DefineFunctionRecCommand(d_funcs
, d_formals
, d_formulas
);
1204 std::string
DefineFunctionRecCommand::getCommandName() const
1206 return "define-fun-rec";
1209 /* -------------------------------------------------------------------------- */
1210 /* class SetUserAttribute */
1211 /* -------------------------------------------------------------------------- */
1213 SetUserAttributeCommand::SetUserAttributeCommand(
1214 const std::string
& attr
,
1216 const std::vector
<Expr
>& expr_values
,
1217 const std::string
& str_value
)
1220 d_expr_values(expr_values
),
1221 d_str_value(str_value
)
1225 SetUserAttributeCommand::SetUserAttributeCommand(const std::string
& attr
,
1227 : SetUserAttributeCommand(attr
, expr
, {}, "")
1231 SetUserAttributeCommand::SetUserAttributeCommand(
1232 const std::string
& attr
, Expr expr
, const std::vector
<Expr
>& values
)
1233 : SetUserAttributeCommand(attr
, expr
, values
, "")
1237 SetUserAttributeCommand::SetUserAttributeCommand(const std::string
& attr
,
1239 const std::string
& value
)
1240 : SetUserAttributeCommand(attr
, expr
, {}, value
)
1244 void SetUserAttributeCommand::invoke(SmtEngine
* smtEngine
)
1248 if (!d_expr
.isNull())
1250 smtEngine
->setUserAttribute(d_attr
, d_expr
, d_expr_values
, d_str_value
);
1252 d_commandStatus
= CommandSuccess::instance();
1254 catch (exception
& e
)
1256 d_commandStatus
= new CommandFailure(e
.what());
1260 Command
* SetUserAttributeCommand::exportTo(
1261 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1263 Expr expr
= d_expr
.exportTo(exprManager
, variableMap
);
1264 return new SetUserAttributeCommand(d_attr
, expr
, d_expr_values
, d_str_value
);
1267 Command
* SetUserAttributeCommand::clone() const
1269 return new SetUserAttributeCommand(
1270 d_attr
, d_expr
, d_expr_values
, d_str_value
);
1273 std::string
SetUserAttributeCommand::getCommandName() const
1275 return "set-user-attribute";
1278 /* -------------------------------------------------------------------------- */
1279 /* class SimplifyCommand */
1280 /* -------------------------------------------------------------------------- */
1282 SimplifyCommand::SimplifyCommand(Expr term
) : d_term(term
) {}
1283 Expr
SimplifyCommand::getTerm() const { return d_term
; }
1284 void SimplifyCommand::invoke(SmtEngine
* smtEngine
)
1288 d_result
= smtEngine
->simplify(d_term
);
1289 d_commandStatus
= CommandSuccess::instance();
1291 catch (UnsafeInterruptException
& e
)
1293 d_commandStatus
= new CommandInterrupted();
1295 catch (exception
& e
)
1297 d_commandStatus
= new CommandFailure(e
.what());
1301 Expr
SimplifyCommand::getResult() const { return d_result
; }
1302 void SimplifyCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1306 this->Command::printResult(out
, verbosity
);
1310 out
<< d_result
<< endl
;
1314 Command
* SimplifyCommand::exportTo(ExprManager
* exprManager
,
1315 ExprManagerMapCollection
& variableMap
)
1317 SimplifyCommand
* c
=
1318 new SimplifyCommand(d_term
.exportTo(exprManager
, variableMap
));
1319 c
->d_result
= d_result
.exportTo(exprManager
, variableMap
);
1323 Command
* SimplifyCommand::clone() const
1325 SimplifyCommand
* c
= new SimplifyCommand(d_term
);
1326 c
->d_result
= d_result
;
1330 std::string
SimplifyCommand::getCommandName() const { return "simplify"; }
1332 /* -------------------------------------------------------------------------- */
1333 /* class ExpandDefinitionsCommand */
1334 /* -------------------------------------------------------------------------- */
1336 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term
) : d_term(term
) {}
1337 Expr
ExpandDefinitionsCommand::getTerm() const { return d_term
; }
1338 void ExpandDefinitionsCommand::invoke(SmtEngine
* smtEngine
)
1340 d_result
= smtEngine
->expandDefinitions(d_term
);
1341 d_commandStatus
= CommandSuccess::instance();
1344 Expr
ExpandDefinitionsCommand::getResult() const { return d_result
; }
1345 void ExpandDefinitionsCommand::printResult(std::ostream
& out
,
1346 uint32_t verbosity
) const
1350 this->Command::printResult(out
, verbosity
);
1354 out
<< d_result
<< endl
;
1358 Command
* ExpandDefinitionsCommand::exportTo(
1359 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1361 ExpandDefinitionsCommand
* c
=
1362 new ExpandDefinitionsCommand(d_term
.exportTo(exprManager
, variableMap
));
1363 c
->d_result
= d_result
.exportTo(exprManager
, variableMap
);
1367 Command
* ExpandDefinitionsCommand::clone() const
1369 ExpandDefinitionsCommand
* c
= new ExpandDefinitionsCommand(d_term
);
1370 c
->d_result
= d_result
;
1374 std::string
ExpandDefinitionsCommand::getCommandName() const
1376 return "expand-definitions";
1379 /* -------------------------------------------------------------------------- */
1380 /* class GetValueCommand */
1381 /* -------------------------------------------------------------------------- */
1383 GetValueCommand::GetValueCommand(Expr term
) : d_terms()
1385 d_terms
.push_back(term
);
1388 GetValueCommand::GetValueCommand(const std::vector
<Expr
>& terms
)
1391 PrettyCheckArgument(
1392 terms
.size() >= 1, terms
, "cannot get-value of an empty set of terms");
1395 const std::vector
<Expr
>& GetValueCommand::getTerms() const { return d_terms
; }
1396 void GetValueCommand::invoke(SmtEngine
* smtEngine
)
1400 vector
<Expr
> result
;
1401 ExprManager
* em
= smtEngine
->getExprManager();
1402 NodeManager
* nm
= NodeManager::fromExprManager(em
);
1403 for (const Expr
& e
: d_terms
)
1405 Assert(nm
== NodeManager::fromExprManager(e
.getExprManager()));
1406 smt::SmtScope
scope(smtEngine
);
1407 Node request
= Node::fromExpr(
1408 options::expandDefinitions() ? smtEngine
->expandDefinitions(e
) : e
);
1409 Node value
= Node::fromExpr(smtEngine
->getValue(e
));
1410 if (value
.getType().isInteger() && request
.getType() == nm
->realType())
1412 // Need to wrap in division-by-one so that output printers know this
1413 // is an integer-looking constant that really should be output as
1414 // a rational. Necessary for SMT-LIB standards compliance.
1415 value
= nm
->mkNode(kind::DIVISION
, value
, nm
->mkConst(Rational(1)));
1417 result
.push_back(nm
->mkNode(kind::SEXPR
, request
, value
).toExpr());
1419 d_result
= em
->mkExpr(kind::SEXPR
, result
);
1420 d_commandStatus
= CommandSuccess::instance();
1422 catch (RecoverableModalException
& e
)
1424 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1426 catch (UnsafeInterruptException
& e
)
1428 d_commandStatus
= new CommandInterrupted();
1430 catch (exception
& e
)
1432 d_commandStatus
= new CommandFailure(e
.what());
1436 Expr
GetValueCommand::getResult() const { return d_result
; }
1437 void GetValueCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1441 this->Command::printResult(out
, verbosity
);
1445 expr::ExprDag::Scope
scope(out
, false);
1446 out
<< d_result
<< endl
;
1450 Command
* GetValueCommand::exportTo(ExprManager
* exprManager
,
1451 ExprManagerMapCollection
& variableMap
)
1453 vector
<Expr
> exportedTerms
;
1454 for (std::vector
<Expr
>::const_iterator i
= d_terms
.begin();
1458 exportedTerms
.push_back((*i
).exportTo(exprManager
, variableMap
));
1460 GetValueCommand
* c
= new GetValueCommand(exportedTerms
);
1461 c
->d_result
= d_result
.exportTo(exprManager
, variableMap
);
1465 Command
* GetValueCommand::clone() const
1467 GetValueCommand
* c
= new GetValueCommand(d_terms
);
1468 c
->d_result
= d_result
;
1472 std::string
GetValueCommand::getCommandName() const { return "get-value"; }
1474 /* -------------------------------------------------------------------------- */
1475 /* class GetAssignmentCommand */
1476 /* -------------------------------------------------------------------------- */
1478 GetAssignmentCommand::GetAssignmentCommand() {}
1479 void GetAssignmentCommand::invoke(SmtEngine
* smtEngine
)
1483 std::vector
<std::pair
<Expr
, Expr
>> assignments
= smtEngine
->getAssignment();
1484 vector
<SExpr
> sexprs
;
1485 for (const auto& p
: assignments
)
1488 if (p
.first
.getKind() == kind::APPLY
)
1490 v
.emplace_back(SExpr::Keyword(p
.first
.getOperator().toString()));
1494 v
.emplace_back(SExpr::Keyword(p
.first
.toString()));
1496 v
.emplace_back(SExpr::Keyword(p
.second
.toString()));
1497 sexprs
.emplace_back(v
);
1499 d_result
= SExpr(sexprs
);
1500 d_commandStatus
= CommandSuccess::instance();
1502 catch (RecoverableModalException
& e
)
1504 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1506 catch (UnsafeInterruptException
& e
)
1508 d_commandStatus
= new CommandInterrupted();
1510 catch (exception
& e
)
1512 d_commandStatus
= new CommandFailure(e
.what());
1516 SExpr
GetAssignmentCommand::getResult() const { return d_result
; }
1517 void GetAssignmentCommand::printResult(std::ostream
& out
,
1518 uint32_t verbosity
) const
1522 this->Command::printResult(out
, verbosity
);
1526 out
<< d_result
<< endl
;
1530 Command
* GetAssignmentCommand::exportTo(ExprManager
* exprManager
,
1531 ExprManagerMapCollection
& variableMap
)
1533 GetAssignmentCommand
* c
= new GetAssignmentCommand();
1534 c
->d_result
= d_result
;
1538 Command
* GetAssignmentCommand::clone() const
1540 GetAssignmentCommand
* c
= new GetAssignmentCommand();
1541 c
->d_result
= d_result
;
1545 std::string
GetAssignmentCommand::getCommandName() const
1547 return "get-assignment";
1550 /* -------------------------------------------------------------------------- */
1551 /* class GetModelCommand */
1552 /* -------------------------------------------------------------------------- */
1554 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
1555 void GetModelCommand::invoke(SmtEngine
* smtEngine
)
1559 d_result
= smtEngine
->getModel();
1560 d_smtEngine
= smtEngine
;
1561 d_commandStatus
= CommandSuccess::instance();
1563 catch (RecoverableModalException
& e
)
1565 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1567 catch (UnsafeInterruptException
& e
)
1569 d_commandStatus
= new CommandInterrupted();
1571 catch (exception
& e
)
1573 d_commandStatus
= new CommandFailure(e
.what());
1577 /* Model is private to the library -- for now
1578 Model* GetModelCommand::getResult() const {
1583 void GetModelCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1587 this->Command::printResult(out
, verbosity
);
1595 Command
* GetModelCommand::exportTo(ExprManager
* exprManager
,
1596 ExprManagerMapCollection
& variableMap
)
1598 GetModelCommand
* c
= new GetModelCommand();
1599 c
->d_result
= d_result
;
1600 c
->d_smtEngine
= d_smtEngine
;
1604 Command
* GetModelCommand::clone() const
1606 GetModelCommand
* c
= new GetModelCommand();
1607 c
->d_result
= d_result
;
1608 c
->d_smtEngine
= d_smtEngine
;
1612 std::string
GetModelCommand::getCommandName() const { return "get-model"; }
1614 /* -------------------------------------------------------------------------- */
1615 /* class GetProofCommand */
1616 /* -------------------------------------------------------------------------- */
1618 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
1619 void GetProofCommand::invoke(SmtEngine
* smtEngine
)
1623 d_smtEngine
= smtEngine
;
1624 d_result
= &smtEngine
->getProof();
1625 d_commandStatus
= CommandSuccess::instance();
1627 catch (RecoverableModalException
& e
)
1629 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1631 catch (UnsafeInterruptException
& e
)
1633 d_commandStatus
= new CommandInterrupted();
1635 catch (exception
& e
)
1637 d_commandStatus
= new CommandFailure(e
.what());
1641 const Proof
& GetProofCommand::getResult() const { return *d_result
; }
1642 void GetProofCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1646 this->Command::printResult(out
, verbosity
);
1650 smt::SmtScope
scope(d_smtEngine
);
1651 d_result
->toStream(out
);
1655 Command
* GetProofCommand::exportTo(ExprManager
* exprManager
,
1656 ExprManagerMapCollection
& variableMap
)
1658 GetProofCommand
* c
= new GetProofCommand();
1659 c
->d_result
= d_result
;
1660 c
->d_smtEngine
= d_smtEngine
;
1664 Command
* GetProofCommand::clone() const
1666 GetProofCommand
* c
= new GetProofCommand();
1667 c
->d_result
= d_result
;
1668 c
->d_smtEngine
= d_smtEngine
;
1672 std::string
GetProofCommand::getCommandName() const { return "get-proof"; }
1674 /* -------------------------------------------------------------------------- */
1675 /* class GetInstantiationsCommand */
1676 /* -------------------------------------------------------------------------- */
1678 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
1679 void GetInstantiationsCommand::invoke(SmtEngine
* smtEngine
)
1683 d_smtEngine
= smtEngine
;
1684 d_commandStatus
= CommandSuccess::instance();
1686 catch (exception
& e
)
1688 d_commandStatus
= new CommandFailure(e
.what());
1692 void GetInstantiationsCommand::printResult(std::ostream
& out
,
1693 uint32_t verbosity
) const
1697 this->Command::printResult(out
, verbosity
);
1701 d_smtEngine
->printInstantiations(out
);
1705 Command
* GetInstantiationsCommand::exportTo(
1706 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1708 GetInstantiationsCommand
* c
= new GetInstantiationsCommand();
1709 // c->d_result = d_result;
1710 c
->d_smtEngine
= d_smtEngine
;
1714 Command
* GetInstantiationsCommand::clone() const
1716 GetInstantiationsCommand
* c
= new GetInstantiationsCommand();
1717 // c->d_result = d_result;
1718 c
->d_smtEngine
= d_smtEngine
;
1722 std::string
GetInstantiationsCommand::getCommandName() const
1724 return "get-instantiations";
1727 /* -------------------------------------------------------------------------- */
1728 /* class GetSynthSolutionCommand */
1729 /* -------------------------------------------------------------------------- */
1731 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
1732 void GetSynthSolutionCommand::invoke(SmtEngine
* smtEngine
)
1736 d_smtEngine
= smtEngine
;
1737 d_commandStatus
= CommandSuccess::instance();
1739 catch (exception
& e
)
1741 d_commandStatus
= new CommandFailure(e
.what());
1745 void GetSynthSolutionCommand::printResult(std::ostream
& out
,
1746 uint32_t verbosity
) const
1750 this->Command::printResult(out
, verbosity
);
1754 d_smtEngine
->printSynthSolution(out
);
1758 Command
* GetSynthSolutionCommand::exportTo(
1759 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1761 GetSynthSolutionCommand
* c
= new GetSynthSolutionCommand();
1762 c
->d_smtEngine
= d_smtEngine
;
1766 Command
* GetSynthSolutionCommand::clone() const
1768 GetSynthSolutionCommand
* c
= new GetSynthSolutionCommand();
1769 c
->d_smtEngine
= d_smtEngine
;
1773 std::string
GetSynthSolutionCommand::getCommandName() const
1775 return "get-instantiations";
1778 /* -------------------------------------------------------------------------- */
1779 /* class GetQuantifierEliminationCommand */
1780 /* -------------------------------------------------------------------------- */
1782 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand() : d_expr() {}
1783 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
1784 const Expr
& expr
, bool doFull
)
1785 : d_expr(expr
), d_doFull(doFull
)
1789 Expr
GetQuantifierEliminationCommand::getExpr() const { return d_expr
; }
1790 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull
; }
1791 void GetQuantifierEliminationCommand::invoke(SmtEngine
* smtEngine
)
1795 d_result
= smtEngine
->doQuantifierElimination(d_expr
, d_doFull
);
1796 d_commandStatus
= CommandSuccess::instance();
1798 catch (exception
& e
)
1800 d_commandStatus
= new CommandFailure(e
.what());
1804 Expr
GetQuantifierEliminationCommand::getResult() const { return d_result
; }
1805 void GetQuantifierEliminationCommand::printResult(std::ostream
& out
,
1806 uint32_t verbosity
) const
1810 this->Command::printResult(out
, verbosity
);
1814 out
<< d_result
<< endl
;
1818 Command
* GetQuantifierEliminationCommand::exportTo(
1819 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1821 GetQuantifierEliminationCommand
* c
= new GetQuantifierEliminationCommand(
1822 d_expr
.exportTo(exprManager
, variableMap
), d_doFull
);
1823 c
->d_result
= d_result
;
1827 Command
* GetQuantifierEliminationCommand::clone() const
1829 GetQuantifierEliminationCommand
* c
=
1830 new GetQuantifierEliminationCommand(d_expr
, d_doFull
);
1831 c
->d_result
= d_result
;
1835 std::string
GetQuantifierEliminationCommand::getCommandName() const
1837 return d_doFull
? "get-qe" : "get-qe-disjunct";
1840 /* -------------------------------------------------------------------------- */
1841 /* class GetUnsatAssumptionsCommand */
1842 /* -------------------------------------------------------------------------- */
1844 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
1846 void GetUnsatAssumptionsCommand::invoke(SmtEngine
* smtEngine
)
1850 d_result
= smtEngine
->getUnsatAssumptions();
1851 d_commandStatus
= CommandSuccess::instance();
1853 catch (RecoverableModalException
& e
)
1855 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1857 catch (exception
& e
)
1859 d_commandStatus
= new CommandFailure(e
.what());
1863 std::vector
<Expr
> GetUnsatAssumptionsCommand::getResult() const
1868 void GetUnsatAssumptionsCommand::printResult(std::ostream
& out
,
1869 uint32_t verbosity
) const
1873 this->Command::printResult(out
, verbosity
);
1877 container_to_stream(out
, d_result
, "(", ")\n", " ");
1881 Command
* GetUnsatAssumptionsCommand::exportTo(
1882 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1884 GetUnsatAssumptionsCommand
* c
= new GetUnsatAssumptionsCommand
;
1885 c
->d_result
= d_result
;
1889 Command
* GetUnsatAssumptionsCommand::clone() const
1891 GetUnsatAssumptionsCommand
* c
= new GetUnsatAssumptionsCommand
;
1892 c
->d_result
= d_result
;
1896 std::string
GetUnsatAssumptionsCommand::getCommandName() const
1898 return "get-unsat-assumptions";
1901 /* -------------------------------------------------------------------------- */
1902 /* class GetUnsatCoreCommand */
1903 /* -------------------------------------------------------------------------- */
1905 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
1906 void GetUnsatCoreCommand::invoke(SmtEngine
* smtEngine
)
1910 d_result
= smtEngine
->getUnsatCore();
1911 d_commandStatus
= CommandSuccess::instance();
1913 catch (RecoverableModalException
& e
)
1915 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1917 catch (exception
& e
)
1919 d_commandStatus
= new CommandFailure(e
.what());
1923 void GetUnsatCoreCommand::printResult(std::ostream
& out
,
1924 uint32_t verbosity
) const
1928 this->Command::printResult(out
, verbosity
);
1932 d_result
.toStream(out
);
1936 const UnsatCore
& GetUnsatCoreCommand::getUnsatCore() const
1938 // of course, this will be empty if the command hasn't been invoked yet
1942 Command
* GetUnsatCoreCommand::exportTo(ExprManager
* exprManager
,
1943 ExprManagerMapCollection
& variableMap
)
1945 GetUnsatCoreCommand
* c
= new GetUnsatCoreCommand
;
1946 c
->d_result
= d_result
;
1950 Command
* GetUnsatCoreCommand::clone() const
1952 GetUnsatCoreCommand
* c
= new GetUnsatCoreCommand
;
1953 c
->d_result
= d_result
;
1957 std::string
GetUnsatCoreCommand::getCommandName() const
1959 return "get-unsat-core";
1962 /* -------------------------------------------------------------------------- */
1963 /* class GetAssertionsCommand */
1964 /* -------------------------------------------------------------------------- */
1966 GetAssertionsCommand::GetAssertionsCommand() {}
1967 void GetAssertionsCommand::invoke(SmtEngine
* smtEngine
)
1972 const vector
<Expr
> v
= smtEngine
->getAssertions();
1974 copy(v
.begin(), v
.end(), ostream_iterator
<Expr
>(ss
, "\n"));
1976 d_result
= ss
.str();
1977 d_commandStatus
= CommandSuccess::instance();
1979 catch (exception
& e
)
1981 d_commandStatus
= new CommandFailure(e
.what());
1985 std::string
GetAssertionsCommand::getResult() const { return d_result
; }
1986 void GetAssertionsCommand::printResult(std::ostream
& out
,
1987 uint32_t verbosity
) const
1991 this->Command::printResult(out
, verbosity
);
1999 Command
* GetAssertionsCommand::exportTo(ExprManager
* exprManager
,
2000 ExprManagerMapCollection
& variableMap
)
2002 GetAssertionsCommand
* c
= new GetAssertionsCommand();
2003 c
->d_result
= d_result
;
2007 Command
* GetAssertionsCommand::clone() const
2009 GetAssertionsCommand
* c
= new GetAssertionsCommand();
2010 c
->d_result
= d_result
;
2014 std::string
GetAssertionsCommand::getCommandName() const
2016 return "get-assertions";
2019 /* -------------------------------------------------------------------------- */
2020 /* class SetBenchmarkStatusCommand */
2021 /* -------------------------------------------------------------------------- */
2023 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status
)
2028 BenchmarkStatus
SetBenchmarkStatusCommand::getStatus() const
2033 void SetBenchmarkStatusCommand::invoke(SmtEngine
* smtEngine
)
2039 SExpr status
= SExpr(ss
.str());
2040 smtEngine
->setInfo("status", status
);
2041 d_commandStatus
= CommandSuccess::instance();
2043 catch (exception
& e
)
2045 d_commandStatus
= new CommandFailure(e
.what());
2049 Command
* SetBenchmarkStatusCommand::exportTo(
2050 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2052 return new SetBenchmarkStatusCommand(d_status
);
2055 Command
* SetBenchmarkStatusCommand::clone() const
2057 return new SetBenchmarkStatusCommand(d_status
);
2060 std::string
SetBenchmarkStatusCommand::getCommandName() const
2065 /* -------------------------------------------------------------------------- */
2066 /* class SetBenchmarkLogicCommand */
2067 /* -------------------------------------------------------------------------- */
2069 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic
)
2074 std::string
SetBenchmarkLogicCommand::getLogic() const { return d_logic
; }
2075 void SetBenchmarkLogicCommand::invoke(SmtEngine
* smtEngine
)
2079 smtEngine
->setLogic(d_logic
);
2080 d_commandStatus
= CommandSuccess::instance();
2082 catch (exception
& e
)
2084 d_commandStatus
= new CommandFailure(e
.what());
2088 Command
* SetBenchmarkLogicCommand::exportTo(
2089 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2091 return new SetBenchmarkLogicCommand(d_logic
);
2094 Command
* SetBenchmarkLogicCommand::clone() const
2096 return new SetBenchmarkLogicCommand(d_logic
);
2099 std::string
SetBenchmarkLogicCommand::getCommandName() const
2104 /* -------------------------------------------------------------------------- */
2105 /* class SetInfoCommand */
2106 /* -------------------------------------------------------------------------- */
2108 SetInfoCommand::SetInfoCommand(std::string flag
, const SExpr
& sexpr
)
2109 : d_flag(flag
), d_sexpr(sexpr
)
2113 std::string
SetInfoCommand::getFlag() const { return d_flag
; }
2114 SExpr
SetInfoCommand::getSExpr() const { return d_sexpr
; }
2115 void SetInfoCommand::invoke(SmtEngine
* smtEngine
)
2119 smtEngine
->setInfo(d_flag
, d_sexpr
);
2120 d_commandStatus
= CommandSuccess::instance();
2122 catch (UnrecognizedOptionException
&)
2124 // As per SMT-LIB spec, silently accept unknown set-info keys
2125 d_commandStatus
= CommandSuccess::instance();
2127 catch (exception
& e
)
2129 d_commandStatus
= new CommandFailure(e
.what());
2133 Command
* SetInfoCommand::exportTo(ExprManager
* exprManager
,
2134 ExprManagerMapCollection
& variableMap
)
2136 return new SetInfoCommand(d_flag
, d_sexpr
);
2139 Command
* SetInfoCommand::clone() const
2141 return new SetInfoCommand(d_flag
, d_sexpr
);
2144 std::string
SetInfoCommand::getCommandName() const { return "set-info"; }
2146 /* -------------------------------------------------------------------------- */
2147 /* class GetInfoCommand */
2148 /* -------------------------------------------------------------------------- */
2150 GetInfoCommand::GetInfoCommand(std::string flag
) : d_flag(flag
) {}
2151 std::string
GetInfoCommand::getFlag() const { return d_flag
; }
2152 void GetInfoCommand::invoke(SmtEngine
* smtEngine
)
2157 v
.push_back(SExpr(SExpr::Keyword(string(":") + d_flag
)));
2158 v
.push_back(smtEngine
->getInfo(d_flag
));
2160 if (d_flag
== "all-options" || d_flag
== "all-statistics")
2162 ss
<< PrettySExprs(true);
2165 d_result
= ss
.str();
2166 d_commandStatus
= CommandSuccess::instance();
2168 catch (UnrecognizedOptionException
&)
2170 d_commandStatus
= new CommandUnsupported();
2172 catch (exception
& e
)
2174 d_commandStatus
= new CommandFailure(e
.what());
2178 std::string
GetInfoCommand::getResult() const { return d_result
; }
2179 void GetInfoCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
2183 this->Command::printResult(out
, verbosity
);
2185 else if (d_result
!= "")
2187 out
<< d_result
<< endl
;
2191 Command
* GetInfoCommand::exportTo(ExprManager
* exprManager
,
2192 ExprManagerMapCollection
& variableMap
)
2194 GetInfoCommand
* c
= new GetInfoCommand(d_flag
);
2195 c
->d_result
= d_result
;
2199 Command
* GetInfoCommand::clone() const
2201 GetInfoCommand
* c
= new GetInfoCommand(d_flag
);
2202 c
->d_result
= d_result
;
2206 std::string
GetInfoCommand::getCommandName() const { return "get-info"; }
2208 /* -------------------------------------------------------------------------- */
2209 /* class SetOptionCommand */
2210 /* -------------------------------------------------------------------------- */
2212 SetOptionCommand::SetOptionCommand(std::string flag
, const SExpr
& sexpr
)
2213 : d_flag(flag
), d_sexpr(sexpr
)
2217 std::string
SetOptionCommand::getFlag() const { return d_flag
; }
2218 SExpr
SetOptionCommand::getSExpr() const { return d_sexpr
; }
2219 void SetOptionCommand::invoke(SmtEngine
* smtEngine
)
2223 smtEngine
->setOption(d_flag
, d_sexpr
);
2224 d_commandStatus
= CommandSuccess::instance();
2226 catch (UnrecognizedOptionException
&)
2228 d_commandStatus
= new CommandUnsupported();
2230 catch (exception
& e
)
2232 d_commandStatus
= new CommandFailure(e
.what());
2236 Command
* SetOptionCommand::exportTo(ExprManager
* exprManager
,
2237 ExprManagerMapCollection
& variableMap
)
2239 return new SetOptionCommand(d_flag
, d_sexpr
);
2242 Command
* SetOptionCommand::clone() const
2244 return new SetOptionCommand(d_flag
, d_sexpr
);
2247 std::string
SetOptionCommand::getCommandName() const { return "set-option"; }
2249 /* -------------------------------------------------------------------------- */
2250 /* class GetOptionCommand */
2251 /* -------------------------------------------------------------------------- */
2253 GetOptionCommand::GetOptionCommand(std::string flag
) : d_flag(flag
) {}
2254 std::string
GetOptionCommand::getFlag() const { return d_flag
; }
2255 void GetOptionCommand::invoke(SmtEngine
* smtEngine
)
2259 SExpr res
= smtEngine
->getOption(d_flag
);
2260 d_result
= res
.toString();
2261 d_commandStatus
= CommandSuccess::instance();
2263 catch (UnrecognizedOptionException
&)
2265 d_commandStatus
= new CommandUnsupported();
2267 catch (exception
& e
)
2269 d_commandStatus
= new CommandFailure(e
.what());
2273 std::string
GetOptionCommand::getResult() const { return d_result
; }
2274 void GetOptionCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
2278 this->Command::printResult(out
, verbosity
);
2280 else if (d_result
!= "")
2282 out
<< d_result
<< endl
;
2286 Command
* GetOptionCommand::exportTo(ExprManager
* exprManager
,
2287 ExprManagerMapCollection
& variableMap
)
2289 GetOptionCommand
* c
= new GetOptionCommand(d_flag
);
2290 c
->d_result
= d_result
;
2294 Command
* GetOptionCommand::clone() const
2296 GetOptionCommand
* c
= new GetOptionCommand(d_flag
);
2297 c
->d_result
= d_result
;
2301 std::string
GetOptionCommand::getCommandName() const { return "get-option"; }
2303 /* -------------------------------------------------------------------------- */
2304 /* class SetExpressionNameCommand */
2305 /* -------------------------------------------------------------------------- */
2307 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr
, std::string name
)
2308 : d_expr(expr
), d_name(name
)
2312 void SetExpressionNameCommand::invoke(SmtEngine
* smtEngine
)
2314 smtEngine
->setExpressionName(d_expr
, d_name
);
2315 d_commandStatus
= CommandSuccess::instance();
2318 Command
* SetExpressionNameCommand::exportTo(
2319 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2321 SetExpressionNameCommand
* c
= new SetExpressionNameCommand(
2322 d_expr
.exportTo(exprManager
, variableMap
), d_name
);
2326 Command
* SetExpressionNameCommand::clone() const
2328 SetExpressionNameCommand
* c
= new SetExpressionNameCommand(d_expr
, d_name
);
2332 std::string
SetExpressionNameCommand::getCommandName() const
2334 return "set-expr-name";
2337 /* -------------------------------------------------------------------------- */
2338 /* class DatatypeDeclarationCommand */
2339 /* -------------------------------------------------------------------------- */
2341 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2342 const DatatypeType
& datatype
)
2345 d_datatypes
.push_back(datatype
);
2348 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2349 const std::vector
<DatatypeType
>& datatypes
)
2350 : d_datatypes(datatypes
)
2354 const std::vector
<DatatypeType
>& DatatypeDeclarationCommand::getDatatypes()
2360 void DatatypeDeclarationCommand::invoke(SmtEngine
* smtEngine
)
2362 d_commandStatus
= CommandSuccess::instance();
2365 Command
* DatatypeDeclarationCommand::exportTo(
2366 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2368 throw ExportUnsupportedException(
2369 "export of DatatypeDeclarationCommand unsupported");
2372 Command
* DatatypeDeclarationCommand::clone() const
2374 return new DatatypeDeclarationCommand(d_datatypes
);
2377 std::string
DatatypeDeclarationCommand::getCommandName() const
2379 return "declare-datatypes";
2382 /* -------------------------------------------------------------------------- */
2383 /* class RewriteRuleCommand */
2384 /* -------------------------------------------------------------------------- */
2386 RewriteRuleCommand::RewriteRuleCommand(const std::vector
<Expr
>& vars
,
2387 const std::vector
<Expr
>& guards
,
2390 const Triggers
& triggers
)
2395 d_triggers(triggers
)
2399 RewriteRuleCommand::RewriteRuleCommand(const std::vector
<Expr
>& vars
,
2402 : d_vars(vars
), d_head(head
), d_body(body
)
2406 const std::vector
<Expr
>& RewriteRuleCommand::getVars() const { return d_vars
; }
2407 const std::vector
<Expr
>& RewriteRuleCommand::getGuards() const
2412 Expr
RewriteRuleCommand::getHead() const { return d_head
; }
2413 Expr
RewriteRuleCommand::getBody() const { return d_body
; }
2414 const RewriteRuleCommand::Triggers
& RewriteRuleCommand::getTriggers() const
2419 void RewriteRuleCommand::invoke(SmtEngine
* smtEngine
)
2423 ExprManager
* em
= smtEngine
->getExprManager();
2424 /** build vars list */
2425 Expr vars
= em
->mkExpr(kind::BOUND_VAR_LIST
, d_vars
);
2426 /** build guards list */
2428 if (d_guards
.size() == 0)
2429 guards
= em
->mkConst
<bool>(true);
2430 else if (d_guards
.size() == 1)
2431 guards
= d_guards
[0];
2433 guards
= em
->mkExpr(kind::AND
, d_guards
);
2434 /** build expression */
2436 if (d_triggers
.empty())
2438 expr
= em
->mkExpr(kind::RR_REWRITE
, vars
, guards
, d_head
, d_body
);
2442 /** build triggers list */
2443 std::vector
<Expr
> vtriggers
;
2444 vtriggers
.reserve(d_triggers
.size());
2445 for (Triggers::const_iterator i
= d_triggers
.begin(),
2446 end
= d_triggers
.end();
2450 vtriggers
.push_back(em
->mkExpr(kind::INST_PATTERN
, *i
));
2452 Expr triggers
= em
->mkExpr(kind::INST_PATTERN_LIST
, vtriggers
);
2454 em
->mkExpr(kind::RR_REWRITE
, vars
, guards
, d_head
, d_body
, triggers
);
2456 smtEngine
->assertFormula(expr
);
2457 d_commandStatus
= CommandSuccess::instance();
2459 catch (exception
& e
)
2461 d_commandStatus
= new CommandFailure(e
.what());
2465 Command
* RewriteRuleCommand::exportTo(ExprManager
* exprManager
,
2466 ExprManagerMapCollection
& variableMap
)
2468 /** Convert variables */
2469 VExpr vars
= ExportTo(exprManager
, variableMap
, d_vars
);
2470 /** Convert guards */
2471 VExpr guards
= ExportTo(exprManager
, variableMap
, d_guards
);
2472 /** Convert triggers */
2474 triggers
.reserve(d_triggers
.size());
2475 for (const std::vector
<Expr
>& trigger_list
: d_triggers
)
2477 triggers
.push_back(ExportTo(exprManager
, variableMap
, trigger_list
));
2479 /** Convert head and body */
2480 Expr head
= d_head
.exportTo(exprManager
, variableMap
);
2481 Expr body
= d_body
.exportTo(exprManager
, variableMap
);
2482 /** Create the converted rules */
2483 return new RewriteRuleCommand(vars
, guards
, head
, body
, triggers
);
2486 Command
* RewriteRuleCommand::clone() const
2488 return new RewriteRuleCommand(d_vars
, d_guards
, d_head
, d_body
, d_triggers
);
2491 std::string
RewriteRuleCommand::getCommandName() const
2493 return "rewrite-rule";
2496 /* -------------------------------------------------------------------------- */
2497 /* class PropagateRuleCommand */
2498 /* -------------------------------------------------------------------------- */
2500 PropagateRuleCommand::PropagateRuleCommand(const std::vector
<Expr
>& vars
,
2501 const std::vector
<Expr
>& guards
,
2502 const std::vector
<Expr
>& heads
,
2504 const Triggers
& triggers
,
2510 d_triggers(triggers
),
2511 d_deduction(deduction
)
2515 PropagateRuleCommand::PropagateRuleCommand(const std::vector
<Expr
>& vars
,
2516 const std::vector
<Expr
>& heads
,
2519 : d_vars(vars
), d_heads(heads
), d_body(body
), d_deduction(deduction
)
2523 const std::vector
<Expr
>& PropagateRuleCommand::getVars() const
2528 const std::vector
<Expr
>& PropagateRuleCommand::getGuards() const
2533 const std::vector
<Expr
>& PropagateRuleCommand::getHeads() const
2538 Expr
PropagateRuleCommand::getBody() const { return d_body
; }
2539 const PropagateRuleCommand::Triggers
& PropagateRuleCommand::getTriggers() const
2544 bool PropagateRuleCommand::isDeduction() const { return d_deduction
; }
2545 void PropagateRuleCommand::invoke(SmtEngine
* smtEngine
)
2549 ExprManager
* em
= smtEngine
->getExprManager();
2550 /** build vars list */
2551 Expr vars
= em
->mkExpr(kind::BOUND_VAR_LIST
, d_vars
);
2552 /** build guards list */
2554 if (d_guards
.size() == 0)
2555 guards
= em
->mkConst
<bool>(true);
2556 else if (d_guards
.size() == 1)
2557 guards
= d_guards
[0];
2559 guards
= em
->mkExpr(kind::AND
, d_guards
);
2560 /** build heads list */
2562 if (d_heads
.size() == 1)
2565 heads
= em
->mkExpr(kind::AND
, d_heads
);
2566 /** build expression */
2568 if (d_triggers
.empty())
2570 expr
= em
->mkExpr(kind::RR_REWRITE
, vars
, guards
, heads
, d_body
);
2574 /** build triggers list */
2575 std::vector
<Expr
> vtriggers
;
2576 vtriggers
.reserve(d_triggers
.size());
2577 for (Triggers::const_iterator i
= d_triggers
.begin(),
2578 end
= d_triggers
.end();
2582 vtriggers
.push_back(em
->mkExpr(kind::INST_PATTERN
, *i
));
2584 Expr triggers
= em
->mkExpr(kind::INST_PATTERN_LIST
, vtriggers
);
2586 em
->mkExpr(kind::RR_REWRITE
, vars
, guards
, heads
, d_body
, triggers
);
2588 smtEngine
->assertFormula(expr
);
2589 d_commandStatus
= CommandSuccess::instance();
2591 catch (exception
& e
)
2593 d_commandStatus
= new CommandFailure(e
.what());
2597 Command
* PropagateRuleCommand::exportTo(ExprManager
* exprManager
,
2598 ExprManagerMapCollection
& variableMap
)
2600 /** Convert variables */
2601 VExpr vars
= ExportTo(exprManager
, variableMap
, d_vars
);
2602 /** Convert guards */
2603 VExpr guards
= ExportTo(exprManager
, variableMap
, d_guards
);
2604 /** Convert heads */
2605 VExpr heads
= ExportTo(exprManager
, variableMap
, d_heads
);
2606 /** Convert triggers */
2608 triggers
.reserve(d_triggers
.size());
2609 for (const std::vector
<Expr
>& trigger_list
: d_triggers
)
2611 triggers
.push_back(ExportTo(exprManager
, variableMap
, trigger_list
));
2613 /** Convert head and body */
2614 Expr body
= d_body
.exportTo(exprManager
, variableMap
);
2615 /** Create the converted rules */
2616 return new PropagateRuleCommand(vars
, guards
, heads
, body
, triggers
);
2619 Command
* PropagateRuleCommand::clone() const
2621 return new PropagateRuleCommand(
2622 d_vars
, d_guards
, d_heads
, d_body
, d_triggers
);
2625 std::string
PropagateRuleCommand::getCommandName() const
2627 return "propagate-rule";