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, 7 insertions, 2 deletions

diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 561d99392..b9cae9431 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -359,6 +359,11 @@ public:
   TupleType mkTupleType(const std::vector<Type>& types);
 
   /**
+   * Make a record type with types from the rec parameter.
+   */
+  RecordType mkRecordType(const Record& rec);
+
+  /**
    * Make a symbolic expressiontype with types from
    * <code>types[0..types.size()-1]</code>.  <code>types</code> may
    * have any number of elements.
@@ -464,8 +469,8 @@ public:
     throw(TypeCheckingException);
 
   // variables are special, because duplicates are permitted
-  Expr mkVar(const std::string& name, Type type);
-  Expr mkVar(Type type);
+  Expr mkVar(const std::string& name, Type type, bool isGlobal = false);
+  Expr mkVar(Type type, bool isGlobal = false);
   Expr mkBoundVar(const std::string& name, Type type);
   Expr mkBoundVar(Type type);