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.)

10 files changed, 299 insertions, 5 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e72706ea3..804bcde11 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -43,6 +43,9 @@ libutil_la_SOURCES = \
 	array.h \
 	datatype.h \
 	datatype.cpp \
+	tuple.h \
+	record.h \
+	record.cpp \
 	matcher.h \
 	gmp_util.h \
 	sexpr.h \
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index a225339cd..be98e40e1 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -558,6 +558,7 @@ Expr DatatypeConstructor::getConstructor() const {
 
 Type DatatypeConstructor::getSpecializedConstructorType(Type returnType) const {
   CheckArgument(isResolved(), this, "this datatype constructor is not yet resolved");
+  ExprManagerScope ems(d_constructor);
   const Datatype& dt = Datatype::datatypeOf(d_constructor);
   CheckArgument(dt.isParametric(), this, "this datatype constructor is not parametric");
   DatatypeType dtt = dt.getDatatypeType();
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index ad21be287..07e85c118 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -59,7 +59,9 @@ private:
   void readInt(const cln::cl_read_flags& flags, const std::string& s, unsigned base) throw(std::invalid_argument) {
     try {
       if(s.find_first_not_of('0') == std::string::npos) {
-        // string of all zeroes, CLN has a bug for these inputs
+        // String of all zeroes, CLN has a bug for these inputs up to and
+        // including CLN v1.3.2.
+        // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
         d_value = read_integer(flags, "0", NULL, NULL);
       } else {
         d_value = read_integer(flags, s.c_str(), NULL, NULL);
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 */
diff --git a/src/util/record.h b/src/util/record.h
new file mode 100644
index 000000000..2c15d30e0
--- /dev/null
+++ b/src/util/record.h
@@ -0,0 +1,156 @@
+/*********************                                                        */
+/*! \file record.h
+ ** \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 "cvc4_public.h"
+
+#ifndef __CVC4__RECORD_H
+#define __CVC4__RECORD_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <utility>
+#include "util/hash.h"
+
+namespace CVC4 {
+
+class Record;
+
+// 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 */
+
+class CVC4_PUBLIC RecordUpdate {
+  std::string d_field;
+public:
+  RecordUpdate(const std::string& field) throw() : d_field(field) { }
+  std::string getField() const throw() { return d_field; }
+  bool operator==(const RecordUpdate& t) const throw() { return d_field == t.d_field; }
+  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 StringHashFunction()(t.getField());
+  }
+};/* struct RecordSelectHashFunction */
+
+struct CVC4_PUBLIC RecordUpdateHashFunction {
+  inline size_t operator()(const RecordUpdate& t) const {
+    return StringHashFunction()(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;
+
+inline std::ostream& operator<<(std::ostream& out, const RecordSelect& t) {
+  return out << "[" << t.getField() << "]";
+}
+
+inline std::ostream& operator<<(std::ostream& out, const RecordUpdate& t) {
+  return out << "[" << t.getField() << "]";
+}
+
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+
+namespace CVC4 {
+
+// now an actual record definition
+
+class CVC4_PUBLIC Record {
+  std::vector< std::pair<std::string, Type> > d_fields;
+
+public:
+
+  typedef std::vector< std::pair<std::string, Type> >::const_iterator const_iterator;
+  typedef const_iterator iterator;
+
+  Record(const std::vector< std::pair<std::string, Type> >& fields) :
+    d_fields(fields) {
+    CheckArgument(! fields.empty(), fields, "fields in record description cannot be empty");
+  }
+
+  const_iterator find(std::string name) const {
+    const_iterator i;
+    for(i = begin(); i != end(); ++i) {
+      if((*i).first == name) {
+        break;
+      }
+    }
+    return i;
+  }
+
+  size_t getIndex(std::string name) const {
+    const_iterator i = find(name);
+    CheckArgument(i != end(), name, "requested field `%s' does not exist in record", name.c_str());
+    return i - begin();
+  }
+
+  size_t getNumFields() const {
+    return d_fields.size();
+  }
+
+  const_iterator begin() const {
+    return d_fields.begin();
+  }
+
+  const_iterator end() const {
+    return d_fields.end();
+  }
+
+  std::pair<std::string, Type> operator[](size_t index) const {
+    CheckArgument(index < d_fields.size(), index, "index out of bounds for record type");
+    return d_fields[index];
+  }
+
+  bool operator==(const Record& r) const {
+    return d_fields == r.d_fields;
+  }
+
+  bool operator!=(const Record& r) const {
+    return !(*this == r);
+  }
+
+};/* class Record */
+
+struct CVC4_PUBLIC RecordHashFunction {
+  inline size_t operator()(const Record& r) const {
+    size_t n = 0;
+    for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+      n = (n << 3) ^ TypeHashFunction()((*i).second);
+    }
+    return n;
+  }
+};/* struct RecordHashFunction */
+
+std::ostream& operator<<(std::ostream& os, const Record& r) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RECORD_H */
diff --git a/src/util/record.i b/src/util/record.i
new file mode 100644
index 000000000..f662178c2
--- /dev/null
+++ b/src/util/record.i
@@ -0,0 +1,5 @@
+%{
+#include "util/record.h"
+%}
+
+%include "util/record.h"
diff --git a/src/util/tuple.h b/src/util/tuple.h
new file mode 100644
index 000000000..6c1e981a4
--- /dev/null
+++ b/src/util/tuple.h
@@ -0,0 +1,74 @@
+/*********************                                                        */
+/*! \file tuple.h
+ ** \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 Tuple operators
+ **
+ ** Tuple operators.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__TUPLE_H
+#define __CVC4__TUPLE_H
+
+#include <iostream>
+#include <string>
+#include <vector>
+#include <utility>
+
+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:
+  TupleUpdate(unsigned index) throw() : d_index(index) { }
+  unsigned getIndex() const throw() { return d_index; }
+  bool operator==(const TupleUpdate& t) const throw() { return d_index == t.d_index; }
+  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() << "]";
+}
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__TUPLE_H */
diff --git a/src/util/tuple.i b/src/util/tuple.i
new file mode 100644
index 000000000..d7301d201
--- /dev/null
+++ b/src/util/tuple.i
@@ -0,0 +1,5 @@
+%{
+#include "util/tuple.h"
+%}
+
+%include "util/tuple.h"
diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index bb2924b51..0c058fce9 100644
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -36,11 +36,17 @@ Model::Model() :
 }
 
 size_t Model::getNumCommands() const {
-  return d_smt.d_modelCommands->size();
+  return d_smt.d_modelCommands->size() + d_smt.d_modelGlobalCommands.size();
 }
 
 const Command* Model::getCommand(size_t i) const {
-  return (*d_smt.d_modelCommands)[i];
+  Assert(i < getNumCommands());
+  // index the global commands first, then the locals
+  if(i < d_smt.d_modelGlobalCommands.size()) {
+    return d_smt.d_modelGlobalCommands[i];
+  } else {
+    return (*d_smt.d_modelCommands)[i - d_smt.d_modelGlobalCommands.size()];
+  }
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 72ff8af60..21c3fb400 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -35,8 +35,8 @@ class Model {
   friend std::ostream& operator<<(std::ostream&, Model&);
 
 protected:
-  /** The SmtEngine we're associated to */
-  const SmtEngine& d_smt;
+  /** The SmtEngine we're associated with */
+  SmtEngine& d_smt;
 
   /** construct the base class; users cannot do this, only CVC4 internals */
   Model();
@@ -48,6 +48,8 @@ public:
   size_t getNumCommands() const;
   /** get command */
   const Command* getCommand(size_t i) const;
+  /** get the smt engine that this model is hooked up to */
+  SmtEngine* getSmtEngine() { return &d_smt; }
 
 public:
   /** get value for expression */