diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-12 16:32:32 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-12 16:32:32 +0200 |
commit | 61415ee2c5659893055f71d84a38eab8701dc47a (patch) | |
tree | ca7c2f9c5f0dc846dd91d6f96d569855eeee531e /src/parser | |
parent | ad0863ae8333c4dcd950153e0db8cd4565a250b3 (diff) |
Make sygus an output language. Parse declare-fun in sygus. Minor improvements to robustness of sygus parsing.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 39 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 3 |
2 files changed, 36 insertions, 6 deletions
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; |