From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 6 Apr 2020 20:29:05 +0000 (-0700)
Subject: New C++ API: Rename Solver::mkTermInternal. (#4217)
X-Git-Tag: cvc5-1.0.0~3403
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9be8854786a6d27dfde21525e810a3b2f15e9d21;p=cvc5.git

New C++ API: Rename Solver::mkTermInternal. (#4217)

This is for consistency with the other helper functions.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index ba42c4a93..8d6de0ade 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2386,7 +2386,7 @@ Term Solver::mkTermFromKind(Kind kind) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-Term Solver::mkTermInternal(Kind kind, const std::vector<Term>& children) const
+Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   for (size_t i = 0, size = children.size(); i < size; ++i)
@@ -3259,12 +3259,12 @@ Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
 Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
 {
   // need to use internal term call to check e.g. associative construction
-  return mkTermInternal(kind, std::vector<Term>{child1, child2, child3});
+  return mkTermHelper(kind, std::vector<Term>{child1, child2, child3});
 }
 
 Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
 {
-  return mkTermInternal(kind, children);
+  return mkTermHelper(kind, children);
 }
 
 Term Solver::mkTerm(Op op) const
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index a2683e773..5c435d93e 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2852,7 +2852,7 @@ class CVC4_PUBLIC Solver
    * @param children the children of the term
    * @return the Term
    */
-  Term mkTermInternal(Kind kind, const std::vector<Term>& children) const;
+  Term mkTermHelper(Kind kind, const std::vector<Term>& children) const;
 
   /**
    * Create a vector of datatype sorts, using unresolved sorts.