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.

4 files changed, 1 insertions, 34 deletions

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