[ExportSMTLIB] Fix printing of too many closing parentheses

The number of open parentheses should not be propagated to quantifier bodies and the first child expression of 'let' which declares the bound variable
llvm · Apr 20, 2024 · 3a08dce · 3a08dce
1 parent b4b4a7b
commit 3a08dce
Show file tree

Hide file tree

Showing 4 changed files with 28 additions and 5 deletions.
diff --git a/integration_test/Target/ExportSMTLIB/attributes.mlir b/integration_test/Target/ExportSMTLIB/attributes.mlir
@@ -20,4 +20,4 @@ smt.solver () : () -> () {
 // CHECK-NOT: ERROR
 // CHECK-NOT: error
 // CHECK-NOT: unsat
-// CHECK: sat
+// CHECK: sat
diff --git a/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp b/lib/Target/ExportSMTLIB/ExportSMTLIB.cpp
@@ -158,7 +158,7 @@ struct ExpressionVisitor
     info.stream << "(let ((" << name << " ";
 
     VisitorInfo newInfo(info.stream, info.valueMap,
-                        info.indentLevel + 7 + name.size(), info.openParens);
+                        info.indentLevel + 8 + name.size(), 0);
     if (failed(Base::dispatchSMTOpVisitor(op, newInfo)))
       return failure();
 
@@ -332,14 +332,14 @@ struct ExpressionVisitor
     worklist.push_back(yieldedValue);
     unsigned indentExt = operatorString.size() + 2;
     VisitorInfo newInfo(info.stream, info.valueMap,
-                        info.indentLevel + indentExt, info.openParens);
+                        info.indentLevel + indentExt, 0);
     newInfo.stream.indent(newInfo.indentLevel);
     if (failed(printExpression(worklist, newInfo)))
       return failure();
 
     info.stream << info.valueMap.lookup(yieldedValue);
 
-    for (int j = 0; j < newInfo.openParens; ++j)
+    for (unsigned j = 0; j < newInfo.openParens; ++j)
       info.stream << ")";
 
     if (weight != 0)

diff --git a/test/Target/ExportSMTLIB/attributes.mlir b/test/Target/ExportSMTLIB/attributes.mlir
@@ -52,4 +52,4 @@ smt.solver () : () -> () {
 
   // CHECK: (reset)
   // CHECK-INLINED: (reset)
-}
+}
diff --git a/test/Target/ExportSMTLIB/core.mlir b/test/Target/ExportSMTLIB/core.mlir
@@ -89,6 +89,29 @@ smt.solver () : () -> () {
   }
   smt.assert %2
 
+  // Test: make sure that open parens from outside quantifier bodies are not
+  // propagated into the body.
+  // CHECK: (assert (let (([[V15:.+]] (exists (([[V16:.+]] Int) ([[V17:.+]] Int)){{$}}
+  // CHECK:                                   (let (([[V18:.+]] (= [[V16]] [[V17]]))){{$}}
+  // CHECK:                                   [[V18]])))){{$}}
+  // CHECK:         (let (([[V19:.+]] (exists (([[V20:.+]] Int) ([[V21:.+]] Int)){{$}}
+  // CHECK:                                   (let (([[V22:.+]] (= [[V20]] [[V21]]))){{$}}
+  // CHECK:                                   [[V22]])))){{$}}
+  // CHECK:         (let (([[V23:.+]] (and [[V19]] [[V15]]))){{$}}
+  // CHECK:         [[V23]])))){{$}}
+  %3 = smt.exists {
+  ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+    %5 = smt.eq %arg2, %arg3 : !smt.int
+    smt.yield %5 : !smt.bool
+  }
+  %5 = smt.exists {
+  ^bb0(%arg2: !smt.int, %arg3: !smt.int):
+    %6 = smt.eq %arg2, %arg3 : !smt.int
+    smt.yield %6 : !smt.bool
+  }
+  %6 = smt.and %3, %5
+  smt.assert %6
+
   // CHECK: (check-sat)
   // CHECK-INLINED: (check-sat)
   smt.check sat {} unknown {} unsat {}
-Original file line number
+Diff line change
@@ Expand Up / @@ -52,4 +52,4 @@ smt.solver () : () -> () { @@
       // CHECK: (reset)
       // CHECK-INLINED: (reset)
-    }
+    }