From 943dfc57d1bbc58046ad10bb4a8a48a8b654aeb5 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 24 Nov 2021 18:39:39 -0800 Subject: [PATCH] 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. --- src/api/cpp/cvc5.cpp | 11 ++++++----- test/unit/api/cpp/solver_black.cpp | 13 +++++++++++++ test/unit/api/python/test_solver.py | 14 ++++++++++++++ 3 files changed, 33 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& 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 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) -- 2.30.2