From 61415ee2c5659893055f71d84a38eab8701dc47a Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 12 Jun 2015 16:32:32 +0200 Subject: [PATCH] Make sygus an output language. Parse declare-fun in sygus. Minor improvements to robustness of sygus parsing. --- src/main/driver_unified.cpp | 2 +- src/parser/smt2/Smt2.g | 39 ++++++++++++++++++++---- src/parser/smt2/smt2.cpp | 3 ++ src/printer/printer.cpp | 3 ++ src/printer/smt2/smt2_printer.cpp | 6 +++- src/printer/smt2/smt2_printer.h | 3 +- src/theory/quantifiers/term_database.cpp | 4 +-- src/util/language.cpp | 10 ++++-- src/util/language.h | 13 +++++--- src/util/language.i | 2 ++ 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::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 args; std::vector 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().size << ")"; + if(d_variant == sygus_variant ){ + out << "(BitVec " << n.getConst().size << ")"; + }else{ + out << "(_ BitVec " << n.getConst().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" -- 2.30.2