New C++ API: Clean up usage of internal Type/TypeNodes. (#6044)

This disables the temporarily available internals of Sort.

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index a426c927018b4ad594361b350e48123bc9e9d310..380a427ffac25512f7cfea9ee83c2f7fb0b2bf36 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1008,6 +1008,38 @@ Sort::~Sort()
   }
 }
 
+std::set<TypeNode> Sort::sortSetToTypeNodes(const std::set<Sort>& sorts)
+{
+  std::set<TypeNode> types;
+  for (const Sort& s : sorts)
+  {
+    types.insert(s.getTypeNode());
+  }
+  return types;
+}
+
+std::vector<TypeNode> Sort::sortVectorToTypeNodes(
+    const std::vector<Sort>& sorts)
+{
+  std::vector<TypeNode> typeNodes;
+  for (const Sort& sort : sorts)
+  {
+    typeNodes.push_back(sort.getTypeNode());
+  }
+  return typeNodes;
+}
+
+std::vector<Sort> Sort::typeNodeVectorToSorts(
+    const Solver* slv, const std::vector<TypeNode>& types)
+{
+  std::vector<Sort> sorts;
+  for (size_t i = 0, tsize = types.size(); i < tsize; i++)
+  {
+    sorts.push_back(Sort(slv, types[i]));
+  }
+  return sorts;
+}
+
 /* Helpers                                                                    */
 /* -------------------------------------------------------------------------- */
 
@@ -1144,14 +1176,6 @@ std::string Sort::toString() const
   return d_type->toString();
 }
 
-// !!! This is only temporarily available until the parser is fully migrated
-// to the new API. !!!
-CVC4::Type Sort::getType(void) const
-{
-  if (d_type->isNull()) return Type();
-  NodeManagerScope scope(d_solver->getNodeManager());
-  return d_type->toType();
-}
 const CVC4::TypeNode& Sort::getTypeNode(void) const { return *d_type; }
 
 /* Constructor sort ------------------------------------------------------- */
@@ -2359,7 +2383,7 @@ DatatypeDecl::DatatypeDecl(const Solver* slv,
                            bool isCoDatatype)
     : d_solver(slv)
 {
-  std::vector<TypeNode> tparams = sortVectorToTypeNodes(params);
+  std::vector<TypeNode> tparams = Sort::sortVectorToTypeNodes(params);
   d_dtype = std::shared_ptr<CVC4::DType>(
       new CVC4::DType(name, tparams, isCoDatatype));
 }
@@ -3131,7 +3155,7 @@ void Grammar::addSygusConstructorTerm(
         d_solver->getExprManager()->mkExpr(
             CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()}));
   }
-  std::vector<TypeNode> cargst = sortVectorToTypeNodes(cargs);
+  std::vector<TypeNode> cargst = Sort::sortVectorToTypeNodes(cargs);
   dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
 }
 
@@ -3513,10 +3537,10 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
     CVC4_API_SOLVER_CHECK_SORT(sort);
   }
 
-  std::set<TypeNode> utypes = sortSetToTypeNodes(unresolvedSorts);
+  std::set<TypeNode> utypes = Sort::sortSetToTypeNodes(unresolvedSorts);
   std::vector<CVC4::TypeNode> dtypes =
       getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes);
-  std::vector<Sort> retTypes = typeNodeVectorToSorts(this, dtypes);
+  std::vector<Sort> retTypes = Sort::typeNodeVectorToSorts(this, dtypes);
   return retTypes;
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -3525,18 +3549,6 @@ std::vector<Sort> Solver::mkDatatypeSortsInternal(
 /* Helpers for converting vectors.                                            */
 /* .......................................................................... */
 
-std::vector<Type> Solver::sortVectorToTypes(
-    const std::vector<Sort>& sorts) const
-{
-  std::vector<Type> res;
-  for (const Sort& s : sorts)
-  {
-    CVC4_API_SOLVER_CHECK_SORT(s);
-    res.push_back(s.d_type->toType());
-  }
-  return res;
-}
-
 std::vector<Expr> Solver::termVectorToExprs(
     const std::vector<Term>& terms) const
 {
@@ -3760,7 +3772,7 @@ Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
       << "first-class sort as codomain sort for function sort";
   Assert(!codomain.isFunction()); /* A function sort is not first-class. */
 
-  std::vector<TypeNode> argTypes = sortVectorToTypeNodes(sorts);
+  std::vector<TypeNode> argTypes = Sort::sortVectorToTypeNodes(sorts);
   return Sort(this,
               getNodeManager()->mkFunctionType(argTypes, *codomain.d_type));
 
@@ -3795,7 +3807,7 @@ Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
         sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
         << "first-class sort as parameter sort for predicate sort";
   }
-  std::vector<TypeNode> types = sortVectorToTypeNodes(sorts);
+  std::vector<TypeNode> types = Sort::sortVectorToTypeNodes(sorts);
 
   return Sort(this, getNodeManager()->mkPredicateType(types));
 
@@ -3901,7 +3913,7 @@ Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
         !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
         << "non-function-like sort as parameter sort for tuple sort";
   }
