diff options
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 | ||||
| -rw-r--r-- | src/util/datatype.cpp | 12 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/datatype-dump.cvc | 20 |
4 files changed, 30 insertions, 9 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)); } diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index de4f47bed..2ec558f20 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -44,7 +44,8 @@ TESTS = \ FAILING_TESTS = \ rec2.cvc \ - rec5.cvc + rec5.cvc \ + datatype-dump.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc new file mode 100644 index 000000000..44103eb1c --- /dev/null +++ b/test/regress/regress0/datatypes/datatype-dump.cvc @@ -0,0 +1,20 @@ +% This regression is the same as datatype.cvc but tests the +% dumping infrastructure. +% +% COMMAND-LINE: --dump assertions +% +% EXPECT: DATATYPE +% EXPECT: nat = succ(pred: nat) | zero +% EXPECT: END; +% EXPECT: x : nat; +% EXPECT: ASSERT NOT(NOT(is_succ(x)) AND NOT(is_zero(x))); +% EXPECT: CHECKSAT; +% EXPECT: invalid +% +% EXIT: 10 + +DATATYPE nat = succ(pred : nat) | zero END; + +x : nat; + +QUERY (NOT is_succ(x) AND NOT is_zero(x)); |