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

1 files changed, 10 insertions, 3 deletions

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;
     }