Allow sygus with no syntactic restrictions for LIA. Add regressions.

3 files changed, 122 insertions, 8 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 57ef44df0..dc00ead8c 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -496,7 +496,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
   std::vector< std::vector<Expr> > ops;
   std::vector< std::vector< std::string > > cnames;
   std::vector< std::vector< std::vector< CVC4::Type > > > cargs;
-  bool allow_const;
+  bool allow_const = false;
+  bool read_syntax = false;
 }
   : /* set the logic */
     SET_LOGIC_TOK symbol[name,CHECK_NONE,SYM_SORT]
@@ -598,7 +599,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
       terms.push_back(bvl);
     }
     sortSymbol[range,CHECK_DECLARED]
-    LPAREN_TOK
+    ( LPAREN_TOK
     ( LPAREN_TOK
       symbol[name,CHECK_NONE,SYM_VARIABLE] { PARSER_STATE->pushScope(true); }
       sortSymbol[t,CHECK_DECLARED]
@@ -614,18 +615,23 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
           // if not unresolved, must be undeclared
           PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
         }
-        allow_const = false;
       }
       // Note the official spec for NTDef is missing the ( parens )
       // but they are necessary to parse SyGuS examples
       LPAREN_TOK sygusGTerm[fun, ops.back(), cnames.back(), cargs.back(), sygus_vars, allow_const]+ RPAREN_TOK
       RPAREN_TOK
-      { datatypes.back().setSygus( t, terms[0], allow_const );
+      { datatypes.back().setSygus( t, terms[0], allow_const, false );
         PARSER_STATE->mkSygusDatatype( datatypes.back(), ops.back(), cnames.back(), cargs.back() );
         PARSER_STATE->popScope(); }
     )+
-    RPAREN_TOK
-    { PARSER_STATE->popScope();
+    RPAREN_TOK { read_syntax = true; }
+    )?
+    { 
+      if( !read_syntax ){
+        //create the default grammar
+        PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars );
+      }
+      PARSER_STATE->popScope();
       seq = new CommandSequence();
       std::vector<DatatypeType> datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes);
       seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes));
