You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Check out our [roadmap](Requirements.md) for detailed description of features and future plans.
63
+
### Solver-agnostic formula representation
64
+
65
+
Various scenarios are available for using SMT solvers: you can use a single solver to determine whether a formula is
66
+
satisfiable, or you can apply several solvers to the same expression successively. In the latter case, you need a _solver-agnostic formula representation_.
67
+
68
+
We implemented it in KSMT, so you can
69
+
* transform expressions from the solver native representation to KSMT representation and vice versa,
70
+
* use _formula introspection_,
71
+
* manipulate expressions without involving a solver,
72
+
* use expressions even if the solver is freed.
73
+
74
+
Expression interning (hash consing) affords faster expression comparison: we do not need to compare the expression
75
+
trees. Expressions are deduplicated, so we avoid redundant memory allocation.
50
76
51
-
# Why KSMT?
77
+
### Kotlin-based DSL for SMT formulas
78
+
79
+
KSMT provides you with a unified DSL for SMT expressions:
52
80
53
-
### Kotlin based DSL for SMT formulas
54
-
KSMT provides simple and concise DSL for expressions.
55
81
```kotlin
56
82
val array by mkArraySort(intSort, intSort)
57
83
val index by intSort
@@ -60,22 +86,43 @@ val value by intSort
60
86
val expr = (array.select(index -1.expr) lt value) and
61
87
(array.select(index +1.expr) gt value)
62
88
```
63
-
Check out our [example project](examples) for more complicated examples.
64
89
65
-
### Solver agnostic SMT formula representation
66
-
KSMT provides a solver-independent formula representation
67
-
with back and forth transformations to the solver's native representation.
68
-
Such representation allows introspection of formulas and transformation of formulas
69
-
independent of the solver.
90
+
### Utilities to simplify and transform expressions
91
+
92
+
KSMT provides a simplification engine applicable to all supported expressions for all supported theories:
93
+
94
+
* reduce expression size and complexity
95
+
* evaluate expressions (including those with free variables) — reduce your expression to a constant
96
+
* perform formula transformations
97
+
* substitute expressions
98
+
99
+
KSMT simplification engine implements more than 200 rules.
100
+
By default, it attempts to apply simplifications when you create the expressions, but you can turn this
101
+
feature off, if necessary. You can also simplify an arbitrary expression manually.
102
+
103
+
### Using multiple solvers (portfolio mode)
104
+
105
+
SMT solvers may differ in performance across different formulas:
106
+
see the [International Satisfiability Modulo Theories Competition](https://smt-comp.github.io/2022/).
107
+
108
+
With KSMT portfolio solving, you can run multiple solvers in parallel on the same formula — until you get the first
109
+
(the fastest) result.
110
+
111
+
For detailed instructions on running multiple solvers, see [Advanced usage](docs/advanced-usage.md).
112
+
113
+
### Running solvers in separate processes
114
+
115
+
Most of the SMT solvers are research projects — they are implemented via native libraries and are sometimes not
116
+
production ready:
117
+
* they may ignore timeouts — they sometimes hang in a long-running operation, and you cannot interrupt it;
118
+
* they may suddenly crash interrupting the entire process — because of a pointer issue, for example.
119
+
120
+
KSMT runs each solver in a separate process, which adds to stability of your application and provides support for
121
+
portfolio mode.
70
122
71
-
### Process based solver runner
72
-
KSMT provides a high-performant API for running SMT solvers in separate processes.
73
-
This feature is important for implementing hard timeouts and
74
-
solving using multiple solvers in portfolio mode.
123
+
### KSMT distribution
75
124
76
-
### Formula simplification and manipulation utils
77
-
KSMT provides a simplification engine that can simplify and especially evaluate all supported expressions in all
78
-
supported theories.
79
-
Also, KSMT provides utilities for performing formula transformation, visiting and expression substitution.
125
+
Many solvers do not have prebuilt binaries, or binaries are for Linux only.
80
126
81
-
Check out our [advanced features tutorial](docs/advanced-usage.md) for the examples.
127
+
KSMT is distributed as JVM library with solver binaries provided. The library has been tested against the SMT-LIB
128
+
benchmarks. Documentation and examples are also available.
0 commit comments