summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/bindings/compat/java/src/cvc3/ValidityChecker.java8
-rw-r--r--src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp4
-rw-r--r--src/expr/expr_manager.i7
-rw-r--r--src/expr/record.cpp4
-rw-r--r--src/expr/record.h19
-rw-r--r--src/expr/record.i5
-rw-r--r--src/util/tuple.h20
-rw-r--r--src/util/tuple.i5
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback