New C++ API: Add templated getIndices method for OpTerm (#3073)

* Implement templated getIndices method for OpTerm

* Add getIndices unit tests

* Update src/api/cvc4cpp.cpp

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Update src/api/cvc4cpp.cpp

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Add comment about DIVISIBLE_OP

* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Update test/unit/api/opterm_black.h

Co-Authored-By: Aina Niemetz <aina.niemetz@gmail.com>

* Add exception checks to other unit tests (instead of having its own function)

* Fix unit test names in opterm_black.h

* Add description to docstring for getIndices

* Formatting

* Clang format older commits

* Use '-' in docstring list to match other docstrings

* Support creating DIVISIBLE_OP with a string (for arbitrary precision integers)

* Move mkOpTerm(DIVISIBLE_OP, <str>) test to solver_black.h

* Fix pointer access

* Replace switch statement with if statement

* Guard string input for CVC4::Integer in mkOpTerm for consistency on GMP/CLN back-end

2 files changed, 152 insertions, 0 deletions

diff --git a/test/unit/api/opterm_black.h b/test/unit/api/opterm_black.h
index 395ee8451..150cebcbf 100644
--- a/test/unit/api/opterm_black.h
+++ b/test/unit/api/opterm_black.h
@@ -27,6 +27,10 @@ class OpTermBlack : public CxxTest::TestSuite
   void testGetKind();
   void testGetSort();
   void testIsNull();
+  void testGetIndicesString();
+  void testGetIndicesKind();
+  void testGetIndicesUint();
+  void testGetIndicesPairUint();
 
  private:
   Solver d_solver;
@@ -55,3 +59,150 @@ void OpTermBlack::testIsNull()
   x = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
   TS_ASSERT(!x.isNull());
 }
