From ce593db9ebb3d7e2bfb196ec968ebc1d15f17201 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 5 Oct 2017 09:11:03 -0500 Subject: [PATCH] Minor change to how SyGus commands are translated to SmtEngine commands. This ensures a single success is printed for synth-fun and synth-inv. (#1193) --- src/parser/smt2/Smt2.g | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 3deffe703..29f507238 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -626,6 +626,9 @@ sygusCommand [std::unique_ptr* cmd] } // allow overloading for synth fun synth_fun = PARSER_STATE->mkVar(fun, synth_fun_type, ExprManager::VAR_FLAG_NONE, true); + // we add a declare function command here + // this is the single unmuted command in the sequence generated by this smt2 command + seq->addCommand(new DeclareFunctionCommand(fun, synth_fun, synth_fun_type)); PARSER_STATE->pushScope(true); for(std::vector >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; @@ -736,7 +739,10 @@ sygusCommand [std::unique_ptr* cmd] } std::vector datatypeTypes = PARSER_STATE->mkMutualDatatypeTypes(datatypes); - seq->addCommand(new DatatypeDeclarationCommand(datatypeTypes)); + Command * cdd = new DatatypeDeclarationCommand(datatypeTypes); + // we set this command muted since there should only be one success printed + cdd->setMuted(true); + seq->addCommand(cdd); if( sorts[0]!=range ){ PARSER_STATE->parseError(std::string("Bad return type in grammar for " "SyGuS function ") + fun); -- 2.30.2