From 3a00b0c4586ef61c93b7b7320cce4d720014f2bf Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 13 Sep 2017 01:31:30 -0700 Subject: [PATCH] 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. --- .../compat/java/src/cvc3/ValidityChecker.java | 8 -------- .../java/src/cvc3/ValidityChecker_impl.cpp | 4 ---- src/expr/expr_manager.i | 7 ------- src/expr/record.cpp | 4 ---- src/expr/record.h | 19 +----------------- src/expr/record.i | 5 ----- src/util/tuple.h | 20 ------------------- src/util/tuple.i | 5 ----- 8 files changed, 1 insertion(+), 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 @@ -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 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; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; -//%template(mkConst) CVC4::ExprManager::mkConst; - #else %template(mkConst) CVC4::ExprManager::mkConst; -%template(mkConst) CVC4::ExprManager::mkConst; -%template(mkConst) CVC4::ExprManager::mkConst; -%template(mkConst) CVC4::ExprManager::mkConst; %template(mkConst) CVC4::ExprManager::mkConst; #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()(t.getField()); - } -};/* struct RecordSelectHashFunction */ - struct CVC4_PUBLIC RecordUpdateHashFunction { inline size_t operator()(const RecordUpdate& t) const { return std::hash()(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" -- 2.30.2