From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 25 Jun 2018 17:57:26 +0000 (-0700)
Subject: Remove parentheses for prefix ops without args (#2082)
X-Git-Tag: cvc5-1.0.0~4959
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4d87f13c473d8c8b9fc47b7823157ea8c57d3f89;p=cvc5.git

Remove parentheses for prefix ops without args (#2082)

In the CVC printer, function definitions without arguments are printed
like constants but when actually using that function we were printing in
the form of `x()`.

For example:

```
(set-logic QF_BV)
(define-fun x1480 () Bool true)
(define-fun x2859 () Bool true)
(define-fun x2387 () Bool x2859)
(check-sat)
```

Was dumped as:

```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```

This commit removes these parentheses when prefix functions with zero arguments
are printed, so the example above becomes:

```
OPTION "incremental" false;
OPTION "logic" "QF_BV";
x1480 : BOOLEAN = TRUE;
x2859 : BOOLEAN = TRUE;
x2387 : BOOLEAN = x2859();
```
---

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index ed218832c..42b1f72c7 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -914,7 +914,11 @@ void CvcPrinter::toStream(
 
   switch (opType) {
   case PREFIX:
-    out << op.str() << '(';
+    out << op.str();
+    if (n.getNumChildren() > 0)
+    {
+      out << '(';
+    }
     break;
   case INFIX:
     if (bracket) {
@@ -939,7 +943,10 @@ void CvcPrinter::toStream(
 
   switch (opType) {
     case PREFIX:
-      out << ')';
+      if (n.getNumChildren() > 0)
+      {
+        out << ')';
+      }
       break;
     case INFIX:
       if (bracket) {