Skip to content

Commit

Permalink
Maven release (#108)
Browse files Browse the repository at this point in the history
* Maven publish config

* Maven publish config

* Test: maven release action

* Disable sign

* Try remove string quotes

* Try fix gpg sign

* deploy all packages

* Rename package from `ork.ksmt` to `io.ksmt`

* Enable maven deploy

* Add javadoc

* try give more memory for dokka

* Update release workflow

* Update docs and examples

* Upgrade version to 0.5.2
  • Loading branch information
Saloed committed Apr 29, 2023
1 parent f0f0fc6 commit 8e9f734
Show file tree
Hide file tree
Showing 256 changed files with 4,345 additions and 4,260 deletions.
11 changes: 10 additions & 1 deletion .github/workflows/release.yml
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,16 @@ jobs:
- name: Build artifacts
uses: gradle/gradle-build-action@v2
with:
arguments: publishAllPublicationsToReleaseDirRepository
arguments: |
publishAllPublicationsToCentralRepository
publishAllPublicationsToReleaseDirRepository
--no-daemon
-Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=2G
-PmavenDeployUrl=https://s01.oss.sonatype.org/service/local/staging/deploy/maven2/
-PmavenDeployUser=${{ secrets.MAVEN_CENTRAL_USER }}
-PmavenDeployPassword=${{ secrets.MAVEN_CENTRAL_PASSWORD }}
-PmavenSignGpgKey="${{ secrets.MAVEN_SIGN_GPG_KEY }}"
-PmavenSignGpgPassword=${{ secrets.MAVEN_SIGN_GPG_PASSWORD }}
- name: Upload release artifacts
uses: softprops/action-gh-release@v1
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/run-long-tests.yml
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ jobs:
uses: gradle/gradle-build-action@v2
with:
arguments: |
:ksmt-test:test --tests ${{ format('"org.ksmt.test.benchmarks.{0}"', matrix.test) }}
:ksmt-test:test --tests ${{ format('"io.ksmt.test.benchmarks.{0}"', matrix.test) }}
--no-daemon
--continue
-PrunBenchmarksBasedTests=true
Expand Down
13 changes: 4 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,21 +2,16 @@
Kotlin API for various SMT solvers.

[![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/workflows/build-and-run-tests.yml)
[![JitPack](https://jitpack.io/v/UnitTestBot/ksmt.svg)](https://jitpack.io/#UnitTestBot/ksmt)
![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)

# Getting started
Install via [JitPack](https://jitpack.io/) and [Gradle](https://gradle.org/).
Install via [Gradle](https://gradle.org/).

```kotlin
// JitPack repository
repositories {
maven { url = uri("https://jitpack.io") }
}

// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
implementation("io.ksmt:ksmt-core:0.5.2")
// z3 solver
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
implementation("io.ksmt:ksmt-z3:0.5.2")
```

## Usage
Expand Down
30 changes: 14 additions & 16 deletions Requirements.md
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
| [External process runner](#external-process-runner) | Done |
| [Portfolio solver](#portfolio-solver) | Done |
| [Solver configuration API](#solver-configuration-api) | Done |
| [Deployment](#deployment) | Done partially |
| [Deployment](#deployment) | Done |
| [Expression simplification / evaluation](#expression-simplification--evaluation) | Done |
| [Performance tests](#performance-tests) | TODO |
| [Better Z3 API](#better-z3-api) | Done partially |
Expand All @@ -34,7 +34,7 @@
Provide a solver-independent formula representation
with back and forth transformations to the solver's native representation.
Such representation allows introspection of formulas and transformation of formulas
independent of the solver. Check out [KASt](ksmt-core/src/main/kotlin/org/ksmt/KAst.kt) and its inheritors
independent of the solver. Check out [KASt](ksmt-core/src/main/kotlin/io/ksmt/KAst.kt) and its inheritors
for implementation details.

### Expression interning
Expand All @@ -44,19 +44,19 @@ Interning (aka [hash consing](https://en.wikipedia.org/wiki/Hash_consing)) is ne
1. **Constant time ast comparison.** Otherwise, we need to compare trees.
2. **Ast deduplication.** We can have many duplicate nodes (e.g. constants).

Currently, interning is implemented via [KContext](ksmt-core/src/main/kotlin/org/ksmt/KContext.kt) which
Currently, interning is implemented via [KContext](ksmt-core/src/main/kotlin/io/ksmt/KContext.kt) which
manages all created asts.

### Basic theories support

Support theories in KSMT expressions system. Each theory consists of:

1. **Expressions.** Theory specific operations over terms.
All implementations are in [expr](ksmt-core/src/main/kotlin/org/ksmt/expr) package.
All implementations are in [expr](ksmt-core/src/main/kotlin/io/ksmt/expr) package.
2. **Sorts.** Theory specific types.
All implementations are in [sort](ksmt-core/src/main/kotlin/org/ksmt/sort) package.
All implementations are in [sort](ksmt-core/src/main/kotlin/io/ksmt/sort) package.
3. **Declarations.** Declarations (name, argument sorts, result sort) of theory specific functions.
All implementations are in [decl](ksmt-core/src/main/kotlin/org/ksmt/decl) package.
All implementations are in [decl](ksmt-core/src/main/kotlin/io/ksmt/decl) package.

KSMT expression system supports following theories and their combinations:

Expand All @@ -78,7 +78,7 @@ Main goals are:
1. Allow the user to instantiate KSMT expressions from SMT-LIB.
2. Provide us the opportunity to use a rich database of [benchmarks](https://smtlib.cs.uiowa.edu/benchmarks.shtml).

Currently, [implemented](ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3SMTLibParser.kt) on top of Z3 SMT solver.
Currently, [implemented](ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3SMTLibParser.kt) on top of Z3 SMT solver.
A solver-agnostic implementation may be done in the future.

### SMT-LIB2 serializer
Expand All @@ -96,7 +96,7 @@ Can be implemented on top of the Z3 SMT solver (easy version) or in a solver-ind

If some solver doesn't support some theory (e.g. BV) or some feature (e.g. unsat-core generation) we need to throw
specialized exception.
Currently, [KSolverUnsupportedFeatureException](ksmt-core/src/main/kotlin/org/ksmt/solver/KSolverUnsupportedFeatureException.kt)
Currently, [KSolverUnsupportedFeatureException](ksmt-core/src/main/kotlin/io/ksmt/solver/KSolverUnsupportedFeatureException.kt)
is thrown.

To simplify the user experience, the exception may contain a recommendation to switch to another solver.
Expand All @@ -114,7 +114,7 @@ Features:
5. Incremental solving via push/pop.
6. Incremental solving via assumptions.

For implementation details, check out [KSolver](ksmt-core/src/main/kotlin/org/ksmt/solver/KSolver.kt).
For implementation details, check out [KSolver](ksmt-core/src/main/kotlin/io/ksmt/solver/KSolver.kt).

### Z3 solver support

Expand All @@ -124,7 +124,7 @@ Z3 has native support for all theories,
listed in [KSMT supported theories](#basic-theories-support)
and provides all the functionality, listed in [SMT solver features](#smt-solver-support).

For implementation details, check out [KZ3Solver](ksmt-z3/src/main/kotlin/org/ksmt/solver/z3/KZ3Solver.kt).
For implementation details, check out [KZ3Solver](ksmt-z3/src/main/kotlin/io/ksmt/solver/z3/KZ3Solver.kt).

### Bitwuzla solver support

Expand All @@ -147,7 +147,7 @@ For the solver features, listed in [SMT solver features](#smt-solver-support),
Bitwuzla provides full native support.

For implementation details, check
out [KBitwuzlaSolver](ksmt-bitwuzla/src/main/kotlin/org/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt).
out [KBitwuzlaSolver](ksmt-bitwuzla/src/main/kotlin/io/ksmt/solver/bitwuzla/KBitwuzlaSolver.kt).

### Yices2 solver support

Expand Down Expand Up @@ -204,11 +204,9 @@ For implementation details, check out [corresponding PR](https://github.com/Unit

### Deployment

Deliver KSMT to end users.
Deliver KSMT to end users.

Currently, we use [JitPack](https://jitpack.io) for deployment.

Use Maven Central in the future.
Released on [Maven Central](https://central.sonatype.com/namespace/io.ksmt).

### Expression simplification / evaluation

Expand All @@ -218,7 +216,7 @@ Implement simplification rules for KSMT expressions, and apply it to:
3. Expression evaluation wrt model (special case of simplification)

List of currently implemented simplification
rules: [simplification rules](ksmt-core/src/main/kotlin/org/ksmt/expr/rewrite/simplify/Rules.md)
rules: [simplification rules](ksmt-core/src/main/kotlin/io/ksmt/expr/rewrite/simplify/Rules.md)

### Performance tests

Expand Down
1 change: 1 addition & 0 deletions buildSrc/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ val versions = loadProperties(rootDir.parentFile.resolve("version.properties").a

dependencies {
implementation("org.jetbrains.kotlin:kotlin-gradle-plugin:${versions["kotlin"]}")
implementation("org.jetbrains.dokka:dokka-gradle-plugin:${versions["kotlin"]}")
implementation("io.gitlab.arturbosch.detekt:detekt-gradle-plugin:${versions["detekt"]}")
implementation("de.undercouch.download:de.undercouch.download.gradle.plugin:5.1.0")
}
Expand Down
62 changes: 54 additions & 8 deletions buildSrc/src/main/kotlin/Publications.kt
Original file line number Diff line number Diff line change
@@ -1,15 +1,61 @@
import gradle.kotlin.dsl.accessors._87b80c14bf1c4d505c7a71d7741e0994.signing
import org.gradle.api.Project
import org.gradle.api.component.AdhocComponentWithVariants
import org.gradle.api.component.SoftwareComponent
import org.gradle.api.publish.maven.MavenPublication
import org.gradle.kotlin.dsl.get

fun Project.removeTestFixtures(softwareComponent: SoftwareComponent) {
with(softwareComponent as AdhocComponentWithVariants) {
withVariantsFromConfiguration(configurations["testFixturesApiElements"]) {
skip()
fun MavenPublication.addKsmtPom() {
pom {
packaging = "jar"
name.set("io.ksmt")
description.set("Kotlin API for various SMT solvers")
url.set("https://www.ksmt.io/")

licenses {
license {
name.set("The Apache License, Version 2.0")
url.set("https://www.apache.org/licenses/LICENSE-2.0.txt")
}
}

issueManagement {
url.set("https://github.com/UnitTestBot/ksmt/issues")
}

scm {
connection.set("scm:git:https://github.com/UnitTestBot/ksmt.git")
developerConnection.set("scm:git:https://github.com/UnitTestBot/ksmt.git")
url.set("https://github.com/UnitTestBot/ksmt")
}

developers {
developer {
id.set("saloed")
name.set("Valentyn Sobol")
email.set("vo.sobol@mail.ru")
}

developer {
id.set("CaelmBleidd")
name.set("Alexey Menshutin")
email.set("alex.menshutin99@gmail.com")
}
}
withVariantsFromConfiguration(configurations["testFixturesRuntimeElements"]) {
skip()
}
}

fun MavenPublication.signKsmtPublication(project: Project) = with(project) {
signing {
val gpgKey = project.stringProperty("mavenSignGpgKey")?.removeSurrounding("\"")
val gpgPassword = project.stringProperty("mavenSignGpgPassword")

if (gpgKey != null && gpgPassword != null) {
useInMemoryPgpKeys(gpgKey, gpgPassword)
sign(this@signKsmtPublication)
}
}
}

fun MavenPublication.addSourcesAndJavadoc(project: Project) {
artifact(project.tasks["kotlinSourcesJar"])
artifact(project.tasks["dokkaJavadocJar"])
}
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,14 @@ plugins {
kotlin("jvm")
id("io.gitlab.arturbosch.detekt")
id("de.undercouch.download")
id("org.jetbrains.dokka")
`java-library`
`maven-publish`
signing
}

group = "org.ksmt"
version = "0.5.1"
group = "io.ksmt"
version = "0.5.2"

repositories {
mavenCentral()
Expand Down Expand Up @@ -42,11 +44,30 @@ tasks.withType<Test> {
systemProperty("junit.jupiter.execution.parallel.enabled", true)
}

tasks.register<Jar>("dokkaJavadocJar") {
dependsOn(tasks.dokkaJavadoc)
from(tasks.dokkaJavadoc.flatMap { it.outputDirectory })
archiveClassifier.set("javadoc")
}

publishing {
repositories {
maven {
name = "releaseDir"
url = uri(layout.buildDirectory.dir("release"))
}

val mavenDeployUrl = project.stringProperty("mavenDeployUrl")
if (mavenDeployUrl != null) {
maven {
name = "central"
url = uri(mavenDeployUrl)

credentials {
username = project.stringProperty("mavenDeployUser") ?: ""
password = project.stringProperty("mavenDeployPassword") ?: ""
}
}
}
}
}
15 changes: 7 additions & 8 deletions docs/getting-started.md
Original file line number Diff line number Diff line change
Expand Up @@ -4,31 +4,30 @@ For code examples, please check out our [project](/examples).

## Installation

Installation via [JitPack](https://jitpack.io/) and [Gradle](https://gradle.org/).
Install via [Gradle](https://gradle.org/).

#### 1. Enable JitPack repository in your build configuration:
#### 1. Enable Maven Central repository in your build configuration:
```kotlin
// JitPack repository
repositories {
maven { url = uri("https://jitpack.io") }
mavenCentral()
}
```

#### 2. Add KSMT core dependency:
```kotlin
dependencies {
// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
implementation("io.ksmt:ksmt-core:0.5.2")
}
```

#### 3. Add one or more SMT solver dependencies:
```kotlin
dependencies {
// z3
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
implementation("io.ksmt:ksmt-z3:0.5.2")
// bitwuzla
implementation("com.github.UnitTestBot.ksmt:ksmt-bitwuzla:0.5.1")
implementation("io.ksmt:ksmt-bitwuzla:0.5.2")
}
```
SMT solver specific packages are provided with solver native binaries.
Expand All @@ -51,7 +50,7 @@ In this example, we want to create an expression
over Boolean variable `a` and integer variables `b` and `c`.

```kotlin
import org.ksmt.utils.getValue
import io.ksmt.utils.getValue

with(ctx) {
// create symbolic variables
Expand Down
5 changes: 2 additions & 3 deletions examples/build.gradle.kts
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,13 @@ plugins {

repositories {
mavenCentral()
maven { url = uri("https://jitpack.io") }
}

dependencies {
// core
implementation("com.github.UnitTestBot.ksmt:ksmt-core:0.5.1")
implementation("io.ksmt:ksmt-core:0.5.2")
// z3 solver
implementation("com.github.UnitTestBot.ksmt:ksmt-z3:0.5.1")
implementation("io.ksmt:ksmt-z3:0.5.2")
}

java {
Expand Down
18 changes: 9 additions & 9 deletions examples/src/main/java/Sudoku.java
Original file line number Diff line number Diff line change
@@ -1,12 +1,12 @@
import org.ksmt.KContext;
import org.ksmt.expr.KExpr;
import org.ksmt.expr.KInt32NumExpr;
import org.ksmt.solver.KModel;
import org.ksmt.solver.KSolver;
import org.ksmt.solver.KSolverStatus;
import org.ksmt.solver.z3.KZ3Solver;
import org.ksmt.sort.KBoolSort;
import org.ksmt.sort.KIntSort;
import io.ksmt.KContext;
import io.ksmt.expr.KExpr;
import io.ksmt.expr.KInt32NumExpr;
import io.ksmt.solver.KModel;
import io.ksmt.solver.KSolver;
import io.ksmt.solver.KSolverStatus;
import io.ksmt.solver.z3.KZ3Solver;
import io.ksmt.sort.KBoolSort;
import io.ksmt.sort.KIntSort;

import java.util.ArrayList;
import java.util.Collection;
Expand Down
Loading

0 comments on commit 8e9f734

Please sign in to comment.