updates to smt2 parser to support datatypes, minor updates to datatypes theory/rewriter to support datatypes with non-datatype subdata

3 files changed, 49 insertions, 28 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a093aa1ef..791e550b9 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -212,7 +212,7 @@ command returns [CVC4::Command* cmd = NULL]
         sorts.push_back(PARSER_STATE->mkSort(*i));
       }
     }
-    sortSymbol[t]
+    sortSymbol[t,CHECK_DECLARED]
     { PARSER_STATE->popScope();
       // Do NOT call mkSort, since that creates a new sort!
       // This name is not its own distinct sort, it's an alias.
@@ -222,7 +222,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* function declaration */
     DECLARE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortList[sorts] RPAREN_TOK
-    sortSymbol[t]
+    sortSymbol[t,CHECK_DECLARED]
     { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
       if( sorts.size() > 0 ) {
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
@@ -232,7 +232,7 @@ command returns [CVC4::Command* cmd = NULL]
   | /* function definition */
     DEFINE_FUN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
-    sortSymbol[t]
+    sortSymbol[t,CHECK_DECLARED]
     { /* add variables to parser state before parsing term */
       Debug("parser") << "define fun: '" << name << "'" << std::endl;
       if( sortedVarNames.size() > 0 ) {
@@ -462,7 +462,16 @@ term[CVC4::Expr& expr]
         kind = CVC4::kind::APPLY;
       } else {
         expr = PARSER_STATE->getVariable(name);
-        kind = CVC4::kind::APPLY_UF;
+        Type t = expr.getType();
+        if( t.isConstructor() ){
+          kind = CVC4::kind::APPLY_CONSTRUCTOR;
+        }else if( t.isSelector() ){
+          kind = CVC4::kind::APPLY_SELECTOR;
+        }else if( t.isTester() ){
+          kind = CVC4::kind::APPLY_TESTER;
+        }else{
+          kind = CVC4::kind::APPLY_UF;
+        }
       }
       args.push_back(expr);
     }
@@ -495,6 +504,11 @@ term[CVC4::Expr& expr]
                        PARSER_STATE->getFunction(name));
       } else {
         expr = PARSER_STATE->getVariable(name);
+        Type t = PARSER_STATE->getType(name);
+        if(t.isConstructor() && ConstructorType(t).getArity() == 0) {
+          // don't require parentheses, immediately turn it into an apply
+          expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr);
+        }
       }
     }
 
@@ -688,7 +702,7 @@ sortList[std::vector<CVC4::Type>& sorts]
 @declarations {
   Type t;
 }
