Remove unused RecordSelect and TupleSelect (#1087)

Commit 62b673a6b8444c14c169a984dd6e3fc8f685851e remove most of the
record/tuple infrastructure but did not remove the classes RecordSelect and
TupleSelect which lead to issues with Java bindings (the references to the
corresponding mkConst implementations could not be resolved). This commit
removes the remaining traces of those classes.

8 files changed, 1 insertions, 71 deletions

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker.java b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
index 7407d0251..1b38a4c95 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker.java
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
@@ -312,8 +312,6 @@ public class ValidityChecker extends Embedded {
     private static native Object
 	jniTupleExpr(Object ValidityChecker, Object[] Exprs) throws Cvc3Exception;
     private static native Object
-	jniTupleSelectExpr(Object ValidityChecker, Object ExprTuple, int index) throws Cvc3Exception;
-    private static native Object
 	jniTupleUpdateExpr(Object ValidityChecker, Object ExprTuple, int index,
 			   Object ExprNewValue) throws Cvc3Exception;
     private static native Object
@@ -1380,12 +1378,6 @@ public class ValidityChecker extends Embedded {
 	  embeddedManager());
     }
 
-    public ExprMut tupleSelectExpr(Expr tuple, int index) throws Cvc3Exception {
-	return new ExprMut(
-	  jniTupleSelectExpr(embedded(), tuple.embedded(), index),
-	  embeddedManager());
-    }
-
     public ExprMut tupleUpdateExpr(Expr tuple, int index, Expr newValue) throws Cvc3Exception {
 	return new ExprMut(
 	  jniTupleUpdateExpr(embedded(), tuple.embedded(), index, newValue.embedded()),
diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index 6bab7d2e0..cfda940d8 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -596,10 +596,6 @@ DEFINITION: Java_cvc3_ValidityChecker_jniTupleExpr
 jobject m ValidityChecker vc cv Expr exprs
 return embed_copy(env, vc->tupleExpr(exprs));
 
-DEFINITION: Java_cvc3_ValidityChecker_jniTupleSelectExpr
-jobject m ValidityChecker vc c Expr tuple n int index
-return embed_copy(env, vc->tupleSelectExpr(*tuple, index));
-
 DEFINITION: Java_cvc3_ValidityChecker_jniTupleUpdateExpr
 jobject m ValidityChecker vc c Expr tuple n int index c Expr value
 return embed_copy(env, vc->tupleUpdateExpr(*tuple, index, *value));
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index 136e75f98..dac3b9312 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -81,15 +81,8 @@
 
 // These cases have trouble too.  Remove them for now.
 //%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
-//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
-//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
-//%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
-
 #else
 %template(mkConst) CVC4::ExprManager::mkConst<CVC4::TypeConstant>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::TupleSelect>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::Record>;
-%template(mkConst) CVC4::ExprManager::mkConst<CVC4::RecordSelect>;
 %template(mkConst) CVC4::ExprManager::mkConst<bool>;
 #endif
 
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index 4b2d50ea6..2c5996213 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -106,10 +106,6 @@ size_t RecordHashFunction::operator()(const Record& r) const {
   return n;
 }
 
-std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
-  return out << "[" << t.getField() << "]";
-}
-
 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
   return out << "[" << t.getField() << "]";
 }
diff --git a/src/expr/record.h b/src/expr/record.h
index 7c5854db2..ae03a7acd 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -34,17 +34,7 @@ class Type;
 
 namespace CVC4 {
 
-// operators for record select and update
-
-class CVC4_PUBLIC RecordSelect {
-  std::string d_field;
-public:
-  RecordSelect(const std::string& field) throw() : d_field(field) { }
-  std::string getField() const throw() { return d_field; }
-  bool operator==(const RecordSelect& t) const throw() { return d_field == t.d_field; }
-  bool operator!=(const RecordSelect& t) const throw() { return d_field != t.d_field; }
-};/* class RecordSelect */
-
+// operators for record update
 class CVC4_PUBLIC RecordUpdate {
   std::string d_field;
 public:
@@ -54,19 +44,12 @@ public:
   bool operator!=(const RecordUpdate& t) const throw() { return d_field != t.d_field; }
 };/* class RecordUpdate */
 
-struct CVC4_PUBLIC RecordSelectHashFunction {
-  inline size_t operator()(const RecordSelect& t) const {
-    return std::hash<std::string>()(t.getField());
-  }
-};/* struct RecordSelectHashFunction */
-
 struct CVC4_PUBLIC RecordUpdateHashFunction {
   inline size_t operator()(const RecordUpdate& t) const {
     return std::hash<std::string>()(t.getField());
   }
 };/* struct RecordUpdateHashFunction */
 
-std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
 
 // now an actual record definition
diff --git a/src/expr/record.i b/src/expr/record.i
index 695ff105b..d5b018f72 100644
--- a/src/expr/record.i
+++ b/src/expr/record.i
@@ -9,9 +9,6 @@
 #endif /* SWIGJAVA */
 %}
 
-%rename(equals) CVC4::RecordSelect::operator==(const RecordSelect&) const;
-%ignore CVC4::RecordSelect::operator!=(const RecordSelect&) const;
-
 %rename(equals) CVC4::RecordUpdate::operator==(const RecordUpdate&) const;
 %ignore CVC4::RecordUpdate::operator!=(const RecordUpdate&) const;
 
@@ -20,11 +17,9 @@
 %rename(getField) CVC4::Record::operator[](size_t) const;
 
 %rename(apply) CVC4::RecordHashFunction::operator()(const Record&) const;
-%rename(apply) CVC4::RecordSelectHashFunction::operator()(const RecordSelect&) const;
 %rename(apply) CVC4::RecordUpdateHashFunction::operator()(const RecordUpdate&) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Record&);
