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.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 0c35abd4c1816b88139d0eafb4d21d70bfd1a23c..3edff5ec335a9ae6971eb576ffabe3d36328dd6a 100644 (file)
--- 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));
 

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 75cb5a13b4c08e04fa298f32bfdcd4d83b5028b2..36b669bca4b2ecbff3385b0a9c7718767c515a9e 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -658,8 +658,21 @@ TEST_F(TestApiBlackSolver, mkTerm)
 
   // mkTerm(Kind kind) const
   ASSERT_NO_THROW(d_solver.mkTerm(PI));
+  ASSERT_NO_THROW(d_solver.mkTerm(PI, v6));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI)));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(PI), v6));
   ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE));
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_NONE, v6));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE)));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_NONE), v6));
   ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR));
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_ALLCHAR, v6));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR)));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(REGEXP_ALLCHAR), v6));
+  ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP));
+  ASSERT_NO_THROW(d_solver.mkTerm(SEP_EMP, v6));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP)));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(SEP_EMP), v6));
   ASSERT_THROW(d_solver.mkTerm(CONST_BITVECTOR), CVC5ApiException);
 
   // mkTerm(Kind kind, Term child) const

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 95ee9826f97c1f8017653fbd2b9db5c08ae22063..4abfe0697d0910a78996a3ad5254ba2571e73c42 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -696,8 +696,22 @@ def test_mk_term(solver):
 
     # mkTerm(Kind kind) const
     solver.mkPi()
+    solver.mkTerm(kinds.Pi)
+    solver.mkTerm(kinds.Pi, v6)
+    solver.mkTerm(solver.mkOp(kinds.Pi))
+    solver.mkTerm(solver.mkOp(kinds.Pi), v6)
     solver.mkTerm(kinds.RegexpNone)
+    solver.mkTerm(kinds.RegexpNone, v6)
+    solver.mkTerm(solver.mkOp(kinds.RegexpNone))
+    solver.mkTerm(solver.mkOp(kinds.RegexpNone), v6)
     solver.mkTerm(kinds.RegexpAllchar)
+    solver.mkTerm(kinds.RegexpAllchar, v6)
+    solver.mkTerm(solver.mkOp(kinds.RegexpAllchar))
+    solver.mkTerm(solver.mkOp(kinds.RegexpAllchar), v6)
+    solver.mkTerm(kinds.SepEmp)
+    solver.mkTerm(kinds.SepEmp, v6)
+    solver.mkTerm(solver.mkOp(kinds.SepEmp))
+    solver.mkTerm(solver.mkOp(kinds.SepEmp), v6)
     with pytest.raises(RuntimeError):
         solver.mkTerm(kinds.ConstBV)