-  : ( sortSymbol[t] { sorts.push_back(t); } )*
+  : ( sortSymbol[t,CHECK_DECLARED] { sorts.push_back(t); } )*
   ;
 
 /**
@@ -700,7 +714,7 @@ sortedVarList[std::vector<std::pair<std::string, CVC4::Type> >& sortedVars]
   std::string name;
   Type t;
 }
-  : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t] RPAREN_TOK
+  : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK
       { sortedVars.push_back(make_pair(name, t)); }
     )*
   ;
@@ -713,14 +727,20 @@ sortName[std::string& name, CVC4::parser::DeclarationCheck check]
   : symbol[name,check,SYM_SORT]
   ;
 
-sortSymbol[CVC4::Type& t]
+sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
 @declarations {
   std::string name;
   std::vector<CVC4::Type> args;
   std::vector<uint64_t> numerals;
 }
   : sortName[name,CHECK_NONE]
-  	{ t = PARSER_STATE->getSort(name); }
+  	{ 
+  	  if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ){ 
+  	    t = PARSER_STATE->getSort(name);                                          
+  	  }else{                                                                    
+  	    t = PARSER_STATE->mkUnresolvedType(name);                                 
+  	  }                                          
+  	}
   | LPAREN_TOK INDEX_TOK symbol[name,CHECK_NONE,SYM_SORT] nonemptyNumeralList[numerals] RPAREN_TOK
     {
       if( name == "BitVec" ) {
@@ -846,7 +866,7 @@ selector[CVC4::DatatypeConstructor& ctor]
   std::string id;
   Type t, t2;
 }
-  : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t]
+  : symbol[id,CHECK_UNDECLARED,SYM_SORT] sortSymbol[t,CHECK_NONE]
     { ctor.addArg(id, t);
       Debug("parser-idt") << "selector: " << id.c_str() << std::endl;
     }
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 23768545d..124e6870d 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -75,11 +75,11 @@ public:
                                    << std::endl;
         return RewriteResponse(REWRITE_DONE, in[0][selectorIndex]);
       } else {
-        TNode gt = in.getType().mkGroundTerm();
+        Node gt = in.getType().mkGroundTerm();
         TypeNode gtt = gt.getType();
-        Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
+        //Assert( gtt.isDatatype() || gtt.isParametricDatatype() );
         if( !gtt.isInstantiatedDatatype() ){
-          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+          gt = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
                                                 NodeManager::currentNM()->mkConst(AscriptionType(in.getType().toType())), gt);
         }
         Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 75980993b..174513c72 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -43,7 +43,7 @@ Node TheoryDatatypes::getConstructorForSelector( Node sel )
   size_t selIndex = Datatype::indexOf( sel.toExpr() );
   const Datatype& dt = ((DatatypeType)((sel.getType()[0]).toType())).getDatatype();
   for( unsigned i = 0; i<dt.getNumConstructors(); i++ ){
-    if( dt[i].getNumArgs()>selIndex && 
+    if( dt[i].getNumArgs()>selIndex &&
         Node::fromExpr( dt[i][selIndex].getSelector() )==sel ){
       return Node::fromExpr( dt[i].getConstructor() );
     }
@@ -87,7 +87,7 @@ void TheoryDatatypes::addSharedTerm(TNode t) {
 void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) {
   Debug("datatypes") << "TheoryDatatypes::notifyEq(): "
                      << lhs << " = " << rhs << endl;
-  
+
 }
 
 void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) {
@@ -99,7 +99,7 @@ void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) {
   Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl;
 }
 
-void TheoryDatatypes::preRegisterTerm(TNode n) {  
+void TheoryDatatypes::preRegisterTerm(TNode n) {
   Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
 }
 
@@ -216,13 +216,13 @@ void TheoryDatatypes::check(Effort e) {
       }
       //Debug("datatypes-conflict") << d_cc << std::endl;
       Node conflict = d_em.getConflict();
-      if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || 
+      if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ||
           Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){
         cout << "Conflict constructed : " << conflict << endl;
       }
-      //if( conflict.getKind()!=kind::AND ){
-      //  conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict);
-      //}
+      if( conflict.getKind()!=kind::AND ){
+        conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict);
+      }
       d_out->conflict(conflict);
       return;
     }
@@ -316,6 +316,7 @@ bool TheoryDatatypes::checkTester( Node assertion, Node& conflict, unsigned& r )
   //check if empty label (no possible constructors for term)
   for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
     Node leqn = (*i);
+    Debug("datatypes-debug") << "checking " << leqn << std::endl;
     if( leqn.getKind() == kind::NOT ) {
       if( leqn[0].getOperator() == tassertion.getOperator() ) {
         if( assertion.getKind() != NOT ) {
@@ -484,7 +485,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
         Debug("datatypes-gt") << "constructor is " << dtc << std::endl;
         Type tspec = dtc.getSpecializedConstructorType(te.getType().toType());
         Debug("datatypes-gt") << "tpec is " << tspec << std::endl;
-        selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, 
+        selectorVals[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
                                             NodeManager::currentNM()->mkConst(AscriptionType(tspec)), cons);
         val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
       }
@@ -532,7 +533,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
 bool TheoryDatatypes::collapseSelector( Node t ) {
   if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) {
     //collapse constructor
-    TypeNode retTyp = t.getType(); 
+    TypeNode retTyp = t.getType();
     TypeNode typ = t[0].getType();
     Node sel = t.getOperator();
     TypeNode selType = sel.getType();
@@ -683,13 +684,13 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
 
   //check for clash
   NodeBuilder<> explanation(kind::AND);
-  if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR 
+  if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR
       && a.getOperator()!=b.getOperator() ){
     Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b );
     d_em.addNode( ccEq, &d_cce );
     d_em.addNodeConflict( ccEq, Reason::idt_clash );
     Debug("datatypes") << "Clash " << a << " " << b << endl;
-    return; 
+    return;
   }
   Debug("datatypes-debug") << "Done clash" << endl;
 
@@ -854,8 +855,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
 }
 
 void TheoryDatatypes::addTermToLabels( Node t ) {
-  if( ( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) &&
-      t.getType().isDatatype() ) {
+  if( t.getType().isDatatype() ) {
+    Debug("datatypes-debug") << "Add term to labels " << t << std::endl;
     Node tmp = find( t );
     if( tmp == t ) {
       //add to labels
@@ -923,7 +924,7 @@ void TheoryDatatypes::collectTerms( Node n, bool recurse ) {
     addTermToLabels( n );
   }
 }
- 
+
 void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) {
   Debug("datatypes") << "appending " << eq << endl
               << "  to diseq list of " << of << endl;
@@ -961,8 +962,8 @@ void TheoryDatatypes::addEquality(TNode eq) {
 
     //record which nodes are waiting to be merged
     vector< pair< Node, Node > > mp;
-    mp.insert( mp.begin(), 
-               d_merge_pending[d_merge_pending.size()-1].begin(), 
+    mp.insert( mp.begin(),
+               d_merge_pending[d_merge_pending.size()-1].begin(),
                d_merge_pending[d_merge_pending.size()-1].end() );
     d_merge_pending.pop_back();