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 ed218832c6f4c22492b826ec101b340c4587cb07..42b1f72c770c5b3fda1848c476660bf60cebc8ac 100644 (file)
--- 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) {