diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-04 17:53:30 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-04 17:53:38 +0200 |
| commit | d3c365a60c88e33a7d73f81484db2cff5ef69bbb (patch) | |
| tree | 0b2779b9a69b6f855a01a4f22e3082e2f5faabd8 /src/expr | |
| parent | 711815d937db09aeb7e8fa568718768113ef7176 (diff) | |
Fix bugs 605 and 667.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/node_manager.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4eb5dd680..dad21e90a 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -448,6 +448,9 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds) TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { Assert(t.isTuple() || t.isRecord()); + //AJR: not sure why .getBaseType() was used in two cases below, + // disabling this, which is necessary to fix bug 605/667, + // which involves records of INT which were mapped to records of REAL below. TypeNode tOrig = t; if(t.isTuple()) { vector<TypeNode> v; @@ -458,7 +461,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { if(tn.isTuple() || tn.isRecord()) { base = getDatatypeForTupleRecord(tn); } else { - base = tn.getBaseType(); + base = tn;//.getBaseType(); } changed = changed || (tn != base); v.push_back(base); @@ -476,7 +479,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { if(tn.isTuple() || tn.isRecord()) { base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType(); } else { - base = tn.getBaseType(); + base = tn;//.getBaseType(); } changed = changed || (tn != base); v.push_back(std::make_pair((*i).first, base)); @@ -498,7 +501,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { dt.addConstructor(c); dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; - dtt.setAttribute(DatatypeTupleAttr(), t); + dtt.setAttribute(DatatypeTupleAttr(), tOrig); } else { const Record& rec = t.getRecord(); Datatype dt("__cvc4_record"); @@ -509,7 +512,7 @@ TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) { dt.addConstructor(c); dtt = TypeNode::fromType(toExprManager()->mkDatatypeType(dt)); Debug("tuprec") << "REWROTE " << t << " to " << dtt << std::endl; - dtt.setAttribute(DatatypeRecordAttr(), t); + dtt.setAttribute(DatatypeRecordAttr(), tOrig); } } else { Debug("tuprec") << "REUSING cached " << t << ": " << dtt << std::endl; |