Make sygus an output language. Parse declare-fun in sygus. Minor improvements to robustness of sygus parsing.

10 files changed, 67 insertions, 18 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9178e9289..653eaca8f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -203,7 +203,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
                 || (len >= 3 && !strcmp(".sl", filename + len - 3))) {
         opts.set(options::inputLanguage, language::input::LANG_SYGUS);
         //since there is no sygus output language, set this to SMT lib 2
-        opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0);
+        //opts.set(options::outputLanguage, language::output::LANG_SMTLIB_V2_0);
       }
     }
   }
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 11ddf2a15..0edd8bc46 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -546,9 +546,20 @@ sygusCommand returns [CVC4::Command* cmd = NULL]
     { PARSER_STATE->mkSygusVar(name, t);
       $cmd = new EmptyCommand(); }
   | /* declare-fun */
-    (DECLARE_FUN_TOK)=>
     DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
-    { PARSER_STATE->parseError("declare-fun not yet supported in SyGuS input"); }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    { PARSER_STATE->checkUserSymbol(name); }
+    LPAREN_TOK sortList[sorts] RPAREN_TOK
+    sortSymbol[t,CHECK_DECLARED]
+    { Debug("parser") << "declare fun: '" << name << "'" << std::endl;
+      if( sorts.size() > 0 ) {
+        if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
+          PARSER_STATE->parseError(std::string("Functions (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString());
+        }
+        t = EXPR_MANAGER->mkFunctionType(sorts, t);
+      }
+      Expr func = PARSER_STATE->mkVar(name, t);
+      $cmd = new DeclareFunctionCommand(name, func, t); }
   | /* function definition */
     DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
@@ -1729,6 +1740,10 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
       } else {
         /* A non-built-in function application */
         PARSER_STATE->checkDeclaration(name, CHECK_DECLARED, SYM_VARIABLE);
+        //hack to allow constants with parentheses (disabled for now)
+        //if( PARSER_STATE->sygus() && !PARSER_STATE->isFunctionLike(name) ){
+        //  op = PARSER_STATE->getVariable(name);
+        //}else{
         PARSER_STATE->checkFunctionLike(name);
         const bool isDefinedFunction =
           PARSER_STATE->isDefinedFunction(name);
@@ -1751,15 +1766,26 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
         args.push_back(expr);
       }
         }
+    //(termList[args,expr])? RPAREN_TOK
     termList[args,expr] RPAREN_TOK
