1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief A class representing a Record definition
14 ** A class representing a Record definition.
17 #include "cvc4_public.h"
19 #ifndef __CVC4__RECORD_H
20 #define __CVC4__RECORD_H
26 #include "util/hash.h"
30 class CVC4_PUBLIC Record
;
32 // operators for record select and update
34 class CVC4_PUBLIC RecordSelect
{
37 RecordSelect(const std::string
& field
) throw() : d_field(field
) { }
38 std::string
getField() const throw() { return d_field
; }
39 bool operator==(const RecordSelect
& t
) const throw() { return d_field
== t
.d_field
; }
40 bool operator!=(const RecordSelect
& t
) const throw() { return d_field
!= t
.d_field
; }
41 };/* class RecordSelect */
43 class CVC4_PUBLIC RecordUpdate
{
46 RecordUpdate(const std::string
& field
) throw() : d_field(field
) { }
47 std::string
getField() const throw() { return d_field
; }
48 bool operator==(const RecordUpdate
& t
) const throw() { return d_field
== t
.d_field
; }
49 bool operator!=(const RecordUpdate
& t
) const throw() { return d_field
!= t
.d_field
; }
50 };/* class RecordUpdate */
52 struct CVC4_PUBLIC RecordSelectHashFunction
{
53 inline size_t operator()(const RecordSelect
& t
) const {
54 return StringHashFunction()(t
.getField());
56 };/* struct RecordSelectHashFunction */
58 struct CVC4_PUBLIC RecordUpdateHashFunction
{
59 inline size_t operator()(const RecordUpdate
& t
) const {
60 return StringHashFunction()(t
.getField());
62 };/* struct RecordUpdateHashFunction */
64 std::ostream
& operator<<(std::ostream
& out
, const RecordSelect
& t
) CVC4_PUBLIC
;
65 std::ostream
& operator<<(std::ostream
& out
, const RecordUpdate
& t
) CVC4_PUBLIC
;
67 inline std::ostream
& operator<<(std::ostream
& out
, const RecordSelect
& t
) {
68 return out
<< "[" << t
.getField() << "]";
71 inline std::ostream
& operator<<(std::ostream
& out
, const RecordUpdate
& t
) {
72 return out
<< "[" << t
.getField() << "]";
77 #include "expr/expr.h"
78 #include "expr/type.h"
82 // now an actual record definition
84 class CVC4_PUBLIC Record
{
85 std::vector
< std::pair
<std::string
, Type
> > d_fields
;
89 typedef std::vector
< std::pair
<std::string
, Type
> >::const_iterator const_iterator
;
90 typedef const_iterator iterator
;
92 Record(const std::vector
< std::pair
<std::string
, Type
> >& fields
) :
94 CheckArgument(! fields
.empty(), fields
, "fields in record description cannot be empty");
97 const_iterator
find(std::string name
) const {
99 for(i
= begin(); i
!= end(); ++i
) {
100 if((*i
).first
== name
) {
107 size_t getIndex(std::string name
) const {
108 const_iterator i
= find(name
);
109 CheckArgument(i
!= end(), name
, "requested field `%s' does not exist in record", name
.c_str());
113 size_t getNumFields() const {
114 return d_fields
.size();
117 const_iterator
begin() const {
118 return d_fields
.begin();
121 const_iterator
end() const {
122 return d_fields
.end();
125 std::pair
<std::string
, Type
> operator[](size_t index
) const {
126 CheckArgument(index
< d_fields
.size(), index
, "index out of bounds for record type");
127 return d_fields
[index
];
130 bool operator==(const Record
& r
) const {
131 return d_fields
== r
.d_fields
;
134 bool operator!=(const Record
& r
) const {
135 return !(*this == r
);
140 struct CVC4_PUBLIC RecordHashFunction
{
141 inline size_t operator()(const Record
& r
) const {
143 for(Record::iterator i
= r
.begin(); i
!= r
.end(); ++i
) {
144 n
= (n
<< 3) ^ TypeHashFunction()((*i
).second
);
148 };/* struct RecordHashFunction */
150 std::ostream
& operator<<(std::ostream
& os
, const Record
& r
) CVC4_PUBLIC
;
152 }/* CVC4 namespace */
154 #endif /* __CVC4__RECORD_H */