*/
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
;
}
;
-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(); }
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(); }
{
// 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 {
}
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
* 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;
// 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;
* 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
}
}
+Smt2::SynthFunFactory::SynthFunFactory(
+ Smt2* smt2,
+ const std::string& fun,
+ bool isInv,
+ Type range,
+ std::vector<std::pair<std::string, CVC4::Type>>& 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<Type> varSorts;
+ for (const std::pair<std::string, CVC4::Type>& 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<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
+{
+ Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
+ return std::unique_ptr<Command>(
+ new SynthFunCommand(d_fun,
+ d_synthFun,
+ grammar.isNull() ? d_sygusType : grammar,
+ d_isInv,
+ d_sygusVars));
+}
+
+std::unique_ptr<Command> Smt2::invConstraint(
+ const std::vector<std::string>& 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<Expr> 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<Command>(new SygusInvConstraintCommand(terms));
+}
+
Command* Smt2::setLogic(std::string name, bool fromCommand)
{
if (fromCommand)
// 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<CVC4::Expr> >& ops,
- std::vector< std::vector<std::string> >& 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<CVC4::Expr>& 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<CVC4::Datatype>& datatypes,
+ std::vector<CVC4::Type>& sorts,
+ std::vector<std::vector<CVC4::Expr>>& ops,
+ std::vector<std::vector<std::string>>& cnames,
+ std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<bool>& allow_const,
+ std::vector<std::vector<std::string>>& unresolved_gterm_sym,
+ const std::vector<CVC4::Expr>& 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)
+{
if (sgt.d_gterm_type == SygusGTerm::gterm_op)
{
Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
return t;
}
-void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
- std::vector< CVC4::Datatype >& datatypes,
- std::vector< CVC4::Type>& sorts,
- std::vector< std::vector<CVC4::Expr> >& ops ) {
+void Smt2::setSygusStartIndex(const std::string& fun,
+ int startIndex,
+ std::vector<CVC4::Datatype>& datatypes,
+ std::vector<CVC4::Type>& sorts,
+ std::vector<std::vector<CVC4::Expr>>& ops)
+{
if( startIndex>0 ){
CVC4::Datatype tmp_dt = datatypes[0];
Type tmp_sort = sorts[0];
}
void Smt2::addSygusConstructorVariables(Datatype& dt,
- std::vector<Expr>& sygusVars,
+ const std::vector<Expr>& sygusVars,
Type type) const
{
// each variable of appropriate type becomes a sygus constructor in dt.
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<std::pair<std::string, CVC4::Type>>& sortedVarNames);
+ ~SynthFunFactory();
+
+ const std::vector<Expr>& 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<Command> mkCommand(Type grammar);
+
+ private:
+ Smt2* d_smt2;
+ std::string d_fun;
+ Expr d_synthFun;
+ Type d_sygusType;
+ bool d_isInv;
+ std::vector<Expr> 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<Command> invConstraint(const std::vector<std::string>& names);
+
/**
* Sets the logic for the current benchmark. Declares any logic and
* theory symbols.
void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
- void processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
- std::vector< CVC4::Datatype >& datatypes,
- std::vector< CVC4::Type>& sorts,
- std::vector< std::vector<CVC4::Expr> >& ops,
- std::vector< std::vector<std::string> >& 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<CVC4::Expr>& 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<CVC4::Datatype>& datatypes,
+ std::vector<CVC4::Type>& sorts,
+ std::vector<std::vector<CVC4::Expr>>& ops,
+ std::vector<std::vector<std::string>>& cnames,
+ std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+ std::vector<bool>& allow_const,
+ std::vector<std::vector<std::string>>& unresolved_gterm_sym,
+ const std::vector<CVC4::Expr>& 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);
static bool pushSygusDatatypeDef( Type t, std::string& dname,
std::vector< CVC4::Datatype >& datatypes,
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<CVC4::Expr> >& ops );
+ void setSygusStartIndex(const std::string& fun,
+ int startIndex,
+ std::vector<CVC4::Datatype>& datatypes,
+ std::vector<CVC4::Type>& sorts,
+ std::vector<std::vector<CVC4::Expr>>& ops);
void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
* term (Variable type) is encountered.
*/
void addSygusConstructorVariables(Datatype& dt,
- std::vector<Expr>& sygusVars,
+ const std::vector<Expr>& sygusVars,
Type type) const;
/**
projects / cvc5.git / commitdiff