-  std::vector<TypeNode> typeNodes = sortVectorToTypeNodes(sorts);
+  std::vector<TypeNode> typeNodes = Sort::sortVectorToTypeNodes(sorts);
   return Sort(this, getNodeManager()->mkTupleType(typeNodes));
 
   CVC4_API_SOLVER_TRY_CATCH_END;
@@ -4969,7 +4981,7 @@ Term Solver::declareFun(const std::string& symbol,
   TypeNode type = *sort.d_type;
   if (!sorts.empty())
   {
-    std::vector<TypeNode> types = sortVectorToTypeNodes(sorts);
+    std::vector<TypeNode> types = Sort::sortVectorToTypeNodes(sorts);
     type = getNodeManager()->mkFunctionType(types, type);
   }
   return Term(this, d_exprMgr->mkVar(symbol, type.toType()));
@@ -6058,36 +6070,6 @@ std::vector<Node> termVectorToNodes(const std::vector<Term>& terms)
   return res;
 }
 
-std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts)
-{
-  std::vector<Type> types;
-  for (size_t i = 0, ssize = sorts.size(); i < ssize; i++)
-  {
-    types.push_back(sorts[i].getTypeNode().toType());
-  }
-  return types;
-}
-
-std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts)
-{
-  std::vector<TypeNode> typeNodes;
-  for (const Sort& sort : sorts)
-  {
-    typeNodes.push_back(sort.getTypeNode());
-  }
-  return typeNodes;
-}
-
-std::set<TypeNode> sortSetToTypeNodes(const std::set<Sort>& sorts)
-{
-  std::set<TypeNode> types;
-  for (const Sort& s : sorts)
-  {
-    types.insert(s.getTypeNode());
-  }
-  return types;
-}
-
 std::vector<Term> exprVectorToTerms(const Solver* slv,
                                     const std::vector<Expr>& exprs)
 {
@@ -6099,27 +6081,6 @@ std::vector<Term> exprVectorToTerms(const Solver* slv,
   return terms;
 }
 
-std::vector<Sort> typeVectorToSorts(const Solver* slv,
-                                    const std::vector<Type>& types)
-{
-  std::vector<Sort> sorts;
-  for (size_t i = 0, tsize = types.size(); i < tsize; i++)
-  {
-    sorts.push_back(Sort(slv, TypeNode::fromType(types[i])));
-  }
-  return sorts;
-}
-std::vector<Sort> typeNodeVectorToSorts(const Solver* slv,
-                                        const std::vector<TypeNode>& types)
-{
-  std::vector<Sort> sorts;
-  for (size_t i = 0, tsize = types.size(); i < tsize; i++)
-  {
-    sorts.push_back(Sort(slv, types[i]));
-  }
-  return sorts;
-}
-
 }  // namespace api
 
 /* -------------------------------------------------------------------------- */

diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index f68fe4c0bba6464598ec4b71c148c18e546f0359..00326204e186ec345f614432a850535fa4a5afcb 100644 (file)
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -40,11 +40,18 @@ template <bool ref_count>
 class NodeTemplate;
 typedef NodeTemplate<true> Node;
 class Expr;
+class DatatypeDeclarationCommand;
+class DeclareFunctionCommand;
+class DeclareHeapCommand;
+class DeclareSortCommand;
+class DeclareSygusVarCommand;
+class DefineSortCommand;
 class DType;
 class DTypeConstructor;
 class DTypeSelector;
 class ExprManager;
 class GetAbductCommand;
+class GetModelCommand;
 class GetInterpolCommand;
 class NodeManager;
 class SmtEngine;
