@@ -4,13 +4,15 @@ import org.ksmt.expr.KExpr
4
4
import org.ksmt.sort.KBoolSort
5
5
import kotlin.time.Duration
6
6
7
+ @Suppress(" OVERLOADS_INTERFACE" , " INAPPLICABLE_JVM_NAME" )
7
8
interface KSolver : AutoCloseable {
8
9
9
10
/* *
10
11
* Assert an expression into solver.
11
12
*
12
13
* @see check
13
14
* */
15
+ @JvmName(" assertExpr" )
14
16
fun assert (expr : KExpr <KBoolSort >)
15
17
16
18
/* *
@@ -36,6 +38,8 @@ interface KSolver : AutoCloseable {
36
38
* @param n number of pushed scopes to revert.
37
39
* @see push
38
40
* */
41
+ @JvmOverloads
42
+ @JvmName(" pop" )
39
43
fun pop (n : UInt = 1u)
40
44
41
45
/* *
@@ -48,6 +52,8 @@ interface KSolver : AutoCloseable {
48
52
* * [KSolverStatus.UNKNOWN] solver failed to check satisfiability due to timeout or internal reasons.
49
53
* Brief reason description may be obtained via [reasonOfUnknown].
50
54
* */
55
+ @JvmOverloads
56
+ @JvmName(" check" )
51
57
fun check (timeout : Duration = Duration .INFINITE ): KSolverStatus
52
58
53
59
/* *
@@ -57,6 +63,8 @@ interface KSolver : AutoCloseable {
57
63
* @see check
58
64
* @see unsatCore
59
65
* */
66
+ @JvmOverloads
67
+ @JvmName(" checkWithAssumptions" )
60
68
fun checkWithAssumptions (assumptions : List <KExpr <KBoolSort >>, timeout : Duration = Duration .INFINITE ): KSolverStatus
61
69
62
70
/* *
@@ -78,4 +86,9 @@ interface KSolver : AutoCloseable {
78
86
* The format of resulting string is solver implementation dependent.
79
87
* */
80
88
fun reasonOfUnknown (): String
89
+
90
+ /* *
91
+ * Close solver and release acquired native resources.
92
+ * */
93
+ override fun close ()
81
94
}
0 commit comments