Add tuple projection operator (#5904)

This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.

1 files changed, 63 insertions, 1 deletions

diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 2e285fcc7..528d697ae 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -554,6 +554,10 @@ TEST_F(TestApiBlackSolver, mkOp)
   // mkOp(Kind kind, uint32_t arg1, uint32_t arg2)
   ASSERT_NO_THROW(d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1));
   ASSERT_THROW(d_solver.mkOp(DIVISIBLE, 1, 2), CVC4ApiException);
+
+  // mkOp(Kind kind, std::vector<uint32_t> args)
+  std::vector<uint32_t> args = {1, 2, 2};
+  ASSERT_NO_THROW(d_solver.mkOp(TUPLE_PROJECT, args));
 }
 
 TEST_F(TestApiBlackSolver, mkPi) { ASSERT_NO_THROW(d_solver.mkPi()); }
@@ -975,7 +979,8 @@ TEST_F(TestApiBlackSolver, defineSort)
   Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1);
   // Now create instantiations of the defined sorts
   ASSERT_NO_THROW(arraySort0.substitute(sortVar0, intSort));
-  ASSERT_NO_THROW(arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
+  ASSERT_NO_THROW(
+      arraySort1.substitute({sortVar0, sortVar1}, {intSort, realSort}));
 }
 
 TEST_F(TestApiBlackSolver, defineFun)
@@ -2292,5 +2297,62 @@ TEST_F(TestApiBlackSolver, getSynthSolutions)
   ASSERT_THROW(slv.getSynthSolutions({x}), CVC4ApiException);
 }
 
+TEST_F(TestApiBlackSolver, tupleProject)
+{
+  std::vector<Sort> sorts = {d_solver.getBooleanSort(),
+                             d_solver.getIntegerSort(),
+                             d_solver.getStringSort(),
+                             d_solver.mkSetSort(d_solver.getStringSort())};
+  std::vector<Term> elements = {
+      d_solver.mkBoolean(true),
+      d_solver.mkInteger(3),
+      d_solver.mkString("C"),
+      d_solver.mkTerm(SINGLETON, d_solver.mkString("Z"))};
+
+  Term tuple = d_solver.mkTuple(sorts, elements);
+
+  std::vector<uint32_t> indices1 = {};
+  std::vector<uint32_t> indices2 = {0};
+  std::vector<uint32_t> indices3 = {0, 1};
+  std::vector<uint32_t> indices4 = {0, 0, 2, 2, 3, 3, 0};
+  std::vector<uint32_t> indices5 = {4};
+  std::vector<uint32_t> indices6 = {0, 4};
+
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), tuple));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), tuple));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), tuple));
+  ASSERT_NO_THROW(
+      d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple));
+
+  ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple),
+               CVC4ApiException);
+  ASSERT_THROW(d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple),
+               CVC4ApiException);
+
+  std::vector<uint32_t> indices = {0, 3, 2, 0, 1, 2};
+
+  Op op = d_solver.mkOp(TUPLE_PROJECT, indices);
+  Term projection = d_solver.mkTerm(op, tuple);
+
+  Datatype datatype = tuple.getSort().getDatatype();
+  DatatypeConstructor constructor = datatype[0];
+
+  for (size_t i = 0; i < indices.size(); i++)
+  {
+    Term selectorTerm = constructor[indices[i]].getSelectorTerm();
+    Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple);
+    Term simplifiedTerm = d_solver.simplify(selectedTerm);
+    ASSERT_EQ(elements[indices[i]], simplifiedTerm);
+  }
+
+  ASSERT_EQ(
+      "((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton "
+      "\"Z\")))",
+      projection.toString());
+}
+
 }  // namespace test
 }  // namespace CVC4