Expand definitions in theory datatypes, now has the expected semantics for incorrectl...

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 64b321613a43e90ad2188830987c3666f581166e..e9e6ba857f965b2e38dc6dca4651216201c80207 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -158,6 +158,7 @@ void Smt2::addTheory(Theory theory) {
     Parser::addOperator(kind::APPLY_CONSTRUCTOR);
     Parser::addOperator(kind::APPLY_TESTER);
     Parser::addOperator(kind::APPLY_SELECTOR);
+    Parser::addOperator(kind::APPLY_SELECTOR_TOTAL);
     break;
 
   case THEORY_STRINGS:

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 4d784c383c07d3860146415c669d43eea8a88a13..63529c2a54e17f02fe9886e2fa24f4c17eec1a5d 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -316,6 +316,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
     case kind::APPLY_CONSTRUCTOR:
     case kind::APPLY_SELECTOR:
+    case kind::APPLY_SELECTOR_TOTAL:
     case kind::APPLY_TESTER:
       toStream(op, n.getOperator(), depth, types, false);
       break;

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index ea335f2e5cd201994432242b9ecc93fe052ee90b..1250bc6591727ddb9a25e31d36a5013739e0d1a2 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -424,6 +424,7 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
   case kind::APPLY_TESTER:
   case kind::APPLY_CONSTRUCTOR:
   case kind::APPLY_SELECTOR:
+  case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE:
     break;
 

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 111324dfa79738d7c16316f820b6b710abee0a7d..e46a76ed7671dcd8499b36dcd23d9a923d874fed 100644 (file)
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -152,7 +152,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
       appctorb << (*dt2)[i].getConstructor();
       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
-        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
       }
       Node appctor = appctorb;
       if(i == 0) {
@@ -191,7 +191,7 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
       for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
         TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
         asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
-        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType);
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), asType);
       }
       Node appctor = appctorb;
       if(i == 0) {

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 37a656555ce6428bcbce9db2dd5881b3f5520a2c..8cb3fb4a2b7c29f68ec82880d39e60b167dc8681 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -88,7 +88,7 @@ public:
       const Record& rec = in[0].getType().getAttribute(expr::DatatypeRecordAttr()).getConst<Record>();
       return RewriteResponse(REWRITE_DONE, in[0][rec.getIndex(in.getOperator().getConst<RecordSelect>().getField())]);
     }
-    if(in.getKind() == kind::APPLY_SELECTOR &&
+    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
        (in[0].getKind() == kind::TUPLE || in[0].getKind() == kind::RECORD)) {
       // These strange (half-tuple-converted) terms can be created by
       // the system if you have something like "foo.1" for a tuple
@@ -118,7 +118,7 @@ public:
       Debug("tuprec") << "==> returning " << in[0][selectorIndex] << std::endl;
       return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
     }
-    if(in.getKind() == kind::APPLY_SELECTOR &&
+    if(in.getKind() == kind::APPLY_SELECTOR_TOTAL &&
        in[0].getKind() == kind::APPLY_CONSTRUCTOR) {
       // Have to be careful not to rewrite well-typed expressions
       // where the selector doesn't match the constructor,

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index bb6fd43732a7e750136352748fac1af62a6444ae..b222738ae0263750429fb8ccec41291fa8687e2e 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -39,6 +39,7 @@ cardinality TESTER_TYPE \
 parameterized APPLY_CONSTRUCTOR APPLY_TYPE_ASCRIPTION 0: "constructor application"
 
 parameterized APPLY_SELECTOR SELECTOR_TYPE 1: "selector application"
+parameterized APPLY_SELECTOR_TOTAL [SELECTOR_TYPE] 1: "selector application (total)"
 
 parameterized APPLY_TESTER TESTER_TYPE 1: "tester application"
 
@@ -82,6 +83,7 @@ constant ASCRIPTION_TYPE \
 
 typerule APPLY_CONSTRUCTOR ::CVC4::theory::datatypes::DatatypeConstructorTypeRule
 typerule APPLY_SELECTOR ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
+typerule APPLY_SELECTOR_TOTAL ::CVC4::theory::datatypes::DatatypeSelectorTypeRule
 typerule APPLY_TESTER ::CVC4::theory::datatypes::DatatypeTesterTypeRule
 typerule APPLY_TYPE_ASCRIPTION ::CVC4::theory::datatypes::DatatypeAscriptionTypeRule
 

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index b00b4148d229ff404f0f606f64bb09d68e240e06..0b0f5807c8698fd1fa0756e4bf19933b003e062c 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -54,7 +54,7 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out,
 
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
 }
 
@@ -318,6 +318,47 @@ void TheoryDatatypes::preRegisterTerm(TNode n) {
   flushPendingFacts();
 }
 
+Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
+  switch( n.getKind() ){
+  case kind::APPLY_SELECTOR: {
+      Node selector = n.getOperator();
+      Expr selectorExpr = selector.toExpr();
+      size_t selectorIndex = Datatype::cindexOf(selectorExpr);
+      const Datatype& dt = Datatype::datatypeOf(selectorExpr);
+      const DatatypeConstructor& c = dt[selectorIndex];
+      Expr tester = c.getTester();
+      Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
+      tst = Rewriter::rewrite( tst );
+      Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
+      Node n_ret;
+      if( tst==NodeManager::currentNM()->mkConst( true ) ){
+        n_ret = sel;
+      }else{
+        if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
+          std::stringstream ss;
+          ss << selector << "_uf";
+          d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
+                                            NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) );
+        }
+        Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
+        if( tst==NodeManager::currentNM()->mkConst( false ) ){
+          n_ret = sk;
+        }else{
+          n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk );
+        }
+      }
+      //n_ret = Rewriter::rewrite( n_ret );
+      Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl;
+      return n_ret;
+    }
+    break;
+  default:
+    return n;
+    break;
+  }
+  Unreachable();
+}
+
 void TheoryDatatypes::presolve() {
   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 }
