Update experimental scripts. Support top-level non-terminals in sygus grammars. Allow -N in sygus terms. Minor bug fix in datatypes_sygus. Add regression.

2 files changed, 12 insertions, 4 deletions

diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index a9e6b3a78..d08c92dd9 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -1114,12 +1114,13 @@ bool SygusSymBreak::processCurrentProgram( Node a, TypeNode at, int depth, Node
 }
 
 bool SygusSymBreak::isSeparation( Node rep_prog, Node tst_curr, std::map< Node, std::vector< Node > >& testers_u, std::vector< Node >& rlv_testers ) {
-  Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << std::endl;
   TypeNode tn = tst_curr[0].getType();
+  Trace("sygus-nf-gen-debug") << "is separation " << rep_prog << " " << tst_curr << " " << tn << std::endl;
   Node rop = rep_prog.getNumChildren()==0 ? rep_prog : rep_prog.getOperator();
   //we can continue if the tester in question is relevant
   if( std::find( rlv_testers.begin(), rlv_testers.end(), tst_curr )!=rlv_testers.end() ){
     unsigned tindex = Datatype::indexOf( tst_curr.getOperator().toExpr() );
+    d_tds->registerSygusType( tn );
     Node op = d_tds->getArgOp( tn, tindex );
     if( op!=rop ){
       Trace("sygus-nf-gen-debug") << "mismatch, success." << std::endl;
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 79199d8b4..60573a7fc 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -2070,7 +2070,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
         }
       }else{
         //print as let term
-        out << "(let (";
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          out << "(let (";
+        }
         std::vector< Node > subs_lvs;
         std::vector< Node > new_lvs;
         for( unsigned i=0; i<dt[cIndex].getNumSygusLetArgs(); i++ ){
@@ -2089,7 +2091,9 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
             out << ")";
           }
         }
-        out << ") ";
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          out << ") ";
+        }
         //print the body
         Node let_body = Node::fromExpr( dt[cIndex].getSygusLetBody() );
         let_body = let_body.substitute( subs_lvs.begin(), subs_lvs.end(), new_lvs.begin(), new_lvs.end() );
@@ -2104,7 +2108,10 @@ void TermDbSygus::printSygusTerm( std::ostream& out, Node n, std::vector< Node >
           printSygusTerm( new_str, n[i], lvs );
           doReplace( body, old_str.str().c_str(), new_str.str().c_str() );
         }
-        out << body << ")";
+        out << body;
+        if( dt[cIndex].getNumSygusLetInputArgs()>0 ){
+          out << ")";
+        }
       }
       return;
     }