cvc4-1.4
record.h
Go to the documentation of this file.
1 /********************* */
17 #include "cvc4_public.h"
18 
19 #ifndef __CVC4__RECORD_H
20 #define __CVC4__RECORD_H
21 
22 #include <iostream>
23 #include <string>
24 #include <vector>
25 #include <utility>
26 #include "util/hash.h"
27 
28 namespace CVC4 {
29 
30 class CVC4_PUBLIC Record;
31 
32 // operators for record select and update
33 
35  std::string d_field;
36 public:
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 */
42 
44  std::string d_field;
45 public:
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 */
51 
53  inline size_t operator()(const RecordSelect& t) const {
54  return StringHashFunction()(t.getField());
55  }
56 };/* struct RecordSelectHashFunction */
57 
59  inline size_t operator()(const RecordUpdate& t) const {
60  return StringHashFunction()(t.getField());
61  }
62 };/* struct RecordUpdateHashFunction */
63 
64 std::ostream& operator<<(std::ostream& out, const RecordSelect& t) CVC4_PUBLIC;
65 std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) CVC4_PUBLIC;
66 
67 inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
68  return out << "[" << t.getField() << "]";
69 }
70 
71 inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
72  return out << "[" << t.getField() << "]";
73 }
74 
75 }/* CVC4 namespace */
76 
77 #include "expr/expr.h"
78 #include "expr/type.h"
79 
80 namespace CVC4 {
81 
82 // now an actual record definition
83 
85  std::vector< std::pair<std::string, Type> > d_fields;
86 
87 public:
88 
89  typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator;
90  typedef const_iterator iterator;
91 
92  Record(const std::vector< std::pair<std::string, Type> >& fields) :
93  d_fields(fields) {
94  }
95 
96  const_iterator find(std::string name) const {
97  const_iterator i;
98  for(i = begin(); i != end(); ++i) {
99  if((*i).first == name) {
100  break;
101  }
102  }
103  return i;
104  }
105 
106  size_t getIndex(std::string name) const {
107  const_iterator i = find(name);
108  CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str());
109  return i - begin();
110  }
111 
112  size_t getNumFields() const {
113  return d_fields.size();
114  }
115 
116  const_iterator begin() const {
117  return d_fields.begin();
118  }
119 
120  const_iterator end() const {
121  return d_fields.end();
122  }
123 
124  std::pair<std::string, Type> operator[](size_t index) const {
125  CheckArgument(index < d_fields.size(), index, "index out of bounds for record type");
126  return d_fields[index];
127  }
128 
129  bool operator==(const Record& r) const {
130  return d_fields == r.d_fields;
131  }
132 
133  bool operator!=(const Record& r) const {
134  return !(*this == r);
135  }
136 
137 };/* class Record */
138 
140  inline size_t operator()(const Record& r) const {
141  size_t n = 0;
142  for(Record::iterator i = r.begin(); i != r.end(); ++i) {
143  n = (n << 3) ^ TypeHashFunction()((*i).second);
144  }
145  return n;
146  }
147 };/* struct RecordHashFunction */
148 
149 std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
150 
151 }/* CVC4 namespace */
152 
153 #endif /* __CVC4__RECORD_H */
const_iterator iterator
Definition: record.h:90
bool operator==(const RecordSelect &t) const
Definition: record.h:39
Definition: options.h:94
size_t getNumFields() const
Definition: record.h:112
std::vector< std::pair< std::string, Type > >::const_iterator const_iterator
Definition: record.h:89
Hash function for Types.
Definition: type.h:69
size_t operator()(const RecordUpdate &t) const
Definition: record.h:59
const_iterator end() const
Definition: record.h:120
bool operator!=(const Record &r) const
Definition: record.h:133
[[ Add one-line brief description here ]]
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
Definition: exception.h:140
std::pair< std::string, Type > operator[](size_t index) const
Definition: record.h:124
bool operator==(const RecordUpdate &t) const
Definition: record.h:48
std::string getField() const
Definition: record.h:47
RecordSelect(const std::string &field)
Definition: record.h:37
size_t operator()(const Record &r) const
Definition: record.h:140
Record(const std::vector< std::pair< std::string, Type > > &fields)
Definition: record.h:92
bool operator!=(const RecordSelect &t) const
Definition: record.h:40
std::string getField() const
Definition: record.h:38
const_iterator find(std::string name) const
Definition: record.h:96
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
Macros that should be defined everywhere during the building of the libraries and driver binary...
bool operator!=(const RecordUpdate &t) const
Definition: record.h:49
const_iterator begin() const
Definition: record.h:116
size_t operator()(const RecordSelect &t) const
Definition: record.h:53
struct CVC4::options::out__option_t out
RecordUpdate(const std::string &field)
Definition: record.h:46
expr.h
std::ostream & operator<<(std::ostream &out, SimplificationMode mode)
bool operator==(const Record &r) const
Definition: record.h:129
Interface for expression types.
size_t getIndex(std::string name) const
Definition: record.h:106