More simplification to internal implementation of tuples and records.

6 files changed, 3 insertions, 187 deletions

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index c31a462bd..d035f0fa7 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -85,12 +85,6 @@ typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionType
 # constructor applications are constant if they are applied only to constants
 construle APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 
-## for co-datatypes
-operator MU 2 "a mu operator, first argument is a bound variable, second argument is body"
-typerule MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-# mu applications are constant expressions
-construle MU ::CVC4::theory::datatypes::DatatypeMuTypeRule
-
 constant TUPLE_UPDATE_OP \
         ::CVC4::TupleUpdate \
         ::CVC4::TupleUpdateHashFunction \
@@ -99,22 +93,6 @@ constant TUPLE_UPDATE_OP \
 parameterized TUPLE_UPDATE TUPLE_UPDATE_OP 2 "tuple update; first parameter is a TUPLE_UPDATE_OP (which references an index), second is the tuple, third is the element to store in the tuple at the given index"
 typerule TUPLE_UPDATE ::CVC4::theory::datatypes::TupleUpdateTypeRule
 
-constant RECORD_TYPE \
-    ::CVC4::Record \
-    ::CVC4::RecordHashFunction \
-    "expr/record.h" \
-    "record type"
-cardinality RECORD_TYPE \
-    "::CVC4::theory::datatypes::RecordProperties::computeCardinality(%TYPE%)" \
-    "theory/datatypes/theory_datatypes_type_rules.h"
-well-founded RECORD_TYPE \
-    "::CVC4::theory::datatypes::RecordProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::datatypes::RecordProperties::mkGroundTerm(%TYPE%)" \
-    "theory/datatypes/theory_datatypes_type_rules.h"
-enumerator RECORD_TYPE \
-    "::CVC4::theory::datatypes::RecordEnumerator" \
-    "theory/datatypes/type_enumerator.h"
-
 constant RECORD_UPDATE_OP \
         ::CVC4::RecordUpdate \
         ::CVC4::RecordUpdateHashFunction \
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index ad2b1a297..51300bfba 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -582,20 +582,6 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     return n;
   }
 
-  if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
-    Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
-    Debug("tuprec") << "so " << t.getDatatype() << " goes to " << in.getAttribute(smt::BooleanTermAttr()).getType().getDatatype() << endl;
-    if(t.isTuple()) {
-      Debug("tuprec") << "current datatype-tuple-attr is " << t.getAttribute(expr::DatatypeTupleAttr()) << endl;
-      Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()) << endl;
-      t.setAttribute(expr::DatatypeTupleAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeTupleAttr()));
-    } else {
-      Debug("tuprec") << "current datatype-record-attr is " << t.getAttribute(expr::DatatypeRecordAttr()) << endl;
-      Debug("tuprec") << "setting to " << in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()) << endl;
-      t.setAttribute(expr::DatatypeRecordAttr(), in.getAttribute(smt::BooleanTermAttr()).getType().getAttribute(expr::DatatypeRecordAttr()));
-    }
-  }
-
   if( in.getKind()==EQUAL ){
     Node nn;
     std::vector< Node > rew;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 477ce6ba5..e50d714e7 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -210,49 +210,6 @@ struct DatatypeAscriptionTypeRule {
   }
 };/* struct DatatypeAscriptionTypeRule */
 
-/* For co-datatypes */
-class DatatypeMuTypeRule {
-private:
-  //a Mu-expression is constant iff its body is composed of constructors applied to constant expr and bound variables only
-  inline static bool computeIsConstNode(TNode n, std::vector< TNode >& fv ){
-    if( n.getKind()==kind::MU ){
-      fv.push_back( n[0] );
-      bool ret = computeIsConstNode( n[1], fv );
-      fv.pop_back();
-      return ret;
-    }else if( n.isConst() || std::find( fv.begin(), fv.end(), n )!=fv.end() ){
-      return true;
-    }else if( n.getKind()==kind::APPLY_CONSTRUCTOR ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !computeIsConstNode( n[i], fv ) ){
-          return false;
-        }
-      }
-      return true; 
-    }else{
-      return false;
-    }
-  }
-public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
-    if( n[0].getKind()!=kind::BOUND_VARIABLE  ) {
-      std::stringstream ss;
-      ss << "expected a bound var for MU expression, got `"
-         << n[0] << "'";
-      throw TypeCheckingExceptionPrivate(n, ss.str());
-    }
-    return n[1].getType(check);
-  }
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n)
-    throw(AssertionException) {
-    Assert(n.getKind() == kind::MU);
-    NodeManagerScope nms(nodeManager);
-    std::vector< TNode > fv;
-    return computeIsConstNode( n, fv );
-  }
-};
-
-
 struct ConstructorProperties {
   inline static Cardinality computeCardinality(TypeNode type) {
     // Constructors aren't exactly functions, they're like
@@ -276,7 +233,6 @@ struct TupleUpdateTypeRule {
     if(check) {
       if(!tupleType.isTuple()) {
         throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
-        tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
       }
       if(tu.getIndex() >= tupleType.getTupleLength()) {
         std::stringstream ss;
@@ -313,23 +269,6 @@ struct RecordUpdateTypeRule {
   }
 };/* struct RecordUpdateTypeRule */
 
-struct RecordProperties {
-  inline static Node mkGroundTerm(TypeNode type) {
-    Assert(type.getKind() == kind::RECORD_TYPE);
-    return Node::null();
-  }
-  inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
-    return true;
-  }
-  inline static Cardinality computeCardinality(TypeNode type) {
-    Cardinality card(1);
-    return card;
-  }
-  inline static bool isWellFounded(TypeNode type) {
-    return true;
-  }
-};/* struct RecordProperties */
-
 class DtSizeTypeRule {
 public:
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 1f30498d6..2cf72e8e9 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -177,92 +177,6 @@ public:
 
 };/* DatatypesEnumerator */
 
-
-class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
-  TypeEnumeratorProperties * d_tep;
-  TypeEnumerator** d_enumerators;
-
-  /** Allocate and initialize the delegate enumerators */
-  void newEnumerators() {
-    const Record& rec = getType().getConst<Record>();
-    d_enumerators = new TypeEnumerator*[rec.getNumFields()];
-    for(size_t i = 0; i < rec.getNumFields(); ++i) {
-      d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
-    }
-  }
-
-  void deleteEnumerators() throw() {
-    if(d_enumerators != NULL) {
-      const Record& rec = getType().getConst<Record>();
-      for(size_t i = 0; i < rec.getNumFields(); ++i) {
-        delete d_enumerators[i];
-      }
-      delete [] d_enumerators;
-      d_enumerators = NULL;
-    }
-  }
-
-public:
-
-  RecordEnumerator(TypeNode type, TypeEnumeratorProperties * tep = NULL) throw() :
-    TypeEnumeratorBase<RecordEnumerator>(type), d_tep(tep) {
-    Assert(type.isRecord());
-    newEnumerators();
-  }
-
-  RecordEnumerator(const RecordEnumerator& re) throw() :
-    TypeEnumeratorBase<RecordEnumerator>(re.getType()),
-    d_tep(re.d_tep),
-    d_enumerators(NULL) {
-
-    if(re.d_enumerators != NULL) {
-      newEnumerators();
-      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
-        *d_enumerators[i] = TypeEnumerator(*re.d_enumerators[i]);
-      }
-    }
-  }
-
-  virtual ~RecordEnumerator() throw() {
-    deleteEnumerators();
-  }
-
-  Node operator*() throw(NoMoreValuesException) {
-    if(isFinished()) {
-      throw NoMoreValuesException(getType());
-    }
-
-
-    return Node::null();
-  }
-
-  RecordEnumerator& operator++() throw() {
-    if(isFinished()) {
-      return *this;
-    }
-
-    size_t i;
-    const Record& rec = getType().getConst<Record>();
-    for(i = 0; i < rec.getNumFields(); ++i) {
-      if(d_enumerators[i]->isFinished()) {
-        *d_enumerators[i] = TypeEnumerator(TypeNode::fromType(rec[i].second));
-      } else {
-        ++*d_enumerators[i];
-        return *this;
-      }
-    }
-
-    deleteEnumerators();
-
-    return *this;
-  }
-
-  bool isFinished() throw() {
-    return d_enumerators == NULL;
-  }
-
-};/* RecordEnumerator */
-
 }/* CVC4::theory::datatypes namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index afe8cd598..881210d78 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -932,8 +932,7 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
       newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
       std::vector< Node > newVars;
       for( unsigned j=0; j<c.getNumArgs(); j++ ){
-        TypeNode tn = TypeNode::fromType( c[j].getSelector().getType() );
-        tn = tn[1];
+        TypeNode tn = TypeNode::fromType( c[j].getRangeType() );
         Node v = NodeManager::currentNM()->mkBoundVar( tn );
         newChildren.push_back( v );
         newVars.push_back( v );
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 560f68810..a679ccfa8 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -855,7 +855,7 @@ Node TermDb::getInstantiatedNode( Node n, Node q, std::vector< Node >& terms ) {
 
 void getSelfSel( const DatatypeConstructor& dc, Node n, TypeNode ntn, std::vector< Node >& selfSel ){
   for( unsigned j=0; j<dc.getNumArgs(); j++ ){
-    TypeNode tn = TypeNode::fromType( ((SelectorType)dc[j].getSelector().getType()).getRangeType() );
+    TypeNode tn = TypeNode::fromType( dc[j].getRangeType() );
     std::vector< Node > ssc;
     if( tn==ntn ){
       ssc.push_back( n );
@@ -1050,7 +1050,7 @@ bool TermDb::isClosedEnumerableType( TypeNode tn ) {
       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
       for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
         for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-          TypeNode ctn = TypeNode::fromType( ((SelectorType)dt[i][j].getSelector().getType()).getRangeType() );
+          TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
           if( tn!=ctn && !isClosedEnumerableType( ctn ) ){
             ret = false;
             break;