String theory support

ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaContext.kt

@@ -18,6 +18,7 @@ import io.ksmt.expr.KFunctionAsArray
 import io.ksmt.expr.KUniversalQuantifier
 import io.ksmt.expr.transformer.KNonRecursiveTransformer
 import io.ksmt.solver.KSolverException
+import io.ksmt.solver.KSolverUnsupportedFeatureException
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaNativeException
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaSort
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaTerm
@@ -34,6 +35,8 @@ import io.ksmt.sort.KFpRoundingModeSort
 import io.ksmt.sort.KFpSort
 import io.ksmt.sort.KIntSort
 import io.ksmt.sort.KRealSort
+import io.ksmt.sort.KStringSort
+import io.ksmt.sort.KRegexSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KSortVisitor
 import io.ksmt.sort.KUninterpretedSort
@@ -362,6 +365,12 @@ open class KBitwuzlaContext(val ctx: KContext) : AutoCloseable {
         override fun visit(sort: KRealSort) {
         }
 
+        override fun visit(sort: KStringSort) {
+        }
+
+        override fun visit(sort: KRegexSort) {
+        }
+
         override fun <S : KBvSort> visit(sort: S) {
         }
 

ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaExprInternalizer.kt

@@ -151,6 +151,48 @@ import io.ksmt.expr.KUnaryMinusArithExpr
 import io.ksmt.expr.KUninterpretedSortValue
 import io.ksmt.expr.KUniversalQuantifier
 import io.ksmt.expr.KXorExpr
+import io.ksmt.expr.KStringConcatExpr
+import io.ksmt.expr.KStringLenExpr
+import io.ksmt.expr.KStringToRegexExpr
+import io.ksmt.expr.KStringInRegexExpr
+import io.ksmt.expr.KStringSuffixOfExpr
+import io.ksmt.expr.KStringPrefixOfExpr
+import io.ksmt.expr.KStringLtExpr
+import io.ksmt.expr.KStringLeExpr
+import io.ksmt.expr.KStringGtExpr
+import io.ksmt.expr.KStringGeExpr
+import io.ksmt.expr.KStringContainsExpr
+import io.ksmt.expr.KStringSingletonSubExpr
+import io.ksmt.expr.KStringSubExpr
+import io.ksmt.expr.KStringIndexOfExpr
+import io.ksmt.expr.KStringIndexOfRegexExpr
+import io.ksmt.expr.KStringReplaceExpr
+import io.ksmt.expr.KStringReplaceAllExpr
+import io.ksmt.expr.KStringReplaceWithRegexExpr
+import io.ksmt.expr.KStringReplaceAllWithRegexExpr
+import io.ksmt.expr.KStringToLowerExpr
+import io.ksmt.expr.KStringToUpperExpr
+import io.ksmt.expr.KStringReverseExpr
+import io.ksmt.expr.KStringIsDigitExpr
+import io.ksmt.expr.KStringToCodeExpr
+import io.ksmt.expr.KStringFromCodeExpr
+import io.ksmt.expr.KStringToIntExpr
+import io.ksmt.expr.KStringFromIntExpr
+import io.ksmt.expr.KStringLiteralExpr
+import io.ksmt.expr.KRegexConcatExpr
+import io.ksmt.expr.KRegexUnionExpr
+import io.ksmt.expr.KRegexIntersectionExpr
+import io.ksmt.expr.KRegexStarExpr
+import io.ksmt.expr.KRegexCrossExpr
+import io.ksmt.expr.KRegexDifferenceExpr
+import io.ksmt.expr.KRegexComplementExpr
+import io.ksmt.expr.KRegexOptionExpr
+import io.ksmt.expr.KRegexRangeExpr
+import io.ksmt.expr.KRegexPowerExpr
+import io.ksmt.expr.KRegexLoopExpr
+import io.ksmt.expr.KRegexEpsilon
+import io.ksmt.expr.KRegexAll
+import io.ksmt.expr.KRegexAllChar
 import io.ksmt.expr.rewrite.simplify.rewriteBvAddNoUnderflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvMulNoUnderflowExpr
 import io.ksmt.expr.rewrite.simplify.rewriteBvNegNoOverflowExpr
@@ -183,6 +225,8 @@ import io.ksmt.sort.KFpRoundingModeSort
 import io.ksmt.sort.KFpSort
 import io.ksmt.sort.KIntSort
 import io.ksmt.sort.KRealSort
+import io.ksmt.sort.KStringSort
+import io.ksmt.sort.KRegexSort
 import io.ksmt.sort.KSort
 import io.ksmt.sort.KSortVisitor
 import io.ksmt.sort.KUninterpretedSort
@@ -1405,6 +1449,174 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
         )
     }
 
+    override fun transform(expr: KStringConcatExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringLenExpr): KExpr<KIntSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringToRegexExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringInRegexExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringSuffixOfExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringPrefixOfExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringLtExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringLeExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringGtExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringGeExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringContainsExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringSingletonSubExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringSubExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringIndexOfExpr): KExpr<KIntSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringIndexOfRegexExpr): KExpr<KIntSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringReplaceExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringReplaceAllExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringReplaceWithRegexExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringReplaceAllWithRegexExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringToLowerExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringToUpperExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringReverseExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringIsDigitExpr): KExpr<KBoolSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringToCodeExpr): KExpr<KIntSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringFromCodeExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringToIntExpr): KExpr<KIntSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringFromIntExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string and int theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KStringLiteralExpr): KExpr<KStringSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexConcatExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexUnionExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexIntersectionExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexStarExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexCrossExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexDifferenceExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexComplementExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexOptionExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexRangeExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexPowerExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexLoopExpr): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexEpsilon): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexAll): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
+    override fun transform(expr: KRegexAllChar): KExpr<KRegexSort> {
+        throw KSolverUnsupportedFeatureException("string theory is not supported in Bitwuzla")
+    }
+
     private inline fun <T : KQuantifier> T.internalizeQuantifier(
         crossinline mkQuantifierTerm: (LongArray) -> BitwuzlaTerm
     ): T {
@@ -1554,14 +1766,20 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
         }
 
         /**
-         * Bitwuzla doesn't support integers and reals.
+         * Bitwuzla doesn't support strings, regular expressions, integers and reals.
          * */
         override fun visit(sort: KIntSort) =
             throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
 
         override fun visit(sort: KRealSort) =
             throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
 
+        override fun visit(sort: KStringSort) =
+            throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
+
+        override fun visit(sort: KRegexSort) =
+            throw KSolverUnsupportedFeatureException("Unsupported sort $sort")
+
         /**
          * Replace Uninterpreted sorts with (BitVec 32).
          * The sort universe size is limited by 2^32 values which should be enough.
@@ -1704,6 +1922,8 @@ open class KBitwuzlaExprInternalizer(val bitwuzlaCtx: KBitwuzlaContext) : KExprL
         override fun visit(sort: KBoolSort): Boolean = false
         override fun visit(sort: KIntSort): Boolean = false
         override fun visit(sort: KRealSort): Boolean = false
+        override fun visit(sort: KStringSort): Boolean = false
+        override fun visit(sort: KRegexSort): Boolean = false
         override fun <S : KBvSort> visit(sort: S): Boolean = false
         override fun <S : KFpSort> visit(sort: S): Boolean = false
         override fun visit(sort: KFpRoundingModeSort): Boolean = false

ksmt-bitwuzla/ksmt-bitwuzla-core/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolverConfiguration.kt

@@ -9,6 +9,7 @@ import io.ksmt.solver.KTheory.LIA
 import io.ksmt.solver.KTheory.LRA
 import io.ksmt.solver.KTheory.NIA
 import io.ksmt.solver.KTheory.NRA
+import io.ksmt.solver.KTheory.S
 import org.ksmt.solver.bitwuzla.bindings.Bitwuzla
 import org.ksmt.solver.bitwuzla.bindings.BitwuzlaOption
 import org.ksmt.solver.bitwuzla.bindings.Native
@@ -52,7 +53,7 @@ class KBitwuzlaSolverConfigurationImpl(private val bitwuzla: Bitwuzla) : KBitwuz
     override fun optimizeForTheories(theories: Set<KTheory>?, quantifiersAllowed: Boolean) {
         if (theories.isNullOrEmpty()) return
 
-        if (setOf(LIA, LRA, NIA, NRA).intersect(theories).isNotEmpty()) {
+        if (setOf(LIA, LRA, NIA, NRA, S).intersect(theories).isNotEmpty()) {
             throw KSolverUnsupportedFeatureException("Unsupported theories $theories")
         }
     }