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-2020 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 "api/cvc4cpp.h"
27 #include "base/check.h"
28 #include "base/output.h"
29 #include "expr/expr_iomanip.h"
30 #include "expr/node.h"
31 #include "expr/type.h"
32 #include "options/options.h"
33 #include "options/smt_options.h"
34 #include "printer/printer.h"
36 #include "smt/model.h"
37 #include "smt/smt_engine.h"
38 #include "smt/smt_engine_scope.h"
39 #include "util/sexpr.h"
40 #include "util/utility.h"
46 const int CommandPrintSuccess::s_iosIndex
= std::ios_base::xalloc();
47 const CommandSuccess
* CommandSuccess::s_instance
= new CommandSuccess();
48 const CommandInterrupted
* CommandInterrupted::s_instance
=
49 new CommandInterrupted();
51 std::ostream
& operator<<(std::ostream
& out
, const Command
& c
)
54 Node::setdepth::getDepth(out
),
55 Node::printtypes::getPrintTypes(out
),
56 Node::dag::getDag(out
),
57 Node::setlanguage::getLanguage(out
));
61 ostream
& operator<<(ostream
& out
, const Command
* c
)
74 std::ostream
& operator<<(std::ostream
& out
, const CommandStatus
& s
)
76 s
.toStream(out
, Node::setlanguage::getLanguage(out
));
80 ostream
& operator<<(ostream
& out
, const CommandStatus
* s
)
93 /* output stream insertion operator for benchmark statuses */
94 std::ostream
& operator<<(std::ostream
& out
, BenchmarkStatus status
)
98 case SMT_SATISFIABLE
: return out
<< "sat";
100 case SMT_UNSATISFIABLE
: return out
<< "unsat";
102 case SMT_UNKNOWN
: return out
<< "unknown";
104 default: return out
<< "BenchmarkStatus::[UNKNOWNSTATUS!]";
108 /* -------------------------------------------------------------------------- */
109 /* class CommandPrintSuccess */
110 /* -------------------------------------------------------------------------- */
112 void CommandPrintSuccess::applyPrintSuccess(std::ostream
& out
)
114 out
.iword(s_iosIndex
) = d_printSuccess
;
117 bool CommandPrintSuccess::getPrintSuccess(std::ostream
& out
)
119 return out
.iword(s_iosIndex
);
122 void CommandPrintSuccess::setPrintSuccess(std::ostream
& out
, bool printSuccess
)
124 out
.iword(s_iosIndex
) = printSuccess
;
127 std::ostream
& operator<<(std::ostream
& out
, CommandPrintSuccess cps
)
129 cps
.applyPrintSuccess(out
);
133 /* -------------------------------------------------------------------------- */
135 /* -------------------------------------------------------------------------- */
137 Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
139 Command::Command(const api::Solver
* solver
)
140 : d_solver(solver
), d_commandStatus(nullptr), d_muted(false)
144 Command::Command(const Command
& cmd
)
147 (cmd
.d_commandStatus
== NULL
) ? NULL
: &cmd
.d_commandStatus
->clone();
148 d_muted
= cmd
.d_muted
;
153 if (d_commandStatus
!= NULL
&& d_commandStatus
!= CommandSuccess::instance())
155 delete d_commandStatus
;
159 bool Command::ok() const
161 // either we haven't run the command yet, or it ran successfully
162 return d_commandStatus
== NULL
163 || dynamic_cast<const CommandSuccess
*>(d_commandStatus
) != NULL
;
166 bool Command::fail() const
168 return d_commandStatus
!= NULL
169 && dynamic_cast<const CommandFailure
*>(d_commandStatus
) != NULL
;
172 bool Command::interrupted() const
174 return d_commandStatus
!= NULL
175 && dynamic_cast<const CommandInterrupted
*>(d_commandStatus
) != NULL
;
178 void Command::invoke(SmtEngine
* smtEngine
, std::ostream
& out
)
181 if (!(isMuted() && ok()))
184 smtEngine
->getOption("command-verbosity:" + getCommandName())
190 std::string
Command::toString() const
192 std::stringstream ss
;
197 void Command::toStream(std::ostream
& out
,
201 OutputLanguage language
) const
203 Printer::getPrinter(language
)->toStream(out
, this, toDepth
, types
, dag
);
206 void CommandStatus::toStream(std::ostream
& out
, OutputLanguage language
) const
208 Printer::getPrinter(language
)->toStream(out
, this);
211 void Command::printResult(std::ostream
& out
, uint32_t verbosity
) const
213 if (d_commandStatus
!= NULL
)
215 if ((!ok() && verbosity
>= 1) || verbosity
>= 2)
217 out
<< *d_commandStatus
;
222 /* -------------------------------------------------------------------------- */
223 /* class EmptyCommand */
224 /* -------------------------------------------------------------------------- */
226 EmptyCommand::EmptyCommand(std::string name
) : d_name(name
) {}
227 std::string
EmptyCommand::getName() const { return d_name
; }
228 void EmptyCommand::invoke(SmtEngine
* smtEngine
)
230 /* empty commands have no implementation */
231 d_commandStatus
= CommandSuccess::instance();
234 Command
* EmptyCommand::exportTo(ExprManager
* exprManager
,
235 ExprManagerMapCollection
& variableMap
)
237 return new EmptyCommand(d_name
);
240 Command
* EmptyCommand::clone() const { return new EmptyCommand(d_name
); }
241 std::string
EmptyCommand::getCommandName() const { return "empty"; }
243 /* -------------------------------------------------------------------------- */
244 /* class EchoCommand */
245 /* -------------------------------------------------------------------------- */
247 EchoCommand::EchoCommand(std::string output
) : d_output(output
) {}
248 std::string
EchoCommand::getOutput() const { return d_output
; }
249 void EchoCommand::invoke(SmtEngine
* smtEngine
)
251 /* we don't have an output stream here, nothing to do */
252 d_commandStatus
= CommandSuccess::instance();
255 void EchoCommand::invoke(SmtEngine
* smtEngine
, std::ostream
& out
)
257 out
<< d_output
<< std::endl
;
258 Trace("dtview::command") << "* ~COMMAND: echo |" << d_output
<< "|~"
260 d_commandStatus
= CommandSuccess::instance();
262 smtEngine
->getOption("command-verbosity:" + getCommandName())
267 Command
* EchoCommand::exportTo(ExprManager
* exprManager
,
268 ExprManagerMapCollection
& variableMap
)
270 return new EchoCommand(d_output
);
273 Command
* EchoCommand::clone() const { return new EchoCommand(d_output
); }
274 std::string
EchoCommand::getCommandName() const { return "echo"; }
276 /* -------------------------------------------------------------------------- */
277 /* class AssertCommand */
278 /* -------------------------------------------------------------------------- */
280 AssertCommand::AssertCommand(const Expr
& e
, bool inUnsatCore
)
281 : d_expr(e
), d_inUnsatCore(inUnsatCore
)
285 Expr
AssertCommand::getExpr() const { return d_expr
; }
286 void AssertCommand::invoke(SmtEngine
* smtEngine
)
290 smtEngine
->assertFormula(d_expr
, d_inUnsatCore
);
291 d_commandStatus
= CommandSuccess::instance();
293 catch (UnsafeInterruptException
& e
)
295 d_commandStatus
= new CommandInterrupted();
299 d_commandStatus
= new CommandFailure(e
.what());
303 Command
* AssertCommand::exportTo(ExprManager
* exprManager
,
304 ExprManagerMapCollection
& variableMap
)
306 return new AssertCommand(d_expr
.exportTo(exprManager
, variableMap
),
310 Command
* AssertCommand::clone() const
312 return new AssertCommand(d_expr
, d_inUnsatCore
);
315 std::string
AssertCommand::getCommandName() const { return "assert"; }
317 /* -------------------------------------------------------------------------- */
318 /* class PushCommand */
319 /* -------------------------------------------------------------------------- */
321 void PushCommand::invoke(SmtEngine
* smtEngine
)
326 d_commandStatus
= CommandSuccess::instance();
328 catch (UnsafeInterruptException
& e
)
330 d_commandStatus
= new CommandInterrupted();
334 d_commandStatus
= new CommandFailure(e
.what());
338 Command
* PushCommand::exportTo(ExprManager
* exprManager
,
339 ExprManagerMapCollection
& variableMap
)
341 return new PushCommand();
344 Command
* PushCommand::clone() const { return new PushCommand(); }
345 std::string
PushCommand::getCommandName() const { return "push"; }
347 /* -------------------------------------------------------------------------- */
348 /* class PopCommand */
349 /* -------------------------------------------------------------------------- */
351 void PopCommand::invoke(SmtEngine
* smtEngine
)
356 d_commandStatus
= CommandSuccess::instance();
358 catch (UnsafeInterruptException
& e
)
360 d_commandStatus
= new CommandInterrupted();
364 d_commandStatus
= new CommandFailure(e
.what());
368 Command
* PopCommand::exportTo(ExprManager
* exprManager
,
369 ExprManagerMapCollection
& variableMap
)
371 return new PopCommand();
374 Command
* PopCommand::clone() const { return new PopCommand(); }
375 std::string
PopCommand::getCommandName() const { return "pop"; }
377 /* -------------------------------------------------------------------------- */
378 /* class CheckSatCommand */
379 /* -------------------------------------------------------------------------- */
381 CheckSatCommand::CheckSatCommand() : d_expr() {}
383 CheckSatCommand::CheckSatCommand(const Expr
& expr
) : d_expr(expr
) {}
385 Expr
CheckSatCommand::getExpr() const { return d_expr
; }
386 void CheckSatCommand::invoke(SmtEngine
* smtEngine
)
388 Trace("dtview::command") << "* ~COMMAND: " << getCommandName() << "~"
392 d_result
= smtEngine
->checkSat(d_expr
);
393 d_commandStatus
= CommandSuccess::instance();
397 d_commandStatus
= new CommandFailure(e
.what());
401 Result
CheckSatCommand::getResult() const { return d_result
; }
402 void CheckSatCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
406 this->Command::printResult(out
, verbosity
);
410 Trace("dtview::command") << "* RESULT: " << d_result
<< std::endl
;
411 out
<< d_result
<< endl
;
415 Command
* CheckSatCommand::exportTo(ExprManager
* exprManager
,
416 ExprManagerMapCollection
& variableMap
)
419 new CheckSatCommand(d_expr
.exportTo(exprManager
, variableMap
));
420 c
->d_result
= d_result
;
424 Command
* CheckSatCommand::clone() const
426 CheckSatCommand
* c
= new CheckSatCommand(d_expr
);
427 c
->d_result
= d_result
;
431 std::string
CheckSatCommand::getCommandName() const { return "check-sat"; }
433 /* -------------------------------------------------------------------------- */
434 /* class CheckSatAssumingCommand */
435 /* -------------------------------------------------------------------------- */
437 CheckSatAssumingCommand::CheckSatAssumingCommand(Expr term
) : d_terms({term
}) {}
439 CheckSatAssumingCommand::CheckSatAssumingCommand(const std::vector
<Expr
>& terms
)
444 const std::vector
<Expr
>& CheckSatAssumingCommand::getTerms() const
449 void CheckSatAssumingCommand::invoke(SmtEngine
* smtEngine
)
451 Trace("dtview::command") << "* ~COMMAND: (check-sat-assuming ( " << d_terms
452 << " )~" << std::endl
;
455 d_result
= smtEngine
->checkSat(d_terms
);
456 d_commandStatus
= CommandSuccess::instance();
460 d_commandStatus
= new CommandFailure(e
.what());
464 Result
CheckSatAssumingCommand::getResult() const
466 Trace("dtview::command") << "* ~RESULT: " << d_result
<< "~" << std::endl
;
470 void CheckSatAssumingCommand::printResult(std::ostream
& out
,
471 uint32_t verbosity
) const
475 this->Command::printResult(out
, verbosity
);
479 out
<< d_result
<< endl
;
483 Command
* CheckSatAssumingCommand::exportTo(
484 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
486 vector
<Expr
> exportedTerms
;
487 for (const Expr
& e
: d_terms
)
489 exportedTerms
.push_back(e
.exportTo(exprManager
, variableMap
));
491 CheckSatAssumingCommand
* c
= new CheckSatAssumingCommand(exportedTerms
);
492 c
->d_result
= d_result
;
496 Command
* CheckSatAssumingCommand::clone() const
498 CheckSatAssumingCommand
* c
= new CheckSatAssumingCommand(d_terms
);
499 c
->d_result
= d_result
;
503 std::string
CheckSatAssumingCommand::getCommandName() const
505 return "check-sat-assuming";
508 /* -------------------------------------------------------------------------- */
509 /* class QueryCommand */
510 /* -------------------------------------------------------------------------- */
512 QueryCommand::QueryCommand(const Expr
& e
, bool inUnsatCore
)
513 : d_expr(e
), d_inUnsatCore(inUnsatCore
)
517 Expr
QueryCommand::getExpr() const { return d_expr
; }
518 void QueryCommand::invoke(SmtEngine
* smtEngine
)
522 d_result
= smtEngine
->checkEntailed(d_expr
);
523 d_commandStatus
= CommandSuccess::instance();
527 d_commandStatus
= new CommandFailure(e
.what());
531 Result
QueryCommand::getResult() const { return d_result
; }
532 void QueryCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
536 this->Command::printResult(out
, verbosity
);
540 out
<< d_result
<< endl
;
544 Command
* QueryCommand::exportTo(ExprManager
* exprManager
,
545 ExprManagerMapCollection
& variableMap
)
547 QueryCommand
* c
= new QueryCommand(d_expr
.exportTo(exprManager
, variableMap
),
549 c
->d_result
= d_result
;
553 Command
* QueryCommand::clone() const
555 QueryCommand
* c
= new QueryCommand(d_expr
, d_inUnsatCore
);
556 c
->d_result
= d_result
;
560 std::string
QueryCommand::getCommandName() const { return "query"; }
562 /* -------------------------------------------------------------------------- */
563 /* class DeclareSygusVarCommand */
564 /* -------------------------------------------------------------------------- */
566 DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string
& id
,
569 : DeclarationDefinitionCommand(id
), d_var(var
), d_type(t
)
573 Expr
DeclareSygusVarCommand::getVar() const { return d_var
; }
574 Type
DeclareSygusVarCommand::getType() const { return d_type
; }
576 void DeclareSygusVarCommand::invoke(SmtEngine
* smtEngine
)
580 smtEngine
->declareSygusVar(d_symbol
, d_var
, d_type
);
581 d_commandStatus
= CommandSuccess::instance();
585 d_commandStatus
= new CommandFailure(e
.what());
589 Command
* DeclareSygusVarCommand::exportTo(ExprManager
* exprManager
,
590 ExprManagerMapCollection
& variableMap
)
592 return new DeclareSygusVarCommand(d_symbol
,
593 d_var
.exportTo(exprManager
, variableMap
),
594 d_type
.exportTo(exprManager
, variableMap
));
597 Command
* DeclareSygusVarCommand::clone() const
599 return new DeclareSygusVarCommand(d_symbol
, d_var
, d_type
);
602 std::string
DeclareSygusVarCommand::getCommandName() const
604 return "declare-var";
607 /* -------------------------------------------------------------------------- */
608 /* class DeclareSygusFunctionCommand */
609 /* -------------------------------------------------------------------------- */
611 DeclareSygusFunctionCommand::DeclareSygusFunctionCommand(const std::string
& id
,
614 : DeclarationDefinitionCommand(id
), d_func(func
), d_type(t
)
618 Expr
DeclareSygusFunctionCommand::getFunction() const { return d_func
; }
619 Type
DeclareSygusFunctionCommand::getType() const { return d_type
; }
621 void DeclareSygusFunctionCommand::invoke(SmtEngine
* smtEngine
)
625 smtEngine
->declareSygusFunctionVar(d_symbol
, d_func
, d_type
);
626 d_commandStatus
= CommandSuccess::instance();
630 d_commandStatus
= new CommandFailure(e
.what());
634 Command
* DeclareSygusFunctionCommand::exportTo(
635 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
637 return new DeclareSygusFunctionCommand(
639 d_func
.exportTo(exprManager
, variableMap
),
640 d_type
.exportTo(exprManager
, variableMap
));
643 Command
* DeclareSygusFunctionCommand::clone() const
645 return new DeclareSygusFunctionCommand(d_symbol
, d_func
, d_type
);
648 std::string
DeclareSygusFunctionCommand::getCommandName() const
650 return "declare-fun";
653 /* -------------------------------------------------------------------------- */
654 /* class SynthFunCommand */
655 /* -------------------------------------------------------------------------- */
657 SynthFunCommand::SynthFunCommand(const api::Solver
* solver
,
658 const std::string
& id
,
660 const std::vector
<api::Term
>& vars
,
664 : DeclarationDefinitionCommand(id
),
674 api::Term
SynthFunCommand::getFunction() const { return d_fun
; }
676 const std::vector
<api::Term
>& SynthFunCommand::getVars() const
681 api::Sort
SynthFunCommand::getSort() const { return d_sort
; }
682 bool SynthFunCommand::isInv() const { return d_isInv
; }
684 const api::Grammar
* SynthFunCommand::getGrammar() const { return d_grammar
; }
686 void SynthFunCommand::invoke(SmtEngine
* smtEngine
)
690 smtEngine
->declareSynthFun(d_symbol
,
694 : d_grammar
->resolve().getType(),
696 api::termVectorToExprs(d_vars
));
697 d_commandStatus
= CommandSuccess::instance();
701 d_commandStatus
= new CommandFailure(e
.what());
705 Command
* SynthFunCommand::exportTo(ExprManager
* exprManager
,
706 ExprManagerMapCollection
& variableMap
)
711 Command
* SynthFunCommand::clone() const
713 return new SynthFunCommand(
714 d_solver
, d_symbol
, d_fun
, d_vars
, d_sort
, d_isInv
, d_grammar
);
717 std::string
SynthFunCommand::getCommandName() const
719 return d_isInv
? "synth-inv" : "synth-fun";
722 /* -------------------------------------------------------------------------- */
723 /* class SygusConstraintCommand */
724 /* -------------------------------------------------------------------------- */
726 SygusConstraintCommand::SygusConstraintCommand(const Expr
& e
) : d_expr(e
) {}
728 void SygusConstraintCommand::invoke(SmtEngine
* smtEngine
)
732 smtEngine
->assertSygusConstraint(d_expr
);
733 d_commandStatus
= CommandSuccess::instance();
737 d_commandStatus
= new CommandFailure(e
.what());
741 Expr
SygusConstraintCommand::getExpr() const { return d_expr
; }
743 Command
* SygusConstraintCommand::exportTo(ExprManager
* exprManager
,
744 ExprManagerMapCollection
& variableMap
)
746 return new SygusConstraintCommand(d_expr
.exportTo(exprManager
, variableMap
));
749 Command
* SygusConstraintCommand::clone() const
751 return new SygusConstraintCommand(d_expr
);
754 std::string
SygusConstraintCommand::getCommandName() const
759 /* -------------------------------------------------------------------------- */
760 /* class SygusInvConstraintCommand */
761 /* -------------------------------------------------------------------------- */
763 SygusInvConstraintCommand::SygusInvConstraintCommand(
764 const std::vector
<Expr
>& predicates
)
765 : d_predicates(predicates
)
769 SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr
& inv
,
773 : SygusInvConstraintCommand(std::vector
<Expr
>{inv
, pre
, trans
, post
})
777 void SygusInvConstraintCommand::invoke(SmtEngine
* smtEngine
)
781 smtEngine
->assertSygusInvConstraint(
782 d_predicates
[0], d_predicates
[1], d_predicates
[2], d_predicates
[3]);
783 d_commandStatus
= CommandSuccess::instance();
787 d_commandStatus
= new CommandFailure(e
.what());
791 const std::vector
<Expr
>& SygusInvConstraintCommand::getPredicates() const
796 Command
* SygusInvConstraintCommand::exportTo(
797 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
799 return new SygusInvConstraintCommand(d_predicates
);
802 Command
* SygusInvConstraintCommand::clone() const
804 return new SygusInvConstraintCommand(d_predicates
);
807 std::string
SygusInvConstraintCommand::getCommandName() const
809 return "inv-constraint";
812 /* -------------------------------------------------------------------------- */
813 /* class CheckSynthCommand */
814 /* -------------------------------------------------------------------------- */
816 void CheckSynthCommand::invoke(SmtEngine
* smtEngine
)
820 d_result
= smtEngine
->checkSynth();
821 d_commandStatus
= CommandSuccess::instance();
822 smt::SmtScope
scope(smtEngine
);
824 // check whether we should print the status
825 if (d_result
.asSatisfiabilityResult() != Result::UNSAT
826 || options::sygusOut() == options::SygusSolutionOutMode::STATUS_AND_DEF
827 || options::sygusOut() == options::SygusSolutionOutMode::STATUS
)
829 if (options::sygusOut() == options::SygusSolutionOutMode::STANDARD
)
831 d_solution
<< "(fail)" << endl
;
835 d_solution
<< d_result
<< endl
;
838 // check whether we should print the solution
839 if (d_result
.asSatisfiabilityResult() == Result::UNSAT
840 && options::sygusOut() != options::SygusSolutionOutMode::STATUS
)
842 // printing a synthesis solution is a non-constant
843 // method, since it invokes a sophisticated algorithm
844 // (Figure 5 of Reynolds et al. CAV 2015).
845 // Hence, we must call here print solution here,
846 // instead of during printResult.
847 smtEngine
->printSynthSolution(d_solution
);
852 d_commandStatus
= new CommandFailure(e
.what());
856 Result
CheckSynthCommand::getResult() const { return d_result
; }
857 void CheckSynthCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
861 this->Command::printResult(out
, verbosity
);
865 out
<< d_solution
.str();
869 Command
* CheckSynthCommand::exportTo(ExprManager
* exprManager
,
870 ExprManagerMapCollection
& variableMap
)
872 return new CheckSynthCommand();
875 Command
* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
877 std::string
CheckSynthCommand::getCommandName() const { return "check-synth"; }
879 /* -------------------------------------------------------------------------- */
880 /* class ResetCommand */
881 /* -------------------------------------------------------------------------- */
883 void ResetCommand::invoke(SmtEngine
* smtEngine
)
888 d_commandStatus
= CommandSuccess::instance();
892 d_commandStatus
= new CommandFailure(e
.what());
896 Command
* ResetCommand::exportTo(ExprManager
* exprManager
,
897 ExprManagerMapCollection
& variableMap
)
899 return new ResetCommand();
902 Command
* ResetCommand::clone() const { return new ResetCommand(); }
903 std::string
ResetCommand::getCommandName() const { return "reset"; }
905 /* -------------------------------------------------------------------------- */
906 /* class ResetAssertionsCommand */
907 /* -------------------------------------------------------------------------- */
909 void ResetAssertionsCommand::invoke(SmtEngine
* smtEngine
)
913 smtEngine
->resetAssertions();
914 d_commandStatus
= CommandSuccess::instance();
918 d_commandStatus
= new CommandFailure(e
.what());
922 Command
* ResetAssertionsCommand::exportTo(ExprManager
* exprManager
,
923 ExprManagerMapCollection
& variableMap
)
925 return new ResetAssertionsCommand();
928 Command
* ResetAssertionsCommand::clone() const
930 return new ResetAssertionsCommand();
933 std::string
ResetAssertionsCommand::getCommandName() const
935 return "reset-assertions";
938 /* -------------------------------------------------------------------------- */
939 /* class QuitCommand */
940 /* -------------------------------------------------------------------------- */
942 void QuitCommand::invoke(SmtEngine
* smtEngine
)
944 Dump("benchmark") << *this;
945 d_commandStatus
= CommandSuccess::instance();
948 Command
* QuitCommand::exportTo(ExprManager
* exprManager
,
949 ExprManagerMapCollection
& variableMap
)
951 return new QuitCommand();
954 Command
* QuitCommand::clone() const { return new QuitCommand(); }
955 std::string
QuitCommand::getCommandName() const { return "exit"; }
957 /* -------------------------------------------------------------------------- */
958 /* class CommentCommand */
959 /* -------------------------------------------------------------------------- */
961 CommentCommand::CommentCommand(std::string comment
) : d_comment(comment
) {}
962 std::string
CommentCommand::getComment() const { return d_comment
; }
963 void CommentCommand::invoke(SmtEngine
* smtEngine
)
965 Dump("benchmark") << *this;
966 d_commandStatus
= CommandSuccess::instance();
969 Command
* CommentCommand::exportTo(ExprManager
* exprManager
,
970 ExprManagerMapCollection
& variableMap
)
972 return new CommentCommand(d_comment
);
975 Command
* CommentCommand::clone() const { return new CommentCommand(d_comment
); }
976 std::string
CommentCommand::getCommandName() const { return "comment"; }
978 /* -------------------------------------------------------------------------- */
979 /* class CommandSequence */
980 /* -------------------------------------------------------------------------- */
982 CommandSequence::CommandSequence() : d_index(0) {}
983 CommandSequence::~CommandSequence()
985 for (unsigned i
= d_index
; i
< d_commandSequence
.size(); ++i
)
987 delete d_commandSequence
[i
];
991 void CommandSequence::addCommand(Command
* cmd
)
993 d_commandSequence
.push_back(cmd
);
996 void CommandSequence::clear() { d_commandSequence
.clear(); }
997 void CommandSequence::invoke(SmtEngine
* smtEngine
)
999 for (; d_index
< d_commandSequence
.size(); ++d_index
)
1001 d_commandSequence
[d_index
]->invoke(smtEngine
);
1002 if (!d_commandSequence
[d_index
]->ok())
1005 d_commandStatus
= d_commandSequence
[d_index
]->getCommandStatus();
1008 delete d_commandSequence
[d_index
];
1011 AlwaysAssert(d_commandStatus
== NULL
);
1012 d_commandStatus
= CommandSuccess::instance();
1015 void CommandSequence::invoke(SmtEngine
* smtEngine
, std::ostream
& out
)
1017 for (; d_index
< d_commandSequence
.size(); ++d_index
)
1019 d_commandSequence
[d_index
]->invoke(smtEngine
, out
);
1020 if (!d_commandSequence
[d_index
]->ok())
1023 d_commandStatus
= d_commandSequence
[d_index
]->getCommandStatus();
1026 delete d_commandSequence
[d_index
];
1029 AlwaysAssert(d_commandStatus
== NULL
);
1030 d_commandStatus
= CommandSuccess::instance();
1033 Command
* CommandSequence::exportTo(ExprManager
* exprManager
,
1034 ExprManagerMapCollection
& variableMap
)
1036 CommandSequence
* seq
= new CommandSequence();
1037 for (iterator i
= begin(); i
!= end(); ++i
)
1039 Command
* cmd_to_export
= *i
;
1040 Command
* cmd
= cmd_to_export
->exportTo(exprManager
, variableMap
);
1041 seq
->addCommand(cmd
);
1042 Debug("export") << "[export] so far converted: " << seq
<< endl
;
1044 seq
->d_index
= d_index
;
1048 Command
* CommandSequence::clone() const
1050 CommandSequence
* seq
= new CommandSequence();
1051 for (const_iterator i
= begin(); i
!= end(); ++i
)
1053 seq
->addCommand((*i
)->clone());
1055 seq
->d_index
= d_index
;
1059 CommandSequence::const_iterator
CommandSequence::begin() const
1061 return d_commandSequence
.begin();
1064 CommandSequence::const_iterator
CommandSequence::end() const
1066 return d_commandSequence
.end();
1069 CommandSequence::iterator
CommandSequence::begin()
1071 return d_commandSequence
.begin();
1074 CommandSequence::iterator
CommandSequence::end()
1076 return d_commandSequence
.end();
1079 std::string
CommandSequence::getCommandName() const { return "sequence"; }
1081 /* -------------------------------------------------------------------------- */
1082 /* class DeclarationDefinitionCommand */
1083 /* -------------------------------------------------------------------------- */
1085 DeclarationDefinitionCommand::DeclarationDefinitionCommand(
1086 const std::string
& id
)
1091 std::string
DeclarationDefinitionCommand::getSymbol() const { return d_symbol
; }
1093 /* -------------------------------------------------------------------------- */
1094 /* class DeclareFunctionCommand */
1095 /* -------------------------------------------------------------------------- */
1097 DeclareFunctionCommand::DeclareFunctionCommand(const std::string
& id
,
1100 : DeclarationDefinitionCommand(id
),
1103 d_printInModel(true),
1104 d_printInModelSetByUser(false)
1108 Expr
DeclareFunctionCommand::getFunction() const { return d_func
; }
1109 Type
DeclareFunctionCommand::getType() const { return d_type
; }
1110 bool DeclareFunctionCommand::getPrintInModel() const { return d_printInModel
; }
1111 bool DeclareFunctionCommand::getPrintInModelSetByUser() const
1113 return d_printInModelSetByUser
;
1116 void DeclareFunctionCommand::setPrintInModel(bool p
)
1119 d_printInModelSetByUser
= true;
1122 void DeclareFunctionCommand::invoke(SmtEngine
* smtEngine
)
1124 d_commandStatus
= CommandSuccess::instance();
1127 Command
* DeclareFunctionCommand::exportTo(ExprManager
* exprManager
,
1128 ExprManagerMapCollection
& variableMap
)
1130 DeclareFunctionCommand
* dfc
=
1131 new DeclareFunctionCommand(d_symbol
,
1132 d_func
.exportTo(exprManager
, variableMap
),
1133 d_type
.exportTo(exprManager
, variableMap
));
1134 dfc
->d_printInModel
= d_printInModel
;
1135 dfc
->d_printInModelSetByUser
= d_printInModelSetByUser
;
1139 Command
* DeclareFunctionCommand::clone() const
1141 DeclareFunctionCommand
* dfc
=
1142 new DeclareFunctionCommand(d_symbol
, d_func
, d_type
);
1143 dfc
->d_printInModel
= d_printInModel
;
1144 dfc
->d_printInModelSetByUser
= d_printInModelSetByUser
;
1148 std::string
DeclareFunctionCommand::getCommandName() const
1150 return "declare-fun";
1153 /* -------------------------------------------------------------------------- */
1154 /* class DeclareTypeCommand */
1155 /* -------------------------------------------------------------------------- */
1157 DeclareTypeCommand::DeclareTypeCommand(const std::string
& id
,
1160 : DeclarationDefinitionCommand(id
), d_arity(arity
), d_type(t
)
1164 size_t DeclareTypeCommand::getArity() const { return d_arity
; }
1165 Type
DeclareTypeCommand::getType() const { return d_type
; }
1166 void DeclareTypeCommand::invoke(SmtEngine
* smtEngine
)
1168 d_commandStatus
= CommandSuccess::instance();
1171 Command
* DeclareTypeCommand::exportTo(ExprManager
* exprManager
,
1172 ExprManagerMapCollection
& variableMap
)
1174 return new DeclareTypeCommand(
1175 d_symbol
, d_arity
, d_type
.exportTo(exprManager
, variableMap
));
1178 Command
* DeclareTypeCommand::clone() const
1180 return new DeclareTypeCommand(d_symbol
, d_arity
, d_type
);
1183 std::string
DeclareTypeCommand::getCommandName() const
1185 return "declare-sort";
1188 /* -------------------------------------------------------------------------- */
1189 /* class DefineTypeCommand */
1190 /* -------------------------------------------------------------------------- */
1192 DefineTypeCommand::DefineTypeCommand(const std::string
& id
, Type t
)
1193 : DeclarationDefinitionCommand(id
), d_params(), d_type(t
)
1197 DefineTypeCommand::DefineTypeCommand(const std::string
& id
,
1198 const std::vector
<Type
>& params
,
1200 : DeclarationDefinitionCommand(id
), d_params(params
), d_type(t
)
1204 const std::vector
<Type
>& DefineTypeCommand::getParameters() const
1209 Type
DefineTypeCommand::getType() const { return d_type
; }
1210 void DefineTypeCommand::invoke(SmtEngine
* smtEngine
)
1212 d_commandStatus
= CommandSuccess::instance();
1215 Command
* DefineTypeCommand::exportTo(ExprManager
* exprManager
,
1216 ExprManagerMapCollection
& variableMap
)
1218 vector
<Type
> params
;
1219 transform(d_params
.begin(),
1221 back_inserter(params
),
1222 ExportTransformer(exprManager
, variableMap
));
1223 Type type
= d_type
.exportTo(exprManager
, variableMap
);
1224 return new DefineTypeCommand(d_symbol
, params
, type
);
1227 Command
* DefineTypeCommand::clone() const
1229 return new DefineTypeCommand(d_symbol
, d_params
, d_type
);
1232 std::string
DefineTypeCommand::getCommandName() const { return "define-sort"; }
1234 /* -------------------------------------------------------------------------- */
1235 /* class DefineFunctionCommand */
1236 /* -------------------------------------------------------------------------- */
1238 DefineFunctionCommand::DefineFunctionCommand(const std::string
& id
,
1242 : DeclarationDefinitionCommand(id
),
1250 DefineFunctionCommand::DefineFunctionCommand(const std::string
& id
,
1252 const std::vector
<Expr
>& formals
,
1255 : DeclarationDefinitionCommand(id
),
1264 Expr
DefineFunctionCommand::getFunction() const { return d_func
; }
1265 const std::vector
<Expr
>& DefineFunctionCommand::getFormals() const
1270 Expr
DefineFunctionCommand::getFormula() const { return d_formula
; }
1271 void DefineFunctionCommand::invoke(SmtEngine
* smtEngine
)
1275 if (!d_func
.isNull())
1277 smtEngine
->defineFunction(d_func
, d_formals
, d_formula
, d_global
);
1279 d_commandStatus
= CommandSuccess::instance();
1281 catch (exception
& e
)
1283 d_commandStatus
= new CommandFailure(e
.what());
1287 Command
* DefineFunctionCommand::exportTo(ExprManager
* exprManager
,
1288 ExprManagerMapCollection
& variableMap
)
1290 Expr func
= d_func
.exportTo(
1291 exprManager
, variableMap
, /* flags = */ ExprManager::VAR_FLAG_DEFINED
);
1292 vector
<Expr
> formals
;
1293 transform(d_formals
.begin(),
1295 back_inserter(formals
),
1296 ExportTransformer(exprManager
, variableMap
));
1297 Expr formula
= d_formula
.exportTo(exprManager
, variableMap
);
1298 return new DefineFunctionCommand(d_symbol
, func
, formals
, formula
, d_global
);
1301 Command
* DefineFunctionCommand::clone() const
1303 return new DefineFunctionCommand(
1304 d_symbol
, d_func
, d_formals
, d_formula
, d_global
);
1307 std::string
DefineFunctionCommand::getCommandName() const
1309 return "define-fun";
1312 /* -------------------------------------------------------------------------- */
1313 /* class DefineNamedFunctionCommand */
1314 /* -------------------------------------------------------------------------- */
1316 DefineNamedFunctionCommand::DefineNamedFunctionCommand(
1317 const std::string
& id
,
1319 const std::vector
<Expr
>& formals
,
1322 : DefineFunctionCommand(id
, func
, formals
, formula
, global
)
1326 void DefineNamedFunctionCommand::invoke(SmtEngine
* smtEngine
)
1328 this->DefineFunctionCommand::invoke(smtEngine
);
1329 if (!d_func
.isNull() && d_func
.getType().isBoolean())
1331 smtEngine
->addToAssignment(d_func
);
1333 d_commandStatus
= CommandSuccess::instance();
1336 Command
* DefineNamedFunctionCommand::exportTo(
1337 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1339 Expr func
= d_func
.exportTo(exprManager
, variableMap
);
1340 vector
<Expr
> formals
;
1341 transform(d_formals
.begin(),
1343 back_inserter(formals
),
1344 ExportTransformer(exprManager
, variableMap
));
1345 Expr formula
= d_formula
.exportTo(exprManager
, variableMap
);
1346 return new DefineNamedFunctionCommand(
1347 d_symbol
, func
, formals
, formula
, d_global
);
1350 Command
* DefineNamedFunctionCommand::clone() const
1352 return new DefineNamedFunctionCommand(
1353 d_symbol
, d_func
, d_formals
, d_formula
, d_global
);
1356 /* -------------------------------------------------------------------------- */
1357 /* class DefineFunctionRecCommand */
1358 /* -------------------------------------------------------------------------- */
1360 DefineFunctionRecCommand::DefineFunctionRecCommand(
1361 const api::Solver
* solver
,
1363 const std::vector
<api::Term
>& formals
,
1366 : Command(solver
), d_global(global
)
1368 d_funcs
.push_back(func
);
1369 d_formals
.push_back(formals
);
1370 d_formulas
.push_back(formula
);
1373 DefineFunctionRecCommand::DefineFunctionRecCommand(
1374 const api::Solver
* solver
,
1375 const std::vector
<api::Term
>& funcs
,
1376 const std::vector
<std::vector
<api::Term
>>& formals
,
1377 const std::vector
<api::Term
>& formulas
,
1382 d_formulas(formulas
),
1387 const std::vector
<api::Term
>& DefineFunctionRecCommand::getFunctions() const
1392 const std::vector
<std::vector
<api::Term
>>&
1393 DefineFunctionRecCommand::getFormals() const
1398 const std::vector
<api::Term
>& DefineFunctionRecCommand::getFormulas() const
1403 void DefineFunctionRecCommand::invoke(SmtEngine
* smtEngine
)
1407 d_solver
->defineFunsRec(d_funcs
, d_formals
, d_formulas
, d_global
);
1408 d_commandStatus
= CommandSuccess::instance();
1410 catch (exception
& e
)
1412 d_commandStatus
= new CommandFailure(e
.what());
1416 Command
* DefineFunctionRecCommand::exportTo(
1417 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1422 Command
* DefineFunctionRecCommand::clone() const
1424 return new DefineFunctionRecCommand(
1425 d_solver
, d_funcs
, d_formals
, d_formulas
, d_global
);
1428 std::string
DefineFunctionRecCommand::getCommandName() const
1430 return "define-fun-rec";
1433 /* -------------------------------------------------------------------------- */
1434 /* class SetUserAttribute */
1435 /* -------------------------------------------------------------------------- */
1437 SetUserAttributeCommand::SetUserAttributeCommand(
1438 const std::string
& attr
,
1440 const std::vector
<Expr
>& expr_values
,
1441 const std::string
& str_value
)
1444 d_expr_values(expr_values
),
1445 d_str_value(str_value
)
1449 SetUserAttributeCommand::SetUserAttributeCommand(const std::string
& attr
,
1451 : SetUserAttributeCommand(attr
, expr
, {}, "")
1455 SetUserAttributeCommand::SetUserAttributeCommand(
1456 const std::string
& attr
, Expr expr
, const std::vector
<Expr
>& values
)
1457 : SetUserAttributeCommand(attr
, expr
, values
, "")
1461 SetUserAttributeCommand::SetUserAttributeCommand(const std::string
& attr
,
1463 const std::string
& value
)
1464 : SetUserAttributeCommand(attr
, expr
, {}, value
)
1468 void SetUserAttributeCommand::invoke(SmtEngine
* smtEngine
)
1472 if (!d_expr
.isNull())
1474 smtEngine
->setUserAttribute(d_attr
, d_expr
, d_expr_values
, d_str_value
);
1476 d_commandStatus
= CommandSuccess::instance();
1478 catch (exception
& e
)
1480 d_commandStatus
= new CommandFailure(e
.what());
1484 Command
* SetUserAttributeCommand::exportTo(
1485 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1487 Expr expr
= d_expr
.exportTo(exprManager
, variableMap
);
1488 return new SetUserAttributeCommand(d_attr
, expr
, d_expr_values
, d_str_value
);
1491 Command
* SetUserAttributeCommand::clone() const
1493 return new SetUserAttributeCommand(
1494 d_attr
, d_expr
, d_expr_values
, d_str_value
);
1497 std::string
SetUserAttributeCommand::getCommandName() const
1499 return "set-user-attribute";
1502 /* -------------------------------------------------------------------------- */
1503 /* class SimplifyCommand */
1504 /* -------------------------------------------------------------------------- */
1506 SimplifyCommand::SimplifyCommand(Expr term
) : d_term(term
) {}
1507 Expr
SimplifyCommand::getTerm() const { return d_term
; }
1508 void SimplifyCommand::invoke(SmtEngine
* smtEngine
)
1512 d_result
= smtEngine
->simplify(d_term
);
1513 d_commandStatus
= CommandSuccess::instance();
1515 catch (UnsafeInterruptException
& e
)
1517 d_commandStatus
= new CommandInterrupted();
1519 catch (exception
& e
)
1521 d_commandStatus
= new CommandFailure(e
.what());
1525 Expr
SimplifyCommand::getResult() const { return d_result
; }
1526 void SimplifyCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1530 this->Command::printResult(out
, verbosity
);
1534 out
<< d_result
<< endl
;
1538 Command
* SimplifyCommand::exportTo(ExprManager
* exprManager
,
1539 ExprManagerMapCollection
& variableMap
)
1541 SimplifyCommand
* c
=
1542 new SimplifyCommand(d_term
.exportTo(exprManager
, variableMap
));
1543 c
->d_result
= d_result
.exportTo(exprManager
, variableMap
);
1547 Command
* SimplifyCommand::clone() const
1549 SimplifyCommand
* c
= new SimplifyCommand(d_term
);
1550 c
->d_result
= d_result
;
1554 std::string
SimplifyCommand::getCommandName() const { return "simplify"; }
1556 /* -------------------------------------------------------------------------- */
1557 /* class ExpandDefinitionsCommand */
1558 /* -------------------------------------------------------------------------- */
1560 ExpandDefinitionsCommand::ExpandDefinitionsCommand(Expr term
) : d_term(term
) {}
1561 Expr
ExpandDefinitionsCommand::getTerm() const { return d_term
; }
1562 void ExpandDefinitionsCommand::invoke(SmtEngine
* smtEngine
)
1564 Node t
= Node::fromExpr(d_term
);
1565 d_result
= smtEngine
->expandDefinitions(t
).toExpr();
1566 d_commandStatus
= CommandSuccess::instance();
1569 Expr
ExpandDefinitionsCommand::getResult() const { return d_result
; }
1570 void ExpandDefinitionsCommand::printResult(std::ostream
& out
,
1571 uint32_t verbosity
) const
1575 this->Command::printResult(out
, verbosity
);
1579 out
<< d_result
<< endl
;
1583 Command
* ExpandDefinitionsCommand::exportTo(
1584 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1586 ExpandDefinitionsCommand
* c
=
1587 new ExpandDefinitionsCommand(d_term
.exportTo(exprManager
, variableMap
));
1588 c
->d_result
= d_result
.exportTo(exprManager
, variableMap
);
1592 Command
* ExpandDefinitionsCommand::clone() const
1594 ExpandDefinitionsCommand
* c
= new ExpandDefinitionsCommand(d_term
);
1595 c
->d_result
= d_result
;
1599 std::string
ExpandDefinitionsCommand::getCommandName() const
1601 return "expand-definitions";
1604 /* -------------------------------------------------------------------------- */
1605 /* class GetValueCommand */
1606 /* -------------------------------------------------------------------------- */
1608 GetValueCommand::GetValueCommand(Expr term
) : d_terms()
1610 d_terms
.push_back(term
);
1613 GetValueCommand::GetValueCommand(const std::vector
<Expr
>& terms
)
1616 PrettyCheckArgument(
1617 terms
.size() >= 1, terms
, "cannot get-value of an empty set of terms");
1620 const std::vector
<Expr
>& GetValueCommand::getTerms() const { return d_terms
; }
1621 void GetValueCommand::invoke(SmtEngine
* smtEngine
)
1625 ExprManager
* em
= smtEngine
->getExprManager();
1626 NodeManager
* nm
= NodeManager::fromExprManager(em
);
1627 smt::SmtScope
scope(smtEngine
);
1628 vector
<Expr
> result
= smtEngine
->getValues(d_terms
);
1629 Assert(result
.size() == d_terms
.size());
1630 for (int i
= 0, size
= d_terms
.size(); i
< size
; i
++)
1632 Expr e
= d_terms
[i
];
1633 Node eNode
= Node::fromExpr(e
);
1634 Assert(nm
== NodeManager::fromExprManager(e
.getExprManager()));
1635 Node request
= options::expandDefinitions()
1636 ? smtEngine
->expandDefinitions(eNode
)
1638 Node value
= Node::fromExpr(result
[i
]);
1639 if (value
.getType().isInteger() && request
.getType() == nm
->realType())
1641 // Need to wrap in division-by-one so that output printers know this
1642 // is an integer-looking constant that really should be output as
1643 // a rational. Necessary for SMT-LIB standards compliance.
1644 value
= nm
->mkNode(kind::DIVISION
, value
, nm
->mkConst(Rational(1)));
1646 result
[i
] = nm
->mkNode(kind::SEXPR
, request
, value
).toExpr();
1648 d_result
= em
->mkExpr(kind::SEXPR
, result
);
1649 d_commandStatus
= CommandSuccess::instance();
1651 catch (RecoverableModalException
& e
)
1653 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1655 catch (UnsafeInterruptException
& e
)
1657 d_commandStatus
= new CommandInterrupted();
1659 catch (exception
& e
)
1661 d_commandStatus
= new CommandFailure(e
.what());
1665 Expr
GetValueCommand::getResult() const { return d_result
; }
1666 void GetValueCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1670 this->Command::printResult(out
, verbosity
);
1674 expr::ExprDag::Scope
scope(out
, false);
1675 out
<< d_result
<< endl
;
1679 Command
* GetValueCommand::exportTo(ExprManager
* exprManager
,
1680 ExprManagerMapCollection
& variableMap
)
1682 vector
<Expr
> exportedTerms
;
1683 for (std::vector
<Expr
>::const_iterator i
= d_terms
.begin();
1687 exportedTerms
.push_back((*i
).exportTo(exprManager
, variableMap
));
1689 GetValueCommand
* c
= new GetValueCommand(exportedTerms
);
1690 c
->d_result
= d_result
.exportTo(exprManager
, variableMap
);
1694 Command
* GetValueCommand::clone() const
1696 GetValueCommand
* c
= new GetValueCommand(d_terms
);
1697 c
->d_result
= d_result
;
1701 std::string
GetValueCommand::getCommandName() const { return "get-value"; }
1703 /* -------------------------------------------------------------------------- */
1704 /* class GetAssignmentCommand */
1705 /* -------------------------------------------------------------------------- */
1707 GetAssignmentCommand::GetAssignmentCommand() {}
1708 void GetAssignmentCommand::invoke(SmtEngine
* smtEngine
)
1712 std::vector
<std::pair
<Expr
, Expr
>> assignments
= smtEngine
->getAssignment();
1713 vector
<SExpr
> sexprs
;
1714 for (const auto& p
: assignments
)
1717 v
.emplace_back(SExpr::Keyword(p
.first
.toString()));
1718 v
.emplace_back(SExpr::Keyword(p
.second
.toString()));
1719 sexprs
.emplace_back(v
);
1721 d_result
= SExpr(sexprs
);
1722 d_commandStatus
= CommandSuccess::instance();
1724 catch (RecoverableModalException
& e
)
1726 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1728 catch (UnsafeInterruptException
& e
)
1730 d_commandStatus
= new CommandInterrupted();
1732 catch (exception
& e
)
1734 d_commandStatus
= new CommandFailure(e
.what());
1738 SExpr
GetAssignmentCommand::getResult() const { return d_result
; }
1739 void GetAssignmentCommand::printResult(std::ostream
& out
,
1740 uint32_t verbosity
) const
1744 this->Command::printResult(out
, verbosity
);
1748 out
<< d_result
<< endl
;
1752 Command
* GetAssignmentCommand::exportTo(ExprManager
* exprManager
,
1753 ExprManagerMapCollection
& variableMap
)
1755 GetAssignmentCommand
* c
= new GetAssignmentCommand();
1756 c
->d_result
= d_result
;
1760 Command
* GetAssignmentCommand::clone() const
1762 GetAssignmentCommand
* c
= new GetAssignmentCommand();
1763 c
->d_result
= d_result
;
1767 std::string
GetAssignmentCommand::getCommandName() const
1769 return "get-assignment";
1772 /* -------------------------------------------------------------------------- */
1773 /* class GetModelCommand */
1774 /* -------------------------------------------------------------------------- */
1776 GetModelCommand::GetModelCommand() : d_result(nullptr), d_smtEngine(nullptr) {}
1777 void GetModelCommand::invoke(SmtEngine
* smtEngine
)
1781 d_result
= smtEngine
->getModel();
1782 d_smtEngine
= smtEngine
;
1783 d_commandStatus
= CommandSuccess::instance();
1785 catch (RecoverableModalException
& e
)
1787 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1789 catch (UnsafeInterruptException
& e
)
1791 d_commandStatus
= new CommandInterrupted();
1793 catch (exception
& e
)
1795 d_commandStatus
= new CommandFailure(e
.what());
1799 /* Model is private to the library -- for now
1800 Model* GetModelCommand::getResult() const {
1805 void GetModelCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1809 this->Command::printResult(out
, verbosity
);
1817 Command
* GetModelCommand::exportTo(ExprManager
* exprManager
,
1818 ExprManagerMapCollection
& variableMap
)
1820 GetModelCommand
* c
= new GetModelCommand();
1821 c
->d_result
= d_result
;
1822 c
->d_smtEngine
= d_smtEngine
;
1826 Command
* GetModelCommand::clone() const
1828 GetModelCommand
* c
= new GetModelCommand();
1829 c
->d_result
= d_result
;
1830 c
->d_smtEngine
= d_smtEngine
;
1834 std::string
GetModelCommand::getCommandName() const { return "get-model"; }
1836 /* -------------------------------------------------------------------------- */
1837 /* class BlockModelCommand */
1838 /* -------------------------------------------------------------------------- */
1840 BlockModelCommand::BlockModelCommand() {}
1841 void BlockModelCommand::invoke(SmtEngine
* smtEngine
)
1845 smtEngine
->blockModel();
1846 d_commandStatus
= CommandSuccess::instance();
1848 catch (RecoverableModalException
& e
)
1850 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1852 catch (UnsafeInterruptException
& e
)
1854 d_commandStatus
= new CommandInterrupted();
1856 catch (exception
& e
)
1858 d_commandStatus
= new CommandFailure(e
.what());
1862 Command
* BlockModelCommand::exportTo(ExprManager
* exprManager
,
1863 ExprManagerMapCollection
& variableMap
)
1865 BlockModelCommand
* c
= new BlockModelCommand();
1869 Command
* BlockModelCommand::clone() const
1871 BlockModelCommand
* c
= new BlockModelCommand();
1875 std::string
BlockModelCommand::getCommandName() const { return "block-model"; }
1877 /* -------------------------------------------------------------------------- */
1878 /* class BlockModelValuesCommand */
1879 /* -------------------------------------------------------------------------- */
1881 BlockModelValuesCommand::BlockModelValuesCommand(const std::vector
<Expr
>& terms
)
1884 PrettyCheckArgument(terms
.size() >= 1,
1886 "cannot block-model-values of an empty set of terms");
1889 const std::vector
<Expr
>& BlockModelValuesCommand::getTerms() const
1893 void BlockModelValuesCommand::invoke(SmtEngine
* smtEngine
)
1897 smtEngine
->blockModelValues(d_terms
);
1898 d_commandStatus
= CommandSuccess::instance();
1900 catch (RecoverableModalException
& e
)
1902 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1904 catch (UnsafeInterruptException
& e
)
1906 d_commandStatus
= new CommandInterrupted();
1908 catch (exception
& e
)
1910 d_commandStatus
= new CommandFailure(e
.what());
1914 Command
* BlockModelValuesCommand::exportTo(
1915 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
1917 vector
<Expr
> exportedTerms
;
1918 for (std::vector
<Expr
>::const_iterator i
= d_terms
.begin();
1922 exportedTerms
.push_back((*i
).exportTo(exprManager
, variableMap
));
1924 BlockModelValuesCommand
* c
= new BlockModelValuesCommand(exportedTerms
);
1928 Command
* BlockModelValuesCommand::clone() const
1930 BlockModelValuesCommand
* c
= new BlockModelValuesCommand(d_terms
);
1934 std::string
BlockModelValuesCommand::getCommandName() const
1936 return "block-model-values";
1939 /* -------------------------------------------------------------------------- */
1940 /* class GetProofCommand */
1941 /* -------------------------------------------------------------------------- */
1943 GetProofCommand::GetProofCommand() : d_smtEngine(nullptr), d_result(nullptr) {}
1944 void GetProofCommand::invoke(SmtEngine
* smtEngine
)
1948 d_smtEngine
= smtEngine
;
1949 d_result
= &smtEngine
->getProof();
1950 d_commandStatus
= CommandSuccess::instance();
1952 catch (RecoverableModalException
& e
)
1954 d_commandStatus
= new CommandRecoverableFailure(e
.what());
1956 catch (UnsafeInterruptException
& e
)
1958 d_commandStatus
= new CommandInterrupted();
1960 catch (exception
& e
)
1962 d_commandStatus
= new CommandFailure(e
.what());
1966 const Proof
& GetProofCommand::getResult() const { return *d_result
; }
1967 void GetProofCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
1971 this->Command::printResult(out
, verbosity
);
1975 smt::SmtScope
scope(d_smtEngine
);
1976 d_result
->toStream(out
);
1980 Command
* GetProofCommand::exportTo(ExprManager
* exprManager
,
1981 ExprManagerMapCollection
& variableMap
)
1983 GetProofCommand
* c
= new GetProofCommand();
1984 c
->d_result
= d_result
;
1985 c
->d_smtEngine
= d_smtEngine
;
1989 Command
* GetProofCommand::clone() const
1991 GetProofCommand
* c
= new GetProofCommand();
1992 c
->d_result
= d_result
;
1993 c
->d_smtEngine
= d_smtEngine
;
1997 std::string
GetProofCommand::getCommandName() const { return "get-proof"; }
1999 /* -------------------------------------------------------------------------- */
2000 /* class GetInstantiationsCommand */
2001 /* -------------------------------------------------------------------------- */
2003 GetInstantiationsCommand::GetInstantiationsCommand() : d_smtEngine(nullptr) {}
2004 void GetInstantiationsCommand::invoke(SmtEngine
* smtEngine
)
2008 d_smtEngine
= smtEngine
;
2009 d_commandStatus
= CommandSuccess::instance();
2011 catch (exception
& e
)
2013 d_commandStatus
= new CommandFailure(e
.what());
2017 void GetInstantiationsCommand::printResult(std::ostream
& out
,
2018 uint32_t verbosity
) const
2022 this->Command::printResult(out
, verbosity
);
2026 d_smtEngine
->printInstantiations(out
);
2030 Command
* GetInstantiationsCommand::exportTo(
2031 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2033 GetInstantiationsCommand
* c
= new GetInstantiationsCommand();
2034 // c->d_result = d_result;
2035 c
->d_smtEngine
= d_smtEngine
;
2039 Command
* GetInstantiationsCommand::clone() const
2041 GetInstantiationsCommand
* c
= new GetInstantiationsCommand();
2042 // c->d_result = d_result;
2043 c
->d_smtEngine
= d_smtEngine
;
2047 std::string
GetInstantiationsCommand::getCommandName() const
2049 return "get-instantiations";
2052 /* -------------------------------------------------------------------------- */
2053 /* class GetSynthSolutionCommand */
2054 /* -------------------------------------------------------------------------- */
2056 GetSynthSolutionCommand::GetSynthSolutionCommand() : d_smtEngine(nullptr) {}
2057 void GetSynthSolutionCommand::invoke(SmtEngine
* smtEngine
)
2061 d_smtEngine
= smtEngine
;
2062 d_commandStatus
= CommandSuccess::instance();
2064 catch (exception
& e
)
2066 d_commandStatus
= new CommandFailure(e
.what());
2070 void GetSynthSolutionCommand::printResult(std::ostream
& out
,
2071 uint32_t verbosity
) const
2075 this->Command::printResult(out
, verbosity
);
2079 d_smtEngine
->printSynthSolution(out
);
2083 Command
* GetSynthSolutionCommand::exportTo(
2084 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2086 GetSynthSolutionCommand
* c
= new GetSynthSolutionCommand();
2087 c
->d_smtEngine
= d_smtEngine
;
2091 Command
* GetSynthSolutionCommand::clone() const
2093 GetSynthSolutionCommand
* c
= new GetSynthSolutionCommand();
2094 c
->d_smtEngine
= d_smtEngine
;
2098 std::string
GetSynthSolutionCommand::getCommandName() const
2100 return "get-instantiations";
2103 /* -------------------------------------------------------------------------- */
2104 /* class GetInterpolCommand */
2105 /* -------------------------------------------------------------------------- */
2107 GetInterpolCommand::GetInterpolCommand(const api::Solver
* solver
,
2108 const std::string
& name
,
2110 : Command(solver
), d_name(name
), d_conj(conj
), d_resultStatus(false)
2113 GetInterpolCommand::GetInterpolCommand(const api::Solver
* solver
,
2114 const std::string
& name
,
2121 d_resultStatus(false)
2125 api::Term
GetInterpolCommand::getConjecture() const { return d_conj
; }
2127 const api::Grammar
* GetInterpolCommand::getGrammar() const
2129 return d_sygus_grammar
;
2132 api::Term
GetInterpolCommand::getResult() const { return d_result
; }
2134 void GetInterpolCommand::invoke(SmtEngine
* smtEngine
)
2138 if (!d_sygus_grammar
)
2140 d_resultStatus
= d_solver
->getInterpolant(d_conj
, d_result
);
2145 d_solver
->getInterpolant(d_conj
, *d_sygus_grammar
, d_result
);
2147 d_commandStatus
= CommandSuccess::instance();
2149 catch (exception
& e
)
2151 d_commandStatus
= new CommandFailure(e
.what());
2155 void GetInterpolCommand::printResult(std::ostream
& out
,
2156 uint32_t verbosity
) const
2160 this->Command::printResult(out
, verbosity
);
2164 expr::ExprDag::Scope
scope(out
, false);
2167 out
<< "(define-fun " << d_name
<< " () Bool " << d_result
<< ")"
2172 out
<< "none" << std::endl
;
2177 Command
* GetInterpolCommand::exportTo(ExprManager
* exprManager
,
2178 ExprManagerMapCollection
& variableMap
)
2183 Command
* GetInterpolCommand::clone() const
2185 GetInterpolCommand
* c
=
2186 new GetInterpolCommand(d_solver
, d_name
, d_conj
, d_sygus_grammar
);
2187 c
->d_result
= d_result
;
2188 c
->d_resultStatus
= d_resultStatus
;
2192 std::string
GetInterpolCommand::getCommandName() const
2194 return "get-interpol";
2197 /* -------------------------------------------------------------------------- */
2198 /* class GetAbductCommand */
2199 /* -------------------------------------------------------------------------- */
2201 GetAbductCommand::GetAbductCommand(const api::Solver
* solver
,
2202 const std::string
& name
,
2204 : Command(solver
), d_name(name
), d_conj(conj
), d_resultStatus(false)
2207 GetAbductCommand::GetAbductCommand(const api::Solver
* solver
,
2208 const std::string
& name
,
2215 d_resultStatus(false)
2219 api::Term
GetAbductCommand::getConjecture() const { return d_conj
; }
2221 const api::Grammar
* GetAbductCommand::getGrammar() const
2223 return d_sygus_grammar
;
2226 std::string
GetAbductCommand::getAbductName() const { return d_name
; }
2227 api::Term
GetAbductCommand::getResult() const { return d_result
; }
2229 void GetAbductCommand::invoke(SmtEngine
* smtEngine
)
2233 if (!d_sygus_grammar
)
2235 d_resultStatus
= d_solver
->getAbduct(d_conj
, d_result
);
2239 d_resultStatus
= d_solver
->getAbduct(d_conj
, *d_sygus_grammar
, d_result
);
2241 d_commandStatus
= CommandSuccess::instance();
2243 catch (exception
& e
)
2245 d_commandStatus
= new CommandFailure(e
.what());
2249 void GetAbductCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
2253 this->Command::printResult(out
, verbosity
);
2257 expr::ExprDag::Scope
scope(out
, false);
2260 out
<< "(define-fun " << d_name
<< " () Bool " << d_result
<< ")"
2265 out
<< "none" << std::endl
;
2270 Command
* GetAbductCommand::exportTo(ExprManager
* exprManager
,
2271 ExprManagerMapCollection
& variableMap
)
2276 Command
* GetAbductCommand::clone() const
2278 GetAbductCommand
* c
=
2279 new GetAbductCommand(d_solver
, d_name
, d_conj
, d_sygus_grammar
);
2280 c
->d_result
= d_result
;
2281 c
->d_resultStatus
= d_resultStatus
;
2285 std::string
GetAbductCommand::getCommandName() const { return "get-abduct"; }
2287 /* -------------------------------------------------------------------------- */
2288 /* class GetQuantifierEliminationCommand */
2289 /* -------------------------------------------------------------------------- */
2291 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand()
2292 : d_expr(), d_doFull(true)
2295 GetQuantifierEliminationCommand::GetQuantifierEliminationCommand(
2296 const Expr
& expr
, bool doFull
)
2297 : d_expr(expr
), d_doFull(doFull
)
2301 Expr
GetQuantifierEliminationCommand::getExpr() const { return d_expr
; }
2302 bool GetQuantifierEliminationCommand::getDoFull() const { return d_doFull
; }
2303 void GetQuantifierEliminationCommand::invoke(SmtEngine
* smtEngine
)
2307 d_result
= smtEngine
->doQuantifierElimination(d_expr
, d_doFull
);
2308 d_commandStatus
= CommandSuccess::instance();
2310 catch (exception
& e
)
2312 d_commandStatus
= new CommandFailure(e
.what());
2316 Expr
GetQuantifierEliminationCommand::getResult() const { return d_result
; }
2317 void GetQuantifierEliminationCommand::printResult(std::ostream
& out
,
2318 uint32_t verbosity
) const
2322 this->Command::printResult(out
, verbosity
);
2326 out
<< d_result
<< endl
;
2330 Command
* GetQuantifierEliminationCommand::exportTo(
2331 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2333 GetQuantifierEliminationCommand
* c
= new GetQuantifierEliminationCommand(
2334 d_expr
.exportTo(exprManager
, variableMap
), d_doFull
);
2335 c
->d_result
= d_result
;
2339 Command
* GetQuantifierEliminationCommand::clone() const
2341 GetQuantifierEliminationCommand
* c
=
2342 new GetQuantifierEliminationCommand(d_expr
, d_doFull
);
2343 c
->d_result
= d_result
;
2347 std::string
GetQuantifierEliminationCommand::getCommandName() const
2349 return d_doFull
? "get-qe" : "get-qe-disjunct";
2352 /* -------------------------------------------------------------------------- */
2353 /* class GetUnsatAssumptionsCommand */
2354 /* -------------------------------------------------------------------------- */
2356 GetUnsatAssumptionsCommand::GetUnsatAssumptionsCommand() {}
2358 void GetUnsatAssumptionsCommand::invoke(SmtEngine
* smtEngine
)
2362 std::vector
<Node
> uassumps
= smtEngine
->getUnsatAssumptions();
2364 for (const Node
& n
: uassumps
)
2366 d_result
.push_back(n
.toExpr());
2368 d_commandStatus
= CommandSuccess::instance();
2370 catch (RecoverableModalException
& e
)
2372 d_commandStatus
= new CommandRecoverableFailure(e
.what());
2374 catch (exception
& e
)
2376 d_commandStatus
= new CommandFailure(e
.what());
2380 std::vector
<Expr
> GetUnsatAssumptionsCommand::getResult() const
2385 void GetUnsatAssumptionsCommand::printResult(std::ostream
& out
,
2386 uint32_t verbosity
) const
2390 this->Command::printResult(out
, verbosity
);
2394 container_to_stream(out
, d_result
, "(", ")\n", " ");
2398 Command
* GetUnsatAssumptionsCommand::exportTo(
2399 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2401 GetUnsatAssumptionsCommand
* c
= new GetUnsatAssumptionsCommand
;
2402 c
->d_result
= d_result
;
2406 Command
* GetUnsatAssumptionsCommand::clone() const
2408 GetUnsatAssumptionsCommand
* c
= new GetUnsatAssumptionsCommand
;
2409 c
->d_result
= d_result
;
2413 std::string
GetUnsatAssumptionsCommand::getCommandName() const
2415 return "get-unsat-assumptions";
2418 /* -------------------------------------------------------------------------- */
2419 /* class GetUnsatCoreCommand */
2420 /* -------------------------------------------------------------------------- */
2422 GetUnsatCoreCommand::GetUnsatCoreCommand() {}
2423 void GetUnsatCoreCommand::invoke(SmtEngine
* smtEngine
)
2427 d_result
= smtEngine
->getUnsatCore();
2428 d_commandStatus
= CommandSuccess::instance();
2430 catch (RecoverableModalException
& e
)
2432 d_commandStatus
= new CommandRecoverableFailure(e
.what());
2434 catch (exception
& e
)
2436 d_commandStatus
= new CommandFailure(e
.what());
2440 void GetUnsatCoreCommand::printResult(std::ostream
& out
,
2441 uint32_t verbosity
) const
2445 this->Command::printResult(out
, verbosity
);
2449 d_result
.toStream(out
);
2453 const UnsatCore
& GetUnsatCoreCommand::getUnsatCore() const
2455 // of course, this will be empty if the command hasn't been invoked yet
2459 Command
* GetUnsatCoreCommand::exportTo(ExprManager
* exprManager
,
2460 ExprManagerMapCollection
& variableMap
)
2462 GetUnsatCoreCommand
* c
= new GetUnsatCoreCommand
;
2463 c
->d_result
= d_result
;
2467 Command
* GetUnsatCoreCommand::clone() const
2469 GetUnsatCoreCommand
* c
= new GetUnsatCoreCommand
;
2470 c
->d_result
= d_result
;
2474 std::string
GetUnsatCoreCommand::getCommandName() const
2476 return "get-unsat-core";
2479 /* -------------------------------------------------------------------------- */
2480 /* class GetAssertionsCommand */
2481 /* -------------------------------------------------------------------------- */
2483 GetAssertionsCommand::GetAssertionsCommand() {}
2484 void GetAssertionsCommand::invoke(SmtEngine
* smtEngine
)
2489 const vector
<Expr
> v
= smtEngine
->getAssertions();
2491 copy(v
.begin(), v
.end(), ostream_iterator
<Expr
>(ss
, "\n"));
2493 d_result
= ss
.str();
2494 d_commandStatus
= CommandSuccess::instance();
2496 catch (exception
& e
)
2498 d_commandStatus
= new CommandFailure(e
.what());
2502 std::string
GetAssertionsCommand::getResult() const { return d_result
; }
2503 void GetAssertionsCommand::printResult(std::ostream
& out
,
2504 uint32_t verbosity
) const
2508 this->Command::printResult(out
, verbosity
);
2516 Command
* GetAssertionsCommand::exportTo(ExprManager
* exprManager
,
2517 ExprManagerMapCollection
& variableMap
)
2519 GetAssertionsCommand
* c
= new GetAssertionsCommand();
2520 c
->d_result
= d_result
;
2524 Command
* GetAssertionsCommand::clone() const
2526 GetAssertionsCommand
* c
= new GetAssertionsCommand();
2527 c
->d_result
= d_result
;
2531 std::string
GetAssertionsCommand::getCommandName() const
2533 return "get-assertions";
2536 /* -------------------------------------------------------------------------- */
2537 /* class SetBenchmarkStatusCommand */
2538 /* -------------------------------------------------------------------------- */
2540 SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status
)
2545 BenchmarkStatus
SetBenchmarkStatusCommand::getStatus() const
2550 void SetBenchmarkStatusCommand::invoke(SmtEngine
* smtEngine
)
2556 SExpr status
= SExpr(ss
.str());
2557 smtEngine
->setInfo("status", status
);
2558 d_commandStatus
= CommandSuccess::instance();
2560 catch (exception
& e
)
2562 d_commandStatus
= new CommandFailure(e
.what());
2566 Command
* SetBenchmarkStatusCommand::exportTo(
2567 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2569 return new SetBenchmarkStatusCommand(d_status
);
2572 Command
* SetBenchmarkStatusCommand::clone() const
2574 return new SetBenchmarkStatusCommand(d_status
);
2577 std::string
SetBenchmarkStatusCommand::getCommandName() const
2582 /* -------------------------------------------------------------------------- */
2583 /* class SetBenchmarkLogicCommand */
2584 /* -------------------------------------------------------------------------- */
2586 SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic
)
2591 std::string
SetBenchmarkLogicCommand::getLogic() const { return d_logic
; }
2592 void SetBenchmarkLogicCommand::invoke(SmtEngine
* smtEngine
)
2596 smtEngine
->setLogic(d_logic
);
2597 d_commandStatus
= CommandSuccess::instance();
2599 catch (exception
& e
)
2601 d_commandStatus
= new CommandFailure(e
.what());
2605 Command
* SetBenchmarkLogicCommand::exportTo(
2606 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2608 return new SetBenchmarkLogicCommand(d_logic
);
2611 Command
* SetBenchmarkLogicCommand::clone() const
2613 return new SetBenchmarkLogicCommand(d_logic
);
2616 std::string
SetBenchmarkLogicCommand::getCommandName() const
2621 /* -------------------------------------------------------------------------- */
2622 /* class SetInfoCommand */
2623 /* -------------------------------------------------------------------------- */
2625 SetInfoCommand::SetInfoCommand(std::string flag
, const SExpr
& sexpr
)
2626 : d_flag(flag
), d_sexpr(sexpr
)
2630 std::string
SetInfoCommand::getFlag() const { return d_flag
; }
2631 SExpr
SetInfoCommand::getSExpr() const { return d_sexpr
; }
2632 void SetInfoCommand::invoke(SmtEngine
* smtEngine
)
2636 smtEngine
->setInfo(d_flag
, d_sexpr
);
2637 d_commandStatus
= CommandSuccess::instance();
2639 catch (UnrecognizedOptionException
&)
2641 // As per SMT-LIB spec, silently accept unknown set-info keys
2642 d_commandStatus
= CommandSuccess::instance();
2644 catch (exception
& e
)
2646 d_commandStatus
= new CommandFailure(e
.what());
2650 Command
* SetInfoCommand::exportTo(ExprManager
* exprManager
,
2651 ExprManagerMapCollection
& variableMap
)
2653 return new SetInfoCommand(d_flag
, d_sexpr
);
2656 Command
* SetInfoCommand::clone() const
2658 return new SetInfoCommand(d_flag
, d_sexpr
);
2661 std::string
SetInfoCommand::getCommandName() const { return "set-info"; }
2663 /* -------------------------------------------------------------------------- */
2664 /* class GetInfoCommand */
2665 /* -------------------------------------------------------------------------- */
2667 GetInfoCommand::GetInfoCommand(std::string flag
) : d_flag(flag
) {}
2668 std::string
GetInfoCommand::getFlag() const { return d_flag
; }
2669 void GetInfoCommand::invoke(SmtEngine
* smtEngine
)
2674 v
.push_back(SExpr(SExpr::Keyword(string(":") + d_flag
)));
2675 v
.push_back(smtEngine
->getInfo(d_flag
));
2677 if (d_flag
== "all-options" || d_flag
== "all-statistics")
2679 ss
<< PrettySExprs(true);
2682 d_result
= ss
.str();
2683 d_commandStatus
= CommandSuccess::instance();
2685 catch (UnrecognizedOptionException
&)
2687 d_commandStatus
= new CommandUnsupported();
2689 catch (RecoverableModalException
& e
)
2691 d_commandStatus
= new CommandRecoverableFailure(e
.what());
2693 catch (exception
& e
)
2695 d_commandStatus
= new CommandFailure(e
.what());
2699 std::string
GetInfoCommand::getResult() const { return d_result
; }
2700 void GetInfoCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
2704 this->Command::printResult(out
, verbosity
);
2706 else if (d_result
!= "")
2708 out
<< d_result
<< endl
;
2712 Command
* GetInfoCommand::exportTo(ExprManager
* exprManager
,
2713 ExprManagerMapCollection
& variableMap
)
2715 GetInfoCommand
* c
= new GetInfoCommand(d_flag
);
2716 c
->d_result
= d_result
;
2720 Command
* GetInfoCommand::clone() const
2722 GetInfoCommand
* c
= new GetInfoCommand(d_flag
);
2723 c
->d_result
= d_result
;
2727 std::string
GetInfoCommand::getCommandName() const { return "get-info"; }
2729 /* -------------------------------------------------------------------------- */
2730 /* class SetOptionCommand */
2731 /* -------------------------------------------------------------------------- */
2733 SetOptionCommand::SetOptionCommand(std::string flag
, const SExpr
& sexpr
)
2734 : d_flag(flag
), d_sexpr(sexpr
)
2738 std::string
SetOptionCommand::getFlag() const { return d_flag
; }
2739 SExpr
SetOptionCommand::getSExpr() const { return d_sexpr
; }
2740 void SetOptionCommand::invoke(SmtEngine
* smtEngine
)
2744 smtEngine
->setOption(d_flag
, d_sexpr
);
2745 d_commandStatus
= CommandSuccess::instance();
2747 catch (UnrecognizedOptionException
&)
2749 d_commandStatus
= new CommandUnsupported();
2751 catch (exception
& e
)
2753 d_commandStatus
= new CommandFailure(e
.what());
2757 Command
* SetOptionCommand::exportTo(ExprManager
* exprManager
,
2758 ExprManagerMapCollection
& variableMap
)
2760 return new SetOptionCommand(d_flag
, d_sexpr
);
2763 Command
* SetOptionCommand::clone() const
2765 return new SetOptionCommand(d_flag
, d_sexpr
);
2768 std::string
SetOptionCommand::getCommandName() const { return "set-option"; }
2770 /* -------------------------------------------------------------------------- */
2771 /* class GetOptionCommand */
2772 /* -------------------------------------------------------------------------- */
2774 GetOptionCommand::GetOptionCommand(std::string flag
) : d_flag(flag
) {}
2775 std::string
GetOptionCommand::getFlag() const { return d_flag
; }
2776 void GetOptionCommand::invoke(SmtEngine
* smtEngine
)
2780 SExpr res
= smtEngine
->getOption(d_flag
);
2781 d_result
= res
.toString();
2782 d_commandStatus
= CommandSuccess::instance();
2784 catch (UnrecognizedOptionException
&)
2786 d_commandStatus
= new CommandUnsupported();
2788 catch (exception
& e
)
2790 d_commandStatus
= new CommandFailure(e
.what());
2794 std::string
GetOptionCommand::getResult() const { return d_result
; }
2795 void GetOptionCommand::printResult(std::ostream
& out
, uint32_t verbosity
) const
2799 this->Command::printResult(out
, verbosity
);
2801 else if (d_result
!= "")
2803 out
<< d_result
<< endl
;
2807 Command
* GetOptionCommand::exportTo(ExprManager
* exprManager
,
2808 ExprManagerMapCollection
& variableMap
)
2810 GetOptionCommand
* c
= new GetOptionCommand(d_flag
);
2811 c
->d_result
= d_result
;
2815 Command
* GetOptionCommand::clone() const
2817 GetOptionCommand
* c
= new GetOptionCommand(d_flag
);
2818 c
->d_result
= d_result
;
2822 std::string
GetOptionCommand::getCommandName() const { return "get-option"; }
2824 /* -------------------------------------------------------------------------- */
2825 /* class SetExpressionNameCommand */
2826 /* -------------------------------------------------------------------------- */
2828 SetExpressionNameCommand::SetExpressionNameCommand(Expr expr
, std::string name
)
2829 : d_expr(expr
), d_name(name
)
2833 void SetExpressionNameCommand::invoke(SmtEngine
* smtEngine
)
2835 smtEngine
->setExpressionName(d_expr
, d_name
);
2836 d_commandStatus
= CommandSuccess::instance();
2839 Command
* SetExpressionNameCommand::exportTo(
2840 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2842 SetExpressionNameCommand
* c
= new SetExpressionNameCommand(
2843 d_expr
.exportTo(exprManager
, variableMap
), d_name
);
2847 Command
* SetExpressionNameCommand::clone() const
2849 SetExpressionNameCommand
* c
= new SetExpressionNameCommand(d_expr
, d_name
);
2853 std::string
SetExpressionNameCommand::getCommandName() const
2855 return "set-expr-name";
2858 /* -------------------------------------------------------------------------- */
2859 /* class DatatypeDeclarationCommand */
2860 /* -------------------------------------------------------------------------- */
2862 DatatypeDeclarationCommand::DatatypeDeclarationCommand(const Type
& datatype
)
2865 d_datatypes
.push_back(datatype
);
2868 DatatypeDeclarationCommand::DatatypeDeclarationCommand(
2869 const std::vector
<Type
>& datatypes
)
2870 : d_datatypes(datatypes
)
2874 const std::vector
<Type
>& DatatypeDeclarationCommand::getDatatypes() const
2879 void DatatypeDeclarationCommand::invoke(SmtEngine
* smtEngine
)
2881 d_commandStatus
= CommandSuccess::instance();
2884 Command
* DatatypeDeclarationCommand::exportTo(
2885 ExprManager
* exprManager
, ExprManagerMapCollection
& variableMap
)
2887 throw ExportUnsupportedException(
2888 "export of DatatypeDeclarationCommand unsupported");
2891 Command
* DatatypeDeclarationCommand::clone() const
2893 return new DatatypeDeclarationCommand(d_datatypes
);
2896 std::string
DatatypeDeclarationCommand::getCommandName() const
2898 return "declare-datatypes";