summaryrefslogtreecommitdiff
path: root/src/util/record.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-11-27 02:13:38 +0000
committerMorgan Deters <mdeters@gmail.com>2012-11-27 02:13:38 +0000
commitb122cec27ca27d0b48e786191448e0053be78ed0 (patch)
tree615981d8623e830894f02fc528b173ac7461f934 /src/util/record.cpp
parent3da16da97df7cd2efd4b113db3bfef8b9c138ebe (diff)
Tuples and records merge. Resolves bug 270.
Also some fixes to parametric datatypes I found, and fixes for a handful of bugs, including some observed with --check-models --incremental on together. (this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/util/record.cpp')
-rw-r--r--src/util/record.cpp40
1 files changed, 40 insertions, 0 deletions
diff --git a/src/util/record.cpp b/src/util/record.cpp
new file mode 100644
index 000000000..f3dc29f81
--- /dev/null
+++ b/src/util/record.cpp
@@ -0,0 +1,40 @@
+/********************* */
+/*! \file record.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A class representing a record definition
+ **
+ ** A class representing a record definition.
+ **/
+
+#include "util/record.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& os, const Record& r) {
+ os << "[# ";
+ bool first = true;
+ for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+ if(!first) {
+ os << ", ";
+ }
+ os << (*i).first << ":" << (*i).second;
+ first = false;
+ }
+ os << " #]";
+
+ return os;
+}
+
+}/* CVC4 namespace */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback