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

1 files changed, 9 insertions, 4 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index cacfa9215..7cb5eb459 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -517,6 +517,11 @@ TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
   return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 }
 
+RecordType ExprManager::mkRecordType(const Record& rec) {
+  NodeManagerScope nms(d_nodeManager);
+  return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+}
+
 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
   std::vector<TypeNode> typeNodes;
@@ -804,20 +809,20 @@ Type ExprManager::getType(Expr e, bool check) throw (TypeCheckingException) {
   return t;
 }
 
-Expr ExprManager::mkVar(const std::string& name, Type type) {
+Expr ExprManager::mkVar(const std::string& name, Type type, bool isGlobal) {
   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
-  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode);
+  Node* n = d_nodeManager->mkVarPtr(name, *type.d_typeNode, isGlobal);
   Debug("nm") << "set " << name << " on " << *n << std::endl;
   INC_STAT_VAR(type, false);
   return Expr(this, n);
 }
 
-Expr ExprManager::mkVar(Type type) {
+Expr ExprManager::mkVar(Type type, bool isGlobal) {
   Assert(NodeManager::currentNM() == NULL, "ExprManager::mkVar() should only be called externally, not from within CVC4 code.  Please use mkSkolem().");
   NodeManagerScope nms(d_nodeManager);
   INC_STAT_VAR(type, false);
-  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode));
+  return Expr(this, d_nodeManager->mkVarPtr(*type.d_typeNode, isGlobal));
 }
 
 Expr ExprManager::mkBoundVar(const std::string& name, Type type) {