Mute `define-fun` command generated for named terms. (#7788)

Kind 2 uses print-success option to track cvc5's status after each command. When I added implicit define-fun commands for each named term (needed for raw-benchmark), cvc5 started printing spurious ; success messages. This change ended up crashing Kind 2's driver for cvc5. This PR fixes this issue by muting the results of those implicit define-fun commands.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 8ecf3340f73f5b521d4e3f797d8d7e7461e423a6..fe401b3697de92b4d7416e4e3a93af0e02b08408 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1794,8 +1794,10 @@ attribute[cvc5::api::Term& expr, cvc5::api::Term& retExpr]
   | ATTRIBUTE_NAMED_TOK symbol[s,CHECK_UNDECLARED,SYM_VARIABLE]
     {
       // notify that expression was given a name
-      PARSER_STATE->preemptCommand(
-          new DefineFunctionCommand(s, expr.getSort(), expr));
+      DefineFunctionCommand* defFunCmd =
+          new DefineFunctionCommand(s, expr.getSort(), expr);
+      defFunCmd->setMuted(true);
+      PARSER_STATE->preemptCommand(defFunCmd);
       PARSER_STATE->notifyNamedExpression(expr, s);
     }
   ;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a51a81b195b62a835122190b4d29ae8105bdae7d..fda3888322bd5e0d06bae38379ec671bfdcf8c17 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -787,6 +787,7 @@ set(regress_0_tests
   regress0/options/didyoumean.smt2
   regress0/options/help.smt2
   regress0/options/interactive-mode.smt2
+  regress0/options/named_muted.smt2
   regress0/options/set-after-init.smt2
   regress0/options/set-and-get-options.smt2
   regress0/options/statistics.smt2

diff --git a/test/regress/regress0/options/named_muted.smt2 b/test/regress/regress0/options/named_muted.smt2
new file mode 100644 (file)
index 0000000..7026298
--- /dev/null
+++ b/test/regress/regress0/options/named_muted.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --print-success
+; EXPECT: success
+; EXPECT: success
+
+(set-logic UF)
+(assert (! true :named t))