-
Notifications
You must be signed in to change notification settings - Fork 14
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
20 changed files
with
1,999 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
26 changes: 26 additions & 0 deletions
26
ksmt-test/src/test/kotlin/org/ksmt/test/YicesBenchmarksBasedTest.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,26 @@ | ||
| package org.ksmt.test | ||
|
|
||
| import org.junit.jupiter.api.parallel.Execution | ||
| import org.junit.jupiter.api.parallel.ExecutionMode | ||
| import org.junit.jupiter.params.ParameterizedTest | ||
| import org.junit.jupiter.params.provider.MethodSource | ||
| import java.nio.file.Path | ||
|
|
||
| class YicesBenchmarksBasedTest : BenchmarksBasedTest() { | ||
|
|
||
| @Execution(ExecutionMode.CONCURRENT) | ||
| @ParameterizedTest(name = "{0}") | ||
| @MethodSource("yicesTestData") | ||
| fun testConverter(name: String, samplePath: Path) = | ||
| testConverter(name, samplePath) { assertions -> | ||
| internalizeAndConvertYices(assertions) | ||
| } | ||
|
|
||
| companion object { | ||
| @JvmStatic | ||
| fun yicesTestData() = testData().skipUnsupportedTheories() | ||
|
|
||
| private fun List<BenchmarkTestArguments>.skipUnsupportedTheories() = | ||
| filterNot { "FP" in it.name } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| import com.github.jengelman.gradle.plugins.shadow.tasks.ShadowJar | ||
|
|
||
| plugins { | ||
| id("org.ksmt.ksmt-base") | ||
| id("com.github.johnrengelman.shadow") version "7.1.2" | ||
| `java-test-fixtures` | ||
| } | ||
|
|
||
| val distDir = projectDir.resolve("dist") | ||
|
|
||
| repositories { | ||
| mavenCentral() | ||
| flatDir { dirs(distDir) } | ||
| } | ||
|
|
||
| val yicesNative by configurations.creating | ||
|
|
||
| dependencies { | ||
| implementation(project(":ksmt-core")) | ||
| testFixturesImplementation(project(":ksmt-core")) | ||
|
|
||
| yicesNative("yices", "yices-native-linux-x86-64", "0.0", ext = "zip") | ||
| api(files("$distDir/com.sri.yices.jar")) | ||
| } | ||
|
|
||
| tasks.withType<ProcessResources> { | ||
| yicesNative.resolvedConfiguration.resolvedArtifacts.forEach { artifact -> | ||
| val destination = "lib/x64" | ||
| from(zipTree(artifact.file)) { | ||
| into(destination) | ||
| } | ||
| } | ||
| } | ||
|
|
||
| tasks.withType<ShadowJar> { | ||
| archiveClassifier.set("") | ||
| dependencies { | ||
| exclude { true } | ||
| } | ||
| val implementation = project.configurations["implementation"].dependencies.toSet() | ||
| val runtimeOnly = project.configurations["runtimeOnly"].dependencies.toSet() | ||
| val dependencies = (implementation + runtimeOnly) | ||
| project.configurations.shadow.get().dependencies.addAll(dependencies) | ||
| } | ||
|
|
||
| publishing { | ||
| publications { | ||
| create<MavenPublication>("maven") { | ||
| project.shadow.component(this) | ||
| artifact(tasks["kotlinSourcesJar"]) | ||
| } | ||
| } | ||
| } |
Binary file not shown.
Binary file not shown.
87 changes: 87 additions & 0 deletions
87
ksmt-yices/src/main/kotlin/org/ksmt/solver/yices/KDeclSubstitutor.kt
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,87 @@ | ||
| package org.ksmt.solver.yices | ||
|
|
||
| import org.ksmt.KContext | ||
| import org.ksmt.decl.KDecl | ||
| import org.ksmt.decl.KFuncDecl | ||
| import org.ksmt.expr.KApp | ||
| import org.ksmt.expr.KArrayLambda | ||
| import org.ksmt.expr.KExistentialQuantifier | ||
| import org.ksmt.expr.KExpr | ||
| import org.ksmt.expr.KFunctionAsArray | ||
| import org.ksmt.expr.KUniversalQuantifier | ||
| import org.ksmt.expr.transformer.KNonRecursiveTransformer | ||
| import org.ksmt.sort.KArraySort | ||
| import org.ksmt.sort.KBoolSort | ||
| import org.ksmt.sort.KSort | ||
| import org.ksmt.utils.mkFreshConstDecl | ||
|
|
||
| class KDeclSubstitutor(ctx: KContext) : KNonRecursiveTransformer(ctx) { | ||
| private val substitution = hashMapOf<KDecl<*>, KDecl<*>>() | ||
|
|
||
| fun <T: KSort> substitute(from: KDecl<T>, to: KDecl<T>) { | ||
| substitution[from] = to | ||
| } | ||
|
|
||
| @Suppress("UNCHECKED_CAST") | ||
| private fun <T : KSort> transformDecl(decl: KDecl<T>): KDecl<T> = | ||
| (substitution[decl] as? KDecl<T>) ?: decl | ||
|
|
||
| @Suppress("UNCHECKED_CAST") | ||
| override fun <T : KSort> transformApp(expr: KApp<T, *>): KExpr<T> = | ||
| transformAppAfterArgsTransformed(expr as KApp<T, KExpr<KSort>>) { transformedArgs -> | ||
| val transformedDecl = transformDecl(expr.decl) | ||
|
|
||
| ctx.mkApp(transformedDecl, transformedArgs) | ||
| } | ||
|
|
||
| @Suppress("UNCHECKED_CAST") | ||
| override fun <D : KSort, R : KSort> transform( | ||
| expr: KArrayLambda<D, R> | ||
| ): KExpr<KArraySort<D, R>> = with(expr) { | ||
| transformQuantifierAfterBodyTransformed(body, listOf(indexVarDecl)) { transformedBody, transformedBounds -> | ||
| ctx.mkArrayLambda(transformedBounds.single() as KDecl<D>, transformedBody) | ||
| } | ||
| } | ||
|
|
||
| override fun transform(expr: KExistentialQuantifier): KExpr<KBoolSort> = with(expr) { | ||
| transformQuantifierAfterBodyTransformed(body, bounds) { transformedBody, transformedBounds -> | ||
| ctx.mkExistentialQuantifier(transformedBody, transformedBounds) | ||
| } | ||
| } | ||
|
|
||
| override fun transform(expr: KUniversalQuantifier): KExpr<KBoolSort> = with(expr) { | ||
| transformQuantifierAfterBodyTransformed(body, bounds) { transformedBody, transformedBounds -> | ||
| ctx.mkUniversalQuantifier(transformedBody, transformedBounds) | ||
| } | ||
| } | ||
|
|
||
| override fun <D : KSort, R : KSort> transform(expr: KFunctionAsArray<D, R>): KExpr<KArraySort<D, R>> { | ||
| val transformedFunction = transformDecl(expr.function) | ||
|
|
||
| return ctx.mkFunctionAsArray(transformedFunction as KFuncDecl<R>) | ||
| } | ||
|
|
||
| @Suppress("UNCHECKED_CAST") | ||
| private inline fun<T: KSort, S: KSort> transformQuantifierAfterBodyTransformed( | ||
| body: KExpr<T>, | ||
| bounds: List<KDecl<*>>, | ||
| transformer: (KExpr<T>, List<KDecl<*>>) -> KExpr<S> | ||
| ): KExpr<S> { | ||
| val newSubstitutor = KDeclSubstitutor(ctx).also { currentSubstitutor -> | ||
| val boundsSet = bounds.toHashSet() | ||
|
|
||
| substitution | ||
| .filterNot { (from, _) -> | ||
| boundsSet.contains(from) | ||
| }.takeIf { it.isNotEmpty() } | ||
| ?.forEach { (from, to) -> | ||
| currentSubstitutor.substitute(from as KDecl<KSort>, to as KDecl<KSort>) | ||
|
|
||
| if (boundsSet.contains(to) && !currentSubstitutor.substitution.contains(to)) | ||
| currentSubstitutor.substitute(to, to.sort.mkFreshConstDecl(to.name)) | ||
| } ?: return transformer(body, bounds) | ||
| } | ||
|
|
||
| return transformer(newSubstitutor.apply(body), bounds.map { newSubstitutor.transformDecl(it) }) | ||
| } | ||
| } |
Oops, something went wrong.