diff options
author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2020-10-20 14:23:30 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-20 14:23:30 -0500 |
commit | 417299119500eac6a910fcb6b2109f4c129b355c (patch) | |
tree | 9f2237f45fd8353e6cc367acabc6b386f85c797f | |
parent | a0ccf529025b86d368dac6b8c4f6b78a97857f4b (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.
-rw-r--r-- | src/api/cvc4cpp.cpp | 20 | ||||
-rw-r--r-- | src/api/cvc4cpp.h | 8 | ||||
-rw-r--r-- | src/api/python/cvc4.pxd | 1 | ||||
-rw-r--r-- | src/api/python/cvc4.pxi | 13 | ||||
-rw-r--r-- | src/printer/printer.cpp | 5 | ||||
-rw-r--r-- | src/printer/printer.h | 3 | ||||
-rw-r--r-- | src/smt/command.cpp | 65 | ||||
-rw-r--r-- | 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 @@ -5043,26 +5043,6 @@ std::vector<Term> Solver::getAssertions(void) const } /** - * ( get-assignment ) - */ -std::vector<std::pair<Term, Term>> 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<std::pair<Expr, Expr>> assignment = d_smtEngine->getAssignment(); - std::vector<std::pair<Term, Term>> 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 <info_flag> ) */ std::string Solver::getInfo(const std::string& flag) const 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 @@ -3041,14 +3041,6 @@ class CVC4_PUBLIC Solver std::vector<Term> 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<std::pair<Term, Term>> getAssignment() const; - - /** * Get info from the solver. * SMT-LIB: ( get-info <info_flag> ) * @return the 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<Node>& 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<Node>& 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 @@ -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: |