summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorAbdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>2020-10-20 14:23:30 -0500
committerGitHub <noreply@github.com>2020-10-20 14:23:30 -0500
commit417299119500eac6a910fcb6b2109f4c129b355c (patch)
tree9f2237f45fd8353e6cc367acabc6b386f85c797f /src/smt
parenta0ccf529025b86d368dac6b8c4f6b78a97857f4b (diff)
Remove some Commands from the API. (#5268)
This PR removes Solver::getAssignment command from the API as there is no way to assign names to terms in the API. It also removes ExpandDefinitionsCommand, an internal functionality in CVC4.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/command.cpp65
-rw-r--r--src/smt/command.h23
2 files changed, 3 insertions, 85 deletions
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 73553a31c..9c45c0b19 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1584,65 +1584,6 @@ void SimplifyCommand::toStream(std::ostream& out,
}
/* -------------------------------------------------------------------------- */
-/* class ExpandDefinitionsCommand */
-/* -------------------------------------------------------------------------- */
-
-ExpandDefinitionsCommand::ExpandDefinitionsCommand(api::Term term)
- : d_term(term)
-{
-}
-api::Term ExpandDefinitionsCommand::getTerm() const { return d_term; }
-void ExpandDefinitionsCommand::invoke(api::Solver* solver)
-{
- try
- {
- d_result = api::Term(
- solver, solver->getSmtEngine()->expandDefinitions(d_term.getNode()));
- d_commandStatus = CommandSuccess::instance();
- }
- catch (exception& e)
- {
- d_commandStatus = new CommandFailure(e.what());
- }
-}
-
-api::Term ExpandDefinitionsCommand::getResult() const { return d_result; }
-void ExpandDefinitionsCommand::printResult(std::ostream& out,
- uint32_t verbosity) const
-{
- if (!ok())
- {
- this->Command::printResult(out, verbosity);
- }
- else
- {
- out << d_result << endl;
- }
-}
-
-Command* ExpandDefinitionsCommand::clone() const
-{
- ExpandDefinitionsCommand* c = new ExpandDefinitionsCommand(d_term);
- c->d_result = d_result;
- return c;
-}
-
-std::string ExpandDefinitionsCommand::getCommandName() const
-{
- return "expand-definitions";
-}
-
-void ExpandDefinitionsCommand::toStream(std::ostream& out,
- int toDepth,
- bool types,
- size_t dag,
- OutputLanguage language) const
-{
- Printer::getPrinter(language)->toStreamCmdExpandDefinitions(out,
- d_term.getNode());
-}
-
-/* -------------------------------------------------------------------------- */
/* class GetValueCommand */
/* -------------------------------------------------------------------------- */
@@ -1741,8 +1682,8 @@ void GetAssignmentCommand::invoke(api::Solver* solver)
{
try
{
- std::vector<std::pair<api::Term, api::Term>> assignments =
- solver->getAssignment();
+ std::vector<std::pair<Expr, Expr>> assignments =
+ solver->getSmtEngine()->getAssignment();
vector<SExpr> sexprs;
for (const auto& p : assignments)
{
@@ -1754,7 +1695,7 @@ void GetAssignmentCommand::invoke(api::Solver* solver)
d_result = SExpr(sexprs);
d_commandStatus = CommandSuccess::instance();
}
- catch (api::CVC4ApiRecoverableException& e)
+ catch (RecoverableModalException& e)
{
d_commandStatus = new CommandRecoverableFailure(e.what());
}
diff --git a/src/smt/command.h b/src/smt/command.h
index 41776cee5..b81b55b91 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -911,29 +911,6 @@ class CVC4_PUBLIC SimplifyCommand : public Command
OutputLanguage language = language::output::LANG_AUTO) const override;
}; /* class SimplifyCommand */
-class CVC4_PUBLIC ExpandDefinitionsCommand : public Command
-{
- protected:
- api::Term d_term;
- api::Term d_result;
-
- public:
- ExpandDefinitionsCommand(api::Term term);
-
- api::Term getTerm() const;
- api::Term getResult() const;
- void invoke(api::Solver* solver) override;
- void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
- Command* clone() const override;
- std::string getCommandName() const override;
- void toStream(
- std::ostream& out,
- int toDepth = -1,
- bool types = false,
- size_t dag = 1,
- OutputLanguage language = language::output::LANG_AUTO) const override;
-}; /* class ExpandDefinitionsCommand */
-
class CVC4_PUBLIC GetValueCommand : public Command
{
protected:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback