From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 25 Nov 2021 02:39:39 +0000 (-0800)
Subject: api: Refactor mkTerm for kinds with arity = 0. (#7699)
X-Git-Tag: cvc5-1.0.0~768
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=943dfc57d1bbc58046ad10bb4a8a48a8b654aeb5;p=cvc5.git

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 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));
 
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 75cb5a13b..36b669bca 100644
--- 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 95ee9826f..4abfe0697 100644
--- 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)