26 lines
833 B
Diff
26 lines
833 B
Diff
--- src/theory/datatypes/kinds.orig 2017-06-23 15:54:52.988063375 -0600
|
|
+++ src/theory/datatypes/kinds 2017-07-15 20:30:31.268986539 -0600
|
|
@@ -108,4 +108,22 @@ typerule DT_SIZE ::CVC4::theory::datatyp
|
|
operator DT_HEIGHT_BOUND 2 "datatypes height bound"
|
|
typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule
|
|
|
|
+constant TUPLE_SELECT_OP \
|
|
+ ::CVC4::TupleSelect \
|
|
+ ::CVC4::TupleSelectHashFunction \
|
|
+ "util/tuple.h" \
|
|
+ "operator for a tuple select"
|
|
+
|
|
+constant RECORD_OP \
|
|
+ ::CVC4::Record \
|
|
+ ::CVC4::RecordHashFunction \
|
|
+ "expr/record.h" \
|
|
+ "operator for a record"
|
|
+
|
|
+constant RECORD_SELECT_OP \
|
|
+ ::CVC4::RecordSelect \
|
|
+ ::CVC4::RecordSelectHashFunction \
|
|
+ "expr/record.h" \
|
|
+ "operator for a record select"
|
|
+
|
|
endtheory
|