api: Fix creation of nary term kinds via Op. (#7688)

Fixes cvc5/cvc5-projects#367.

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 38cbdd7a6b245a7c932c5c310df31d86cb40067c..0c35abd4c1816b88139d0eafb4d21d70bfd1a23c 100644 (file)
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -5247,15 +5247,15 @@ Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
 
 Term Solver::mkTermHelper(const Op& op, const std::vector<Term>& children) const
 {
-  // Note: Op and children are checked in the caller to avoid double checks
-  checkMkTerm(op.d_kind, children.size());
-  //////// all checks before this line
-
   if (!op.isIndexedHelper())
   {
     return mkTermHelper(op.d_kind, children);
   }
 
+  // Note: Op and children are checked in the caller to avoid double checks
+  checkMkTerm(op.d_kind, children.size());
+  //////// all checks before this line
+
   const cvc5::Kind int_kind = extToIntKind(op.d_kind);
   std::vector<Node> echildren = Term::termVectorToNodes(children);
 

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 74910df1e8fadc6f4a91ce896ab505ac6107c8bc..75cb5a13b4c08e04fa298f32bfdcd4d83b5028b2 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -700,6 +700,44 @@ TEST_F(TestApiBlackSolver, mkTerm)
   ASSERT_THROW(d_solver.mkTerm(EQUAL, v2), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(EQUAL, v3), CVC5ApiException);
   ASSERT_THROW(d_solver.mkTerm(DISTINCT, v6), CVC5ApiException);
+
+  // Test cases that are nary via the API but have arity = 2 internally
+  Sort s_bool = d_solver.getBooleanSort();
+  Term t_bool = d_solver.mkConst(s_bool, "t_bool");
+  ASSERT_NO_THROW(d_solver.mkTerm(IMPLIES, {t_bool, t_bool, t_bool}));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(IMPLIES), {t_bool, t_bool, t_bool}));
+  ASSERT_NO_THROW(d_solver.mkTerm(XOR, {t_bool, t_bool, t_bool}));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(XOR), {t_bool, t_bool, t_bool}));
+  Term t_int = d_solver.mkConst(d_solver.getIntegerSort(), "t_int");
+  ASSERT_NO_THROW(d_solver.mkTerm(DIVISION, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(DIVISION), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(INTS_DIVISION, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(INTS_DIVISION), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(MINUS, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(MINUS), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(EQUAL, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(EQUAL), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(LT, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(LT), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(GT, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(GT), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(LEQ, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(LEQ), {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(GEQ, {t_int, t_int, t_int}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(GEQ), {t_int, t_int, t_int}));
+  Term t_reg = d_solver.mkConst(d_solver.getRegExpSort(), "t_reg");
+  ASSERT_NO_THROW(d_solver.mkTerm(REGEXP_DIFF, {t_reg, t_reg, t_reg}));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(REGEXP_DIFF), {t_reg, t_reg, t_reg}));
+  Term t_fun = d_solver.mkConst(
+      d_solver.mkFunctionSort({s_bool, s_bool, s_bool}, s_bool));
+  ASSERT_NO_THROW(d_solver.mkTerm(HO_APPLY, {t_fun, t_bool, t_bool, t_bool}));
+  ASSERT_NO_THROW(d_solver.mkTerm(d_solver.mkOp(HO_APPLY),
+                                  {t_fun, t_bool, t_bool, t_bool}));
 }
 
 TEST_F(TestApiBlackSolver, mkTermFromOp)

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 89e99bd9e574e65f28274f102db6f1673b4d8fb8..c163e10945622bbdaf5784f89369f12c8c5af2f1 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -747,6 +747,36 @@ def test_mk_term(solver):
     with pytest.raises(RuntimeError):
         solver.mkTerm(kinds.Distinct, v6)
 
+    # Test cases that are nary via the API but have arity = 2 internally
+    s_bool = solver.getBooleanSort()
+    t_bool = solver.mkConst(s_boo, "t_bool")
+    solver.mkTerm(kinds.Implies, [t_bool, t_bool, t_bool])
+    solver.mkTerm(kinds.Xor, [t_bool, t_bool, t_bool])
+    solver.mkTerm(solver.mkOp(kinds.Xor), [t_bool, t_bool, t_bool])
+    t_int = solver.mkConst(solver.getIntegerSort(), "t_int")
+    solver.mkTerm(kinds.Division, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Division), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.IntsDivision, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.IntsDivision), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.Minus, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Minus), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.Equal, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Equal), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.Lt, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Lt), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.Gt, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Gt), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.Leq, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Leq), [t_int, t_int, t_int])
+    solver.mkTerm(kinds.Geq, [t_int, t_int, t_int])
+    solver.mkTerm(solver.mkOp(kinds.Geq), [t_int, t_int, t_int])
+    t_reg = solver.mkConst(solver.getRegExpSort(), "t_reg")
+    solver.mkTerm(kinds.RegexpDiff, [t_reg, t_reg, t_reg])
+    solver.mkTerm(solver.mkOp(kinds.RegexpDiff), [t_reg, t_reg, t_reg])
+    t_fun = solver.mkConst(solver.mkFunctionSort(
+        [s_bool, s_bool, s_bool], s_bool))
+    solver.mkTerm(kinds.HoApply, [t_fun, t_bool, t_bool, t_bool])
+    solver.mkTerm(solver.mkOp(kinds.HoApply), [t_fun, t_bool, t_bool, t_bool])
 
 def test_mk_term_from_op(solver):
     bv32 = solver.mkBitVectorSort(32)