-%ignore CVC4::operator<<(std::ostream&, const RecordSelect&);
 %ignore CVC4::operator<<(std::ostream&, const RecordUpdate&);
 
 #ifdef SWIGJAVA
diff --git a/src/util/tuple.h b/src/util/tuple.h
index 8d7eca3fd..e2440cc39 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -26,15 +26,6 @@
 
 namespace CVC4 {
 
-class CVC4_PUBLIC TupleSelect {
-  unsigned d_index;
-public:
-  TupleSelect(unsigned index) throw() : d_index(index) { }
-  unsigned getIndex() const throw() { return d_index; }
-  bool operator==(const TupleSelect& t) const throw() { return d_index == t.d_index; }
-  bool operator!=(const TupleSelect& t) const throw() { return d_index != t.d_index; }
-};/* class TupleSelect */
-
 class CVC4_PUBLIC TupleUpdate {
   unsigned d_index;
 public:
@@ -44,25 +35,14 @@ public:
   bool operator!=(const TupleUpdate& t) const throw() { return d_index != t.d_index; }
 };/* class TupleUpdate */
 
-struct CVC4_PUBLIC TupleSelectHashFunction {
-  inline size_t operator()(const TupleSelect& t) const {
-    return t.getIndex();
-  }
-};/* struct TupleSelectHashFunction */
-
 struct CVC4_PUBLIC TupleUpdateHashFunction {
   inline size_t operator()(const TupleUpdate& t) const {
     return t.getIndex();
   }
 };/* struct TupleUpdateHashFunction */
 
-std::ostream& operator<<(std::ostream& out, const TupleSelect& t) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) CVC4_PUBLIC;
 
-inline std::ostream& operator<<(std::ostream& out, const TupleSelect& t) {
-  return out << "[" << t.getIndex() << "]";
-}
-
 inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) {
   return out << "[" << t.getIndex() << "]";
 }
diff --git a/src/util/tuple.i b/src/util/tuple.i
index 1498f9289..d5bf22f30 100644
--- a/src/util/tuple.i
+++ b/src/util/tuple.i
@@ -2,16 +2,11 @@
 #include "util/tuple.h"
 %}
 
-%rename(equals) CVC4::TupleSelect::operator==(const TupleSelect&) const;
-%ignore CVC4::TupleSelect::operator!=(const TupleSelect&) const;
-
 %rename(equals) CVC4::TupleUpdate::operator==(const TupleUpdate&) const;
 %ignore CVC4::TupleUpdate::operator!=(const TupleUpdate&) const;
 
-%rename(apply) CVC4::TupleSelectHashFunction::operator()(const TupleSelect&) const;
 %rename(apply) CVC4::TupleUpdateHashFunction::operator()(const TupleUpdate&) const;
 
-%ignore CVC4::operator<<(std::ostream&, const TupleSelect&);
 %ignore CVC4::operator<<(std::ostream&, const TupleUpdate&);
 
 %include "util/tuple.h"