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

2 files changed, 0 insertions, 75 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index bcf787f6b..e3bc506e2 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -296,7 +296,6 @@ operator DISTINCT 2: "disequality"
 variable VARIABLE "variable"
 variable BOUND_VARIABLE "bound variable"
 variable SKOLEM "skolem var"
-operator TUPLE 1: "a tuple"
 operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
@@ -313,14 +312,6 @@ cardinality FUNCTION_TYPE \
     "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 well-founded FUNCTION_TYPE false
-operator TUPLE_TYPE 1: "tuple type"
-cardinality TUPLE_TYPE \
-    "::CVC4::theory::builtin::TupleProperties::computeCardinality(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
-well-founded TUPLE_TYPE \
-    "::CVC4::theory::builtin::TupleProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::TupleProperties::mkGroundTerm(%TYPE%)" \
-    "theory/builtin/theory_builtin_type_rules.h"
 operator SEXPR_TYPE 0: "symbolic expression type"
 cardinality SEXPR_TYPE \
     "::CVC4::theory::builtin::SExprProperties::computeCardinality(%TYPE%)" \
@@ -350,7 +341,6 @@ typerule CONST_STRING ::CVC4::theory::builtin::StringConstantTypeRule
 typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
-typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 720e55be3..4aa7c0982 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -115,19 +115,6 @@ public:
   }
 };/* class DistinctTypeRule */
 
-class TupleTypeRule {
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    std::vector<TypeNode> types;
-    for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
-        child_it != child_it_end;
-        ++child_it) {
-      types.push_back((*child_it).getType(check));
-    }
-    return nodeManager->mkTupleType(types);
-  }
-};/* class TupleTypeRule */
-
 class SExprTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
@@ -269,58 +256,6 @@ public:
   }
 };/* class FuctionProperties */
 
-class TupleProperties {
-public:
-  inline static Cardinality computeCardinality(TypeNode type) {
-    // Don't assert this; allow other theories to use this cardinality
-    // computation.
-    //
-    // Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    Cardinality card(1);
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      card *= (*i).getCardinality();
-    }
-
-    return card;
-  }
-
-  inline static bool isWellFounded(TypeNode type) {
-    // Don't assert this; allow other theories to use this
-    // wellfoundedness computation.
-    //
-    // Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      if(! (*i).isWellFounded()) {
-        return false;
-      }
-    }
-
-    return true;
-  }
-
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::TUPLE_TYPE);
-
-    std::vector<Node> children;
-    for(TypeNode::iterator i = type.begin(),
-          i_end = type.end();
-        i != i_end;
-        ++i) {
-      children.push_back((*i).mkGroundTerm());
-    }
-
-    return NodeManager::currentNM()->mkNode(kind::TUPLE, children);
-  }
-};/* class TupleProperties */
-
 class SExprProperties {
 public:
   inline static Cardinality computeCardinality(TypeNode type) {