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.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 2417936a755fcd61cb3295a59d6731b7eb7f64a0..f4717158a5beabc5778927f47474fb09536f960e 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -5042,26 +5042,6 @@ std::vector<Term> Solver::getAssertions(void) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-/**
- *  ( 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> )
  */

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 5c6b01d5928c1eb7f92808ca03904e8ac61dbe31..99e67dd2ae93176e33f254a11eb7a5b47a30023f 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3040,14 +3040,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> )

diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index a9f2e3abc37edc730457415eacad768afcb2a357..73ccde14a313dcb89b5313b71116c0db435a6c88 100644 (file)
--- 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 deadc68493ea963262cab39eb2d5c89178014fc9..188b678d1398e7c600438c53ef2786c0b8a261f3 100644 (file)
--- 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 ba062c20fcb0bd0e42de13b62cac4b597b8ae35b..e760c21aab08fc46de298d3921844715065fd70e 100644 (file)
--- 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 b95b02ca836c8adaca10a0366d17c416972fd019..85b16175f45f6a0282e6fb6335fd335f162ad0b2 100644 (file)
--- 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 73553a31cef312c809aca9d29fa39268b50fcd95..9c45c0b196fbd40ba86f9be79a849d5bbad9bf29 100644 (file)
--- 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<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 41776cee50db3b1687424834d8795993eaf4f1f3..b81b55b91fa35bf201b075a13872c47bfb57ce2d 100644 (file)
--- 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: