Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.

3 files changed, 20 insertions, 154 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 4372c0c18..07d78a6fd 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -139,14 +139,15 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
     processing[in_t] = true;
     if(in.getType().isRecord()) {
       Assert(as.isRecord());
-      const Record& inRec = in.getType().getConst<Record>();
-      const Record& asRec = as.getConst<Record>();
+      const Record& inRec = in.getType().getRecord();
+      const Record& asRec = as.getRecord();
       Assert(inRec.getNumFields() == asRec.getNumFields());
-      NodeBuilder<> nb(kind::RECORD);
+      const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
+      NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
       nb << NodeManager::currentNM()->mkConst(asRec);
       for(size_t i = 0; i < asRec.getNumFields(); ++i) {
         Assert(inRec[i].first == asRec[i].first);
-        Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(RecordSelect(inRec[i].first)), in);
+        Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
         if(inRec[i].second != asRec[i].second) {
           arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
         }
@@ -156,21 +157,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
       processing.erase( in_t );
       return out;
     }
-    if(in.getType().isTuple()) {
-      Assert(as.isTuple());
-      Assert(in.getType().getNumChildren() == as.getNumChildren());
-      NodeBuilder<> nb(kind::TUPLE);
-      for(size_t i = 0; i < as.getNumChildren(); ++i) {
-        Node arg = NodeManager::currentNM()->mkNode(NodeManager::currentNM()->mkConst(TupleSelect(i)), in);
-        if(in.getType()[i] != as[i]) {
-          arg = rewriteAs(arg, as[i], processing);
-        }
-        nb << arg;
-      }
-      Node out = nb;
-      processing.erase( in_t );
-      return out;
-    }
     if(in.getType().isDatatype()) {
       if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
         processing.erase( in_t );
@@ -387,25 +373,6 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext)
     } else Debug("boolean-terms") << "OUT is DIFFERENT FROM TYPE" << endl;
     return out;
   }
-  if(type.isRecord()) {
-    const Record& rec = type.getConst<Record>();
-    const Record::FieldVector& fields = rec.getFields();
-    vector< pair<string, Type> > flds;
-    for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
-      TypeNode converted = convertType(TypeNode::fromType((*i).second), true);
-      if(TypeNode::fromType((*i).second) != converted) {
-        flds.push_back(make_pair((*i).first, converted.toType()));
-      } else {
-        flds.push_back(*i);
-      }
-    }
-    TypeNode newRec = NodeManager::currentNM()->mkRecordType(Record(flds));
-    Debug("tuprec") << "converted " << type << " to " << newRec << endl;
-    if(newRec != type) {
-      outNode = newRec;// cache it
-    }
-    return newRec;
-  }
   if(!type.isSort() && type.getNumChildren() > 0) {
     Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
     // This should handle tuples and arrays ok.
@@ -460,7 +427,9 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
   stack< triple<TNode, theory::TheoryId, bool> > worklist;
   worklist.push(triple<TNode, theory::TheoryId, bool>(top, parentTheory, false));
   stack< NodeBuilder<> > result;
-  result.push(NodeBuilder<>(kind::TUPLE));
+  //AJR: not sure what the significance of "TUPLE" is here, seems to be a placeholder.  Since TUPLE is no longer a kind, replacing this with "AND".
+  //result.push(NodeBuilder<>(kind::TUPLE));
+  result.push(NodeBuilder<>(kind::AND));
 
   NodeManager* nm = NodeManager::currentNM();
 
@@ -670,26 +639,6 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
           result.top() << top;
           worklist.pop();
           goto next_worklist;
-        } else if(t.isTuple() || t.isRecord()) {
-          TypeNode newType = convertType(t, true);
-          if(t != newType) {
-            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
-                                  newType, "a tuple/record variable introduced by Boolean-term conversion",
-                                  NodeManager::SKOLEM_EXACT_NAME);
-            top.setAttribute(BooleanTermAttr(), n);
-            n.setAttribute(BooleanTermAttr(), top);
-            Debug("boolean-terms") << "adding subs: " << top << " :=> " << n << endl;
-            d_smt.d_theoryEngine->getModel()->addSubstitution(top, n);
-            Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
-            d_varCache[top] = n;
-            result.top() << n;
-            worklist.pop();
-            goto next_worklist;
-          }
-          d_varCache[top] = Node::null();
-          result.top() << top;
-          worklist.pop();
-          goto next_worklist;
         } else if(t.isDatatype() || t.isParametricDatatype()) {
           Debug("boolean-terms") << "found a var of datatype type" << endl;
           TypeNode newT = convertType(t, parentTheory == theory::THEORY_DATATYPES);
@@ -857,17 +806,13 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         Debug("bt") << "looking at: " << top << endl;
         // rewrite the operator, as necessary
         if(mk == kind::metakind::PARAMETERIZED) {
-          if(k == kind::RECORD) {
-            result.top() << convertType(top.getType(), parentTheory == theory::THEORY_DATATYPES);
-          } else if(k == kind::APPLY_TYPE_ASCRIPTION) {
+          if(k == kind::APPLY_TYPE_ASCRIPTION) {
             Node asc = nm->mkConst(AscriptionType(convertType(TypeNode::fromType(top.getOperator().getConst<AscriptionType>().getType()), parentTheory == theory::THEORY_DATATYPES).toType()));
             result.top() << asc;
             Debug("boolean-terms") << "setting " << top.getOperator() << ":" << top.getOperator().getId() << " to point to " << asc << ":" << asc.getId() << endl;
             asc.setAttribute(BooleanTermAttr(), top.getOperator());
           } else if(kindToTheoryId(k) != THEORY_BV &&
-                    k != kind::TUPLE_SELECT &&
                     k != kind::TUPLE_UPDATE &&
-                    k != kind::RECORD_SELECT &&
                     k != kind::RECORD_UPDATE &&
                     k != kind::DIVISIBLE &&
         // Theory parametric functions go here
@@ -899,7 +844,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
     } else {
       Node n = result.top();
       result.pop();
-      Debug("boolean-terms") << "constructed: " << n << endl;
+      Debug("boolean-terms") << "constructed: " << n << " of type " << n.getType() << endl;
       if(parentTheory == theory::THEORY_BOOL) {
         if(n.getType().isBitVector() &&
            n.getType().getBitVectorSize() == 1) {
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 0ba668b33..aa645954b 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -71,21 +71,6 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
       return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, (tf ? asDatatype[0] : asDatatype[1]).getConstructor());
     }
   }
-  if(n.getType().isRecord() && asType.isRecord()) {
-    Debug("boolean-terms") << "+++ got a record - rewriteAs " << n << " : " << asType << endl;
-    const Record& rec CVC4_UNUSED = n.getType().getConst<Record>();
-    const Record& asRec = asType.getConst<Record>();
-    Assert(rec.getNumFields() == asRec.getNumFields());
-    Assert(n.getNumChildren() == asRec.getNumFields());
-    NodeBuilder<> b(n.getKind());
-    b << asType;
-    for(size_t i = 0; i < n.getNumChildren(); ++i) {
-      b << rewriteAs(n[i], TypeNode::fromType(asRec[i].second));
-    }
-    Node out = b;
-    Debug("boolean-terms") << "+++ returning record " << out << endl;
-    return out;
-  }
   Debug("boolean-terms") << "+++ rewriteAs " << n << " : " << asType << endl;
   if(n.getType().isArray()) {
     Assert(asType.isArray());
@@ -157,80 +142,7 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
   Debug("tuprec") << "visiting " << current << endl;
   Assert(!alreadyVisited(current, TNode::null()));
   bool rewriteChildren = false;
-  if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
-    if(current.getKind() == kind::APPLY_CONSTRUCTOR){
-      TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
-      NodeBuilder<> b(kind::TUPLE);
-      TypeNode::iterator t = expectType.begin();
-      for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
-        Assert(alreadyVisited(*i, TNode::null()));
-        Assert(t != expectType.end());
-        TNode n = d_nodes[*i];
-        n = n.isNull() ? *i : n;
-        if(!n.getType().isSubtypeOf(*t)) {
-          Assert(n.getType().isBitVector(1u) ||
-                 (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-          Assert(n.isConst());
-          Assert((*t).isBoolean());
-          if(n.getType().isBitVector(1u)) {
-            b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
-          } else {
-            // we assume (by construction) false is first; see boolean_terms.cpp
-            b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
-          }
-        } else {
-          b << n;
-        }
-      }
-      Assert(t == expectType.end());
-      d_nodes[current] = b;
-      Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-      // The assert below is too strong---we might be returning a model value but
-      // expect a type that still uses datatypes for tuples/records.  If it's
-      // really not the right type we should catch it in SmtEngine anyway.
-      // Assert(d_nodes[current].getType() == expectType);
-      return;
-    }else{
-      rewriteChildren = true;
-    }
-  } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
-    if(current.getKind() == kind::APPLY_CONSTRUCTOR){
-      //Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
-      TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
-      const Record& expectRec = expectType.getConst<Record>();
-      NodeBuilder<> b(kind::RECORD);
-      b << current.getType().getAttribute(expr::DatatypeRecordAttr());
-      const Record::FieldVector& fields = expectRec.getFields();
-      Record::FieldVector::const_iterator t = fields.begin();
-      for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
-        Assert(alreadyVisited(*i, TNode::null()));
-        Assert(t != fields.end());
-        TNode n = d_nodes[*i];
-        n = n.isNull() ? *i : n;
-        if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
-          Assert(n.getType().isBitVector(1u) ||
-                 (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-          Assert(n.isConst());
-          Assert((*t).second.isBoolean());
-          if(n.getType().isBitVector(1u)) {
-            b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
-          } else {
-            // we assume (by construction) false is first; see boolean_terms.cpp
-            b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
-          }
-        } else {
-          b << n;
-        }
-      }
-      Assert(t == fields.end());
-      d_nodes[current] = b;
-      Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-      Assert(d_nodes[current].getType() == expectType);
-      return;
-    }else{
-      rewriteChildren = true;
-    }
-  } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
+  if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
             ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
               ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
                 current.getOperator()[0].hasAttribute(BooleanTermAttr()) ) )) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index deb9770c0..007c5e049 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2587,6 +2587,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   TimerStat::CodeTimer nonclausalTimer(d_smt.d_stats->d_nonclausalSimplificationTime);
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl;
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Trace("simplify") << "Assertion #" << i << " : " << d_assertions[i] << std::endl;
+  }
 
   if(d_propagatorNeedsFinish) {
     d_propagator.finish();
@@ -2622,6 +2625,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     return false;
   }
 
+
+  Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
   SubstitutionMap constantPropagations(d_smt.d_context);
   SubstitutionMap newSubstitutions(d_smt.d_context);
@@ -2632,10 +2637,12 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     Node learnedLiteral = d_nonClausalLearnedLiterals[i];
     Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral);
     Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
+    Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
     Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
     if (learnedLiteral != learnedLiteralNew) {
       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
     }
+    Trace("simplify") << "Process learnedLiteral, after newSubs : " << learnedLiteral << std::endl;
     for (;;) {
       learnedLiteralNew = constantPropagations.apply(learnedLiteral);
       if (learnedLiteralNew == learnedLiteral) {
@@ -2644,6 +2651,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
       ++d_smt.d_stats->d_numConstantProps;
       learnedLiteral = Rewriter::rewrite(learnedLiteralNew);
     }
+    Trace("simplify") << "Process learnedLiteral, after constProp : " << learnedLiteral << std::endl;
     // It might just simplify to a constant
     if (learnedLiteral.isConst()) {
       if (learnedLiteral.getConst<bool>()) {
@@ -2763,6 +2771,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 #endif /* CVC4_ASSERTIONS */
   }
   // Resize the learnt
+  Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
   d_nonClausalLearnedLiterals.resize(j);
 
   hash_set<TNode, TNodeHashFunction> s;