api: Refactor mkTerm for kinds with arity = 0. (#7699)

This refactors mkTerm to allow creation of terms of kinds with arity = 0
via Op and/or empty children vector.

1 files changed, 6 insertions, 5 deletions

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0c35abd4c..3edff5ec3 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5164,7 +5164,10 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
 {
   // Note: Kind and children are checked in the caller to avoid double checks
   //////// all checks before this line
-
+  if (children.size() == 0)
+  {
+    return mkTermFromKind(kind);
+  }
   std::vector<Node> echildren = Term::termVectorToNodes(children);
   cvc5::Kind k = extToIntKind(kind);
   Node res;
@@ -6303,14 +6306,12 @@ Term Solver::mkTerm(const Op& op) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_OP(op);
-  checkMkTerm(op.d_kind, 0);
-  //////// all checks before this line
-
   if (!op.isIndexedHelper())
   {
     return mkTermFromKind(op.d_kind);
   }
-
+  checkMkTerm(op.d_kind, 0);
+  //////// all checks before this line
   const cvc5::Kind int_kind = extToIntKind(op.d_kind);
   Term res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node));