@@ -223,8 +230,19 @@ class Datatype;
  */
 class CVC4_PUBLIC Sort
 {
+  friend class CVC4::DatatypeDeclarationCommand;
+  friend class CVC4::DeclareFunctionCommand;
+  friend class CVC4::DeclareHeapCommand;
+  friend class CVC4::DeclareSortCommand;
+  friend class CVC4::DeclareSygusVarCommand;
+  friend class CVC4::DefineSortCommand;
+  friend class CVC4::GetAbductCommand;
+  friend class CVC4::GetInterpolCommand;
+  friend class CVC4::GetModelCommand;
+  friend class CVC4::SynthFunCommand;
   friend class DatatypeConstructor;
   friend class DatatypeConstructorDecl;
+  friend class DatatypeSelector;
   friend class DatatypeDecl;
   friend class Op;
   friend class Solver;
@@ -233,17 +251,6 @@ class CVC4_PUBLIC Sort
   friend class Term;
 
  public:
-  // !!! This constructor is only temporarily public until the parser is fully
-  // migrated to the new API. !!!
-  /**
-   * Constructor.
-   * @param slv the associated solver object
-   * @param t the internal type that is to be wrapped by this sort
-   * @return the Sort
-   */
-  Sort(const Solver* slv, const CVC4::Type& t);
-  Sort(const Solver* slv, const CVC4::TypeNode& t);
-
   /**
    * Constructor.
    */
@@ -519,11 +526,6 @@ class CVC4_PUBLIC Sort
    */
   std::string toString() const;
 
-  // !!! This is only temporarily available until the parser is fully migrated
-  // to the new API. !!!
-  CVC4::Type getType(void) const;
-  const CVC4::TypeNode& getTypeNode(void) const;
-
   /* Constructor sort ------------------------------------------------------- */
 
   /**
@@ -688,6 +690,27 @@ class CVC4_PUBLIC Sort
   std::vector<Sort> getTupleSorts() const;
 
  private:
+  /** @return the internal wrapped TypeNode of this sort. */
+  const CVC4::TypeNode& getTypeNode(void) const;
+
+  /** Helper to convert a set of Sorts to internal TypeNodes. */
+  std::set<TypeNode> static sortSetToTypeNodes(const std::set<Sort>& sorts);
+  /* Helper to convert a vector of Sorts to internal TypeNodes. */
+  std::vector<TypeNode> static sortVectorToTypeNodes(
+      const std::vector<Sort>& sorts);
+  /** Helper to convert a vector of internal TypeNodes to Sorts. */
+  std::vector<Sort> static typeNodeVectorToSorts(
+      const Solver* slv, const std::vector<TypeNode>& types);
+
+  /**
+   * Constructor.
+   * @param slv the associated solver object
+   * @param t the internal type that is to be wrapped by this sort
+   * @return the Sort
+   */
+  Sort(const Solver* slv, const CVC4::Type& t);
+  Sort(const Solver* slv, const CVC4::TypeNode& t);
+
   /**
    * Helper for isNull checks. This prevents calling an API function with
    * CVC4_API_CHECK_NOT_NULL
@@ -3530,9 +3553,7 @@ class CVC4_PUBLIC Solver
   Options& getOptions(void);
 
  private:
-  /* Helper to convert a vector of internal types to sorts. */
-  std::vector<Type> sortVectorToTypes(const std::vector<Sort>& vector) const;
-  /* Helper to convert a vector of sorts to internal types. */
+  /* Helper to convert a vector of Terms to internal Exprs. */
   std::vector<Expr> termVectorToExprs(const std::vector<Term>& vector) const;
   /* Helper to check for API misuse in mkOp functions. */
   void checkMkTerm(Kind kind, uint32_t nchildren) const;
@@ -3626,15 +3647,8 @@ class CVC4_PUBLIC Solver
 // new API. !!!
 std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms);
 std::vector<Node> termVectorToNodes(const std::vector<Term>& terms);
-std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts);
-std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts);
-std::set<TypeNode> sortSetToTypeNodes(const std::set<Sort>& sorts);
 std::vector<Term> exprVectorToTerms(const Solver* slv,
                                     const std::vector<Expr>& terms);
-std::vector<Sort> typeVectorToSorts(const Solver* slv,
-                                    const std::vector<Type>& sorts);
-std::vector<Sort> typeNodeVectorToSorts(const Solver* slv,
-                                        const std::vector<TypeNode>& types);
 
 }  // namespace api
 

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 9227c37031a2adb3c19738b99f7064f97673470c..3b723de1f3b085bb2ba419fc6bc34116fe7762b8 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1213,7 +1213,7 @@ void DefineSortCommand::toStream(std::ostream& out,
   Printer::getPrinter(language)->toStreamCmdDefineType(
       out,
       d_symbol,
-      api::sortVectorToTypeNodes(d_params),
+      api::Sort::sortVectorToTypeNodes(d_params),
       d_sort.getTypeNode());
 }
 
@@ -2809,7 +2809,7 @@ void DatatypeDeclarationCommand::toStream(std::ostream& out,
                                           OutputLanguage language) const
 {
   Printer::getPrinter(language)->toStreamCmdDatatypeDeclaration(
-      out, api::sortVectorToTypeNodes(d_datatypes));
+      out, api::Sort::sortVectorToTypeNodes(d_datatypes));
 }
 
 }  // namespace CVC4