-    { Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
+    { //if( PARSER_STATE->sygus() && !isBuiltinOperator && !PARSER_STATE->isFunctionLike(name) ){
+      //  if( !args.empty() ){
+      //    PARSER_STATE->parseError("Non-empty list of arguments for constant.");
+      //  }
+      //  expr = op; 
+      //}else{
+      //  if( args.empty() ){
+      //    PARSER_STATE->parseError("Empty list of arguments for non-constant.");
+      //  }
+      Debug("parser") << "args has size " << args.size() << std::endl << "expr is " << expr << std::endl;
       for(std::vector<Expr>::iterator i = args.begin(); i != args.end(); ++i) {
         Debug("parser") << "++ " << *i << std::endl;
       }
       if(isBuiltinOperator) {
         PARSER_STATE->checkOperator(kind, args.size());
       }
-      expr = MK_EXPR(kind, args); }
+      expr = MK_EXPR(kind, args); 
+    }
 
   | LPAREN_TOK
     ( /* An indexed function application */
@@ -1821,7 +1847,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
     /* a variable */
   | symbol[name,CHECK_DECLARED,SYM_VARIABLE]
-    { if( PARSER_STATE->sygus() && name[0]=='-' ){ //allow unary minus in sygus
+    { if( PARSER_STATE->sygus() && name[0]=='-' && 
+          name.find_first_not_of("0123456789", 1) == std::string::npos ){ //allow unary minus in sygus
         expr = MK_CONST(Rational(name));
       }else{
         const bool isDefinedFunction =
@@ -2358,7 +2385,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check]
   std::string name;
   std::vector<CVC4::Type> args;
   std::vector<uint64_t> numerals;
-  bool indexed;
+  bool indexed = false;
 }
   : sortName[name,CHECK_NONE]
     {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8ed8e40a1..3420a3e7f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -347,6 +347,9 @@ void Smt2::setLogic(std::string name) {
       ss << "Unknown SyGuS background logic `" << name << "'";
       parseError(ss.str());
     }
+    //TODO : add additional non-standard define-funs here
+    
+    
   }
 
   d_logicSet = true;
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index a8e2534dc..242638f82 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -55,6 +55,9 @@ Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   case LANG_Z3STR:
     return new printer::smt2::Smt2Printer(printer::smt2::z3str_variant);
 
+  case LANG_SYGUS:
+    return new printer::smt2::Smt2Printer(printer::smt2::sygus_variant);
+    
   case LANG_AST:
     return new printer::ast::AstPrinter();
 
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 7648a1587..79cb18d92 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -152,7 +152,11 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
       }
       break;
     case kind::BITVECTOR_TYPE:
-      out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
+      if(d_variant == sygus_variant ){
+        out << "(BitVec " << n.getConst<BitVectorSize>().size << ")";
+      }else{
+        out << "(_ BitVec " << n.getConst<BitVectorSize>().size << ")";
+      }
       break;
     case kind::FLOATINGPOINT_TYPE:
       out << "(_ FloatingPoint "
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 4455a053c..ba6276aa2 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -30,7 +30,8 @@ namespace smt2 {
 enum Variant {
   no_variant,
   smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
-  z3str_variant // old-style 2.0 and also z3str syntax
+  z3str_variant, // old-style 2.0 and also z3str syntax
+  sygus_variant  // variant for sygus
 };/* enum Variant */
 
 class Smt2Printer : public CVC4::Printer {
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 646a1565e..2507209f4 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -2153,7 +2153,7 @@ Node TermDbSygus::expandBuiltinTerm( Node t ){
 
 
 Kind TermDbSygus::getComparisonKind( TypeNode tn ) {
-  if( tn.isInteger() ){
+  if( tn.isInteger() || tn.isReal() ){
     return LT;
   }else if( tn.isBitVector() ){
     return BITVECTOR_ULT;
@@ -2163,7 +2163,7 @@ Kind TermDbSygus::getComparisonKind( TypeNode tn ) {
 }
 
 Kind TermDbSygus::getPlusKind( TypeNode tn, bool is_neg ) {
-  if( tn.isInteger() ){
+  if( tn.isInteger() || tn.isReal() ){
     return is_neg ? MINUS : PLUS;
   }else if( tn.isBitVector() ){
     return is_neg ? BITVECTOR_SUB : BITVECTOR_PLUS;
diff --git a/src/util/language.cpp b/src/util/language.cpp
index 4b213422c..193db09e8 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Francois Bobot
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -27,6 +27,7 @@ InputLanguage toInputLanguage(OutputLanguage language) {
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
+  case output::LANG_SYGUS:
     // these entries directly correspond (by design)
     return InputLanguage(int(language));
 
@@ -47,6 +48,7 @@ OutputLanguage toOutputLanguage(InputLanguage language) {
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
+  case input::LANG_SYGUS:
     // these entries directly correspond (by design)
     return OutputLanguage(int(language));
 
@@ -88,6 +90,8 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "z3str" || language == "z3-str" ||
             language == "LANG_Z3STR") {
     return output::LANG_Z3STR;
+  } else if(language == "sygus" || language == "LANG_SYGUS") {
+    return output::LANG_SYGUS;
   } else if(language == "ast" || language == "LANG_AST") {
     return output::LANG_AST;
   } else if(language == "auto" || language == "LANG_AUTO") {
@@ -113,13 +117,13 @@ InputLanguage toInputLanguage(std::string language) {
   } else if(language == "smtlib2.5" || language == "smt2.5" ||
             language == "LANG_SMTLIB_V2_5") {
     return input::LANG_SMTLIB_V2_5;
-  } else if(language == "sygus" || language == "LANG_SYGUS") {
-    return input::LANG_SYGUS;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
             language == "LANG_Z3STR") {
     return input::LANG_Z3STR;
+  } else if(language == "sygus" || language == "LANG_SYGUS") {
+    return input::LANG_SYGUS;
   } else if(language == "auto" || language == "LANG_AUTO") {
     return input::LANG_AUTO;
   }
diff --git a/src/util/language.h b/src/util/language.h
index c865c2615..05574880f 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Morgan Deters
  ** Major contributors: none
- ** Minor contributors (to current version): Francois Bobot
+ ** Minor contributors (to current version): Francois Bobot, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -57,11 +57,11 @@ enum CVC4_PUBLIC Language {
   LANG_CVC4,
   /** The Z3-str input language */
   LANG_Z3STR,
-
-  // START INPUT-ONLY LANGUAGES AT ENUM VALUE 10
-  // THESE ARE IN PRINCIPLE NOT POSSIBLE OUTPUT LANGUAGES
   /** The SyGuS input language */
   LANG_SYGUS,
+  
+  // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
+  // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
 
   /** LANG_MAX is > any valid InputLanguage id */
   LANG_MAX
@@ -131,6 +131,8 @@ enum CVC4_PUBLIC Language {
   LANG_CVC4 = input::LANG_CVC4,
   /** The Z3-str output language */
   LANG_Z3STR = input::LANG_Z3STR,
+  /** The sygus output language */
+  LANG_SYGUS = input::LANG_SYGUS,
 
   // START OUTPUT-ONLY LANGUAGES AT ENUM VALUE 10
   // THESE ARE IN PRINCIPLE NOT POSSIBLE INPUT LANGUAGES
@@ -165,6 +167,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_Z3STR:
     out << "LANG_Z3STR";
     break;
+  case LANG_SYGUS:
+    out << "LANG_SYGUS";
+    break;
   case LANG_AST:
     out << "LANG_AST";
     break;
diff --git a/src/util/language.i b/src/util/language.i
index 3ffc518ac..ac20db33a 100644
--- a/src/util/language.i
+++ b/src/util/language.i
@@ -27,6 +27,7 @@ namespace CVC4 {
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
 %rename(INPUT_LANG_Z3STR) CVC4::language::input::LANG_Z3STR;
+%rename(INPUT_LANG_SYGUS) CVC4::language::input::LANG_SYGUS;
 
 %rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
 %rename(OUTPUT_LANG_SMTLIB_V1) CVC4::language::output::LANG_SMTLIB_V1;
@@ -38,5 +39,6 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
 %rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX;
 %rename(OUTPUT_LANG_Z3STR) CVC4::language::output::LANG_Z3STR;
+%rename(OUTPUT_LANG_SYGUS) CVC4::language::output::LANG_SYGUS;
 
 %include "util/language.h"