summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-09-21 21:09:18 +0000
committerMorgan Deters <mdeters@gmail.com>2012-09-21 21:09:18 +0000
commitba7aea0d9310015546bab5e5743c7dfcb0d2092d (patch)
tree19ba631f0457b7946374c9a91a10121fe8839393 /src
parentb5e4b809d1913c9cfc5cf95c04e9fc34c1ca42f3 (diff)
Fixes for datatype dumping and printing. Add a new test case for dumping.
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src')
-rw-r--r--src/printer/cvc/cvc_printer.cpp4
-rw-r--r--src/util/datatype.cpp12
2 files changed, 8 insertions, 8 deletions
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b14f6a9c8..35a85e681 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -991,13 +991,13 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
}
firstSelector = false;
const DatatypeConstructorArg& selector = *k;
- out << selector.getName() << ": " << selector.getType();
+ out << selector.getName() << ": " << SelectorType(selector.getType()).getRangeType();
}
out << ')';
}
}
}
- out << endl << "END;" << endl;
+ out << endl << "END;";
}
static void toStream(std::ostream& out, const CommentCommand* c) throw() {
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 522bcd935..ec8c8e166 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -414,7 +414,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
(*i).d_name.resize((*i).d_name.find('\0'));
if(typeName == "") {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector").toExpr();
+ (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, selfTypeNode), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
} else {
map<string, DatatypeType>::const_iterator j = resolutions.find(typeName);
if(j == resolutions.end()) {
@@ -424,7 +424,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
<< "of constructor \"" << d_name << "\"";
throw DatatypeResolutionException(msg.str());
} else {
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector").toExpr();
+ (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType((*j).second)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
}
}
} else {
@@ -437,7 +437,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
if(!paramTypes.empty() ) {
range = doParametricSubstitution( range, paramTypes, paramReplacements );
}
- (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector").toExpr();
+ (*i).d_selector = nm->mkSkolem((*i).d_name, nm->mkSelectorType(selfTypeNode, TypeNode::fromType(range)), "is a selector", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
}
Node::fromExpr((*i).d_selector).setAttribute(DatatypeIndexAttr(), index++);
(*i).d_resolved = true;
@@ -450,8 +450,8 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
// fails above, we want Constuctor::isResolved() to remain "false".
// Further, mkConstructorType() iterates over the selectors, so
// should get the results of any resolutions we did above.
- d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester").toExpr();
- d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor").toExpr();
+ d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
+ d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
// associate constructor with all selectors
for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
(*i).d_constructor = d_constructor;
@@ -521,7 +521,7 @@ void DatatypeConstructor::addArg(std::string selectorName, Type selectorType) {
// we're using some internals, so we have to set up this library context
ExprManagerScope ems(selectorType);
- Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName + "_$$", TypeNode::fromType(selectorType), "is an unresolved selector type placeholder").toExpr();
+ Expr type = NodeManager::currentNM()->mkSkolem("unresolved_" + selectorName, TypeNode::fromType(selectorType), "is an unresolved selector type placeholder", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
Debug("datatypes") << type << endl;
d_args.push_back(DatatypeConstructorArg(selectorName, type));
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback