From 417299119500eac6a910fcb6b2109f4c129b355c Mon Sep 17 00:00:00 2001 From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> Date: Tue, 20 Oct 2020 14:23:30 -0500 Subject: [PATCH] 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. --- src/api/cvc4cpp.cpp | 20 ------------- src/api/cvc4cpp.h | 8 ----- src/api/python/cvc4.pxd | 1 - src/api/python/cvc4.pxi | 13 --------- src/printer/printer.cpp | 5 ---- src/printer/printer.h | 3 -- src/smt/command.cpp | 65 ++--------------------------------------- src/smt/command.h | 23 --------------- 8 files changed, 3 insertions(+), 135 deletions(-) diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp index 2417936a7..f4717158a 100644 --- a/src/api/cvc4cpp.cpp +++ b/src/api/cvc4cpp.cpp @@ -5042,26 +5042,6 @@ std::vector Solver::getAssertions(void) const CVC4_API_SOLVER_TRY_CATCH_END; } -/** - * ( get-assignment ) - */ -std::vector> Solver::getAssignment(void) const -{ - CVC4_API_SOLVER_TRY_CATCH_BEGIN; - CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get())); - CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceAssignments]) - << "Cannot get assignment unless assignment generation is enabled " - "(try --produce-assignments)"; - std::vector> assignment = d_smtEngine->getAssignment(); - std::vector> res; - for (const auto& p : assignment) - { - res.emplace_back(Term(this, p.first), Term(this, p.second)); - } - return res; - CVC4_API_SOLVER_TRY_CATCH_END; -} - /** * ( get-info ) */ diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h index 5c6b01d59..99e67dd2a 100644 --- a/src/api/cvc4cpp.h +++ b/src/api/cvc4cpp.h @@ -3040,14 +3040,6 @@ class CVC4_PUBLIC Solver */ std::vector getAssertions() const; - /** - * Get the assignment of asserted formulas. - * SMT-LIB: ( get-assignment ) - * Requires to enable option 'produce-assignments'. - * @return a list of formula-assignment pairs - */ - std::vector> getAssignment() const; - /** * Get info from the solver. * SMT-LIB: ( get-info ) diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd index a9f2e3abc..73ccde14a 100644 --- a/src/api/python/cvc4.pxd +++ b/src/api/python/cvc4.pxd @@ -229,7 +229,6 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api": Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars, vector[Term]& terms, bint glbl) except + vector[Term] getAssertions() except + - vector[pair[Term, Term]] getAssignment() except + string getInfo(const string& flag) except + string getOption(string& option) except + vector[Term] getUnsatAssumptions() except + diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi index deadc6849..188b678d1 100644 --- a/src/api/python/cvc4.pxi +++ b/src/api/python/cvc4.pxi @@ -1088,19 +1088,6 @@ cdef class Solver: assertions.append(term) return assertions - def getAssignment(self): - ''' - Gives the assignment of *named* formulas as a dictionary. - ''' - assignments = {} - for a in self.csolver.getAssignment(): - varterm = Term(self) - valterm = Term(self) - varterm.cterm = a.first - valterm.cterm = a.second - assignments[varterm] = valterm - return assignments - def getInfo(self, str flag): return self.csolver.getInfo(flag.encode()) diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp index ba062c20f..e760c21aa 100644 --- a/src/printer/printer.cpp +++ b/src/printer/printer.cpp @@ -262,11 +262,6 @@ void Printer::toStreamCmdSimplify(std::ostream& out, Node n) const printUnknownCommand(out, "simplify"); } -void Printer::toStreamCmdExpandDefinitions(std::ostream& out, Node n) const -{ - printUnknownCommand(out, "expand-definitions"); -} - void Printer::toStreamCmdGetValue(std::ostream& out, const std::vector& nodes) const { diff --git a/src/printer/printer.h b/src/printer/printer.h index b95b02ca8..85b16175f 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -160,9 +160,6 @@ class Printer /** Print simplify command */ virtual void toStreamCmdSimplify(std::ostream& out, Node n) const; - /** Print expand-definitions command */ - void toStreamCmdExpandDefinitions(std::ostream& out, Node n) const; - /** Print get-value command */ virtual void toStreamCmdGetValue(std::ostream& out, const std::vector& nodes) const; 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 @@ -1583,65 +1583,6 @@ void SimplifyCommand::toStream(std::ostream& out, Printer::getPrinter(language)->toStreamCmdSimplify(out, d_term.getNode()); } -/* -------------------------------------------------------------------------- */ -/* 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> assignments = - solver->getAssignment(); + std::vector> assignments = + solver->getSmtEngine()->getAssignment(); vector 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: -- 2.30.2