From ccdd564ea6a610f9020a1dd328a67e9ff82fe3f5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 23 Nov 2021 16:50:44 -0800 Subject: [PATCH] api: Fix creation of nary term kinds via Op. (#7688) Fixes cvc5/cvc5-projects#367. --- src/api/cpp/cvc5.cpp | 8 +++--- test/unit/api/cpp/solver_black.cpp | 38 +++++++++++++++++++++++++++++ test/unit/api/python/test_solver.py | 30 +++++++++++++++++++++++ 3 files changed, 72 insertions(+), 4 deletions(-) diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 38cbdd7a6..0c35abd4c 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -5247,15 +5247,15 @@ Term Solver::mkTermHelper(Kind kind, const std::vector& children) const Term Solver::mkTermHelper(const Op& op, const std::vector& 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 echildren = Term::termVectorToNodes(children); diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index 74910df1e..75cb5a13b 100644 --- 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 89e99bd9e..c163e1094 100644 --- 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) -- 2.30.2