Documentation update

README.md

@@ -1,8 +1,16 @@
 # KSMT
-Kotlin API for various SMT solvers.
+Kotlin/Java 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)
 ![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)
+[![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
+
+# Overview
+
+`KSMT` provides a simple and unified way to work with SMT:
+* Define formulas in a simple and solver-independent way
+* Simplify and transform formulas without involving the SMT solver
+* Solve SMT formulas using various SMT solvers through a unified API
 
 # Getting started
 Install via [Gradle](https://gradle.org/).
@@ -64,3 +72,10 @@ independent of the solver.
 KSMT provides a high-performant API for running SMT solvers in separate processes.
 This feature is important for implementing hard timeouts and 
 solving using multiple solvers in portfolio mode.
+
+### Formula simplification and manipulation utils
+KSMT provides a simplification engine that can simplify and especially evaluate all supported expressions in all
+supported theories.
+Also, KSMT provides utilities for performing formula transformation, visiting and expression substitution.
+
+Check out our [advanced features tutorial](docs/advanced-usage.md) for the examples.

docs/advanced-usage.md

@@ -0,0 +1,239 @@
+# Advanced usage
+
+Advanced features usage tutorial.
+If you are new to KSMT, please check out our [getting started guide](/docs/getting-started.md) first.
+
+For complete code examples, see our [example project](/examples) and
+particularly [`AdvancedExamples.kt`](/examples/src/main/kotlin/AdvancedExamples.kt)
+
+## Working with SMT formulas
+
+### Parsing formulas in SMT-LIB2 format
+
+KSMT provides an API for parsing formulas in the SMT-LIB2 format.
+Currently, KSMT provides a parser implemented on top of the Z3 solver API
+and therefore `ksmt-z3` module is required for parsing.
+
+```kotlin
+val formula = """
+    (declare-fun x () Int)
+    (declare-fun y () Int)
+    (assert (>= x y))
+    (assert (>= y x))
+"""
+with(ctx) {
+   val assertions = KZ3SMTLibParser().parse(formula)
+}
+```
+
+### Simplification during expressions creation
+
+By default, `KContext` will attempt to apply lightweight simplifications during expression creation. If simplifications
+are not suitable for your use cases you can disable them using the `KContext.simplificationMode` parameter.
+
+```kotlin
+// Simplification is enabled by default
+val simplifyingContext = KContext()
+
+// Disable simplifications on a context level
+val nonSimplifyingContext = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+val simplifiedExpr = with(simplifyingContext) {
+   val a by boolSort
+   !(a and falseExpr)
+}
+
+val nonSimplifiedExpr = with(nonSimplifyingContext) {
+   val a by boolSort
+   !(a and falseExpr)
+}
+
+println(nonSimplifiedExpr) // (not (and a false))
+println(simplifiedExpr) // true
+```
+
+### Manual expression simplification
+
+KSMT provides a `KExprSimplifier` which allows you to manually perform simplification of an arbitrary expression.
+
+```kotlin
+// Context do not simplify expressions during creation
+val ctx = KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY)
+
+with(ctx) {
+   val a by boolSort
+   val nonSimplifiedExpr = !(a and falseExpr)
+
+   val simplifier = KExprSimplifier(ctx)
+   val simplifiedExpr = simplifier.apply(nonSimplifiedExpr)
+
+   println(nonSimplifiedExpr) // (not (and a false))
+   println(simplifiedExpr) // true
+}
+```
+
+### Expression substitution
+
+KSMT provides a `KExprSubstitutor` which allows you to replace all occurrences of one expression with another
+expression.
+
+```kotlin
+val a by boolSort
+val b by boolSort
+val expr = !(a and b)
+
+val substitutor = KExprSubstitutor(this).apply {
+   // Substitute all occurrences of `b` with `false`
+   substitute(b, falseExpr)
+}
+
+val exprAfterSubstitution = substitutor.apply(expr)
+
+println(expr) // (not (and a b))
+println(exprAfterSubstitution) // true
+```
+
+## Working with SMT solvers
+
+### Solver configuration
+
+KSMT provides an API for modifying solver-specific parameters.
+Since the parameters and their correct values are solver-specific
+KSMT does not perform any checks.
+See the corresponding solver documentation for a list of available options.
+
+```kotlin
+with(ctx) {
+   KZ3Solver(this).use { solver ->
+      solver.configure {
+         // set Z3 solver parameter random_seed to 42 
+         setZ3Option("random_seed", 42)
+      }
+   }
+}
+```
+
+### Solver independent models
+
+By default, SMT solver models lazily initialized.
+The values of the declared variables are loaded from the underlying solver's native model on demand.
+Therefore, models become invalid after solver close. Also, solvers like `Bitwuzla` invalidate their models every
+time `check-sat` is called.
+To overcome these problems, KSMT provides the `KModel.detach` function that allows you to make the model independent of
+the underlying native representation.
+
+```kotlin
+val a by boolSort
+val b by boolSort
+val expr = a and b
+
+val (model, detachedModel) = KZ3Solver(this).use { solver ->
+   solver.assert(expr)
+   println(solver.check()) // SAT
+   val model = solver.model()
+
+   // Detach model from solver
+   val detachedModel = model.detach()
+
+   model to detachedModel
+}
+
+try {
+   model.eval(expr)
+} catch (ex: Exception) {
+   println("Model no longer valid after solver close")
+}
+
+println(detachedModel.eval(expr)) // true
+```
+
+Note: it is usually a good idea to use `KModel.detach` when you need to keep model e.g. in a `List`.
+
+### Solver runner
+
+SMT solvers are implemented via native libraries and usually have the following issues:
+
+1. Timeout ignore. SMT solver may hang in a long-running operation before reaching a checkpoint.
+   Since solver is a native library, there is no way to interrupt it.
+2. Solvers are usually research projects with a bunch of bugs, e.g. pointer issues. Such
+   errors lead to the interruption of the entire process, including the user's app.
+
+To overcome these problems KSMT provides a solver runner that runs solvers in separate processes to preserve your
+application stability.
+
+```kotlin
+// Create a long-lived solver manager that manages a pool of solver workers
+KSolverRunnerManager().use { solverManager ->
+
+   // Use solver API as usual
+   with(ctx) {
+      val a by boolSort
+      val b by boolSort
+      val expr = a and b
+
+      // Create solver using manager instead of direct constructor invocation
+      solverManager.createSolver(this, KZ3Solver::class).use { solver ->
+         solver.assert(expr)
+         println(solver.check()) // SAT
+      }
+   }
+}
+```
+
+### Using custom solvers in a runner
+
+Solver runner also supports user defined solvers. Custom solvers must be registered before being used in the runner
+using `registerSolver`.
+
+```kotlin
+// Create a long-lived solver manager that manages a pool of solver workers
+KSolverRunnerManager().use { solverManager ->
+   // Register user-defined solver in a current manager
+   solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
+
+   // Use solver API as usual
+   with(ctx) {
+      val a by boolSort
+      val b by boolSort
+      val expr = a and b
+
+      // Create solver using manager instead of direct constructor invocation
+      solverManager.createSolver(this, CustomZ3BasedSolver::class).use { solver ->
+         solver.assert(expr)
+         println(solver.check()) // SAT
+      }
+   }
+}
+```
+
+### Solver portfolio
+
+Various SMT solvers usually show different performance on a same SMT formula.
+[Portfolio solving](https://arxiv.org/abs/1505.03340) is a simple idea of
+running different solvers on the same formula simultaneously and waiting only
+for the first result.
+The portfolio solver workflow in KSMT is similar to the solver runner.
+
+```kotlin
+// Create a long-lived portfolio solver manager that manages a pool of solver workers
+KPortfolioSolverManager(
+   // Solvers to include in portfolio
+   listOf(KZ3Solver::class, CustomZ3BasedSolver::class)
+).use { solverManager ->
+   // Since we use user-defined solver in our portfolio we must register it in the current manager
+   solverManager.registerSolver(CustomZ3BasedSolver::class, KZ3SolverUniversalConfiguration::class)
+
+   // Use solver API as usual
+   with(ctx) {
+      val a by boolSort
+      val b by boolSort
+      val expr = a and b
+
+      // Create portfolio solver using manager
+      solverManager.createPortfolioSolver(this).use { solver ->
+         solver.assert(expr)
+         println(solver.check()) // SAT
+      }
+   }
+}
+```

docs/getting-started.md

@@ -340,39 +340,3 @@ with(ctx) {
     }
 }
 ```
-
-### Parsing formulas in SMT-LIB2 format
-
-KSMT provides an API for parsing formulas in the SMT-LIB2 format. 
-Currently, KSMT provides a parser implemented on top of the Z3 solver API 
-and therefore `ksmt-z3` module is required for parsing.
-
-```kotlin
-val formula = """
-    (declare-fun x () Int)
-    (declare-fun y () Int)
-    (assert (>= x y))
-    (assert (>= y x))
-"""
-with(ctx) {
-    val assertions = KZ3SMTLibParser().parse(formula)
-}
-```
-
-### Solver configuration
-
-KSMT provides an API for modifying solver-specific parameters. 
-Since the parameters and their correct values are solver-specific 
-KSMT does not perform any checks. 
-See the corresponding solver documentation for a list of available options. 
-
-```kotlin
-with(ctx) {
-    KZ3Solver(this).use { solver ->
-        solver.configure {
-            // set Z3 solver parameter random_seed to 42 
-            setZ3Option("random_seed", 42)
-        }
-    }
-}
-```

examples/build.gradle.kts

@@ -12,6 +12,8 @@ dependencies {
     implementation("io.ksmt:ksmt-core:0.5.3")
     // z3 solver
     implementation("io.ksmt:ksmt-z3:0.5.3")
+    // Runner and portfolio solver
+    implementation("io.ksmt:ksmt-runner:0.5.3")
 }
 
 java {