diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-25 10:57:26 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-25 10:57:26 -0700 |
| commit | 4d87f13c473d8c8b9fc47b7823157ea8c57d3f89 (patch) | |
| tree | 56c3331f60b96bed9f4beb9b5a7b30f979371cf3 /src/printer/cvc | |
| parent | 5f997ea7363bd29ae53b57051ebac8d1da8f9439 (diff) | |
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();
```
Diffstat (limited to 'src/printer/cvc')
| -rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 11 |
1 files changed, 9 insertions, 2 deletions
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) { |