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

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 9178e928962345d17fe14bba5979280cfa936ee0..653eaca8f937bd9b56d3cfba48323eb228b11bcd 100644 (file)
--- 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 11ddf2a155e6426062e4d96e410ffee26aae5e1f..0edd8bc4605d050cd0163f5135432daf9bdd25bd 100644 (file)
--- 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 8ed8e40a181533a8b0bd8c6a845526d33b5780c1..3420a3e7f39c63b7903a60cfd64ebbe21726b19c 100644 (file)
--- 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 a8e2534dcdc3948432d4daaa7d94aeff5fd23bf0..242638f8251bee9b99f5442ec2b388f691d669bd 100644 (file)
--- 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 7648a158702d2d1eb61e6125f4867506ddb5802a..79cb18d92c472574a251473e8be05b32cfaf940d 100644 (file)
--- 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 4455a053c81dc2c771e6b4dcb37e340ba761c99a..ba6276aa23c002136dc3a90045e734a2037b392c 100644 (file)
--- 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 646a1565e3a4f7757e4ca8d8bc344beb726298af..2507209f48d43c3eb9a9ce9ee96404734bbc5ede 100644 (file)
--- 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 4b213422cb021c7d296b7cb99524b058bf2d3e32..193db09e871cc5ab6a97a05a229a06b0b1ff84bd 100644 (file)
--- 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 c865c2615c52bbcabb51bf3808652165fe1b3ac4..05574880f05df0b2b6dbe4c4286f96402eb23421 100644 (file)
--- 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 3ffc518ace36a7c31630ea15bdb0c350a54f1538..ac20db33a8f5442c1bd57aa9ed5de15823a6531a 100644 (file)
--- 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"