diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-05 09:11:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-10-05 09:11:03 -0500 |
| commit | ce593db9ebb3d7e2bfb196ec968ebc1d15f17201 (patch) | |
| tree | b60f48a2f08f0aac8d6fb14723c5ff9d2edc6b4b /src/parser/smt2/Smt2.g | |
| parent | f56f46f5bb5845cff0c329926f51a0377379365b (diff) | |
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)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
| -rw-r--r-- | src/parser/smt2/Smt2.g | 8 |
1 files changed, 7 insertions, 1 deletions
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<CVC4::Command>* 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<std::pair<std::string, CVC4::Type> >::const_iterator i = sortedVarNames.begin(), iend = sortedVarNames.end(); i != iend; @@ -736,7 +739,10 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd] } std::vector<DatatypeType> 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); |