From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 5 Oct 2017 14:11:03 +0000 (-0500)
Subject: Minor change to how SyGus commands are translated to SmtEngine commands. This ensures... 
X-Git-Tag: cvc5-1.0.0~5575
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ce593db9ebb3d7e2bfb196ec968ebc1d15f17201;p=cvc5.git

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)
---

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);