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.)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index b14f6a9c81838f4789091a96eaa9dd1a6f27dbb7..35a85e681809f294c4e33a06e1e98c24636630e2 100644 (file)
--- 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 522bcd935e3e7cbcbbc8e56aea7327e33e80f178..ec8c8e1665dc51ff4f3aa6cc0ef8f9cff6333fa2 100644 (file)
--- 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 de4f47bed77ff4d30fd3d9c55a28d950fe08b083..2ec558f201672285bde745134deb0e8adbc17035 100644 (file)
--- 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 (file)
index 0000000..44103eb
--- /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));