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.

13 files changed, 313 insertions, 2 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 02cb26760..2b04bb40d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -584,6 +584,8 @@ libcvc4_add_sources(
   theory/datatypes/theory_datatypes_type_rules.h
   theory/datatypes/theory_datatypes_utils.cpp
   theory/datatypes/theory_datatypes_utils.h
+  theory/datatypes/tuple_project_op.cpp
+  theory/datatypes/tuple_project_op.h
   theory/datatypes/type_enumerator.cpp
   theory/datatypes/type_enumerator.h
   theory/decision_manager.cpp
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index e1c64b750..c3490938b 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -232,6 +232,7 @@ const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
     {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
     {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
     {DT_SIZE, CVC4::Kind::DT_SIZE},
+    {TUPLE_PROJECT, CVC4::Kind::TUPLE_PROJECT},
     /* Separation Logic ---------------------------------------------------- */
     {SEP_NIL, CVC4::Kind::SEP_NIL},
     {SEP_EMP, CVC4::Kind::SEP_EMP},
@@ -538,6 +539,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
         {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
         {CVC4::Kind::DT_SIZE, DT_SIZE},
+        {CVC4::Kind::TUPLE_PROJECT, TUPLE_PROJECT},
         /* Separation Logic ------------------------------------------------ */
         {CVC4::Kind::SEP_NIL, SEP_NIL},
         {CVC4::Kind::SEP_EMP, SEP_EMP},
@@ -4749,6 +4751,35 @@ Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+Op Solver::mkOp(Kind kind, const std::vector<uint32_t>& args) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  CVC4_API_KIND_CHECK(kind);
+
+  Op res;
+  switch (kind)
+  {
+    case TUPLE_PROJECT:
+    {
+      res = Op(this,
+               kind,
+               *mkValHelper<CVC4::TupleProjectOp>(CVC4::TupleProjectOp(args))
+                    .d_node);
+    }
+    break;
+    default:
+    {
+      std::string message = "operator kind with " + std::to_string(args.size())
+                            + " uint32_t arguments";
+      CVC4_API_KIND_CHECK_EXPECTED(false, kind) << message;
+    }
+  }
+  Assert(!res.isNull());
+  return res;
+
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 /* Non-SMT-LIB commands                                                       */
 /* -------------------------------------------------------------------------- */
 
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 60127d18b..d503a317e 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -2620,6 +2620,14 @@ class CVC4_PUBLIC Solver
    */
   Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const;
 
+  /**
+   * Create operator of Kind:
+   *   - TUPLE_PROJECT
+   * See enum Kind for a description of the parameters.
+   * @param kind the kind of the operator
+   */
+  Op mkOp(Kind kind, const std::vector<uint32_t>& args) const;
+
   /* .................................................................... */
   /* Create Constants                                                     */
   /* .................................................................... */
diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 3fb16abcb..b2413486e 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -1715,6 +1715,22 @@ enum CVC4_PUBLIC Kind : int32_t
    *   mkTerm(Kind kind, const std::vector<Term>& children)
    */
   DT_SIZE,
+  /**
+   * Operator for tuple projection indices
+   * Parameters: 1
+   *   -[1]: The tuple projection indices
+   * Create with:
+   *   mkOp(Kind TUPLE_PROJECT, std::vector<uint32_t> param)
+   *
+   * constructs a new tuple from an existing one using the elements at the
+   * given indices
+   * Parameters: 1
+   *   -[1]: a term of tuple sort
+   * Create with:
+   *   mkTerm(Op op, Term child)
+   *   mkTerm(Op op, const std::vector<Term>& children)
+   */
+  TUPLE_PROJECT,
 #if 0
   /* datatypes height bound */
   DT_HEIGHT_BOUND,
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 11ccb4935..7ef7edbbe 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1549,6 +1549,12 @@ termNonVariable[CVC4::api::Term& expr, CVC4::api::Term& expr2]
     }
     expr = SOLVER->mkTuple(sorts, terms);
   }
+  | LPAREN_TOK TUPLE_PROJECT_TOK term[expr,expr2] RPAREN_TOK
+  {
+    std::vector<uint32_t> indices;
+    api::Op op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
+    expr = SOLVER->mkTerm(op, expr);
+  }
   | /* an atomic term (a term with no subterms) */
     termAtomic[atomTerm] { expr = atomTerm; }
   ;
@@ -1672,6 +1678,19 @@ identifier[CVC4::ParseOp& p]
         // put m in expr so that the caller can deal with this case
         p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
       }
+    | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals]
+      {
+        // we adopt a special syntax (_ tuple_project i_1 ... i_n) where
+        // i_1, ..., i_n are numerals
+        p.d_kind = api::TUPLE_PROJECT;
+        std::vector<uint32_t> indices(numerals.size());
+        for(size_t i = 0; i < numerals.size(); ++i)
+        {
+          // convert uint64_t to uint32_t
+          indices[i] = numerals[i];
+        }
+        p.d_op = SOLVER->mkOp(api::TUPLE_PROJECT, indices);
+      }
     | sym=SIMPLE_SYMBOL nonemptyNumeralList[numerals]
       {
         p.d_op = PARSER_STATE->mkIndexedOp(AntlrInput::tokenText($sym), numerals);
@@ -2279,6 +2298,7 @@ EMP_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_SEP) }? 'emp';
 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'mkTuple';
 TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tupSel';
+TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
 
 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
 HO_LAMBDA_TOK : { PARSER_STATE->isHoEnabled() }? 'lambda';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 4d75a982b..049bf8b4d 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1097,6 +1097,12 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     Debug("parser") << "applyParseOp: return selector " << ret << std::endl;
     return ret;
   }
+  else if (p.d_kind == api::TUPLE_PROJECT)
+  {
+    api::Term ret = d_solver->mkTerm(p.d_op, args[0]);
+    Debug("parser") << "applyParseOp: return projection " << ret << std::endl;
+    return ret;
+  }
   else if (p.d_kind != api::NULL_EXPR)
   {
     // it should not have an expression or type specified at this point
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index fd9d20e4b..8c122f26d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -903,6 +903,21 @@ void Smt2Printer::toStream(std::ostream& out,
     }
     break;
   }
+  case kind::TUPLE_PROJECT:
+  {
+    TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
+    if (op.getIndices().empty())
+    {
+      // e.g. (tuple_project tuple)
+      out << "project " << n[0] << ")";
+    }
+    else
+    {
+      // e.g. ((_ tuple_project 2 4 4) tuple)
+      out << "(_ tuple_project" << op << ") " << n[0] << ")";
+    }
+    return;
+  }
   case kind::CONSTRUCTOR_TYPE:
   {
     out << n[n.getNumChildren()-1];
diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h
index a53000651..36bd3f5df 100644
--- a/src/theory/bags/make_bag_op.h
+++ b/src/theory/bags/make_bag_op.h
@@ -34,7 +34,7 @@ class TypeNode;
 class MakeBagOp
 {
  public:
-  MakeBagOp(const TypeNode& elementType);
+  explicit MakeBagOp(const TypeNode& elementType);
   MakeBagOp(const MakeBagOp& op);
 
   /** return the type of the current object */
@@ -43,7 +43,6 @@ class MakeBagOp
   bool operator==(const MakeBagOp& op) const;
 
  private:
-  MakeBagOp();
   /** a pointer to the type of the bag element */
   std::unique_ptr<TypeNode> d_type;
 }; /* class MakeBagOp */
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 5334e76df..4bf745f16 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -224,6 +224,41 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
         << "Rewrite match: " << in << " ... " << ret << std::endl;
     return RewriteResponse(REWRITE_AGAIN_FULL, ret);
   }
