Expression printer (#48)

* Expression printer

Author: Saloed

ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaExprConverter.kt

@@ -6,6 +6,7 @@ import org.ksmt.decl.KFuncDecl
 import org.ksmt.expr.KBitVecValue
 import org.ksmt.expr.KExpr
 import org.ksmt.expr.KFpRoundingMode
+import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KNonRecursiveTransformer
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaBitVector
@@ -741,10 +742,10 @@ open class KBitwuzlaExprConverter(
         override val sort: KBv1Sort
             get() = ctx.bv1Sort
 
-        override fun print(builder: StringBuilder) {
-            builder.append("(toBV1 ")
-            arg.print(builder)
-            builder.append(')')
+        override fun print(printer: ExpressionPrinter) = with(printer) {
+            append("(toBV1 ")
+            append(arg)
+            append(")")
         }
 
         override fun accept(transformer: KTransformerBase): KExpr<KBv1Sort> {
@@ -757,10 +758,10 @@ open class KBitwuzlaExprConverter(
         override val sort: KBoolSort
             get() = ctx.boolSort
 
-        override fun print(builder: StringBuilder) {
-            builder.append("(toBool ")
-            arg.print(builder)
-            builder.append(')')
+        override fun print(printer: ExpressionPrinter) = with(printer) {
+            append("(toBool ")
+            append(arg)
+            append(")")
         }
 
         override fun accept(transformer: KTransformerBase): KExpr<KBoolSort> {
@@ -777,12 +778,12 @@ open class KBitwuzlaExprConverter(
         override val sort: KArraySort<ToDomain, ToRange>
             get() = ctx.mkArraySort(toDomainSort, toRangeSort)
 
-        override fun print(builder: StringBuilder) {
-            builder.append("(toArray ")
-            sort.print(builder)
-            builder.append(' ')
-            arg.print(builder)
-            builder.append(')')
+        override fun print(printer: ExpressionPrinter) = with(printer) {
+            append("(toArray ")
+            append("$sort")
+            append(" ")
+            append(arg)
+            append(")")
         }
 
         override fun accept(transformer: KTransformerBase): KExpr<KArraySort<ToDomain, ToRange>> {

ksmt-core/src/main/kotlin/org/ksmt/expr/Array.kt

@@ -4,6 +4,7 @@ import org.ksmt.KContext
 import org.ksmt.decl.KArrayConstDecl
 import org.ksmt.decl.KDecl
 import org.ksmt.decl.KFuncDecl
+import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.KArraySort
 import org.ksmt.sort.KSort
@@ -89,10 +90,10 @@ class KFunctionAsArray<D : KSort, R : KSort> internal constructor(
     override val sort: KArraySort<D, R>
         get() = ctx.mkArraySort(domainSort, function.sort)
 
-    override fun print(builder: StringBuilder): Unit = with(builder) {
+    override fun print(printer: ExpressionPrinter): Unit = with(printer) {
         append("(asArray ")
         append(function.name)
-        append(')')
+        append(")")
     }
 
     override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)
@@ -108,17 +109,20 @@ class KArrayLambda<D : KSort, R : KSort> internal constructor(
     val body: KExpr<R>
 ) : KExpr<KArraySort<D, R>>(ctx) {
 
-    override fun print(builder: StringBuilder): Unit = with(builder) {
-        append("(lambda ((")
-        append(indexVarDecl.name)
-        append(' ')
+    override fun print(printer: ExpressionPrinter) {
+        val str = buildString {
+            append("(lambda ((")
+            append(indexVarDecl.name)
+            append(' ')
 
-        indexVarDecl.sort.print(this)
-        append(")) ")
+            indexVarDecl.sort.print(this)
+            append(")) ")
 
-        body.print(this)
+            body.print(this)
 
-        append(')')
+            append(')')
+        }
+        printer.append(str)
     }
 
     override fun accept(transformer: KTransformerBase): KExpr<KArraySort<D, R>> = transformer.transform(this)

ksmt-core/src/main/kotlin/org/ksmt/expr/KApp.kt

@@ -2,6 +2,8 @@ package org.ksmt.expr
 
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
+import org.ksmt.decl.KParameterizedFuncDecl
+import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.KSort
 
@@ -14,22 +16,33 @@ abstract class KApp<T : KSort, A : KExpr<*>> internal constructor(ctx: KContext)
     @Deprecated("Use property", ReplaceWith("decl"))
     fun decl(): KDecl<T> = decl
 
-    override fun print(builder: StringBuilder): Unit = with(ctx) {
-        with(builder) {
+    override fun print(printer: ExpressionPrinter) {
+        with(printer) {
             if (args.isEmpty()) {
-                append(decl.name)
+                append(decl)
                 return
             }
 
-            append('(')
-            append(decl.name)
+            append("(")
+            append(decl)
 
             for (arg in args) {
-                append(' ')
-                arg.print(this)
+                append(" ")
+                append(arg)
             }
 
-            append(')')
+            append(")")
+        }
+    }
+
+    private fun ExpressionPrinter.append(decl: KDecl<*>) {
+        append(decl.name)
+        if (decl is KParameterizedFuncDecl) {
+            append(" (_")
+            for (param in decl.parameters) {
+                append(" $param")
+            }
+            append(")")
         }
     }
 }

ksmt-core/src/main/kotlin/org/ksmt/expr/KExpr.kt

@@ -2,8 +2,10 @@ package org.ksmt.expr
 
 import org.ksmt.KAst
 import org.ksmt.KContext
+import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.expr.transformer.KTransformerBase
 import org.ksmt.sort.KSort
+import org.ksmt.expr.printer.ExpressionPrinterWithLetBindings
 
 abstract class KExpr<T : KSort>(ctx: KContext) : KAst(ctx) {
 
@@ -31,4 +33,10 @@ abstract class KExpr<T : KSort>(ctx: KContext) : KAst(ctx) {
      * @see [computeExprSort]
      * */
     open fun sortComputationExprDependency(dependency: MutableList<KExpr<*>>) {}
+
+    override fun print(builder: StringBuilder) {
+        ExpressionPrinterWithLetBindings().print(this, builder)
+    }
+
+    abstract fun print(printer: ExpressionPrinter)
 }

ksmt-core/src/main/kotlin/org/ksmt/expr/KQuantifier.kt

@@ -2,6 +2,7 @@ package org.ksmt.expr
 
 import org.ksmt.KContext
 import org.ksmt.decl.KDecl
+import org.ksmt.expr.printer.ExpressionPrinter
 import org.ksmt.sort.KBoolSort
 
 abstract class KQuantifier(
@@ -14,21 +15,25 @@ abstract class KQuantifier(
 
     abstract fun printQuantifierName(): String
 
-    override fun print(builder: StringBuilder): Unit = with(builder) {
-        append('(')
-        append(printQuantifierName())
-        append('(')
-
-        bounds.forEach { bound ->
+    override fun print(printer: ExpressionPrinter) {
+        val str = buildString {
+            append('(')
+            append(printQuantifierName())
             append('(')
-            append(bound.name)
-            append(' ')
-            bound.sort.print(this)
+
+            bounds.forEach { bound ->
+                append('(')
+                append(bound.name)
+                append(' ')
+                bound.sort.print(this)
+                append(')')
+            }
+
+            appendLine(')')
+            body.print(this)
+            appendLine()
             append(')')
         }
-
-        append(')')
-        body.print(this)
-        append(')')
+        printer.append(str)
     }
 }

ksmt-core/src/main/kotlin/org/ksmt/expr/printer/ExpressionPrinter.kt

@@ -0,0 +1,15 @@
+package org.ksmt.expr.printer
+
+import org.ksmt.expr.KExpr
+
+interface ExpressionPrinter {
+    /**
+     * Append string as in StringBuilder.
+     * */
+    fun append(str: String)
+
+    /**
+     * Append an expression.
+     * */
+    fun append(expr: KExpr<*>)
+}