@@ -794,7 +800,6 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri
           cargs.pop_back();
           Debug("parser-sygus") << "Make constructors for Constant/Variable of type " << t << std::endl;
           if( gtermType==1 ){
-            //PARSER_STATE->parseError(std::string("Constant/Variable in sygus not supported."));
             std::vector< Expr > consts;
             PARSER_STATE->mkSygusConstantsForType( t, consts );
             for( unsigned i=0; i<consts.size(); i++ ){
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 10e742d45..e837980bd 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -496,7 +496,113 @@ void Smt2::includeFile(const std::string& filename) {
   }
 }
 
-
+void Smt2::mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
+                                  std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars ) {
+  
+  Debug("parser-sygus") << "Construct default grammar for " << fun << " " << range << std::endl;
+  
+  std::stringstream ssb;
+  ssb << fun << "_Bool";
+  std::string dbname = ssb.str();
+  
+  std::stringstream ss;
+  ss << fun << "_" << range;
+  std::string dname = ss.str();
+  datatypes.push_back(Datatype(dname));
+  ops.push_back(std::vector<Expr>());
+  std::vector<std::string> cnames;
+  std::vector<std::vector<CVC4::Type> > cargs;
+  //variables
+  for( unsigned i=0; i<sygus_vars.size(); i++ ){
+    if( sygus_vars[i].getType()==range ){
+      std::stringstream ss;
+      ss << sygus_vars[i];
+      Debug("parser-sygus") << "...add for variable " << ss.str() << std::endl;
+      ops.back().push_back( sygus_vars[i] );
+      cnames.push_back( ss.str() );
+      cargs.push_back( std::vector< CVC4::Type >() );
+    }
+  }
+  //constants
+  std::vector< Expr > consts;
+  mkSygusConstantsForType( range, consts );
+  for( unsigned i=0; i<consts.size(); i++ ){
+    std::stringstream ss;
+    ss << consts[i];
+    Debug("parser-sygus") << "...add for constant " << ss.str() << std::endl;
+    ops.back().push_back( consts[i] );
+    cnames.push_back( ss.str() );
+    cargs.push_back( std::vector< CVC4::Type >() );
+  }
+  //ITE
+  CVC4::Kind k = kind::ITE;
+  Debug("parser-sygus") << "...add for " << k << std::endl;
+  ops.back().push_back(getExprManager()->operatorOf(k));
+  cnames.push_back( kind::kindToString(k) );
+  cargs.push_back( std::vector< CVC4::Type >() );
+  cargs.back().push_back(mkUnresolvedType(ssb.str()));
+  cargs.back().push_back(mkUnresolvedType(ss.str()));
+  cargs.back().push_back(mkUnresolvedType(ss.str()));
+    
+  if( range.isInteger() ){
+    for( unsigned i=0; i<2; i++ ){
+      CVC4::Kind k = i==0 ? kind::PLUS : kind::MINUS;
+      Debug("parser-sygus") << "...add for " << k << std::endl;
+      ops.back().push_back(getExprManager()->operatorOf(k));
+      cnames.push_back(kind::kindToString(k));
+      cargs.push_back( std::vector< CVC4::Type >() );
+      cargs.back().push_back(mkUnresolvedType(ss.str()));
+      cargs.back().push_back(mkUnresolvedType(ss.str()));
+    }
+  }else{
+    std::stringstream sserr;
+    sserr << "Don't know default Sygus grammar for type " << range << std::endl;
+    parseError(sserr.str());
+  }
+  Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
+  datatypes.back().setSygus( range, bvl, true, true );
+  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs );
+  sorts.push_back( range );
+  
+  //Boolean type
+  datatypes.push_back(Datatype(dbname));
+  ops.push_back(std::vector<Expr>());
+  cnames.clear();
+  cargs.clear();
+  for( unsigned i=0; i<4; i++ ){
+    CVC4::Kind k = i==0 ? kind::NOT : ( i==1 ? kind::AND : ( i==2 ? kind::OR : kind::EQUAL ) );
+    Debug("parser-sygus") << "...add for " << k << std::endl;
+    ops.back().push_back(getExprManager()->operatorOf(k));
+    cnames.push_back(kind::kindToString(k));
+    cargs.push_back( std::vector< CVC4::Type >() );
+    if( k==kind::NOT ){
+      cargs.back().push_back(mkUnresolvedType(ssb.str()));
+    }else if( k==kind::AND || k==kind::OR ){
+      cargs.back().push_back(mkUnresolvedType(ssb.str()));
+      cargs.back().push_back(mkUnresolvedType(ssb.str()));
+    }else if( k==kind::EQUAL ){
+      cargs.back().push_back(mkUnresolvedType(ss.str()));
+      cargs.back().push_back(mkUnresolvedType(ss.str()));
+    }
+  }
+  if( range.isInteger() ){
+    CVC4::Kind k = kind::LEQ;
+    Debug("parser-sygus") << "...add for " << k << std::endl;
+    ops.back().push_back(getExprManager()->operatorOf(k));
+    cnames.push_back(kind::kindToString(k));
+    cargs.push_back( std::vector< CVC4::Type >() );
+    cargs.back().push_back(mkUnresolvedType(ss.str()));
+    cargs.back().push_back(mkUnresolvedType(ss.str()));
+  }
+  Debug("parser-sygus") << "...make datatype " << datatypes.back() << std::endl;
+  Type btype = getExprManager()->booleanType();
+  datatypes.back().setSygus( btype, bvl, true, true );
+  mkSygusDatatype( datatypes.back(), ops.back(), cnames, cargs );
+  sorts.push_back( btype );
+  
+  Debug("parser-sygus") << "...finished make default grammar for " << fun << " " << range << std::endl;
+}
+  
 void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops ) {
   if( type.isInteger() ){
     ops.push_back(getExprManager()->mkConst(Rational(0)));
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 67c019d50..eaf9e7b47 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -178,6 +178,9 @@ public:
     return e;
   }
 
+  void mkSygusDefaultGrammar( const Type& range, Expr& bvl, const std::string& fun, std::vector<CVC4::Datatype>& datatypes,
+                              std::vector<Type>& sorts, std::vector< std::vector<Expr> >& ops, std::vector<Expr> sygus_vars );
+  
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
   
   void addSygusFun(const std::string& fun, Expr eval) {