From a3050a31487c9115293f1ee9a097ce27dae31218 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sun, 13 Nov 2016 20:34:10 -0800 Subject: [PATCH] Adding garbage collection for the Smt2 Parser for Commands when exceptions are thrown. --- src/parser/smt2/Smt2.g | 900 ++++++++++++++++++++++++++--------------- src/parser/smt2/smt2.h | 9 +- 2 files changed, 574 insertions(+), 335 deletions(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index b2a0cfc0c..27c5a62bd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -84,6 +84,7 @@ using namespace CVC4::parser; // files. See the documentation in "parser/antlr_undefines.h" for more details. #include "parser/antlr_undefines.h" +#include "base/ptr_closer.h" #include "parser/parser.h" #include "parser/antlr_tracing.h" #include "smt/command.h" @@ -201,47 +202,59 @@ parseExpr returns [CVC4::parser::smt2::myExpr expr] * Parses a command * @return the parsed command, or NULL if we've reached the end of the input */ -parseCommand returns [CVC4::Command* cmd = NULL] +parseCommand returns [CVC4::Command* cmd_return = NULL] @declarations { + CVC4::PtrCloser cmd; std::string name; } - : LPAREN_TOK c = command RPAREN_TOK { $cmd = c; } +@after { + cmd_return = cmd.release(); +} + : LPAREN_TOK command[&cmd] RPAREN_TOK /* This extended command has to be in the outermost production so that * the RPAREN_TOK is properly eaten and we are in a good state to read * the included file's tokens. */ | LPAREN_TOK INCLUDE_TOK str[name,true] RPAREN_TOK { if(!PARSER_STATE->canIncludeFile()) { - PARSER_STATE->parseError("include-file feature was disabled for this run."); + PARSER_STATE->parseError("include-file feature was disabled for this " + "run."); } if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); + PARSER_STATE->parseError("Extended commands are not permitted while " + "operating in strict compliance mode."); } PARSER_STATE->includeFile(name); - // The command of the included file will be produced at the next parseCommand() call - cmd = new EmptyCommand("include::" + name); + // The command of the included file will be produced at the next + // parseCommand() call + cmd.reset(new EmptyCommand("include::" + name)); } - | EOF { $cmd = 0; } + | EOF ; /** - * Parses a SyGuS command - * @return the parsed SyGuS command, or NULL if we've reached the end of the input + * Parses a SyGuS command. + * @return the parsed SyGuS command, or NULL if we've reached the end of the + * input */ -parseSygus returns [CVC4::Command* cmd = NULL] +parseSygus returns [CVC4::Command* cmd_return = NULL] @declarations { + CVC4::PtrCloser cmd; std::string name; } - : LPAREN_TOK c=sygusCommand RPAREN_TOK { $cmd = c; } - | EOF { $cmd = 0; } +@after { + cmd_return = cmd.release(); +} + : LPAREN_TOK sygusCommand[&cmd] RPAREN_TOK + | EOF ; /** * Parse the internal portion of the command, ignoring the surrounding * parentheses. */ -command returns [CVC4::Command* cmd = NULL] +command [CVC4::PtrCloser* cmd] @declarations { std::string name; std::vector names; @@ -259,27 +272,32 @@ command returns [CVC4::Command* cmd = NULL] } PARSER_STATE->setLogic(name); if( PARSER_STATE->sygus() ){ - $cmd = new SetBenchmarkLogicCommand("ALL_SUPPORTED"); + cmd->reset(new SetBenchmarkLogicCommand("ALL_SUPPORTED")); }else{ - $cmd = new SetBenchmarkLogicCommand(name); - } } + cmd->reset(new SetBenchmarkLogicCommand(name)); + } + } | /* set-info */ SET_INFO_TOK metaInfoInternal[cmd] | /* get-info */ GET_INFO_TOK KEYWORD - { cmd = new GetInfoCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); } + { cmd->reset(new GetInfoCommand( + AntlrInput::tokenText($KEYWORD).c_str() + 1)); + } | /* set-option */ SET_OPTION_TOK setOptionInternal[cmd] | /* get-option */ GET_OPTION_TOK KEYWORD - { cmd = new GetOptionCommand(AntlrInput::tokenText($KEYWORD).c_str() + 1); } + { cmd->reset(new GetOptionCommand( + AntlrInput::tokenText($KEYWORD).c_str() + 1)); + } | /* sort declaration */ DECLARE_SORT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) { - PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString()); + PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in "); } } symbol[name,CHECK_UNDECLARED,SYM_SORT] @@ -290,10 +308,10 @@ command returns [CVC4::Command* cmd = NULL] unsigned arity = AntlrInput::tokenToUnsigned(n); if(arity == 0) { Type type = PARSER_STATE->mkSort(name); - $cmd = new DeclareTypeCommand(name, 0, type); + cmd->reset(new DeclareTypeCommand(name, 0, type)); } else { Type type = PARSER_STATE->mkSortConstructor(name, arity); - $cmd = new DeclareTypeCommand(name, arity, type); + cmd->reset(new DeclareTypeCommand(name, arity, type)); } } | /* sort definition */ @@ -314,7 +332,7 @@ command returns [CVC4::Command* cmd = NULL] // Do NOT call mkSort, since that creates a new sort! // This name is not its own distinct sort, it's an alias. PARSER_STATE->defineParameterizedType(name, sorts, t); - $cmd = new DefineTypeCommand(name, sorts, t); + cmd->reset(new DefineTypeCommand(name, sorts, t)); } | /* function declaration */ DECLARE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -325,12 +343,14 @@ command returns [CVC4::Command* cmd = NULL] { 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()); + PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot " + "be declared in logic "); } t = EXPR_MANAGER->mkFunctionType(sorts, t); } Expr func = PARSER_STATE->mkVar(name, t); - $cmd = new DeclareFunctionCommand(name, func, t); } + cmd->reset(new DeclareFunctionCommand(name, func, t)); + } | /* function definition */ DEFINE_FUN_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] @@ -363,128 +383,159 @@ command returns [CVC4::Command* cmd = NULL] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); - $cmd = new DefineFunctionCommand(name, func, terms, expr); + Expr func = PARSER_STATE->mkFunction(name, t, + ExprManager::VAR_FLAG_DEFINED); + cmd->reset(new DefineFunctionCommand(name, func, terms, expr)); } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( LPAREN_TOK termList[terms,expr] RPAREN_TOK - { $cmd = new GetValueCommand(terms); } + { cmd->reset(new GetValueCommand(terms)); } | ~LPAREN_TOK - { PARSER_STATE->parseError("The get-value command expects a list of terms. Perhaps you forgot a pair of parentheses?"); } ) + { PARSER_STATE->parseError("The get-value command expects a list of " + "terms. Perhaps you forgot a pair of " + "parentheses?"); + } + ) | /* get-assignment */ GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetAssignmentCommand(); } + { cmd->reset(new GetAssignmentCommand()); } | /* assertion */ ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - /* { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support assert command."); } } */ + /* { if( PARSER_STATE->sygus() ){ + * PARSER_STATE->parseError("Sygus does not support assert command."); + * } + * } */ { PARSER_STATE->clearLastNamedTerm(); } term[expr, expr2] { bool inUnsatCore = PARSER_STATE->lastNamedTerm().first == expr; - cmd = new AssertCommand(expr, inUnsatCore); + cmd->reset(new AssertCommand(expr, inUnsatCore)); if(inUnsatCore) { PARSER_STATE->registerUnsatCoreName(PARSER_STATE->lastNamedTerm()); } } | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support check-sat command."); } } + { if( PARSER_STATE->sygus() ){ + PARSER_STATE->parseError("Sygus does not support check-sat command."); + } + } ( term[expr, expr2] { if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Extended commands (such as check-sat with an argument) are not permitted while operating in strict compliance mode."); + PARSER_STATE->parseError( + "Extended commands (such as check-sat with an argument) are not " + "permitted while operating in strict compliance mode."); } } - | { expr = MK_CONST(bool(true)); } ) - { cmd = new CheckSatCommand(expr); } + | { expr = MK_CONST(bool(true)); } + ) + { cmd->reset(new CheckSatCommand(expr)); } | /* get-assertions */ GET_ASSERTIONS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetAssertionsCommand(); } + { cmd->reset(new GetAssertionsCommand()); } | /* get-proof */ GET_PROOF_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetProofCommand(); } + { cmd->reset(new GetProofCommand()); } | /* get-unsat-core */ GET_UNSAT_CORE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames()); } + { cmd->reset(new GetUnsatCoreCommand(PARSER_STATE->getUnsatCoreNames())); } | /* push */ PUSH_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support push command."); } } + { if( PARSER_STATE->sygus() ){ + PARSER_STATE->parseError("Sygus does not support push command."); + } + } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n == 0) { - cmd = new EmptyCommand(); + cmd->reset(new EmptyCommand()); } else if(n == 1) { PARSER_STATE->pushScope(); PARSER_STATE->pushUnsatCoreNameScope(); - cmd = new PushCommand(); + cmd->reset(new PushCommand()); } else { - CommandSequence* seq = new CommandSequence(); + CVC4::PtrCloser seq(new CommandSequence()); do { PARSER_STATE->pushScope(); PARSER_STATE->pushUnsatCoreNameScope(); - Command* c = new PushCommand(); - c->setMuted(n > 1); - seq->addCommand(c); - } while(--n > 0); - cmd = seq; + Command* push_cmd = new PushCommand(); + push_cmd->setMuted(n > 1); + seq->addCommand(push_cmd); + --n; + } while(n > 0); + cmd->reset(seq.release()); } } | { if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to PUSH. Maybe you want (push 1)?"); + PARSER_STATE->parseError( + "Strict compliance mode demands an integer to be provided to " + "PUSH. Maybe you want (push 1)?"); } else { PARSER_STATE->pushScope(); PARSER_STATE->pushUnsatCoreNameScope(); - cmd = new PushCommand(); + cmd->reset(new PushCommand()); } } ) | POP_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { if( PARSER_STATE->sygus() ){ PARSER_STATE->parseError("Sygus does not support pop command."); } } + { if( PARSER_STATE->sygus() ){ + PARSER_STATE->parseError("Sygus does not support pop command."); + } + } ( k=INTEGER_LITERAL { unsigned n = AntlrInput::tokenToUnsigned(k); if(n > PARSER_STATE->scopeLevel()) { - PARSER_STATE->parseError("Attempted to pop above the top stack frame."); + PARSER_STATE->parseError("Attempted to pop above the top stack " + "frame."); } if(n == 0) { - cmd = new EmptyCommand(); + cmd->reset(new EmptyCommand()); } else if(n == 1) { PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); - cmd = new PopCommand(); + cmd->reset(new PopCommand()); } else { - CommandSequence* seq = new CommandSequence(); + CVC4::PtrCloser seq(new CommandSequence()); do { PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); - Command* c = new PopCommand(); - c->setMuted(n > 1); - seq->addCommand(c); - } while(--n > 0); - cmd = seq; + Command* pop_command = new PopCommand(); + pop_command->setMuted(n > 1); + seq->addCommand(pop_command); + --n; + } while(n > 0); + cmd->reset(seq.release()); } } | { if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Strict compliance mode demands an integer to be provided to POP. Maybe you want (pop 1)?"); + PARSER_STATE->parseError( + "Strict compliance mode demands an integer to be provided to POP." + "Maybe you want (pop 1)?"); } else { PARSER_STATE->popUnsatCoreNameScope(); PARSER_STATE->popScope(); - cmd = new PopCommand(); + cmd->reset(new PopCommand()); } - } ) - + } + ) /* exit */ | EXIT_TOK - { cmd = new QuitCommand(); } + { cmd->reset(new QuitCommand()); } /* New SMT-LIB 2.5 command set */ | smt25Command[cmd] { if(PARSER_STATE->v2_0() && PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("SMT-LIB 2.5 commands are not permitted while operating in strict compliance mode and in SMT-LIB 2.0 mode."); + PARSER_STATE->parseError( + "SMT-LIB 2.5 commands are not permitted while operating in strict " + "compliance mode and in SMT-LIB 2.0 mode."); } } /* CVC4-extended SMT-LIB commands */ | extendedCommand[cmd] { if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("Extended commands are not permitted while operating in strict compliance mode."); + PARSER_STATE->parseError( + "Extended commands are not permitted while operating in strict " + "compliance mode."); } } @@ -492,14 +543,17 @@ command returns [CVC4::Command* cmd = NULL] | SIMPLE_SYMBOL { std::string id = AntlrInput::tokenText($SIMPLE_SYMBOL); if(id == "benchmark") { - PARSER_STATE->parseError("In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. Use --lang smt1 for SMT-LIBv1."); + PARSER_STATE->parseError( + "In SMT-LIBv2 mode, but got something that looks like SMT-LIBv1. " + "Use --lang smt1 for SMT-LIBv1."); } else { - PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id + "'."); + PARSER_STATE->parseError("expected SMT-LIBv2 command, got `" + id + + "'."); } } ; -sygusCommand returns [CVC4::Command* cmd = NULL] +sygusCommand [CVC4::PtrCloser* cmd] @declarations { std::string name, fun; std::vector names; @@ -510,7 +564,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::vector sygus_vars; std::vector > sortedVarNames; SExpr sexpr; - CommandSequence* seq; + CVC4::PtrCloser seq; std::vector< std::vector< CVC4::SygusGTerm > > sgts; std::vector< CVC4::Datatype > datatypes; std::vector< std::vector > ops; @@ -530,24 +584,26 @@ sygusCommand returns [CVC4::Command* cmd = NULL] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] { PARSER_STATE->mkSygusVar(name, t); - $cmd = new EmptyCommand(); } + cmd->reset(new EmptyCommand()); + } | /* declare-primed-var */ DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] { PARSER_STATE->mkSygusVar(name, t, true); - $cmd = new EmptyCommand(); } + cmd->reset(new EmptyCommand()); + } | /* synth-fun */ - ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) { PARSER_STATE->checkThatLogicIsSet(); } + ( SYNTH_FUN_TOK | SYNTH_INV_TOK { range = EXPR_MANAGER->booleanType(); } ) + { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - { seq = new CommandSequence(); + { seq.reset(new CommandSequence()); PARSER_STATE->pushScope(true); for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); terms.push_back( v ); @@ -577,11 +633,14 @@ sygusCommand returns [CVC4::Command* cmd = NULL] std::string dname = ss.str(); sgts.push_back( std::vector< CVC4::SygusGTerm >() ); sgts.back().push_back( CVC4::SygusGTerm() ); - PARSER_STATE->pushSygusDatatypeDef(t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym); + PARSER_STATE->pushSygusDatatypeDef( + t, dname, datatypes, sorts, ops, cnames, cargs, allow_const, + unresolved_gterm_sym); Type unres_t; if(!PARSER_STATE->isUnresolvedType(dname)) { // if not unresolved, must be undeclared - Debug("parser-sygus") << "Make unresolved type : " << dname << std::endl; + Debug("parser-sygus") << "Make unresolved type : " << dname + << std::endl; PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT); unres_t = PARSER_STATE->mkUnresolvedType(dname); }else{ @@ -589,13 +648,16 @@ sygusCommand returns [CVC4::Command* cmd = NULL] unres_t = PARSER_STATE->getSort(dname); } sygus_to_builtin[unres_t] = t; - Debug("parser-sygus") << "--- Read sygus grammar " << name << " under function " << fun << "..." << std::endl; - Debug("parser-sygus") << " type to resolve " << unres_t << std::endl; - Debug("parser-sygus") << " builtin type " << t << std::endl; + Debug("parser-sygus") << "--- Read sygus grammar " << name + << " under function " << fun << "..." + << std::endl + << " type to resolve " << unres_t << std::endl + << " builtin type " << t << std::endl; } // Note the official spec for NTDef is missing the ( parens ) // but they are necessary to parse SyGuS examples - LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun] { sgts.back().push_back( CVC4::SygusGTerm() ); } )+ + LPAREN_TOK ( sygusGTerm[ sgts.back().back(), fun] + { sgts.back().push_back( CVC4::SygusGTerm() ); } )+ RPAREN_TOK { sgts.back().pop_back(); } RPAREN_TOK )+ @@ -605,45 +667,64 @@ sygusCommand returns [CVC4::Command* cmd = NULL] if( !read_syntax ){ //create the default grammar Debug("parser-sygus") << "Make default grammar..." << std::endl; - PARSER_STATE->mkSygusDefaultGrammar( range, terms[0], fun, datatypes, sorts, ops, sygus_vars, startIndex ); + PARSER_STATE->mkSygusDefaultGrammar( + range, terms[0], fun, datatypes, sorts, ops, sygus_vars, + startIndex); //set start index - Debug("parser-sygus") << "Set start index " << startIndex << "..." << std::endl; - PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops ); + Debug("parser-sygus") << "Set start index " << startIndex << "..." + << std::endl; + PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, + ops); }else{ - Debug("parser-sygus") << "--- Process " << sgts.size() << " sygus gterms..." << std::endl; + Debug("parser-sygus") << "--- Process " << sgts.size() + << " sygus gterms..." << std::endl; for( unsigned i=0; iprocessSygusGTerm( sgts[i][j], i, datatypes, sorts, ops, cnames, cargs, allow_const, unresolved_gterm_sym, - sygus_vars, sygus_to_builtin, sygus_to_builtin_expr, sub_ret ); + PARSER_STATE->processSygusGTerm( + sgts[i][j], i, datatypes, sorts, ops, cnames, cargs, + allow_const, unresolved_gterm_sym, sygus_vars, sygus_to_builtin, + sygus_to_builtin_expr, sub_ret ); } } //swap index if necessary Debug("parser-sygus") << "--- Making sygus datatypes..." << std::endl; for( unsigned i=0; iparseError(std::string("Internal error : could not infer builtin sort for nested gterm.")); + PARSER_STATE->parseError("Internal error : could not infer " + "builtin sort for nested gterm."); } datatypes[i].setSygus( sorts[i], terms[0], allow_const[i], false ); - PARSER_STATE->mkSygusDatatype( datatypes[i], ops[i], cnames[i], cargs[i], unresolved_gterm_sym[i], sygus_to_builtin ); + PARSER_STATE->mkSygusDatatype( + datatypes[i], ops[i], cnames[i], cargs[i], + unresolved_gterm_sym[i], sygus_to_builtin ); } - PARSER_STATE->setSygusStartIndex( fun, startIndex, datatypes, sorts, ops ); + PARSER_STATE->setSygusStartIndex(fun, startIndex, datatypes, sorts, + ops); } //only care about datatypes/sorts/ops past here PARSER_STATE->popScope(); - Debug("parser-sygus") << "--- Make " << datatypes.size() << " mutual datatypes..." << std::endl; + Debug("parser-sygus") << "--- Make " << datatypes.size() + << " mutual datatypes..." << std::endl; for( unsigned i=0; i datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); + std::vector datatypeTypes = + PARSER_STATE->mkMutualDatatypeTypes(datatypes); seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); std::map evals; if( sorts[0]!=range ){ - PARSER_STATE->parseError(std::string("Bad return type in grammar for SyGuS function ") + fun); + PARSER_STATE->parseError(std::string("Bad return type in grammar for " + "SyGuS function ") + fun); } // make all the evals first, since they are mutually referential for(size_t i = 0; i < datatypeTypes.size(); ++i) { @@ -659,8 +740,11 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } } evalType.push_back(sorts[i]); - Expr eval = PARSER_STATE->mkVar(name, EXPR_MANAGER->mkFunctionType(evalType)); - Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName() << std::endl; + const FunctionType eval_func_type = + EXPR_MANAGER->mkFunctionType(evalType); + Expr eval = PARSER_STATE->mkVar(name, eval_func_type); + Debug("parser-sygus") << "Make eval " << eval << " for " << dt.getName() + << std::endl; evals.insert(std::make_pair(dtt, eval)); if(i == 0) { PARSER_STATE->addSygusFun(fun, eval); @@ -671,13 +755,15 @@ sygusCommand returns [CVC4::Command* cmd = NULL] DatatypeType dtt = datatypeTypes[i]; const Datatype& dt = dtt.getDatatype(); Expr eval = evals[dtt]; - Debug("parser-sygus") << "Sygus : process grammar : " << dt << std::endl; + Debug("parser-sygus") << "Sygus : process grammar : " << dt + << std::endl; for(size_t j = 0; j < dt.getNumConstructors(); ++j) { - Expr assertion = PARSER_STATE->getSygusAssertion( datatypeTypes, ops, evals, terms, eval, dt, i, j ); + Expr assertion = PARSER_STATE->getSygusAssertion( + datatypeTypes, ops, evals, terms, eval, dt, i, j ); seq->addCommand(new AssertCommand(assertion)); } } - $cmd = seq; + cmd->reset(seq.release()); } | /* constraint */ CONSTRAINT_TOK { @@ -689,7 +775,7 @@ sygusCommand returns [CVC4::Command* cmd = NULL] term[expr, expr2] { Debug("parser-sygus") << "...read constraint " << expr << std::endl; PARSER_STATE->addSygusConstraint(expr); - $cmd = new EmptyCommand(); + cmd->reset(new EmptyCommand()); } | INV_CONSTRAINT_TOK { PARSER_STATE->checkThatLogicIsSet(); @@ -709,7 +795,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } )+ { if( terms.size()!=4 ){ - PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 arguments."); + PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 " + "arguments."); } //get primed variables std::vector< Expr > primed[2]; @@ -720,7 +807,8 @@ sygusCommand returns [CVC4::Command* cmd = NULL] } //make relevant terms for( unsigned i=0; i<4; i++ ){ - Debug("parser-sygus") << "Make inv-constraint term #" << i << "..." << std::endl; + Debug("parser-sygus") << "Make inv-constraint term #" << i << "..." + << std::endl; Expr op = terms[i]; std::vector< Expr > children; children.push_back( op ); @@ -733,42 +821,57 @@ sygusCommand returns [CVC4::Command* cmd = NULL] if( i==0 ){ std::vector< Expr > children2; children2.push_back( op ); - children2.insert( children2.end(), primed[1].begin(), primed[1].end() ); + children2.insert(children2.end(), primed[1].begin(), + primed[1].end()); terms.push_back( EXPR_MANAGER->mkExpr(kind::APPLY,children2) ); } } //make constraints std::vector< Expr > conj; - conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1], terms[0] ) ); - conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, EXPR_MANAGER->mkExpr(kind::AND, terms[0], terms[2] ), terms[4] ) ); - conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3] ) ); + conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[1], + terms[0] ) ); + const Expr term0_and_2 = EXPR_MANAGER->mkExpr(kind::AND, terms[0], + terms[2] ); + conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, term0_and_2, + terms[4] ) ); + conj.push_back( EXPR_MANAGER->mkExpr(kind::IMPLIES, terms[0], terms[3]) ); Expr ic = EXPR_MANAGER->mkExpr( kind::AND, conj ); - Debug("parser-sygus") << "...read invariant constraint " << ic << std::endl; + Debug("parser-sygus") << "...read invariant constraint " << ic + << std::endl; PARSER_STATE->addSygusConstraint(ic); - $cmd = new EmptyCommand(); + cmd->reset(new EmptyCommand()); } | /* check-synth */ - CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet();PARSER_STATE->defineSygusFuns(); } + CHECK_SYNTH_TOK + { PARSER_STATE->checkThatLogicIsSet(); PARSER_STATE->defineSygusFuns(); } { Expr sygusVar = EXPR_MANAGER->mkVar("sygus", EXPR_MANAGER->booleanType()); - Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar)); + Expr inst_attr =EXPR_MANAGER->mkExpr(kind::INST_ATTRIBUTE, sygusVar); + Expr sygusAttr = EXPR_MANAGER->mkExpr(kind::INST_PATTERN_LIST, inst_attr); std::vector bodyv; - Debug("parser-sygus") << "Sygus : Constructing sygus constraint..." << std::endl; - Expr body = EXPR_MANAGER->mkExpr(kind::NOT, PARSER_STATE->getSygusConstraints()); - Debug("parser-sygus") << "...constructed sygus constraint " << body << std::endl; + Debug("parser-sygus") << "Sygus : Constructing sygus constraint..." + << std::endl; + Expr body = EXPR_MANAGER->mkExpr(kind::NOT, + PARSER_STATE->getSygusConstraints()); + Debug("parser-sygus") << "...constructed sygus constraint " << body + << std::endl; if( !PARSER_STATE->getSygusVars().empty() ){ - body = EXPR_MANAGER->mkExpr(kind::EXISTS, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusVars()), body); - Debug("parser-sygus") << "...constructed exists " << body << std::endl; + Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, + PARSER_STATE->getSygusVars()); + body = EXPR_MANAGER->mkExpr(kind::EXISTS, boundVars, body); + Debug("parser-sygus") << "...constructed exists " << body << std::endl; } if( !PARSER_STATE->getSygusFunSymbols().empty() ){ - body = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()), body, sygusAttr); + Expr boundVars = EXPR_MANAGER->mkExpr( + kind::BOUND_VAR_LIST, PARSER_STATE->getSygusFunSymbols()); + body = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, body, sygusAttr); } Debug("parser-sygus") << "...constructed forall " << body << std::endl; Command* c = new SetUserAttributeCommand("sygus", sygusVar); c->setMuted(true); PARSER_STATE->preemptCommand(c); - $cmd = new CheckSynthCommand(body); + cmd->reset(new CheckSynthCommand(body)); } - | c = command { $cmd = c; } + | command[cmd] // /* error handling */ // | (~(CHECK_SYNTH_TOK))=> token=. // { std::string id = AntlrInput::tokenText($token); @@ -778,10 +881,13 @@ sygusCommand returns [CVC4::Command* cmd = NULL] // } ; -// SyGuS grammar term -// fun is the name of the synth-fun this grammar term is for. -// This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1) -// This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. +// SyGuS grammar term. +// +// fun is the name of the synth-fun this grammar term is for. +// This method adds N operators to ops[index], N names to cnames[index] and N +// type argument vectors to cargs[index] (where typically N=1) +// This method may also add new elements pairwise into +// datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms. sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] @declarations { std::string name, name2; @@ -797,8 +903,10 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] : LPAREN_TOK //read operator ( builtinOp[k]{ - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; - //since we enforce satisfaction completeness, immediately convert to total version + Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " + << name << std::endl; + // Since we enforce satisfaction completeness, immediately convert to + // total version. if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; }else if( k==CVC4::kind::BITVECTOR_UREM ){ @@ -824,17 +932,32 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] sygusGTerm[sgt.d_children.back(), fun] RPAREN_TOK )+ RPAREN_TOK | SYGUS_CONSTANT_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_constant; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar constant." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_constant; + sgt.d_type = t; + Debug("parser-sygus") << "Sygus grammar constant." << std::endl; + } | SYGUS_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar variable." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_variable; + sgt.d_type = t; + Debug("parser-sygus") << "Sygus grammar variable." << std::endl; + } | SYGUS_LOCAL_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar local variable...ignore." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_local_variable; + sgt.d_type = t; + Debug("parser-sygus") << "Sygus grammar local variable...ignore." + << std::endl; + } | SYGUS_INPUT_VARIABLE_TOK sortSymbol[t,CHECK_DECLARED] - { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; sgt.d_type = t;Debug("parser-sygus") << "Sygus grammar (input) variable." << std::endl; } + { sgt.d_gterm_type = SygusGTerm::gterm_input_variable; + sgt.d_type = t; + Debug("parser-sygus") << "Sygus grammar (input) variable." + << std::endl; + } | symbol[name,CHECK_NONE,SYM_VARIABLE] { bool isBuiltinOperator = PARSER_STATE->isOperatorEnabled(name); if(isBuiltinOperator) { - Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " + << name << std::endl; k = PARSER_STATE->getOperatorKind(name); if( k==CVC4::kind::BITVECTOR_UDIV ){ k = CVC4::kind::BITVECTOR_UDIV_TOTAL; @@ -848,10 +971,15 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] // what is this sygus term trying to accomplish here, if the // symbol isn't yet declared?! probably the following line will // fail, but we need an operator to continue here.. - Debug("parser-sygus") << "Sygus grammar " << fun; - Debug("parser-sygus") << " : op (declare=" << PARSER_STATE->isDeclared(name) << ", define=" << PARSER_STATE->isDefinedFunction(name) << ") : " << name << std::endl; - if( !PARSER_STATE->isDeclared(name) && !PARSER_STATE->isDefinedFunction(name) ){ - PARSER_STATE->parseError(std::string("Functions in sygus grammars must be defined.")); + Debug("parser-sygus") + << "Sygus grammar " << fun << " : op (declare=" + << PARSER_STATE->isDeclared(name) << ", define=" + << PARSER_STATE->isDefinedFunction(name) << ") : " << name + << std::endl; + if(!PARSER_STATE->isDeclared(name) && + !PARSER_STATE->isDefinedFunction(name) ){ + PARSER_STATE->parseError("Functions in sygus grammars must be " + "defined."); } sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; @@ -860,13 +988,16 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] } ) //read arguments - { Debug("parser-sygus") << "Read arguments under " << sgt.d_name << std::endl; + { Debug("parser-sygus") << "Read arguments under " << sgt.d_name + << std::endl; sgt.addChild(); } ( sygusGTerm[sgt.d_children.back(), fun] - { Debug("parser-sygus") << "Finished read argument #" << sgt.d_children.size() << "..." << std::endl; + { Debug("parser-sygus") << "Finished read argument #" + << sgt.d_children.size() << "..." << std::endl; sgt.addChild(); - } )* + } + )* RPAREN_TOK { //pop last child index sgt.d_children.pop_back(); @@ -875,13 +1006,16 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] } } | INTEGER_LITERAL - { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " << AntlrInput::tokenText($INTEGER_LITERAL) << std::endl; + { Debug("parser-sygus") << "Sygus grammar " << fun << " : integer literal " + << AntlrInput::tokenText($INTEGER_LITERAL) + << std::endl; sgt.d_expr = MK_CONST(Rational(AntlrInput::tokenText($INTEGER_LITERAL))); sgt.d_name = AntlrInput::tokenText($INTEGER_LITERAL); sgt.d_gterm_type = SygusGTerm::gterm_op; } | HEX_LITERAL - { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " << AntlrInput::tokenText($HEX_LITERAL) << std::endl; + { Debug("parser-sygus") << "Sygus grammar " << fun << " : hex literal " + << AntlrInput::tokenText($HEX_LITERAL) << std::endl; assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 ); std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2); sgt.d_expr = MK_CONST( BitVector(hexString, 16) ); @@ -889,7 +1023,9 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] sgt.d_gterm_type = SygusGTerm::gterm_op; } | BINARY_LITERAL - { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " << AntlrInput::tokenText($BINARY_LITERAL) << std::endl; + { Debug("parser-sygus") << "Sygus grammar " << fun << " : binary literal " + << AntlrInput::tokenText($BINARY_LITERAL) + << std::endl; assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 ); std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2); sgt.d_expr = MK_CONST( BitVector(binString, 2) ); @@ -897,27 +1033,35 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] sgt.d_gterm_type = SygusGTerm::gterm_op; } | str[s,false] - { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" << s << "\"" << std::endl; + { Debug("parser-sygus") << "Sygus grammar " << fun << " : string literal \"" + << s << "\"" << std::endl; sgt.d_expr = MK_CONST( ::CVC4::String(s) ); sgt.d_name = s; sgt.d_gterm_type = SygusGTerm::gterm_op; } - | symbol[name,CHECK_NONE,SYM_VARIABLE] ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { readEnum = true; } )? + | symbol[name,CHECK_NONE,SYM_VARIABLE] + ( SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] + { readEnum = true; } + )? { if( readEnum ){ name = name + "__Enum__" + name2; - Debug("parser-sygus") << "Sygus grammar " << fun << " : Enum constant " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun << " : Enum constant " + << name << std::endl; Expr c = PARSER_STATE->getVariable(name); sgt.d_expr = MK_EXPR(kind::APPLY_CONSTRUCTOR,c); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else{ if( name[0] == '-' ){ //hack for unary minus - Debug("parser-sygus") << "Sygus grammar " << fun << " : unary minus integer literal " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun + << " : unary minus integer literal " << name + << std::endl; sgt.d_expr = MK_CONST(Rational(name)); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){ - Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol " + << name << std::endl; sgt.d_expr = PARSER_STATE->getVariable(name); sgt.d_name = name; sgt.d_gterm_type = SygusGTerm::gterm_op; @@ -927,11 +1071,14 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] ss << fun << "_" << name; name = ss.str(); if( PARSER_STATE->isDeclared(name, SYM_SORT) ){ - Debug("parser-sygus") << "Sygus grammar " << fun << " : nested sort " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun + << " : nested sort " << name << std::endl; sgt.d_type = PARSER_STATE->getSort(name); sgt.d_gterm_type = SygusGTerm::gterm_nested_sort; }else{ - Debug("parser-sygus") << "Sygus grammar " << fun << " : unresolved symbol " << name << std::endl; + Debug("parser-sygus") << "Sygus grammar " << fun + << " : unresolved symbol " << name + << std::endl; sgt.d_gterm_type = SygusGTerm::gterm_unresolved; sgt.d_name = name; } @@ -941,7 +1088,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] ; // Separate this into its own rule (can be invoked by set-info or meta-info) -metaInfoInternal[CVC4::Command*& cmd] +metaInfoInternal[CVC4::PtrCloser* cmd] @declarations { std::string name; SExpr sexpr; @@ -956,24 +1103,25 @@ metaInfoInternal[CVC4::Command*& cmd] sexpr.getValue() == "2" || sexpr.getValue() == "2.0" ) { PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_0); - } else if( (sexpr.isRational() && sexpr.getRationalValue() == Rational(5, 2)) || - sexpr.getValue() == "2.5" ) { + } else if( (sexpr.isRational() && + sexpr.getRationalValue() == Rational(5, 2)) || + sexpr.getValue() == "2.5" ) { PARSER_STATE->setLanguage(language::input::LANG_SMTLIB_V2_5); } } PARSER_STATE->setInfo(name.c_str() + 1, sexpr); - cmd = new SetInfoCommand(name.c_str() + 1, sexpr); + cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr)); } ; -setOptionInternal[CVC4::Command*& cmd] +setOptionInternal[CVC4::PtrCloser* cmd] @init { std::string name; SExpr sexpr; } : keyword[name] symbolicExpr[sexpr] { PARSER_STATE->setOption(name.c_str() + 1, sexpr); - cmd = new SetOptionCommand(name.c_str() + 1, sexpr); + cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr)); // Ugly that this changes the state of the parser; but // global-declarations affects parsing, so we can't hold off // on this until some SmtEngine eventually (if ever) executes it. @@ -983,7 +1131,7 @@ setOptionInternal[CVC4::Command*& cmd] } ; -smt25Command[CVC4::Command*& cmd] +smt25Command[CVC4::PtrCloser* cmd] @declarations { std::string name; std::string fname; @@ -997,6 +1145,7 @@ smt25Command[CVC4::Command*& cmd] std::vector funcs; std::vector func_defs; Expr aexpr; + CVC4::PtrCloser seq; } /* meta-info */ : META_INFO_TOK metaInfoInternal[cmd] @@ -1007,115 +1156,120 @@ smt25Command[CVC4::Command*& cmd] { PARSER_STATE->checkUserSymbol(name); } sortSymbol[t,CHECK_DECLARED] { Expr c = PARSER_STATE->mkVar(name, t); - $cmd = new DeclareFunctionCommand(name, c, t); } + cmd->reset(new DeclareFunctionCommand(name, c, t)); } /* get model */ | GET_MODEL_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { cmd = new GetModelCommand(); } + { cmd->reset(new GetModelCommand()); } /* echo */ | ECHO_TOK ( simpleSymbolicExpr[sexpr] - { cmd = new EchoCommand(sexpr.toString()); } - | { cmd = new EchoCommand(); } + { cmd->reset(new EchoCommand(sexpr.toString())); } + | { cmd->reset(new EchoCommand()); } ) /* reset: reset everything, returning solver to initial state. * Logic and options must be set again. */ | RESET_TOK - { cmd = new ResetCommand(); + { cmd->reset(new ResetCommand()); PARSER_STATE->reset(); } /* reset-assertions: reset assertions, assertion stack, declarations, * etc., but the logic and options remain as they were. */ | RESET_ASSERTIONS_TOK - { cmd = new ResetAssertionsCommand(); + { cmd->reset(new ResetAssertionsCommand()); PARSER_STATE->resetAssertions(); } - | DEFINE_FUN_REC_TOK { - PARSER_STATE->checkThatLogicIsSet(); - cmd = new CommandSequence();} - symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] - { PARSER_STATE->checkUserSymbol(fname); } - LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - sortSymbol[t,CHECK_DECLARED] { - if( sortedVarNames.size() > 0 ) { - std::vector sorts; - sorts.reserve(sortedVarNames.size()); - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; - ++i) { - sorts.push_back((*i).second); - } - t = EXPR_MANAGER->mkFunctionType(sorts, t); - } - Expr func = PARSER_STATE->mkVar(fname, t); - static_cast($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t)); - std::vector< Expr > f_app; - f_app.push_back( func ); - PARSER_STATE->pushScope(true); + | DEFINE_FUN_REC_TOK + { PARSER_STATE->checkThatLogicIsSet(); + seq.reset(new CVC4::CommandSequence()); + } + symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] + { PARSER_STATE->checkUserSymbol(fname); } + LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK + sortSymbol[t,CHECK_DECLARED] + { if( sortedVarNames.size() > 0 ) { + std::vector sorts; + sorts.reserve(sortedVarNames.size()); for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { - Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); - bvs.push_back( v ); - f_app.push_back( v ); + sorts.push_back((*i).second); } - func_app = MK_EXPR( kind::APPLY_UF, f_app ); + t = EXPR_MANAGER->mkFunctionType(sorts, t); } - term[expr, expr2] - { PARSER_STATE->popScope(); - std::string attr_name("fun-def"); - aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); - aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr); - //set the attribute to denote this is a function definition - static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); - //assert it - Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr); - static_cast($cmd)->addCommand( new AssertCommand(as, false) ); - } - | DEFINE_FUNS_REC_TOK { - PARSER_STATE->checkThatLogicIsSet(); - cmd = new CommandSequence();} + Expr func = PARSER_STATE->mkVar(fname, t); + seq->addCommand(new DeclareFunctionCommand(fname, func, t)); + std::vector< Expr > f_app; + f_app.push_back( func ); + PARSER_STATE->pushScope(true); + for(std::vector >::const_iterator i = + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; + ++i) { + Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); + bvs.push_back( v ); + f_app.push_back( v ); + } + func_app = MK_EXPR( kind::APPLY_UF, f_app ); + } + term[expr, expr2] + { PARSER_STATE->popScope(); + std::string attr_name("fun-def"); + aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); + aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr); + //set the attribute to denote this is a function definition + seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); + //assert it + Expr equality = MK_EXPR( func_app.getType().isBoolean() ? + kind::IFF : kind::EQUAL, func_app, expr); + Expr boundVars = EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs); + Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, boundVars, equality, aexpr); + seq->addCommand( new AssertCommand(as, false) ); + cmd->reset(seq.release()); + } + | DEFINE_FUNS_REC_TOK + { PARSER_STATE->checkThatLogicIsSet(); + seq.reset(new CVC4::CommandSequence()); + } LPAREN_TOK ( LPAREN_TOK symbol[fname,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(fname); } LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK - sortSymbol[t,CHECK_DECLARED] { - sortedVarNamesList.push_back( sortedVarNames ); + sortSymbol[t,CHECK_DECLARED] + { sortedVarNamesList.push_back( sortedVarNames ); if( sortedVarNamesList[0].size() > 0 ) { std::vector sorts; - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; - ++i) { + for(std::vector >::const_iterator + i = sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; ++i) { sorts.push_back((*i).second); } t = EXPR_MANAGER->mkFunctionType(sorts, t); } sortedVarNames.clear(); Expr func = PARSER_STATE->mkVar(fname, t); - static_cast($cmd)->addCommand(new DeclareFunctionCommand(fname, func, t)); + seq->addCommand(new DeclareFunctionCommand(fname, func, t)); funcs.push_back( func ); } RPAREN_TOK - )+ + )+ RPAREN_TOK LPAREN_TOK { //set up the first scope if( sortedVarNamesList.empty() ){ - PARSER_STATE->parseError(std::string("Must define at least one function in define-funs-rec")); + PARSER_STATE->parseError("Must define at least one function in " + "define-funs-rec"); } std::vector< Expr > f_app; f_app.push_back( funcs[0] ); PARSER_STATE->pushScope(true); bvs.clear(); - for(std::vector >::const_iterator i = sortedVarNamesList[0].begin(), - iend = sortedVarNamesList[0].end(); i != iend; ++i) { + for(std::vector >::const_iterator + i = sortedVarNamesList[0].begin(), + iend = sortedVarNamesList[0].end(); i != iend; ++i) { Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); bvs.push_back( v ); f_app.push_back( v ); @@ -1131,10 +1285,15 @@ smt25Command[CVC4::Command*& cmd] aexpr = MK_EXPR(kind::INST_ATTRIBUTE, func_app); aexpr = MK_EXPR(kind::INST_PATTERN_LIST, aexpr ); //set the attribute to denote these are function definitions - static_cast($cmd)->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); + seq->addCommand( new SetUserAttributeCommand( attr_name, func_app ) ); //assert it - Expr as = EXPR_MANAGER->mkExpr(kind::FORALL, EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), MK_EXPR( func_app.getType().isBoolean() ? kind::IFF : kind::EQUAL, func_app, expr ), aexpr); - static_cast($cmd)->addCommand( new AssertCommand(as, false) ); + Expr as = EXPR_MANAGER->mkExpr( + kind::FORALL, + EXPR_MANAGER->mkExpr(kind::BOUND_VAR_LIST, bvs), + MK_EXPR( func_app.getType().isBoolean() ? + kind::IFF : kind::EQUAL, func_app, expr ), + aexpr); + seq->addCommand( new AssertCommand(as, false) ); //set up the next scope PARSER_STATE->popScope(); if( func_defs.size()pushScope(true); bvs.clear(); - for(std::vector >::const_iterator i = sortedVarNamesList[j].begin(), - iend = sortedVarNamesList[j].end(); i != iend; ++i) { + for(std::vector >::const_iterator + i = sortedVarNamesList[j].begin(), + iend = sortedVarNamesList[j].end(); i != iend; ++i) { Expr v = PARSER_STATE->mkBoundVar((*i).first, (*i).second); bvs.push_back( v ); f_app.push_back( v ); @@ -1154,18 +1314,18 @@ smt25Command[CVC4::Command*& cmd] } )+ RPAREN_TOK - { - if( funcs.size()!=func_defs.size() ){ - PARSER_STATE->parseError(std::string("Number of functions defined does not match number listed in define-funs-rec")); + { if( funcs.size()!=func_defs.size() ){ + PARSER_STATE->parseError(std::string( + "Number of functions defined does not match number listed in " + "define-funs-rec")); } + cmd->reset(seq.release()); } - - // CHECK_SAT_ASSUMING still being discussed // GET_UNSAT_ASSUMPTIONS ; -extendedCommand[CVC4::Command*& cmd] +extendedCommand[CVC4::PtrCloser* cmd] @declarations { std::vector dts; Expr e, e2; @@ -1175,6 +1335,7 @@ extendedCommand[CVC4::Command*& cmd] std::vector terms; std::vector sorts; std::vector > sortedVarNames; + CVC4::PtrCloser seq; } /* Extended SMT-LIB set of commands syntax, not permitted in * --smtlib2 compliance mode. */ @@ -1189,21 +1350,22 @@ extendedCommand[CVC4::Command*& cmd] !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_DATATYPES) && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS)) { - PARSER_STATE->parseError(std::string("Free sort symbols not allowed in ") + PARSER_STATE->getLogic().getLogicString()); + PARSER_STATE->parseErrorLogic("Free sort symbols not allowed in "); } } - { $cmd = new CommandSequence(); } + { seq.reset(new CVC4::CommandSequence()); } LPAREN_TOK ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { PARSER_STATE->checkUserSymbol(name); Type type = PARSER_STATE->mkSort(name); - static_cast($cmd)->addCommand(new DeclareTypeCommand(name, 0, type)); + seq->addCommand(new DeclareTypeCommand(name, 0, type)); } )+ RPAREN_TOK + { cmd->reset(seq.release()); } | DECLARE_FUNS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { $cmd = new CommandSequence(); } + { seq.reset(new CVC4::CommandSequence()); } LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } @@ -1211,21 +1373,22 @@ extendedCommand[CVC4::Command*& cmd] { Type t; if(sorts.size() > 1) { 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()); + PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) " + "cannot be declared in logic "); } t = EXPR_MANAGER->mkFunctionType(sorts); } else { t = sorts[0]; } Expr func = PARSER_STATE->mkVar(name, t); - static_cast($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } )+ RPAREN_TOK - + { cmd->reset(seq.release()); } | DECLARE_PREDS_TOK { PARSER_STATE->checkThatLogicIsSet(); } - { $cmd = new CommandSequence(); } + { seq.reset(new CVC4::CommandSequence()); } LPAREN_TOK ( LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } @@ -1233,23 +1396,26 @@ extendedCommand[CVC4::Command*& cmd] { Type t = EXPR_MANAGER->booleanType(); if(sorts.size() > 0) { if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) { - PARSER_STATE->parseError(std::string("Predicates (of non-zero arity) cannot be declared in logic ") + PARSER_STATE->getLogic().getLogicString()); + PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) " + "cannot be declared in logic "); } t = EXPR_MANAGER->mkFunctionType(sorts, t); } Expr func = PARSER_STATE->mkVar(name, t); - static_cast($cmd)->addCommand(new DeclareFunctionCommand(name, func, t)); + seq->addCommand(new DeclareFunctionCommand(name, func, t)); sorts.clear(); } )+ RPAREN_TOK + { cmd->reset(seq.release()); } | DEFINE_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] { PARSER_STATE->checkUserSymbol(name); } term[e,e2] - { Expr func = PARSER_STATE->mkFunction(name, e.getType(), ExprManager::VAR_FLAG_DEFINED); - $cmd = new DefineFunctionCommand(name, func, e); + { Expr func = PARSER_STATE->mkFunction(name, e.getType(), + ExprManager::VAR_FLAG_DEFINED); + cmd->reset(new DefineFunctionCommand(name, func, e)); } | LPAREN_TOK symbol[name,CHECK_UNDECLARED,SYM_VARIABLE] @@ -1259,8 +1425,7 @@ extendedCommand[CVC4::Command*& cmd] Debug("parser") << "define fun: '" << name << "'" << std::endl; PARSER_STATE->pushScope(true); for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } @@ -1274,16 +1439,16 @@ extendedCommand[CVC4::Command*& cmd] if( sortedVarNames.size() > 0 ) { std::vector sorts; sorts.reserve(sortedVarNames.size()); - for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; - ++i) { + for(std::vector >::const_iterator + i = sortedVarNames.begin(), iend = sortedVarNames.end(); + i != iend; ++i) { sorts.push_back((*i).second); } t = EXPR_MANAGER->mkFunctionType(sorts, t); } - Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); - $cmd = new DefineFunctionCommand(name, func, terms, e); + Expr func = PARSER_STATE->mkFunction(name, t, + ExprManager::VAR_FLAG_DEFINED); + cmd->reset(new DefineFunctionCommand(name, func, terms, e)); } ) | DEFINE_CONST_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -1294,8 +1459,7 @@ extendedCommand[CVC4::Command*& cmd] Debug("parser") << "define const: '" << name << "'" << std::endl; PARSER_STATE->pushScope(true); for(std::vector >::const_iterator i = - sortedVarNames.begin(), iend = sortedVarNames.end(); - i != iend; + sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; ++i) { terms.push_back(PARSER_STATE->mkBoundVar((*i).first, (*i).second)); } @@ -1305,23 +1469,24 @@ extendedCommand[CVC4::Command*& cmd] // declare the name down here (while parsing term, signature // must not be extended with the name itself; no recursion // permitted) - Expr func = PARSER_STATE->mkFunction(name, t, ExprManager::VAR_FLAG_DEFINED); - $cmd = new DefineFunctionCommand(name, func, terms, e); + Expr func = PARSER_STATE->mkFunction(name, t, + ExprManager::VAR_FLAG_DEFINED); + cmd->reset(new DefineFunctionCommand(name, func, terms, e)); } | SIMPLIFY_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd = new SimplifyCommand(e); } + { cmd->reset(new SimplifyCommand(e)); } | GET_QE_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd = new GetQuantifierEliminationCommand(e, true); } + { cmd->reset(new GetQuantifierEliminationCommand(e, true)); } | GET_QE_DISJUNCT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[e,e2] - { cmd = new GetQuantifierEliminationCommand(e, false); } + { cmd->reset(new GetQuantifierEliminationCommand(e, false)); } ; -datatypesDefCommand[bool isCo, CVC4::Command*& cmd] +datatypesDefCommand[bool isCo, CVC4::PtrCloser* cmd] @declarations { std::vector dts; std::string name; @@ -1331,16 +1496,18 @@ datatypesDefCommand[bool isCo, CVC4::Command*& cmd] /* open a scope to keep the UnresolvedTypes contained */ PARSER_STATE->pushScope(true); } LPAREN_TOK /* parametric sorts */ - ( symbol[name,CHECK_UNDECLARED,SYM_SORT] { - sorts.push_back( PARSER_STATE->mkSort(name) ); } + ( symbol[name,CHECK_UNDECLARED,SYM_SORT] + { sorts.push_back( PARSER_STATE->mkSort(name) ); } )* RPAREN_TOK LPAREN_TOK ( LPAREN_TOK datatypeDef[isCo, dts, sorts] RPAREN_TOK )+ RPAREN_TOK { PARSER_STATE->popScope(); - cmd = new DatatypeDeclarationCommand(PARSER_STATE->mkMutualDatatypeTypes(dts)); } + cmd->reset(new DatatypeDeclarationCommand( + PARSER_STATE->mkMutualDatatypeTypes(dts))); + } ; -rewriterulesCommand[CVC4::Command*& cmd] +rewriterulesCommand[CVC4::PtrCloser* cmd] @declarations { std::vector > sortedVarNames; std::vector args, guards, heads, triggers; @@ -1388,7 +1555,7 @@ rewriterulesCommand[CVC4::Command*& cmd] }; args.push_back(expr); expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - cmd = new AssertCommand(expr, false); } + cmd->reset(new AssertCommand(expr, false)); } /* propagation rule */ | rewritePropaKind[kind] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK @@ -1439,7 +1606,8 @@ rewriterulesCommand[CVC4::Command*& cmd] }; args.push_back(expr); expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args); - cmd = new AssertCommand(expr, false); } + cmd->reset(new AssertCommand(expr, false)); + } ; rewritePropaKind[CVC4::Kind& kind] @@ -1488,11 +1656,19 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] // } | symbol[s,CHECK_NONE,SYM_SORT] { sexpr = SExpr(SExpr::Keyword(s)); } - | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) + | tok=(ASSERT_TOK | CHECKSAT_TOK | DECLARE_FUN_TOK | DECLARE_SORT_TOK + | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK + | DEFINE_SORT_TOK | GET_VALUE_TOK | GET_ASSIGNMENT_TOK + | GET_ASSERTIONS_TOK | GET_PROOF_TOK | GET_UNSAT_CORE_TOK | EXIT_TOK + | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK + | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK + | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | REWRITE_RULE_TOK + | REDUCTION_RULE_TOK | PROPAGATION_RULE_TOK | SIMPLIFY_TOK) { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); } | builtinOp[k] { std::stringstream ss; - ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) << EXPR_MANAGER->mkConst(k); + ss << language::SetLanguage(CVC4::language::output::LANG_SMTLIB_V2_5) + << EXPR_MANAGER->mkConst(k); sexpr = SExpr(ss.str()); } ; @@ -1586,7 +1762,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] args.size() == 1 && !args[0].getType().isInteger() ) { /* first, check that ABS is even defined in this logic */ PARSER_STATE->checkOperator(kind, args.size()); - PARSER_STATE->parseError("abs can only be applied to Int, not Real, while in strict SMT-LIB compliance mode"); + PARSER_STATE->parseError("abs can only be applied to Int, not Real, " + "while in strict SMT-LIB compliance mode"); } else { PARSER_STATE->checkOperator(kind, args.size()); expr = MK_EXPR(kind, args); @@ -1597,7 +1774,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) { std::vector v; Expr e = f.getOperator(); - const DatatypeConstructor& dtc = Datatype::datatypeOf(e)[Datatype::indexOf(e)]; + const DatatypeConstructor& dtc = + Datatype::datatypeOf(e)[Datatype::indexOf(e)]; v.push_back(MK_EXPR( CVC4::kind::APPLY_TYPE_ASCRIPTION, MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() )); v.insert(v.end(), f.begin(), f.end()); @@ -1607,8 +1785,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) { - //We don't want the nil reference to be a constant: for instance, it could be of type Int but is not a const rational. - //However, the expression has 0 children. So we convert to a SEP_NIL variable. + //We don't want the nil reference to be a constant: for instance, it + //could be of type Int but is not a const rational. However, the + //expression has 0 children. So we convert to a SEP_NIL variable. expr = EXPR_MANAGER->mkUniqueVar(type, kind::SEP_NIL); } else { if(f.getType() != type) { @@ -1638,7 +1817,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] case CVC4::kind::RR_REDUCTION: case CVC4::kind::RR_DEDUCTION: if(kind == CVC4::kind::EXISTS) { - PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite rule."); + PARSER_STATE->parseError("Use Exists instead of Forall for a rewrite " + "rule."); } args.push_back(f2); // guards args.push_back(f); // rule @@ -1688,16 +1868,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] } //(termList[args,expr])? RPAREN_TOK termList[args,expr] RPAREN_TOK - { //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; + { 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; } @@ -1719,7 +1891,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] { if(!type.isArray()) { std::stringstream ss; - ss << "expected array constant term, but cast is not of array type" << std::endl + ss << "expected array constant term, but cast is not of array type" + << std::endl << "cast type: " << type; PARSER_STATE->parseError(ss.str()); } @@ -1734,7 +1907,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] std::stringstream ss; ss << "type mismatch inside array constant term:" << std::endl << "array type: " << type << std::endl - << "expected const type: " << ArrayType(type).getConstituentType() << std::endl + << "expected const type: " << ArrayType(type).getConstituentType() + << std::endl << "computed const type: " << f.getType(); PARSER_STATE->parseError(ss.str()); } @@ -1744,21 +1918,27 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | /* a let binding */ LPAREN_TOK LET_TOK LPAREN_TOK { PARSER_STATE->pushScope(true); } - ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] { readLetSort = true; } term[expr, f2] ) RPAREN_TOK + ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] + (term[expr, f2] | sortSymbol[type,CHECK_DECLARED] + { readLetSort = true; } term[expr, f2] + ) + RPAREN_TOK // this is a parallel let, so we have to save up all the contributions // of the let and define them only later on { if( !PARSER_STATE->sygus() && readLetSort ){ PARSER_STATE->parseError("Bad syntax for let term."); }else if(names.count(name) == 1) { std::stringstream ss; - ss << "warning: symbol `" << name << "' bound multiple times by let; the last binding will be used, shadowing earlier ones"; + ss << "warning: symbol `" << name << "' bound multiple times by let;" + << " the last binding will be used, shadowing earlier ones"; PARSER_STATE->warning(ss.str()); } else { names.insert(name); } binders.push_back(std::make_pair(name, expr)); } )+ { // now implement these bindings - for(std::vector< std::pair >::iterator i = binders.begin(); i != binders.end(); ++i) { + for(std::vector< std::pair >::iterator + i = binders.begin(); i != binders.end(); ++i) { PARSER_STATE->defineVar((*i).first, (*i).second); } } @@ -1766,17 +1946,20 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] term[expr, f2] RPAREN_TOK { PARSER_STATE->popScope(); } - | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK symbol[name2,CHECK_NONE,SYM_VARIABLE] { - std::string cname = name + "__Enum__" + name2; + | symbol[name,CHECK_NONE,SYM_VARIABLE] SYGUS_ENUM_CONS_TOK + symbol[name2,CHECK_NONE,SYM_VARIABLE] + { std::string cname = name + "__Enum__" + name2; Debug("parser-sygus") << "Check for enum const " << cname << std::endl; expr = PARSER_STATE->getVariable(cname); - //expr.getType().isConstructor() && ConstructorType(expr.getType()).getArity()==0; + // expr.getType().isConstructor() && + // ConstructorType(expr.getType()).getArity()==0; expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, expr); } /* a variable */ | symbol[name,CHECK_DECLARED,SYM_VARIABLE] { if( PARSER_STATE->sygus() && name[0]=='-' && - name.find_first_not_of("0123456789", 1) == std::string::npos ){ //allow unary minus in sygus + name.find_first_not_of("0123456789", 1) == std::string::npos ){ + //allow unary minus in sygus expr = MK_CONST(Rational(name)); }else{ const bool isDefinedFunction = @@ -1838,7 +2021,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] patexprs.push_back( f2[i] ); }else{ std::stringstream ss; - ss << "warning: rewrite rules do not support " << f2[i] << " within instantiation pattern list"; + ss << "warning: rewrite rules do not support " << f2[i] + << " within instantiation pattern list"; PARSER_STATE->warning(ss.str()); } } @@ -1862,7 +2046,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] { if(AntlrInput::tokenText($bvLit).find("bv") == 0) { expr = MK_CONST( AntlrInput::tokenToBitvector($bvLit, $size) ); } else { - PARSER_STATE->parseError("Unexpected symbol `" + AntlrInput::tokenText($bvLit) + "'"); + PARSER_STATE->parseError("Unexpected symbol `" + + AntlrInput::tokenText($bvLit) + "'"); } } | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL @@ -1906,10 +2091,14 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | FP_RTZ_FULL_TOK { expr = MK_CONST(roundTowardZero); } | RENOSTR_TOK - { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); } + { std::vector< Expr > nvec; + expr = MK_EXPR( CVC4::kind::REGEXP_EMPTY, nvec ); + } | REALLCHAR_TOK - { std::vector< Expr > nvec; expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); } + { std::vector< Expr > nvec; + expr = MK_EXPR( CVC4::kind::REGEXP_SIGMA, nvec ); + } | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet(Type())); } @@ -1922,7 +2111,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] /** * Read attribute */ -attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] +attribute[CVC4::Expr& expr, CVC4::Expr& retExpr, std::string& attr] @init { SExpr sexpr; Expr patexpr; @@ -1937,14 +2126,17 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] if(attr == ":rewrite-rule") { if(hasValue) { std::stringstream ss; - ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; + ss << "warning: Attribute " << attr + << " does not take a value (ignoring)"; PARSER_STATE->warning(ss.str()); } // do nothing - } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" || attr==":sygus" || attr==":synthesis") { + } else if(attr==":axiom" || attr==":conjecture" || attr==":fun-def" || + attr==":sygus" || attr==":synthesis") { if(hasValue) { std::stringstream ss; - ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; + ss << "warning: Attribute " << attr + << " does not take a value (ignoring)"; PARSER_STATE->warning(ss.str()); } Expr avar; @@ -1952,12 +2144,14 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] std::string attr_name = attr; attr_name.erase( attr_name.begin() ); if( attr==":fun-def" ){ - if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || expr[0].getKind()!=kind::APPLY_UF ){ + if( ( expr.getKind()!=kind::EQUAL && expr.getKind()!=kind::IFF ) || + expr[0].getKind()!=kind::APPLY_UF ){ success = false; }else{ FunctionType t = (FunctionType)expr[0].getOperator().getType(); for( unsigned i=0; iwarning(ss.str()); }else{ avar = expr[0]; @@ -1982,7 +2177,8 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] avar = PARSER_STATE->mkVar(attr_name, t); } if( success ){ - //will set the attribute on auxiliary var (preserves attribute on formula through rewriting) + //Will set the attribute on auxiliary var (preserves attribute on + //formula through rewriting). retExpr = MK_EXPR(kind::INST_ATTRIBUTE, avar); Command* c = new SetUserAttributeCommand( attr_name, avar ); c->setMuted(true); @@ -1992,7 +2188,10 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] PARSER_STATE->attributeNotSupported(attr); } } - | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); } )+ RPAREN_TOK + | ATTRIBUTE_PATTERN_TOK LPAREN_TOK + ( term[patexpr, e2] + { patexprs.push_back( patexpr ); } + )+ RPAREN_TOK { attr = std::string(":pattern"); retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); @@ -2029,8 +2228,10 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] if(!isClosed(expr, freeVars)) { assert(!freeVars.empty()); std::stringstream ss; - ss << ":named annotations can only name terms that are closed; this one contains free variables:"; - for(std::set::const_iterator i = freeVars.begin(); i != freeVars.end(); ++i) { + ss << ":named annotations can only name terms that are closed; this " + << "one contains free variables:"; + for(std::set::const_iterator i = freeVars.begin(); + i != freeVars.end(); ++i) { ss << " " << *i; } PARSER_STATE->parseError(ss.str()); @@ -2072,7 +2273,9 @@ indexedFunctionName[CVC4::Expr& op] | INT2BV_TOK n=INTEGER_LITERAL { op = MK_CONST(IntToBitVector(AntlrInput::tokenToUnsigned($n))); if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); + PARSER_STATE->parseError( + "bv2nat and int2bv are not part of SMT-LIB, and aren't available " + "in SMT-LIB strict compliance mode"); } } | FP_PINF_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL { op = MK_CONST(FloatingPoint(AntlrInput::tokenToUnsigned($eb), @@ -2095,23 +2298,34 @@ indexedFunctionName[CVC4::Expr& op] AntlrInput::tokenToUnsigned($sb), -0.0)); } | FP_TO_FP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPGeneric(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); } + { op = MK_CONST(FloatingPointToFPGeneric( + AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb))); + } | FP_TO_FPBV_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPIEEEBitVector(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); } + { op = MK_CONST(FloatingPointToFPIEEEBitVector( + AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb))); + } | FP_TO_FPFP_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPFloatingPoint(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); } + { op = MK_CONST(FloatingPointToFPFloatingPoint( + AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb))); + } | FP_TO_FPR_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL { op = MK_CONST(FloatingPointToFPReal(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); } + AntlrInput::tokenToUnsigned($sb))); + } | FP_TO_FPS_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPSignedBitVector(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); } + { op = MK_CONST(FloatingPointToFPSignedBitVector( + AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb))); + } | FP_TO_FPU_TOK eb=INTEGER_LITERAL sb=INTEGER_LITERAL - { op = MK_CONST(FloatingPointToFPUnsignedBitVector(AntlrInput::tokenToUnsigned($eb), - AntlrInput::tokenToUnsigned($sb))); } + { op = MK_CONST(FloatingPointToFPUnsignedBitVector( + AntlrInput::tokenToUnsigned($eb), + AntlrInput::tokenToUnsigned($sb))); + } | FP_TO_UBV_TOK m=INTEGER_LITERAL { op = MK_CONST(FloatingPointToUBV(AntlrInput::tokenToUnsigned($m))); } | FP_TO_SBV_TOK m=INTEGER_LITERAL @@ -2130,7 +2344,9 @@ badIndexedFunctionName std::string name; } : id=(SIMPLE_SYMBOL | QUOTED_SYMBOL | UNTERMINATED_QUOTED_SYMBOL) - { PARSER_STATE->parseError(std::string("Unknown indexed function `") + AntlrInput::tokenText($id) + "'"); } + { PARSER_STATE->parseError(std::string("Unknown indexed function `") + + AntlrInput::tokenText($id) + "'"); + } ; /** @@ -2158,7 +2374,9 @@ str[std::string& s, bool fsmtlib] s = s.substr(1, s.size() - 2); for(size_t i=0; i 127 && !isprint(s[i])) { - PARSER_STATE->parseError("Extended/unprintable characters are not part of SMT-LIB, and they must be encoded as escape sequences"); + PARSER_STATE->parseError("Extended/unprintable characters are not " + "part of SMT-LIB, and they must be encoded " + "as escape sequences"); } } if(fsmtlib) { @@ -2190,7 +2408,9 @@ str[std::string& s, bool fsmtlib] s = s.substr(1, s.size() - 2); for(size_t i=0; i 127 && !isprint(s[i])) { - PARSER_STATE->parseError("Extended/unprintable characters are not part of SMT-LIB, and they must be encoded as escape sequences"); + PARSER_STATE->parseError("Extended/unprintable characters are not " + "part of SMT-LIB, and they must be encoded " + "as escape sequences"); } } // In the 2.5 version, always handle escapes (regardless of fsmtlib flag). @@ -2237,14 +2457,18 @@ builtinOp[CVC4::Kind& kind] | STAR_TOK { $kind = CVC4::kind::MULT; } | DIV_TOK { $kind = CVC4::kind::DIVISION; } - | BV2NAT_TOK { $kind = CVC4::kind::BITVECTOR_TO_NAT; - if(PARSER_STATE->strictModeEnabled()) { - PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, and aren't available in SMT-LIB strict compliance mode"); - } } + | BV2NAT_TOK + { $kind = CVC4::kind::BITVECTOR_TO_NAT; + if(PARSER_STATE->strictModeEnabled()) { + PARSER_STATE->parseError("bv2nat and int2bv are not part of SMT-LIB, " + "and aren't available in SMT-LIB strict " + "compliance mode"); + } + } - | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } - | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } - | FMFCARDVAL_TOK { $kind = CVC4::kind::CARDINALITY_VALUE; } + | DTSIZE_TOK { $kind = CVC4::kind::DT_SIZE; } + | FMFCARD_TOK { $kind = CVC4::kind::CARDINALITY_CONSTRAINT; } + | FMFCARDVAL_TOK { $kind = CVC4::kind::CARDINALITY_VALUE; } | INST_CLOSURE_TOK { $kind = CVC4::kind::INST_CLOSURE; } // NOTE: Theory operators no longer go here, add to smt2.cpp. Only @@ -2298,7 +2522,8 @@ sortedVarList[std::vector >& sortedVars] std::string name; Type t; } - : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] sortSymbol[t,CHECK_DECLARED] RPAREN_TOK + : ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] + sortSymbol[t,CHECK_DECLARED] RPAREN_TOK { sortedVars.push_back(make_pair(name, t)); } )* ; @@ -2320,7 +2545,7 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] } : sortName[name,CHECK_NONE] { - if( check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT) ) { + if(check == CHECK_DECLARED || PARSER_STATE->isDeclared(name, SYM_SORT)) { t = PARSER_STATE->getSort(name); } else { t = PARSER_STATE->mkUnresolvedType(name); @@ -2332,7 +2557,8 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] { // allow sygus inputs to elide the `_' if( !indexed && !PARSER_STATE->sygus() ) { std::stringstream ss; - ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name << " ...)"; + ss << "SMT-LIB requires use of an indexed sort here, e.g. (_ " << name + << " ...)"; PARSER_STATE->parseError(ss.str()); } if( name == "BitVec" ) { @@ -2363,11 +2589,13 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] | sortList[args] { if( indexed ) { std::stringstream ss; - ss << "Unexpected use of indexing operator `_' before `" << name << "', try leaving it out"; + ss << "Unexpected use of indexing operator `_' before `" << name + << "', try leaving it out"; PARSER_STATE->parseError(ss.str()); } if(args.empty()) { - PARSER_STATE->parseError("Extra parentheses around sort name not permitted in SMT-LIB"); + PARSER_STATE->parseError("Extra parentheses around sort name not " + "permitted in SMT-LIB"); } else if(name == "Array" && PARSER_STATE->isTheoryEnabled(Smt2::THEORY_ARRAYS) ) { if(args.size() != 2) { @@ -2387,12 +2615,14 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] // make unresolved type if(args.empty()) { t = PARSER_STATE->mkUnresolvedType(name); - Debug("parser-param") << "param: make unres type " << name << std::endl; + Debug("parser-param") << "param: make unres type " << name + << std::endl; } else { t = PARSER_STATE->mkUnresolvedTypeConstructor(name,args); t = SortConstructorType(t).instantiate( args ); - Debug("parser-param") << "param: make unres param type " << name << " " << args.size() << " " - << PARSER_STATE->getArity( name ) << std::endl; + Debug("parser-param") + << "param: make unres param type " << name << " " << args.size() + << " " << PARSER_STATE->getArity( name ) << std::endl; } } } @@ -2454,7 +2684,8 @@ symbol[std::string& id, ( EOF { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); } | '\\' - { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| symbol"); } + { PARSER_STATE->unexpectedEOF("backslash not permitted in |quoted| " + "symbol"); } ) ; @@ -2471,7 +2702,8 @@ nonemptyNumeralList[std::vector& numerals] /** * Parses a datatype definition */ -datatypeDef[bool isCo, std::vector& datatypes, std::vector< CVC4::Type >& params] +datatypeDef[bool isCo, std::vector& datatypes, + std::vector< CVC4::Type >& params] @init { std::string id; } diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index b99e142ba..fc930dc79 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -295,7 +295,8 @@ public: case kind::BITVECTOR_MULT: case kind::BITVECTOR_PLUS: if(numArgs != 2) { - parseError("Operator requires exact 2 arguments in strict SMT-LIB compliance mode: " + kindToString(kind)); + parseError("Operator requires exact 2 arguments in strict SMT-LIB " + "compliance mode: " + kindToString(kind)); } break; default: @@ -304,6 +305,12 @@ public: } } + // Throw a ParserException with msg appended with the current logic. + inline void parseErrorLogic(const std::string& msg) throw(ParserException) { + const std::string withLogic = msg + getLogic().getLogicString(); + parseError(withLogic); + } + private: std::map< CVC4::Expr, CVC4::Type > d_sygus_bound_var_type; std::map< CVC4::Expr, std::vector< CVC4::Expr > > d_sygus_let_func_to_vars; -- 2.30.2