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.

diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker.java b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
index 7407d0251826343364c46a74b6a1cac180ece9a2..1b38a4c9526e45d380da57e3800a9272283db5a9 100644 (file)
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker.java
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker.java
@@ -311,8 +311,6 @@ public class ValidityChecker extends Embedded {
         jniComputeBVConst(Object ValidityChecker, Object Expr) throws Cvc3Exception;
     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;
@@ -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 6bab7d2e0a0ccb74de74cf3488ebb3507cbbef97..cfda940d83f9ab4ac493e8a6a4a2d4e61414d4c3 100644 (file)
--- 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 136e75f98d9a682e0dbf401d625462a4d6a6ad18..dac3b93125fb30995068767a3216a4e40a15c993 100644 (file)
--- 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 4b2d50ea60dcc830ee8cb625b0c021401b59129e..2c59962137c81adeddd46d307766edfed73e9bc8 100644 (file)
--- 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 7c5854db256f272d1e9b5475f0ab8614e15fbb21..ae03a7acd933d41ed26efbb51d0fb1f5c3623947 100644 (file)
--- 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 695ff105b9ba4d1d0067191d433d19464308e3e3..d5b018f72a5a6d639afd5458b7db510423d0f3b1 100644 (file)
--- 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 8d7eca3fdc11a237bc9aa4f32242afc338cbe2d8..e2440cc39d57d76a5e2ae932e3cbe6e58461b92b 100644 (file)
--- 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 1498f92891ac24c4ff0ffda03b1ae68c15eea04d..d5bf22f306d2e88441617fbc254c88dffa584f8a 100644 (file)
--- 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"