@@ -332,7 +373,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     }
     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
   } else if(in.getKind() == kind::RECORD_SELECT) {
     TypeNode t = in[0].getType();
     if(t.hasAttribute(expr::DatatypeRecordAttr())) {
@@ -340,7 +381,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
     }
     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
-    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
+    return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
   }
 
   TypeNode t = in.getType();
@@ -404,7 +445,7 @@ Node TheoryDatatypes::ppRewrite(TNode in) {
         b << in[1];
         Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
       } else {
-        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]);
+        b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]);
         Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
       }
     }
@@ -848,7 +889,7 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 }
 
 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
-  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c );
+  Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
   Node rr = Rewriter::rewrite( r );
   //if( r!=rr ){
     //Node eq_exp = NodeManager::currentNM()->mkConst(true);
@@ -1075,7 +1116,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
         //eqc->d_selectors = true;
       }
       */
-    }else if( n.getKind() == APPLY_SELECTOR ){
+    }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){
       //we must also record which selectors exist
       Debug("datatypes") << "  Found selector " << n << endl;
       if (n.getType().isBoolean()) {
@@ -1117,7 +1158,7 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index,
     std::vector< Node > children;
     children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
     for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
-      Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n );
+      Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR_TOTAL, Node::fromExpr( dt[index][i].getSelector() ), n );
       if( mkVar ){
         TypeNode tn = nc.getType();
         if( dt.isParametric() ){

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 3a29433f8f5d42786e65de81cb4bda6b90b4166e..2a93878d0b0edccff1770fe6c4a83fcf60c39088 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -166,6 +166,8 @@ private:
   std::vector< Node > d_pending;
   std::map< Node, Node > d_pending_exp;
   std::vector< Node > d_pending_merge;
+  /** expand definition skolem functions */
+  std::map< Node, Node > d_exp_def_skolem;
 private:
   /** assert fact */
   void assertFact( Node fact, Node exp );
@@ -208,6 +210,7 @@ public:
 
   void check(Effort e);
   void preRegisterTerm(TNode n);
+  Node expandDefinition(LogicRequest &logicRequest, Node n);
   Node ppRewrite(TNode n);
   void presolve();
   void addSharedTerm(TNode t);

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 527d110e0e9109417e787946b5944860387f399f..d08b511dd431b7f44e28e19c79d1edb665e804d3 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -98,7 +98,7 @@ struct DatatypeConstructorTypeRule {
 struct DatatypeSelectorTypeRule {
   inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
     throw(TypeCheckingExceptionPrivate) {
-    Assert(n.getKind() == kind::APPLY_SELECTOR);
+    Assert(n.getKind() == kind::APPLY_SELECTOR || n.getKind() == kind::APPLY_SELECTOR_TOTAL );
     TypeNode selType = n.getOperator().getType(check);
     Type t = selType[0].toType();
     Assert( t.isDatatype() );

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index 164e9e6432f5f2039aeff078d0121835309f3afe..b7e624a66c4eb8bc61973bf806db62488aa89d69 100644 (file)
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -92,8 +92,8 @@ instgen \n\
 + Use instantiation algorithm that mimics Inst-Gen calculus. \n\
 \n\
 gen-ev \n\
-+ Default, use model-based quantifier instantiation algorithm from CADE 24 finite\n\
-  model finding paper.\n\
++ Use model-based quantifier instantiation algorithm from CADE 24 finite\n\
+  model finding paper based on generalizing evaluations.\n\
 \n\
 fmc-interval \n\
 + Same as default, but with intervals for models of integer functions.\n\
@@ -131,9 +131,6 @@ conflict \n\
 partial \n\
 + Apply QCF algorithm to instantiate heuristically as well. \n\
 \n\
-partial \n\
-+ Apply QCF to instantiate heuristically as well. \n\
-\n\
 mc \n\
 + Apply QCF algorithm in a complete way, so that a model is ensured when it fails. \n\
 \n\
@@ -217,21 +214,21 @@ inline AxiomInstMode stringToAxiomInstMode(std::string option, std::string optar
 }
 
 inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
-  if(optarg ==  "gen-ev") {
+  if(optarg == "gen-ev") {
     return MBQI_GEN_EVAL;
-  } else if(optarg ==  "none") {
+  } else if(optarg == "none") {
     return MBQI_NONE;
-  } else if(optarg ==  "instgen") {
+  } else if(optarg == "instgen") {
     return MBQI_INST_GEN;
-  } else if(optarg ==  "default" || optarg ==  "fmc") {
+  } else if(optarg == "default" || optarg ==  "fmc") {
     return MBQI_FMC;
-  } else if(optarg ==  "fmc-interval") {
+  } else if(optarg == "fmc-interval") {
     return MBQI_FMC_INTERVAL;
-  } else if(optarg ==  "interval") {
+  } else if(optarg == "interval") {
     return MBQI_INTERVAL;
-  } else if(optarg ==  "trust") {
+  } else if(optarg == "trust") {
     return MBQI_TRUST;
-  } else if(optarg ==  "help") {
+  } else if(optarg == "help") {
     puts(mbqiModeHelp.c_str());
     exit(1);
   } else {

diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index c0b318f23dc2be5b07dbd0281248eb3df68c95ac..e27d438be98e8b27966b9f43334c59469fbfceea 100755 (executable)
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1488,7 +1488,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 \r
 bool MatchGen::isHandledUfTerm( TNode n ) {\r
   return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||\r
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;// || n.getKind()==GEQ;\r
+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;\r
 }\r
 \r
 Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {\r

diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 6912c9e89072d546b8b53ba4948eb967a24eccbd..3de12b9c97e89e5324dce0cf5c04f89054bc989f 100644 (file)
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -324,7 +324,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 
 bool Trigger::isAtomicTrigger( Node n ){
   return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE ||
-         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;
+         n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
 }
 bool Trigger::isSimpleTrigger( Node n ){
   if( isAtomicTrigger( n ) ){

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 405fceb6f1d77a454add470e0ae8f74f9a40279c..f207bdb8eb923c511b17a3f6c396d12a88a2435b 100644 (file)
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -41,7 +41,7 @@ TheoryModel::TheoryModel( context::Context* c, std::string name, bool enableFunc
   d_equalityEngine->addFunctionKind(kind::SELECT);
   // d_equalityEngine->addFunctionKind(kind::STORE);
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_eeContext->push();
 }
@@ -422,7 +422,7 @@ TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( t
 
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
-  return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR);
+  return (n.isVar() || n.getKind() == kind::APPLY_UF || n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL);
 }
 
 

diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 84adb4f8474a1d674f3d6f88f7e90556eb59f28e..e8a8f16f593e4723663d768944aaf420d60043e8 100644 (file)
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -31,7 +31,6 @@ TESTS =       \
        datatype0.cvc \
        datatype1.cvc \
        datatype2.cvc \
-       datatype3.cvc \
        datatype4.cvc \
        datatype13.cvc \
        empty_tuprec.cvc \
@@ -64,6 +63,8 @@ TESTS =       \
 FAILING_TESTS = \
        datatype-dump.cvc
 
+# takes a long time to build model on debug : datatype3.cvc
+
 EXTRA_DIST = $(TESTS)
 
 if CVC4_BUILD_PROFILE_COMPETITION

diff --git a/test/regress/regress0/datatypes/datatype1.cvc b/test/regress/regress0/datatypes/datatype1.cvc
index 5172eeb484cc10f75b18aafa89eb7c37ed2f4e73..3934959f14077a057f87bfb5fd846557bc45ea9e 100644 (file)
--- a/test/regress/regress0/datatypes/datatype1.cvc
+++ b/test/regress/regress0/datatypes/datatype1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: invalid
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf

diff --git a/test/regress/regress0/datatypes/datatype3.cvc b/test/regress/regress0/datatypes/datatype3.cvc
index 5f130b6ae3dc0b6507494505ff8d0f8002e39c28..fff1a5dd766534dd5bbb43202b6ec6dc1b722948 100644 (file)
--- a/test/regress/regress0/datatypes/datatype3.cvc
+++ b/test/regress/regress0/datatypes/datatype3.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: invalid
 
 DATATYPE
   tree = node(left : tree, right : tree) | leaf

diff --git a/test/regress/regress0/datatypes/wrong-sel-simp.cvc b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
index 7455f809c1e60d9ceeb635d0e1f2e4d1f3c786d9..b0dbdc46e9bb46e28f8d2d9850384bda549c632d 100644 (file)
--- a/test/regress/regress0/datatypes/wrong-sel-simp.cvc
+++ b/test/regress/regress0/datatypes/wrong-sel-simp.cvc
@@ -1,4 +1,4 @@
-% EXPECT: valid
+% EXPECT: invalid
 DATATYPE
   nat = succ(pred : nat) | zero
 END;