From: Andres Noetzli Date: Thu, 3 Oct 2019 17:19:12 +0000 (-0700) Subject: [SMT2 Parser] Move code of `sygusCommand` (#3335) X-Git-Tag: cvc5-1.0.0~3919 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=51181eb3382ae9c94f90a39103e33ec6e9063dee;p=cvc5.git [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. --- 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 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* cmd] } ; -sygusCommand [std::unique_ptr* cmd] +sygusCommand returns [std::unique_ptr cmd] @declarations { - std::string name, fun; - std::vector names; Expr expr, expr2; Type t, range; - std::vector terms; - std::vector sygus_vars; + std::vector names; std::vector > sortedVarNames; - Type sygus_ret; - Expr synth_fun; - Type sygus_type; + std::unique_ptr 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* 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* 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 var_sorts; - for (const std::pair& 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 var_sorts; - for (const std::pair& 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* 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* cmd] * datatypes constructed by this call. */ sygusGrammarV1[CVC4::Type & ret, - std::vector& sygus_vars, - std::string& fun] + const std::vector& 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& sygusVars, - std::string& fun] + const std::vector& sygusVars, + const std::string& fun] @declarations { // the pre-declaration diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index bb0881030..ec4fd0fa3 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -627,6 +627,87 @@ void Smt2::resetAssertions() { } } +Smt2::SynthFunFactory::SynthFunFactory( + Smt2* smt2, + const std::string& fun, + bool isInv, + Type range, + std::vector>& sortedVarNames) + : d_smt2(smt2), d_fun(fun), d_isInv(isInv) +{ + smt2->checkThatLogicIsSet(); + if (range.isNull()) + { + smt2->parseError("Must supply return type for synth-fun."); + } + if (range.isFunction()) + { + smt2->parseError("Cannot use synth-fun with function return type."); + } + std::vector varSorts; + for (const std::pair& p : sortedVarNames) + { + varSorts.push_back(p.second); + } + Debug("parser-sygus") << "Define synth fun : " << fun << std::endl; + Type synthFunType = + varSorts.size() > 0 + ? d_smt2->getExprManager()->mkFunctionType(varSorts, range) + : range; + + // we do not allow overloading for synth fun + d_synthFun = d_smt2->mkBoundVar(fun, synthFunType); + // set the sygus type to be range by default, which is overwritten below + // if a grammar is provided + d_sygusType = range; + + d_smt2->pushScope(true); + d_sygusVars = d_smt2->mkBoundVars(sortedVarNames); +} + +Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); } + +std::unique_ptr Smt2::SynthFunFactory::mkCommand(Type grammar) +{ + Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl; + return std::unique_ptr( + new SynthFunCommand(d_fun, + d_synthFun, + grammar.isNull() ? d_sygusType : grammar, + d_isInv, + d_sygusVars)); +} + +std::unique_ptr Smt2::invConstraint( + const std::vector& names) +{ + checkThatLogicIsSet(); + Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl; + Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl; + + if (names.size() != 4) + { + parseError( + "Bad syntax for inv-constraint: expected 4 " + "arguments."); + } + + std::vector terms; + for (const std::string& name : names) + { + if (!isDeclared(name)) + { + std::stringstream ss; + ss << "Function " << name << " in inv-constraint is not defined."; + parseError(ss.str()); + } + + terms.push_back(getVariable(name)); + } + + return std::unique_ptr(new SygusInvConstraintCommand(terms)); +} + Command* Smt2::setLogic(std::string name, bool fromCommand) { if (fromCommand) @@ -868,17 +949,22 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector& o // 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. -void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops, - std::vector< std::vector >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::vector& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, - CVC4::Type& ret, bool isNested ){ +void Smt2::processSygusGTerm( + CVC4::SygusGTerm& sgt, + int index, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops, + std::vector>& cnames, + std::vector>>& cargs, + std::vector& allow_const, + std::vector>& unresolved_gterm_sym, + const std::vector& sygus_vars, + std::map& sygus_to_builtin, + std::map& sygus_to_builtin_expr, + CVC4::Type& ret, + bool isNested) +{ if (sgt.d_gterm_type == SygusGTerm::gterm_op) { Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index @@ -1103,10 +1189,12 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st return t; } -void Smt2::setSygusStartIndex( std::string& fun, int startIndex, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops ) { +void Smt2::setSygusStartIndex(const std::string& fun, + int startIndex, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops) +{ if( startIndex>0 ){ CVC4::Datatype tmp_dt = datatypes[0]; Type tmp_sort = sorts[0]; @@ -1420,7 +1508,7 @@ Expr Smt2::purifySygusGTerm(Expr term, } void Smt2::addSygusConstructorVariables(Datatype& dt, - std::vector& sygusVars, + const std::vector& sygusVars, Type type) const { // each variable of appropriate type becomes a sygus constructor in dt. diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 178634693..5caedb934 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -197,6 +197,60 @@ class Smt2 : public Parser void resetAssertions(); + /** + * Class for creating instances of `SynthFunCommand`s. Creating an instance + * of this class pushes the scope, destroying it pops the scope. + */ + class SynthFunFactory + { + public: + /** + * Creates an instance of `SynthFunFactory`. + * + * @param smt2 Pointer to the parser state + * @param fun Name of the function to synthesize + * @param isInv True if the goal is to synthesize an invariant, false + * otherwise + * @param range The return type of the function-to-synthesize + * @param sortedVarNames The parameters of the function-to-synthesize + */ + SynthFunFactory( + Smt2* smt2, + const std::string& fun, + bool isInv, + Type range, + std::vector>& sortedVarNames); + ~SynthFunFactory(); + + const std::vector& getSygusVars() const { return d_sygusVars; } + + /** + * Create an instance of `SynthFunCommand`. + * + * @param grammar Optional grammar associated with the synth-fun command + * @return The instance of `SynthFunCommand` + */ + std::unique_ptr mkCommand(Type grammar); + + private: + Smt2* d_smt2; + std::string d_fun; + Expr d_synthFun; + Type d_sygusType; + bool d_isInv; + std::vector d_sygusVars; + }; + + /** + * Creates a command that adds an invariant constraint. + * + * @param names Name of four symbols corresponding to the + * function-to-synthesize, precondition, postcondition, + * transition relation. + * @return The command that adds an invariant constraint + */ + std::unique_ptr invConstraint(const std::vector& names); + /** * Sets the logic for the current benchmark. Declares any logic and * theory symbols. @@ -295,17 +349,21 @@ class Smt2 : public Parser void mkSygusConstantsForType( const Type& type, std::vector& ops ); - void processSygusGTerm( CVC4::SygusGTerm& sgt, int index, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops, - std::vector< std::vector >& cnames, - std::vector< std::vector< std::vector< CVC4::Type > > >& cargs, - std::vector< bool >& allow_const, - std::vector< std::vector< std::string > >& unresolved_gterm_sym, - std::vector& sygus_vars, - std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr, - CVC4::Type& ret, bool isNested = false ); + void processSygusGTerm( + CVC4::SygusGTerm& sgt, + int index, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops, + std::vector>& cnames, + std::vector>>& cargs, + std::vector& allow_const, + std::vector>& unresolved_gterm_sym, + const std::vector& sygus_vars, + std::map& sygus_to_builtin, + std::map& sygus_to_builtin_expr, + CVC4::Type& ret, + bool isNested = false); static bool pushSygusDatatypeDef( Type t, std::string& dname, std::vector< CVC4::Datatype >& datatypes, @@ -324,10 +382,11 @@ class Smt2 : public Parser std::vector< bool >& allow_const, std::vector< std::vector< std::string > >& unresolved_gterm_sym ); - void setSygusStartIndex( std::string& fun, int startIndex, - std::vector< CVC4::Datatype >& datatypes, - std::vector< CVC4::Type>& sorts, - std::vector< std::vector >& ops ); + void setSygusStartIndex(const std::string& fun, + int startIndex, + std::vector& datatypes, + std::vector& sorts, + std::vector>& ops); void mkSygusDatatype( CVC4::Datatype& dt, std::vector& ops, std::vector& cnames, std::vector< std::vector< CVC4::Type > >& cargs, @@ -356,7 +415,7 @@ class Smt2 : public Parser * term (Variable type) is encountered. */ void addSygusConstructorVariables(Datatype& dt, - std::vector& sygusVars, + const std::vector& sygusVars, Type type) const; /**