+  else if (kind == TUPLE_PROJECT)
+  {
+    // returns a tuple that represents
+    // (mkTuple ((_ tupSel i_1) t) ... ((_ tupSel i_n) t))
+    // where each i_j is less than the length of t
+
+    Trace("dt-rewrite-project") << "Rewrite project: " << in << std::endl;
+    TupleProjectOp op = in.getOperator().getConst<TupleProjectOp>();
+    std::vector<uint32_t> indices = op.getIndices();
+    Node tuple = in[0];
+    std::vector<TypeNode> tupleTypes = tuple.getType().getTupleTypes();
+    std::vector<TypeNode> types;
+    std::vector<Node> elements;
+    for (uint32_t index : indices)
+    {
+      TypeNode type = tupleTypes[index];
+      types.push_back(type);
+    }
+    TypeNode projectType = nm->mkTupleType(types);
+    const DType& dt = projectType.getDType();
+    elements.push_back(dt[0].getConstructor());
+    const DType& tupleDType = tuple.getType().getDType();
+    const DTypeConstructor& constructor = tupleDType[0];
+    for (uint32_t index : indices)
+    {
+      Node selector = constructor[index].getSelector();
+      Node element = nm->mkNode(kind::APPLY_SELECTOR, selector, tuple);
+      elements.push_back(element);
+    }
+    Node ret = nm->mkNode(kind::APPLY_CONSTRUCTOR, elements);
+
+    Trace("dt-rewrite-project")
+        << "Rewrite project: " << in << " ... " << ret << std::endl;
+    return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+  }
 
   if (kind == kind::EQUAL)
   {
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index ef8dd47f1..f3e5be5c7 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -138,4 +138,17 @@ typerule MATCH ::CVC4::theory::datatypes::MatchTypeRule
 typerule MATCH_CASE ::CVC4::theory::datatypes::MatchCaseTypeRule
 typerule MATCH_BIND_CASE ::CVC4::theory::datatypes::MatchBindCaseTypeRule
 
+
+constant TUPLE_PROJECT_OP \
+	::CVC4::TupleProjectOp \
+	::CVC4::TupleProjectOpHashFunction \
+	"theory/datatypes/tuple_project_op.h" \
+	"operator for TUPLE_PROJECT; payload is an instance of the CVC4::TupleProjectOp class"
+
+parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \
+    "projects a tuple from an existing tuple using indices passed in TupleProjectOp"
+
+typerule TUPLE_PROJECT_OP  "SimpleTypeRule<RBuiltinOperator>"
+typerule TUPLE_PROJECT     ::CVC4::theory::datatypes::TupleProjectTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 73aef4dd7..d7fb984e0 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -572,6 +572,60 @@ class MatchBindCaseTypeRule
   }
 }; /* class MatchBindCaseTypeRule */
 
