Skip to content

Commit

Permalink
Upgrade cvc5 to 1.1.2 (#158)
Browse files Browse the repository at this point in the history
  • Loading branch information
Saloed authored Apr 15, 2024
1 parent d941124 commit 81ec9b5
Show file tree
Hide file tree
Showing 31 changed files with 601 additions and 643 deletions.
6 changes: 3 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
* Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings

[![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.22)
[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.23)
[![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)

## Get started
Expand All @@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):

```kotlin
// core
implementation("io.ksmt:ksmt-core:0.5.22")
implementation("io.ksmt:ksmt-core:0.5.23")
// z3 solver
implementation("io.ksmt:ksmt-z3:0.5.22")
implementation("io.ksmt:ksmt-z3:0.5.23")
```

Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the
Expand Down
2 changes: 1 addition & 1 deletion buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ plugins {
}

group = "io.ksmt"
version = "0.5.22"
version = "0.5.23"

repositories {
mavenCentral()
Expand Down
6 changes: 3 additions & 3 deletions docs/getting-started.md
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@ repositories {
```kotlin
dependencies {
// core
implementation("io.ksmt:ksmt-core:0.5.22")
implementation("io.ksmt:ksmt-core:0.5.23")
}
```

Expand All @@ -43,9 +43,9 @@ dependencies {
```kotlin
dependencies {
// z3
implementation("io.ksmt:ksmt-z3:0.5.22")
implementation("io.ksmt:ksmt-z3:0.5.23")
// bitwuzla
implementation("io.ksmt:ksmt-bitwuzla:0.5.22")
implementation("io.ksmt:ksmt-bitwuzla:0.5.23")
}
```

Expand Down
6 changes: 3 additions & 3 deletions examples/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -9,11 +9,11 @@ repositories {

dependencies {
// core
implementation("io.ksmt:ksmt-core:0.5.22")
implementation("io.ksmt:ksmt-core:0.5.23")
// z3 solver
implementation("io.ksmt:ksmt-z3:0.5.22")
implementation("io.ksmt:ksmt-z3:0.5.23")
// Runner and portfolio solver
implementation("io.ksmt:ksmt-runner:0.5.22")
implementation("io.ksmt:ksmt-runner:0.5.23")
}

java {
Expand Down
8 changes: 4 additions & 4 deletions ksmt-core/src/main/kotlin/io/ksmt/KContext.kt
Original file line number Diff line number Diff line change
Expand Up @@ -2675,16 +2675,16 @@ open class KContext(
private val zeroExtensionExprCache = mkAstInterner<KBvZeroExtensionExpr>()

/**
* Create BitVec signed extension (`signext`) expression.
* Returns a BitVec expression with [extensionSize] extra sign (leftmost, highest) bits.
* Create BitVec zero extension (`zeroext`) expression.
* Returns a BitVec expression with [extensionSize] extra zero bits.
* The extra bits are prepended to the provided [value].
* */
open fun <T : KBvSort> mkBvZeroExtensionExpr(extensionSize: Int, value: KExpr<T>): KExpr<KBvSort> =
mkSimplified(extensionSize, value, KContext::simplifyBvZeroExtensionExpr, ::mkBvZeroExtensionExprNoSimplify)

/**
* Create BitVec signed extension (`signext`) expression.
* Returns a BitVec expression with [extensionSize] extra sign (leftmost, highest) bits.
* Create BitVec zero extension (`zeroext`) expression.
* Returns a BitVec expression with [extensionSize] extra zero bits.
* The extra bits are prepended to the provided [value].
* */
open fun <T : KBvSort> mkBvZeroExtensionExprNoSimplify(
Expand Down
3 changes: 3 additions & 0 deletions ksmt-cvc5/dist/build.md
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
### Build details

Build is based on the cvc5 fork: https://github.com/Saloed/cvc5/tree/ksmt
This fork provides fixed Java API and buildscripts (`build_(linux|windows|mac).sh`)

We build cvc5 with the following configuration:
```shell
./configure.sh production --auto-download --ipo --no-static --no-cln --no-glpk --no-editline --cryptominisat --java-bindings
Expand Down
Binary file removed ksmt-cvc5/dist/cvc5-1.0.2.jar
Binary file not shown.
Binary file added ksmt-cvc5/dist/cvc5-1.1.2.jar
Binary file not shown.
Binary file removed ksmt-cvc5/dist/cvc5-native-linux-x86-64-1.0.2.zip
Binary file not shown.
Binary file not shown.
Binary file removed ksmt-cvc5/dist/cvc5-native-osx-arm64-1.0.2.zip
Binary file not shown.
Binary file added ksmt-cvc5/dist/cvc5-native-osx-arm64-1.1.2.zip
Binary file not shown.
Binary file added ksmt-cvc5/dist/cvc5-native-win-x86-64-1.1.2.zip
Binary file not shown.
2 changes: 1 addition & 1 deletion ksmt-cvc5/ksmt-cvc5-core/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ repositories {
mavenCentral()
}

val cvc5Version = "1.0.2"
val cvc5Version = "1.1.2"
val cvc5Jar = distDir.resolve("cvc5-$cvc5Version.jar")

dependencies {
Expand Down
100 changes: 0 additions & 100 deletions ksmt-cvc5/ksmt-cvc5-core/src/main/kotlin/io/github/cvc5/SolverUtils.kt

This file was deleted.

Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,10 @@ import io.ksmt.sort.KRealSort
import io.ksmt.sort.KSort
import io.ksmt.sort.KSortVisitor
import io.ksmt.sort.KUninterpretedSort
import java.util.TreeMap

class KCvc5Context(
private val solver: Solver,
private val ctx: KContext
val termManager: KCvc5TermManager,
val ctx: KContext
) : AutoCloseable {
private var isClosed = false

Expand Down Expand Up @@ -62,11 +61,11 @@ class KCvc5Context(
private val currentScopeExpressions = HashMap<KExpr<*>, Term>()
private val expressions = HashMap<KExpr<*>, Term>()
// we can't use HashMap with Term and Sort (hashcode is not implemented)
private val cvc5Expressions = TreeMap<Term, KExpr<*>>()
private val cvc5Expressions = KCvc5TermMap<KExpr<*>>()
private val sorts = HashMap<KSort, Sort>()
private val cvc5Sorts = TreeMap<Sort, KSort>()
private val cvc5Sorts = KCvc5SortMap<KSort>()
private val decls = HashMap<KDecl<*>, Term>()
private val cvc5Decls = TreeMap<Term, KDecl<*>>()
private val cvc5Decls = KCvc5TermMap<KDecl<*>>()

private var currentLevelUninterpretedSorts = hashSetOf<KUninterpretedSort>()
private val uninterpretedSorts = mutableListOf(currentLevelUninterpretedSorts)
Expand All @@ -91,9 +90,6 @@ class KCvc5Context(
*/
fun declarations(): List<Set<KDecl<*>>> = declarations

val nativeSolver: Solver
get() = solver

val isActive: Boolean
get() = !isClosed

Expand Down Expand Up @@ -287,7 +283,7 @@ class KCvc5Context(
val interpreter = uninterpretedSortValueInterpreter[value.value.sort]
?: error("Interpreter was not registered for sort: ${value.value.sort}")

val constraintLhs = solver.mkTerm(Kind.APPLY_UF, arrayOf(interpreter, value.nativeValueTerm))
val constraintLhs = termManager.mkTerm(Kind.APPLY_UF, arrayOf(interpreter, value.nativeValueTerm))
val constraint = constraintLhs.eqTerm(value.nativeUniqueValueDescriptor)

solver.assertFormula(constraint)
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,6 @@
package io.ksmt.solver.cvc5

import io.github.cvc5.Solver
import io.github.cvc5.Term
import io.ksmt.decl.KConstDecl
import io.ksmt.decl.KDeclVisitor
Expand All @@ -8,8 +9,10 @@ import io.ksmt.sort.KSort

open class KCvc5DeclInternalizer(
private val cvc5Ctx: KCvc5Context,
private val solver: Solver,
private val sortInternalizer: KCvc5SortInternalizer
) : KDeclVisitor<Term> {
private val tm = cvc5Ctx.termManager

override fun <S : KSort> visit(decl: KFuncDecl<S>): Term = cvc5Ctx.internalizeDecl(decl) {
// declarations incremental collection optimization
Expand All @@ -18,17 +21,17 @@ open class KCvc5DeclInternalizer(
val domainSorts = decl.argSorts.map { it.accept(sortInternalizer) }
val rangeSort = decl.sort.accept(sortInternalizer)

cvc5Ctx.nativeSolver.declareFun(
solver.declareFun(
decl.name,
domainSorts.toTypedArray(),
rangeSort
)
).also { tm.registerPointer(it) }
}

override fun <S : KSort> visit(decl: KConstDecl<S>): Term = cvc5Ctx.internalizeDecl(decl) {
cvc5Ctx.addDeclaration(decl)

val sort = decl.sort.accept(sortInternalizer)
cvc5Ctx.nativeSolver.mkConst(sort, decl.name)
tm.builder { mkConst(sort, decl.name) }
}
}
Loading

0 comments on commit 81ec9b5

Please sign in to comment.