From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Fri, 10 Dec 2021 18:44:10 +0000 (-0600)
Subject: Mute `define-fun` command generated for named terms. (#7788)
X-Git-Tag: cvc5-1.0.0~687
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=051a568564958be1433ff64a98808398c1f6e238;p=cvc5.git

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 8ecf3340f..fe401b369 100644
--- 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 a51a81b19..fda388832 100644
--- 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
index 000000000..7026298c6
--- /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))