+class TupleProjectTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nm, TNode n, bool check)
+  {
+    Assert(n.getKind() == kind::TUPLE_PROJECT && n.hasOperator()
+           && n.getOperator().getKind() == kind::TUPLE_PROJECT_OP);
+    TupleProjectOp op = n.getOperator().getConst<TupleProjectOp>();
+    const std::vector<uint32_t>& indices = op.getIndices();
+    if (check)
+    {
+      if (n.getNumChildren() != 1)
+      {
+        std::stringstream ss;
+        ss << "operands in term " << n << " are " << n.getNumChildren()
+           << ", but TUPLE_PROJECT expects 1 operand.";
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+      TypeNode tupleType = n[0].getType(check);
+      if (!tupleType.isTuple())
+      {
+        std::stringstream ss;
+        ss << "TUPLE_PROJECT expects a tuple for " << n[0] << ". Found" << tupleType;
+        throw TypeCheckingExceptionPrivate(n, ss.str());
+      }
+
+      // make sure all indices are less than the length of the tuple type
+      DType dType = tupleType.getDType();
+      DTypeConstructor constructor = dType[0];
+      size_t numArgs = constructor.getNumArgs();
+      for (uint32_t index : indices)
+      {
+        std::stringstream ss;
+        if (index >= numArgs)
+        {
+          ss << "Project index " << index << " in term " << n
+             << " is >= " << numArgs << " which is the length of tuple " << n[0]
+             << std::endl;
+          throw TypeCheckingExceptionPrivate(n, ss.str());
+        }
+      }
+    }
+    TypeNode tupleType = n[0].getType(check);
+    std::vector<TypeNode> types;
+    DType dType = tupleType.getDType();
+    DTypeConstructor constructor = dType[0];
+    for (uint32_t index : indices)
+    {
+      types.push_back(constructor.getArgType(index));
+    }
+    return nm->mkTupleType(types);
+  }
+}; /* class TupleProjectTypeRule */
+
 } /* CVC4::theory::datatypes namespace */
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
diff --git a/src/theory/datatypes/tuple_project_op.cpp b/src/theory/datatypes/tuple_project_op.cpp
new file mode 100644
index 000000000..d09d43317
--- /dev/null
+++ b/src/theory/datatypes/tuple_project_op.cpp
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file tuple_project_op.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **/
+
+#include "tuple_project_op.h"
+
+#include <iostream>
+
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const TupleProjectOp& op)
+{
+  for (const uint32_t& index : op.getIndices())
+  {
+    out << " " << index;
+  }
+  return out;
+}
+
+size_t TupleProjectOpHashFunction::operator()(const TupleProjectOp& op) const
+{
+  // we expect most tuples to have length < 10.
+  // Therefore we can implement a simple hash function
+  size_t hash = 0;
+  for (uint32_t index : op.getIndices())
+  {
+    hash = hash * 10 + index;
+  }
+  return hash;
+}
+
+TupleProjectOp::TupleProjectOp(std::vector<uint32_t> indices)
+    : d_indices(std::move(indices))
+{
+}
+
+const std::vector<uint32_t>& TupleProjectOp::getIndices() const { return d_indices; }
+
+bool TupleProjectOp::operator==(const TupleProjectOp& op) const
+{
+  return d_indices == op.d_indices;
+}
+
+}  // namespace CVC4
diff --git a/src/theory/datatypes/tuple_project_op.h b/src/theory/datatypes/tuple_project_op.h
new file mode 100644
index 000000000..045f05cc2
--- /dev/null
+++ b/src/theory/datatypes/tuple_project_op.h
@@ -0,0 +1,58 @@
+/*********************                                                        */
+/*! \file tuple_project_op.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Mudathir Mohamed
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief a class for TupleProjectOp operator
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__PROJECT_OP_H
+#define CVC4__PROJECT_OP_H
+
+#include <ostream>
+#include <vector>
+
+namespace CVC4 {
+
+class TypeNode;
+
+/**
+ * The class is an operator for kind project used to project elements in a tuple
+ * It stores the indices of projected elements
+ */
+class TupleProjectOp
+{
+ public:
+  explicit TupleProjectOp(std::vector<uint32_t> indices);
+  TupleProjectOp(const TupleProjectOp& op) = default;
+
+  /** return the indices of the projection */
+  const std::vector<uint32_t>& getIndices() const;
+
+  bool operator==(const TupleProjectOp& op) const;
+
+ private:
+  std::vector<uint32_t> d_indices;
+}; /* class TupleProjectOp */
+
+std::ostream& operator<<(std::ostream& out, const TupleProjectOp& op);
+
+/**
+ * Hash function for the TupleProjectOpHashFunction objects.
+ */
+struct CVC4_PUBLIC TupleProjectOpHashFunction
+{
+  size_t operator()(const TupleProjectOp& op) const;
+}; /* struct TupleProjectOpHashFunction */
+
+}  // namespace CVC4
+
+#endif /* CVC4__PROJECT_OP_H */