diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-03 10:19:12 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-03 10:19:12 -0700 |
commit | 51181eb3382ae9c94f90a39103e33ec6e9063dee (patch) | |
tree | 59fc47fc7ba9e1e50ba82cd359ba2bd8e8f679f2 /src/parser/smt2/Smt2.g | |
parent | ba73019ebea069607ff1a66863bbdb6a5d501344 (diff) |
[SMT2 Parser] Move code of `sygusCommand` (#3335)
This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 144 |
1 files changed, 33 insertions, 111 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e838398ba..c63bc4a95 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -208,13 +208,12 @@ parseCommand returns [CVC4::Command* cmd_return = NULL] */ parseSygus returns [CVC4::Command* cmd_return = NULL] @declarations { - std::unique_ptr<CVC4::Command> cmd; std::string name; } @after { cmd_return = cmd.release(); } - : LPAREN_TOK sygusCommand[&cmd] RPAREN_TOK + : LPAREN_TOK cmd=sygusCommand RPAREN_TOK | EOF ; @@ -551,19 +550,16 @@ command [std::unique_ptr<CVC4::Command>* cmd] } ; -sygusCommand [std::unique_ptr<CVC4::Command>* cmd] +sygusCommand returns [std::unique_ptr<CVC4::Command> cmd] @declarations { - std::string name, fun; - std::vector<std::string> names; Expr expr, expr2; Type t, range; - std::vector<Expr> terms; - std::vector<Expr> sygus_vars; + std::vector<std::string> names; std::vector<std::pair<std::string, Type> > sortedVarNames; - Type sygus_ret; - Expr synth_fun; - Type sygus_type; + std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory; + std::string name, fun; bool isInv; + Type grammar; } : /* declare-var */ DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -572,7 +568,7 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] sortSymbol[t,CHECK_DECLARED] { Expr var = PARSER_STATE->mkBoundVar(name, t); - cmd->reset(new DeclareSygusVarCommand(name, var, t)); + cmd.reset(new DeclareSygusVarCommand(name, var, t)); } | /* declare-primed-var */ DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); } @@ -582,106 +578,50 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] { // spurious command, we do not need to create a variable. We only keep // track of the command for sanity checking / dumping - cmd->reset(new DeclareSygusPrimedVarCommand(name, t)); + cmd.reset(new DeclareSygusPrimedVarCommand(name, t)); } | /* synth-fun */ ( SYNTH_FUN_V1_TOK { isInv = false; } | SYNTH_INV_V1_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } ) - { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK ( sortSymbol[range,CHECK_DECLARED] )? { - if (range.isNull()) - { - PARSER_STATE->parseError("Must supply return type for synth-fun."); - } - if (range.isFunction()) - { - PARSER_STATE->parseError( - "Cannot use synth-fun with function return type."); - } - std::vector<Type> var_sorts; - for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames) - { - var_sorts.push_back(p.second); - } - Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; - Type synth_fun_type = var_sorts.size() > 0 - ? EXPR_MANAGER->mkFunctionType(var_sorts, range) - : range; - // we do not allow overloading for synth fun - synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type); - // set the sygus type to be range by default, which is overwritten below - // if a grammar is provided - sygus_type = range; - // create new scope for parsing the grammar, if any - PARSER_STATE->pushScope(true); - sygus_vars = PARSER_STATE->mkBoundVars(sortedVarNames); + synthFunFactory.reset(new Smt2::SynthFunFactory( + PARSER_STATE, fun, isInv, range, sortedVarNames)); } ( // optionally, read the sygus grammar // - // the sygus type specifies the required grammar for synth_fun, expressed - // as a type - sygusGrammarV1[sygus_type, sygus_vars, fun] + // `grammar` specifies the required grammar for the function to + // synthesize, expressed as a type + sygusGrammarV1[grammar, synthFunFactory->getSygusVars(), fun] )? { - PARSER_STATE->popScope(); - Debug("parser-sygus") << "...read synth fun " << fun << std::endl; - cmd->reset( - new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars)); + cmd = synthFunFactory->mkCommand(grammar); } | /* synth-fun */ ( SYNTH_FUN_TOK { isInv = false; } | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); } ) - { PARSER_STATE->checkThatLogicIsSet(); } symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE] LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK ( sortSymbol[range,CHECK_DECLARED] )? { - if (range.isNull()) - { - PARSER_STATE->parseError("Must supply return type for synth-fun."); - } - if (range.isFunction()) - { - PARSER_STATE->parseError( - "Cannot use synth-fun with function return type."); - } - std::vector<Type> var_sorts; - for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames) - { - var_sorts.push_back(p.second); - } - Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; - Type synth_fun_type = var_sorts.size() > 0 - ? EXPR_MANAGER->mkFunctionType(var_sorts, range) - : range; - // we do not allow overloading for synth fun - synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type); - // set the sygus type to be range by default, which is overwritten below - // if a grammar is provided - sygus_type = range; - // create new scope for parsing the grammar, if any - PARSER_STATE->pushScope(true); - sygus_vars = PARSER_STATE->mkBoundVars(sortedVarNames); + synthFunFactory.reset(new Smt2::SynthFunFactory( + PARSER_STATE, fun, isInv, range, sortedVarNames)); } ( // optionally, read the sygus grammar // - // the sygus type specifies the required grammar for synth_fun, expressed - // as a type - sygusGrammar[sygus_type, sygus_vars, fun] + // `grammar` specifies the required grammar for the function to + // synthesize, expressed as a type + sygusGrammar[grammar, synthFunFactory->getSygusVars(), fun] )? { - PARSER_STATE->popScope(); - Debug("parser-sygus") << "...read synth fun " << fun << std::endl; - cmd->reset( - new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars)); + cmd = synthFunFactory->mkCommand(grammar); } | /* constraint */ CONSTRAINT_TOK { @@ -691,39 +631,21 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] } term[expr, expr2] { Debug("parser-sygus") << "...read constraint " << expr << std::endl; - cmd->reset(new SygusConstraintCommand(expr)); - } - | INV_CONSTRAINT_TOK { - PARSER_STATE->checkThatLogicIsSet(); - Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; - Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl; + cmd.reset(new SygusConstraintCommand(expr)); } - ( symbol[name,CHECK_NONE,SYM_VARIABLE] { - if( !terms.empty() ){ - if (!PARSER_STATE->isDeclared(name)) - { - std::stringstream ss; - ss << "Function " << name << " in inv-constraint is not defined."; - PARSER_STATE->parseError(ss.str()); - } - } - terms.push_back( PARSER_STATE->getVariable(name) ); - } - )+ { - if( terms.size()!=4 ){ - PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 " - "arguments."); - } - - cmd->reset(new SygusInvConstraintCommand(terms)); + | /* inv-constraint */ + INV_CONSTRAINT_TOK + ( symbol[name,CHECK_NONE,SYM_VARIABLE] { names.push_back(name); } )+ + { + cmd = PARSER_STATE->invConstraint(names); } | /* check-synth */ CHECK_SYNTH_TOK { PARSER_STATE->checkThatLogicIsSet(); } { - cmd->reset(new CheckSynthCommand()); + cmd.reset(new CheckSynthCommand()); } - | command[cmd] + | command[&cmd] ; /** Reads a sygus grammar @@ -736,8 +658,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] * datatypes constructed by this call. */ sygusGrammarV1[CVC4::Type & ret, - std::vector<CVC4::Expr>& sygus_vars, - std::string& fun] + const std::vector<CVC4::Expr>& sygus_vars, + const std::string& fun] @declarations { Type t; @@ -879,7 +801,7 @@ sygusGrammarV1[CVC4::Type & ret, // 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] +sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun] @declarations { std::string name, name2; Kind k; @@ -1013,8 +935,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun] * datatypes constructed by this call. */ sygusGrammar[CVC4::Type & ret, - std::vector<CVC4::Expr>& sygusVars, - std::string& fun] + const std::vector<CVC4::Expr>& sygusVars, + const std::string& fun] @declarations { // the pre-declaration |