forked from UnitTestBot/ksmt
-
Notifications
You must be signed in to change notification settings - Fork 0
/
AdvancedExamples.kt
197 lines (163 loc) · 5.76 KB
/
AdvancedExamples.kt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
import io.ksmt.KContext
import io.ksmt.expr.rewrite.KExprSubstitutor
import io.ksmt.expr.rewrite.simplify.KExprSimplifier
import io.ksmt.solver.KSolver
import io.ksmt.solver.portfolio.KPortfolioSolverManager
import io.ksmt.solver.runner.KSolverRunnerManager
import io.ksmt.solver.z3.KZ3SMTLibParser
import io.ksmt.solver.z3.KZ3Solver
import io.ksmt.solver.z3.KZ3SolverConfiguration
import io.ksmt.solver.z3.KZ3SolverUniversalConfiguration
import io.ksmt.utils.getValue
fun main() {
val ctx = KContext()
parseSmtFormula(ctx)
simplificationOnCreation()
manualExpressionSimplification()
expressionSubstitution(ctx)
solverConfiguration(ctx)
solverModelDetach(ctx)
solverRunnerUsageExample(ctx)
solverRunnerWithCustomSolverExample(ctx)
solverPortfolioExample(ctx)
}
fun simplificationOnCreation() {
// 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
}
fun manualExpressionSimplification() {
// 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
}
}
fun expressionSubstitution(ctx: KContext) = with(ctx) {
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
}
fun parseSmtFormula(ctx: KContext) = with(ctx) {
val formula = """
(declare-fun x () Int)
(declare-fun y () Int)
(assert (>= x y))
(assert (>= y x))
"""
val assertions = KZ3SMTLibParser(this).parse(formula)
println(assertions)
}
fun solverConfiguration(ctx: KContext) = with(ctx) {
KZ3Solver(this).use { solver ->
solver.configure {
// set Z3 solver parameter random_seed to 42
setZ3Option("random_seed", 42)
}
}
}
fun solverModelDetach(ctx: KContext) = with(ctx) {
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
}
fun solverRunnerUsageExample(ctx: KContext) {
// 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
}
}
}
}
// User defined solver
class CustomZ3BasedSolver(ctx: KContext) : KSolver<KZ3SolverConfiguration> by KZ3Solver(ctx) {
init {
configure {
setZ3Option("smt.logic", "QF_BV")
}
}
}
fun solverRunnerWithCustomSolverExample(ctx: KContext) {
// 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
}
}
}
}
fun solverPortfolioExample(ctx: KContext) {
// 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
}
}
}
}