Skip to content

Commit 6532b35

Browse files
SaloedSaloed
authored
Faster runner sync solver (#100)
* Support custom solvers in runner * initial solver sync api * More comments * Reduce code duplication
1 parent 551cdcf commit 6532b35

13 files changed

Lines changed: 972 additions & 246 deletions

File tree

‎ksmt-runner/solver-generator/src/main/kotlin/SolverUtilsGenerator.kt‎

Lines changed: 32 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -30,15 +30,17 @@ data class SolverDescription(
3030

3131
private const val SOLVER_TYPE = "SolverType"
3232
private const val SOLVER_TYPE_QUALIFIED_NAME = "org.ksmt.runner.generated.models.SolverType"
33+
private const val CUSTOM_SOLVER_TYPE = "${SOLVER_TYPE}.Custom"
3334

3435
private val kSolverTypeName = "${KSolver::class.simpleName}<*>"
3536
private val kContextTypeName = "${KContext::class.simpleName}"
3637
private val kSolverConfigTypeName = "${KSolverConfiguration::class.simpleName}"
3738
private val kSolverConfigBuilderTypeName = "${KSolverUniversalConfigurationBuilder::class.simpleName}"
38-
private const val DOLLAR = "$"
3939

4040
private const val CONFIG_CONSTRUCTOR = "configConstructor"
4141
private const val SOLVER_CONSTRUCTOR = "solverConstructor"
42+
private const val CONFIG_CONSTRUCTOR_CREATOR = "createConfigConstructor"
43+
private const val SOLVER_CONSTRUCTOR_CREATOR = "createSolverConstructor"
4244

4345
private fun generateHeader(packageName: String) = """
4446
/**
@@ -74,27 +76,41 @@ private fun checkHasSuitableConfigConstructor(solver: SolverDescription) {
7476
check(constructor != null) { "No constructor for solver $solver" }
7577
}
7678

79+
private fun generateSolverConstructor(): String = """
80+
internal fun $SOLVER_CONSTRUCTOR_CREATOR(solverQualifiedName: String): ($kContextTypeName) -> $kSolverTypeName {
81+
val cls = Class.forName(solverQualifiedName)
82+
val ctor = cls.getConstructor($kContextTypeName::class.java)
83+
return { ctx: $kContextTypeName -> ctor.newInstance(ctx) as $kSolverTypeName }
84+
}
85+
""".trimIndent()
86+
7787
private fun generateSolverConstructor(solver: SolverDescription): String {
7888
checkHasSuitableSolverConstructor(solver)
7989

8090
return """
8191
private val $SOLVER_CONSTRUCTOR${solver.solverType}: ($kContextTypeName) -> $kSolverTypeName by lazy {
82-
val cls = Class.forName("${solver.solverCls.qualifiedName}")
83-
val ctor = cls.getConstructor($kContextTypeName::class.java)
84-
({ ctx: $kContextTypeName -> ctor.newInstance(ctx) as $kSolverTypeName })
92+
$SOLVER_CONSTRUCTOR_CREATOR("${solver.solverCls.qualifiedName}")
8593
}
8694
""".trimIndent()
8795
}
8896

97+
private fun generateConfigConstructor(): String = """
98+
internal fun $CONFIG_CONSTRUCTOR_CREATOR(
99+
configQualifiedName: String
100+
): ($kSolverConfigBuilderTypeName) -> $kSolverConfigTypeName {
101+
val cls = Class.forName(configQualifiedName)
102+
val ctor = cls.getConstructor($kSolverConfigBuilderTypeName::class.java)
103+
return { builder: $kSolverConfigBuilderTypeName -> ctor.newInstance(builder) as $kSolverConfigTypeName }
104+
}
105+
""".trimIndent()
106+
89107
@Suppress("MaxLineLength")
90108
private fun generateConfigConstructor(solver: SolverDescription): String {
91109
checkHasSuitableConfigConstructor(solver)
92110

93111
return """
94112
private val $CONFIG_CONSTRUCTOR${solver.solverType}: ($kSolverConfigBuilderTypeName) -> $kSolverConfigTypeName by lazy {
95-
val cls = Class.forName("${solver.solverUniversalConfig.qualifiedName}")
96-
val ctor = cls.getConstructor($kSolverConfigBuilderTypeName::class.java)
97-
({ builder: $kSolverConfigBuilderTypeName -> ctor.newInstance(builder) as $kSolverConfigTypeName })
113+
$CONFIG_CONSTRUCTOR_CREATOR("${solver.solverUniversalConfig.qualifiedName}")
98114
}
99115
""".trimIndent()
100116
}
@@ -109,7 +125,7 @@ private fun generateSolverTypeGetter(): String = """
109125
|)
110126
|
111127
|val KClass<out ${kSolverTypeName}>.solverType: $SOLVER_TYPE
112-
| get() = solverTypes[qualifiedName] ?: error("Unsupported solver: $DOLLAR{qualifiedName}")
128+
| get() = solverTypes[qualifiedName] ?: $CUSTOM_SOLVER_TYPE
113129
""".trimMargin()
114130

115131
private fun generateSolverInstanceCreation(prefix: String) = solvers.joinToString("\n") {
@@ -119,6 +135,7 @@ private fun generateSolverInstanceCreation(prefix: String) = solvers.joinToStrin
119135
private fun generateSolverCreateInstance(): String = """
120136
|fun $SOLVER_TYPE.createInstance(ctx: $kContextTypeName): $kSolverTypeName = when (this) {
121137
${generateSolverInstanceCreation(prefix = "| ")}
138+
| $CUSTOM_SOLVER_TYPE -> error("User defined solvers should not be created with this builder")
122139
|}
123140
""".trimMargin()
124141

@@ -130,6 +147,7 @@ private fun generateConfigCreateInstance(): String = """
130147
|@Suppress("UNCHECKED_CAST")
131148
|fun <C : $kSolverConfigTypeName> $SOLVER_TYPE.createConfigurationBuilder(): ConfigurationBuilder<C> = when (this) {
132149
${generateConfigInstanceCreation(prefix = "| ")}
150+
| $CUSTOM_SOLVER_TYPE -> error("User defined solver config builders should not be created with this builder")
133151
|}
134152
""".trimMargin()
135153

@@ -140,6 +158,12 @@ fun main(args: Array<String>) {
140158
it.appendLine(generateHeader(generatedFilePackage))
141159
it.newLine()
142160

161+
it.appendLine(generateSolverConstructor())
162+
it.newLine()
163+
164+
it.appendLine(generateConfigConstructor())
165+
it.newLine()
166+
143167
solvers.forEach { solver ->
144168
it.appendLine(generateSolverConstructor(solver))
145169
it.newLine()

‎ksmt-runner/src/main/kotlin/org/ksmt/runner/generated/SolverUtils.kt‎

Lines changed: 25 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -14,52 +14,50 @@ import kotlin.reflect.KClass
1414

1515
typealias ConfigurationBuilder<C> = (KSolverUniversalConfigurationBuilder) -> C
1616

17-
private val solverConstructorZ3: (KContext) -> KSolver<*> by lazy {
18-
val cls = Class.forName("org.ksmt.solver.z3.KZ3Solver")
17+
internal fun createSolverConstructor(solverQualifiedName: String): (KContext) -> KSolver<*> {
18+
val cls = Class.forName(solverQualifiedName)
1919
val ctor = cls.getConstructor(KContext::class.java)
20-
({ ctx: KContext -> ctor.newInstance(ctx) as KSolver<*> })
20+
return { ctx: KContext -> ctor.newInstance(ctx) as KSolver<*> }
2121
}
2222

23-
private val configConstructorZ3: (KSolverUniversalConfigurationBuilder) -> KSolverConfiguration by lazy {
24-
val cls = Class.forName("org.ksmt.solver.z3.KZ3SolverUniversalConfiguration")
23+
internal fun createConfigConstructor(
24+
configQualifiedName: String
25+
): (KSolverUniversalConfigurationBuilder) -> KSolverConfiguration {
26+
val cls = Class.forName(configQualifiedName)
2527
val ctor = cls.getConstructor(KSolverUniversalConfigurationBuilder::class.java)
26-
({ builder: KSolverUniversalConfigurationBuilder -> ctor.newInstance(builder) as KSolverConfiguration })
28+
return { builder: KSolverUniversalConfigurationBuilder -> ctor.newInstance(builder) as KSolverConfiguration }
29+
}
30+
31+
private val solverConstructorZ3: (KContext) -> KSolver<*> by lazy {
32+
createSolverConstructor("org.ksmt.solver.z3.KZ3Solver")
33+
}
34+
35+
private val configConstructorZ3: (KSolverUniversalConfigurationBuilder) -> KSolverConfiguration by lazy {
36+
createConfigConstructor("org.ksmt.solver.z3.KZ3SolverUniversalConfiguration")
2737
}
2838

2939
private val solverConstructorBitwuzla: (KContext) -> KSolver<*> by lazy {
30-
val cls = Class.forName("org.ksmt.solver.bitwuzla.KBitwuzlaSolver")
31-
val ctor = cls.getConstructor(KContext::class.java)
32-
({ ctx: KContext -> ctor.newInstance(ctx) as KSolver<*> })
40+
createSolverConstructor("org.ksmt.solver.bitwuzla.KBitwuzlaSolver")
3341
}
3442

3543
private val configConstructorBitwuzla: (KSolverUniversalConfigurationBuilder) -> KSolverConfiguration by lazy {
36-
val cls = Class.forName("org.ksmt.solver.bitwuzla.KBitwuzlaSolverUniversalConfiguration")
37-
val ctor = cls.getConstructor(KSolverUniversalConfigurationBuilder::class.java)
38-
({ builder: KSolverUniversalConfigurationBuilder -> ctor.newInstance(builder) as KSolverConfiguration })
44+
createConfigConstructor("org.ksmt.solver.bitwuzla.KBitwuzlaSolverUniversalConfiguration")
3945
}
4046

4147
private val solverConstructorYices: (KContext) -> KSolver<*> by lazy {
42-
val cls = Class.forName("org.ksmt.solver.yices.KYicesSolver")
43-
val ctor = cls.getConstructor(KContext::class.java)
44-
({ ctx: KContext -> ctor.newInstance(ctx) as KSolver<*> })
48+
createSolverConstructor("org.ksmt.solver.yices.KYicesSolver")
4549
}
4650

4751
private val configConstructorYices: (KSolverUniversalConfigurationBuilder) -> KSolverConfiguration by lazy {
48-
val cls = Class.forName("org.ksmt.solver.yices.KYicesSolverUniversalConfiguration")
49-
val ctor = cls.getConstructor(KSolverUniversalConfigurationBuilder::class.java)
50-
({ builder: KSolverUniversalConfigurationBuilder -> ctor.newInstance(builder) as KSolverConfiguration })
52+
createConfigConstructor("org.ksmt.solver.yices.KYicesSolverUniversalConfiguration")
5153
}
5254

5355
private val solverConstructorCvc5: (KContext) -> KSolver<*> by lazy {
54-
val cls = Class.forName("org.ksmt.solver.cvc5.KCvc5Solver")
55-
val ctor = cls.getConstructor(KContext::class.java)
56-
({ ctx: KContext -> ctor.newInstance(ctx) as KSolver<*> })
56+
createSolverConstructor("org.ksmt.solver.cvc5.KCvc5Solver")
5757
}
5858

5959
private val configConstructorCvc5: (KSolverUniversalConfigurationBuilder) -> KSolverConfiguration by lazy {
60-
val cls = Class.forName("org.ksmt.solver.cvc5.KCvc5SolverUniversalConfiguration")
61-
val ctor = cls.getConstructor(KSolverUniversalConfigurationBuilder::class.java)
62-
({ builder: KSolverUniversalConfigurationBuilder -> ctor.newInstance(builder) as KSolverConfiguration })
60+
createConfigConstructor("org.ksmt.solver.cvc5.KCvc5SolverUniversalConfiguration")
6361
}
6462

6563
private val solverTypes = mapOf(
@@ -70,13 +68,14 @@ private val solverTypes = mapOf(
7068
)
7169

7270
val KClass<out KSolver<*>>.solverType: SolverType
73-
get() = solverTypes[qualifiedName] ?: error("Unsupported solver: ${qualifiedName}")
71+
get() = solverTypes[qualifiedName] ?: SolverType.Custom
7472

7573
fun SolverType.createInstance(ctx: KContext): KSolver<*> = when (this) {
7674
SolverType.Z3 -> solverConstructorZ3(ctx)
7775
SolverType.Bitwuzla -> solverConstructorBitwuzla(ctx)
7876
SolverType.Yices -> solverConstructorYices(ctx)
7977
SolverType.Cvc5 -> solverConstructorCvc5(ctx)
78+
SolverType.Custom -> error("User defined solvers should not be created with this builder")
8079
}
8180

8281
@Suppress("UNCHECKED_CAST")
@@ -85,5 +84,6 @@ fun <C : KSolverConfiguration> SolverType.createConfigurationBuilder(): Configur
8584
SolverType.Bitwuzla -> { builder -> configConstructorBitwuzla(builder) as C }
8685
SolverType.Yices -> { builder -> configConstructorYices(builder) as C }
8786
SolverType.Cvc5 -> { builder -> configConstructorCvc5(builder) as C }
87+
SolverType.Custom -> error("User defined solver config builders should not be created with this builder")
8888
}
8989

0 commit comments

Comments
 (0)