+
+void OpTermBlack::testGetIndicesString()
+{
+  OpTerm x;
+  TS_ASSERT_THROWS(x.getIndices<std::string>(), CVC4ApiException&);
+
+  OpTerm divisible_ot = d_solver.mkOpTerm(DIVISIBLE_OP, 4);
+  std::string divisible_idx = divisible_ot.getIndices<std::string>();
+  TS_ASSERT(divisible_idx == "4");
+
+  OpTerm record_update_ot = d_solver.mkOpTerm(RECORD_UPDATE_OP, "test");
+  std::string record_update_idx = record_update_ot.getIndices<std::string>();
+  TS_ASSERT(record_update_idx == "test");
+  TS_ASSERT_THROWS(record_update_ot.getIndices<uint32_t>(), CVC4ApiException&);
+}
+
+void OpTermBlack::testGetIndicesKind()
+{
+  OpTerm chain_ot = d_solver.mkOpTerm(CHAIN_OP, AND);
+  Kind chain_idx = chain_ot.getIndices<Kind>();
+  TS_ASSERT(chain_idx == AND);
+}
+
+void OpTermBlack::testGetIndicesUint()
+{
+  OpTerm bitvector_repeat_ot = d_solver.mkOpTerm(BITVECTOR_REPEAT_OP, 5);
+  uint32_t bitvector_repeat_idx = bitvector_repeat_ot.getIndices<uint32_t>();
+  TS_ASSERT(bitvector_repeat_idx == 5);
+  TS_ASSERT_THROWS(
+      (bitvector_repeat_ot.getIndices<std::pair<uint32_t, uint32_t>>()),
+      CVC4ApiException&);
+
+  OpTerm bitvector_zero_extend_ot =
+      d_solver.mkOpTerm(BITVECTOR_ZERO_EXTEND_OP, 6);
+  uint32_t bitvector_zero_extend_idx =
+      bitvector_zero_extend_ot.getIndices<uint32_t>();
+  TS_ASSERT(bitvector_zero_extend_idx == 6);
+
+  OpTerm bitvector_sign_extend_ot =
+      d_solver.mkOpTerm(BITVECTOR_SIGN_EXTEND_OP, 7);
+  uint32_t bitvector_sign_extend_idx =
+      bitvector_sign_extend_ot.getIndices<uint32_t>();
+  TS_ASSERT(bitvector_sign_extend_idx == 7);
+
+  OpTerm bitvector_rotate_left_ot =
+      d_solver.mkOpTerm(BITVECTOR_ROTATE_LEFT_OP, 8);
+  uint32_t bitvector_rotate_left_idx =
+      bitvector_rotate_left_ot.getIndices<uint32_t>();
+  TS_ASSERT(bitvector_rotate_left_idx == 8);
+
+  OpTerm bitvector_rotate_right_ot =
+      d_solver.mkOpTerm(BITVECTOR_ROTATE_RIGHT_OP, 9);
+  uint32_t bitvector_rotate_right_idx =
+      bitvector_rotate_right_ot.getIndices<uint32_t>();
+  TS_ASSERT(bitvector_rotate_right_idx == 9);
+
+  OpTerm int_to_bitvector_ot = d_solver.mkOpTerm(INT_TO_BITVECTOR_OP, 10);
+  uint32_t int_to_bitvector_idx = int_to_bitvector_ot.getIndices<uint32_t>();
+  TS_ASSERT(int_to_bitvector_idx == 10);
+
+  OpTerm floatingpoint_to_ubv_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_OP, 11);
+  uint32_t floatingpoint_to_ubv_idx =
+      floatingpoint_to_ubv_ot.getIndices<uint32_t>();
+  TS_ASSERT(floatingpoint_to_ubv_idx == 11);
+
+  OpTerm floatingpoint_to_ubv_total_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_UBV_TOTAL_OP, 12);
+  uint32_t floatingpoint_to_ubv_total_idx =
+      floatingpoint_to_ubv_total_ot.getIndices<uint32_t>();
+  TS_ASSERT(floatingpoint_to_ubv_total_idx == 12);
+
+  OpTerm floatingpoint_to_sbv_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_OP, 13);
+  uint32_t floatingpoint_to_sbv_idx =
+      floatingpoint_to_sbv_ot.getIndices<uint32_t>();
+  TS_ASSERT(floatingpoint_to_sbv_idx == 13);
+
+  OpTerm floatingpoint_to_sbv_total_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_SBV_TOTAL_OP, 14);
+  uint32_t floatingpoint_to_sbv_total_idx =
+      floatingpoint_to_sbv_total_ot.getIndices<uint32_t>();
+  TS_ASSERT(floatingpoint_to_sbv_total_idx == 14);
+
+  OpTerm tuple_update_ot = d_solver.mkOpTerm(TUPLE_UPDATE_OP, 5);
+  uint32_t tuple_update_idx = tuple_update_ot.getIndices<uint32_t>();
+  TS_ASSERT(tuple_update_idx == 5);
+  TS_ASSERT_THROWS(tuple_update_ot.getIndices<std::string>(),
+                   CVC4ApiException&);
+}
+
+void OpTermBlack::testGetIndicesPairUint()
+{
+  OpTerm bitvector_extract_ot = d_solver.mkOpTerm(BITVECTOR_EXTRACT_OP, 4, 0);
+  std::pair<uint32_t, uint32_t> bitvector_extract_indices =
+      bitvector_extract_ot.getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((bitvector_extract_indices == std::pair<uint32_t, uint32_t>{4, 0}));
+
+  OpTerm floatingpoint_to_fp_ieee_bitvector_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP, 4, 25);
+  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_ieee_bitvector_indices =
+      floatingpoint_to_fp_ieee_bitvector_ot
+          .getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((floatingpoint_to_fp_ieee_bitvector_indices
+             == std::pair<uint32_t, uint32_t>{4, 25}));
+
+  OpTerm floatingpoint_to_fp_floatingpoint_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP, 4, 25);
+  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_floatingpoint_indices =
+      floatingpoint_to_fp_floatingpoint_ot
+          .getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((floatingpoint_to_fp_floatingpoint_indices
+             == std::pair<uint32_t, uint32_t>{4, 25}));
+
+  OpTerm floatingpoint_to_fp_real_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_REAL_OP, 4, 25);
+  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_real_indices =
+      floatingpoint_to_fp_real_ot.getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((floatingpoint_to_fp_real_indices
+             == std::pair<uint32_t, uint32_t>{4, 25}));
+
+  OpTerm floatingpoint_to_fp_signed_bitvector_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP, 4, 25);
+  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_signed_bitvector_indices =
+      floatingpoint_to_fp_signed_bitvector_ot
+          .getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((floatingpoint_to_fp_signed_bitvector_indices
+             == std::pair<uint32_t, uint32_t>{4, 25}));
+
+  OpTerm floatingpoint_to_fp_unsigned_bitvector_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP, 4, 25);
+  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_unsigned_bitvector_indices =
+      floatingpoint_to_fp_unsigned_bitvector_ot
+          .getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((floatingpoint_to_fp_unsigned_bitvector_indices
+             == std::pair<uint32_t, uint32_t>{4, 25}));
+
+  OpTerm floatingpoint_to_fp_generic_ot =
+      d_solver.mkOpTerm(FLOATINGPOINT_TO_FP_GENERIC_OP, 4, 25);
+  std::pair<uint32_t, uint32_t> floatingpoint_to_fp_generic_indices =
+      floatingpoint_to_fp_generic_ot
+          .getIndices<std::pair<uint32_t, uint32_t>>();
+  TS_ASSERT((floatingpoint_to_fp_generic_indices
+             == std::pair<uint32_t, uint32_t>{4, 25}));
+  TS_ASSERT_THROWS(floatingpoint_to_fp_generic_ot.getIndices<std::string>(),
+                   CVC4ApiException&);
+}
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index a82807b3b..3782b900a 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -451,6 +451,7 @@ void SolverBlack::testMkOpTerm()
 
   // mkOpTerm(Kind kind, const std::string& arg)
   TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(RECORD_UPDATE_OP, "asdf"));
+  TS_ASSERT_THROWS_NOTHING(d_solver->mkOpTerm(DIVISIBLE_OP, "2147483648"));
   TS_ASSERT_THROWS(d_solver->mkOpTerm(BITVECTOR_EXTRACT_OP, "asdf"),
                    CVC4ApiException&);