Skip to content

Commit b5ed3ab

Browse files
dee-treedee-tree
committed
Yices forking solver, uninterpreted values in universe fix
1 parent d88500e commit b5ed3ab

15 files changed

+989
-261
lines changed

‎ksmt-test/src/main/kotlin/io/ksmt/test/TestWorkerProcess.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -108,7 +108,7 @@ class TestWorkerProcess : ChildProcessBase<TestProtocolModel>() {
108108

109109
private fun internalizeAndConvertYices(assertions: List<KExpr<KBoolSort>>): List<KExpr<KBoolSort>> {
110110
// Yices doesn't reverse cache internalized expressions (only interpreted values)
111-
KYicesContext().use { internContext ->
111+
KYicesContext(ctx).use { internContext ->
112112
val internalizer = KYicesExprInternalizer(internContext)
113113

114114
val yicesAssertions = with(internalizer) {

‎ksmt-test/src/test/kotlin/io/ksmt/test/KForkingSolverTest.kt‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@ import io.ksmt.KContext
44
import io.ksmt.solver.KForkingSolverManager
55
import io.ksmt.solver.KSolverStatus
66
import io.ksmt.solver.cvc5.KCvc5ForkingSolverManager
7+
import io.ksmt.solver.yices.KYicesForkingSolverManager
78
import io.ksmt.solver.z3.KZ3ForkingSolverManager
89
import io.ksmt.utils.getValue
910
import org.junit.jupiter.api.Nested
@@ -38,6 +39,29 @@ class KForkingSolverTest {
3839
private fun mkCvc5ForkingSolverManager(ctx: KContext) = KCvc5ForkingSolverManager(ctx)
3940
}
4041

42+
@Nested
43+
inner class KForkingSolverTestYices {
44+
@Test
45+
fun testCheckSat() = testCheckSat(::mkYicesForkingSolverManager)
46+
47+
@Test
48+
fun testModel() = testModel(::mkYicesForkingSolverManager)
49+
50+
@Test
51+
fun testUnsatCore() = testUnsatCore(::mkYicesForkingSolverManager)
52+
53+
@Test
54+
fun testUninterpretedSort() = testUninterpretedSort(::mkYicesForkingSolverManager)
55+
56+
@Test
57+
fun testScopedAssertions() = testScopedAssertions(::mkYicesForkingSolverManager)
58+
59+
@Test
60+
fun testLifeTime() = testLifeTime(::mkYicesForkingSolverManager)
61+
62+
private fun mkYicesForkingSolverManager(ctx: KContext) = KYicesForkingSolverManager(ctx)
63+
}
64+
4165
@Nested
4266
inner class KForkingSolverTestZ3 {
4367
@Test
@@ -336,6 +360,7 @@ class KForkingSolverTest {
336360
}
337361
}
338362

363+
parentSolver.assert(u1 neq pu1v)
339364
assertEquals(KSolverStatus.SAT, parentSolver.check())
340365
parentSolver.model().uninterpretedSortUniverse(uSort)?.also { universe ->
341366
assertContains(universe, pu1v)

‎ksmt-test/src/test/kotlin/io/ksmt/test/MultiIndexedArrayTest.kt‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ class MultiIndexedArrayTest {
9595
@Test
9696
fun testMultiIndexedArraysYicesWithZ3Oracle(): Unit = with(KContext(simplificationMode = NO_SIMPLIFY)) {
9797
oracleManager.createSolver(this, KZ3Solver::class).use { oracleSolver ->
98-
KYicesContext().use { yicesNativeCtx ->
98+
KYicesContext(this).use { yicesNativeCtx ->
9999
runMultiIndexedArraySamples(oracleSolver) { expr ->
100100
internalizeAndConvertYices(yicesNativeCtx, expr)
101101
}
@@ -117,7 +117,7 @@ class MultiIndexedArrayTest {
117117
@Test
118118
fun testMultiIndexedArraysYicesWithYicesOracle(): Unit = with(KContext(simplificationMode = NO_SIMPLIFY)) {
119119
oracleManager.createSolver(this, KYicesSolver::class).use { oracleSolver ->
120-
KYicesContext().use { yicesNativeCtx ->
120+
KYicesContext(this).use { yicesNativeCtx ->
121121
runMultiIndexedArraySamples(oracleSolver) { expr ->
122122
internalizeAndConvertYices(yicesNativeCtx, expr)
123123
}

‎ksmt-test/src/test/kotlin/io/ksmt/test/UninterpretedSortUniverseTest.kt‎

Lines changed: 76 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,76 @@
1+
package io.ksmt.test
2+
3+
import io.ksmt.KContext
4+
import io.ksmt.solver.KSolver
5+
import io.ksmt.solver.KSolverStatus
6+
import io.ksmt.solver.bitwuzla.KBitwuzlaSolver
7+
import io.ksmt.solver.cvc5.KCvc5Solver
8+
import io.ksmt.solver.yices.KYicesSolver
9+
import io.ksmt.solver.z3.KZ3Solver
10+
import io.ksmt.utils.getValue
11+
import org.junit.jupiter.api.Nested
12+
import org.junit.jupiter.api.Test
13+
import kotlin.test.assertContains
14+
import kotlin.test.assertEquals
15+
import kotlin.test.assertNotEquals
16+
import kotlin.test.assertNotNull
17+
18+
class UninterpretedSortUniverseTest {
19+
20+
@Nested
21+
inner class UninterpretedSortUniverseTestBitwuzla {
22+
@Test
23+
fun testUniverseContainsValue() = testUniverseContainsValue(::mkBitwuzlaSolver)
24+
25+
private fun mkBitwuzlaSolver(ctx: KContext) = KBitwuzlaSolver(ctx)
26+
}
27+
28+
@Nested
29+
inner class UninterpretedSortUniverseTestCvc5 {
30+
@Test
31+
fun testUniverseContainsValue() = testUniverseContainsValue(::mkCvc5Solver)
32+
33+
private fun mkCvc5Solver(ctx: KContext) = KCvc5Solver(ctx)
34+
}
35+
36+
@Nested
37+
inner class UninterpretedSortUniverseTestYices {
38+
@Test
39+
fun testUniverseContainsValue() = testUniverseContainsValue(::mkYicesSolver)
40+
41+
private fun mkYicesSolver(ctx: KContext) = KYicesSolver(ctx)
42+
}
43+
44+
@Nested
45+
inner class UninterpretedSortUniverseTestZ3 {
46+
@Test
47+
fun testUniverseContainsValue() = testUniverseContainsValue(::mkZ3Solver)
48+
49+
private fun mkZ3Solver(ctx: KContext) = KZ3Solver(ctx)
50+
}
51+
52+
fun testUniverseContainsValue(mkSolver: (KContext) -> KSolver<*>): Unit =
53+
KContext(simplificationMode = KContext.SimplificationMode.NO_SIMPLIFY).use { ctx ->
54+
mkSolver(ctx).use { s ->
55+
with(ctx) {
56+
val u = mkUninterpretedSort("u")
57+
val u1 by u
58+
val uval5 = mkUninterpretedSortValue(u, 5)
59+
60+
s.assert(u1 neq uval5)
61+
assertEquals(KSolverStatus.SAT, s.check())
62+
val u1v = s.model().eval(u1)
63+
assertNotEquals(uval5, u1v)
64+
65+
s.assert(u1 neq u1v)
66+
assertEquals(KSolverStatus.SAT, s.check())
67+
68+
val universe = s.model().uninterpretedSortUniverse(u)
69+
assertNotNull(universe)
70+
71+
assertContains(universe, u1v)
72+
assertContains(universe, uval5)
73+
}
74+
}
75+
}
76+
}

‎ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesContext.kt‎

Lines changed: 55 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,12 @@ package io.ksmt.solver.yices
33
import com.sri.yices.Terms
44
import com.sri.yices.Types
55
import com.sri.yices.Yices
6-
import it.unimi.dsi.fastutil.ints.Int2ObjectOpenHashMap
7-
import it.unimi.dsi.fastutil.ints.IntOpenHashSet
8-
import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap
6+
import io.ksmt.KContext
97
import io.ksmt.decl.KDecl
108
import io.ksmt.expr.KConst
119
import io.ksmt.expr.KExpr
1210
import io.ksmt.expr.KInterpretedValue
11+
import io.ksmt.expr.KUninterpretedSortValue
1312
import io.ksmt.solver.KSolverUnsupportedFeatureException
1413
import io.ksmt.solver.util.KExprIntInternalizerBase.Companion.NOT_INTERNALIZED
1514
import io.ksmt.solver.yices.TermUtils.addTerm
@@ -19,37 +18,45 @@ import io.ksmt.solver.yices.TermUtils.funApplicationTerm
1918
import io.ksmt.solver.yices.TermUtils.mulTerm
2019
import io.ksmt.solver.yices.TermUtils.orTerm
2120
import io.ksmt.sort.KSort
22-
import io.ksmt.utils.NativeLibraryLoader
21+
import io.ksmt.sort.KUninterpretedSort
22+
import it.unimi.dsi.fastutil.ints.Int2ObjectOpenHashMap
23+
import it.unimi.dsi.fastutil.ints.IntOpenHashSet
24+
import it.unimi.dsi.fastutil.objects.Object2IntOpenHashMap
2325
import java.math.BigInteger
2426
import java.util.concurrent.atomic.AtomicInteger
2527

26-
open class KYicesContext : AutoCloseable {
27-
private var isClosed = false
28+
open class KYicesContext(ctx: KContext) : AutoCloseable {
29+
protected var isClosed = false
2830

29-
private val expressions = mkTermCache<KExpr<*>>()
30-
private val yicesExpressions = mkTermReverseCache<KExpr<*>>()
31+
protected open val expressions = mkTermCache<KExpr<*>>()
32+
protected open val yicesExpressions = mkTermReverseCache<KExpr<*>>()
3133

32-
private val sorts = mkSortCache<KSort>()
33-
private val yicesSorts = mkSortReverseCache<KSort>()
34+
protected open val sorts = mkSortCache<KSort>()
35+
protected open val yicesSorts = mkSortReverseCache<KSort>()
3436

35-
private val decls = mkTermCache<KDecl<*>>()
36-
private val yicesDecls = mkTermReverseCache<KDecl<*>>()
37+
protected open val decls = mkTermCache<KDecl<*>>()
38+
protected open val yicesDecls = mkTermReverseCache<KDecl<*>>()
3739

38-
private val vars = mkTermCache<KDecl<*>>()
39-
private val yicesVars = mkTermReverseCache<KDecl<*>>()
40+
protected open val vars = mkTermCache<KDecl<*>>()
41+
protected open val yicesVars = mkTermReverseCache<KDecl<*>>()
4042

41-
private val yicesTypes = mkSortSet()
42-
private val yicesTerms = mkTermSet()
43+
protected open val yicesTypes = mkSortSet()
44+
protected open val yicesTerms = mkTermSet()
4345

4446
val isActive: Boolean
4547
get() = !isClosed
4648

47-
fun findInternalizedExpr(expr: KExpr<*>): YicesTerm = expressions.getInt(expr)
49+
fun findInternalizedExpr(expr: KExpr<*>): YicesTerm = expressions.getInt(expr).also {
50+
if (it != NOT_INTERNALIZED)
51+
uninterpretedSortValuesTracker.expressionUse(expr)
52+
}
53+
4854
fun saveInternalizedExpr(expr: KExpr<*>, internalized: YicesTerm) {
4955
if (expressions.putIfAbsent(expr, internalized) == NOT_INTERNALIZED) {
5056
if (expr is KInterpretedValue<*> || expr is KConst<*>) {
5157
yicesExpressions.put(internalized, expr)
5258
}
59+
uninterpretedSortValuesTracker.expressionSave(expr)
5360
}
5461
}
5562

@@ -175,9 +182,9 @@ open class KYicesContext : AutoCloseable {
175182
fun functionType(domain: YicesSortArray, range: YicesSort) = mkType { Types.functionType(domain, range) }
176183
fun newUninterpretedType(name: String) = mkType { Types.newUninterpretedType(name) }
177184

178-
val zero = mkTerm { Terms.intConst(0L) }
179-
val one = mkTerm { Terms.intConst(1L) }
180-
val minusOne = mkTerm { Terms.intConst(-1L) }
185+
val zero by lazy { mkTerm { Terms.intConst(0L) } }
186+
val one by lazy { mkTerm { Terms.intConst(1L) } }
187+
val minusOne by lazy { mkTerm { Terms.intConst(-1L) } }
181188

182189
private inline fun mkTerm(mk: () -> YicesTerm): YicesTerm = withGcGuard {
183190
val term = mk()
@@ -294,7 +301,32 @@ open class KYicesContext : AutoCloseable {
294301

295302
fun uninterpretedSortConst(sort: YicesSort, idx: Int) = mkTerm { Terms.mkConst(sort, idx) }
296303

297-
private var maxValueIndex = 0
304+
protected open var maxValueIndex = 0
305+
306+
/**
307+
* Collects uninterpreted sort values usage for [KYicesModel.uninterpretedSortUniverse]
308+
*/
309+
protected open val uninterpretedSortValuesTracker = UninterpretedValuesTracker(
310+
ctx,
311+
ScopedArrayFrame(::HashSet),
312+
ScopedArrayFrame(::HashMap),
313+
Object2IntOpenHashMap<KExpr<*>>()
314+
)
315+
316+
fun pushAssertionLevel() {
317+
uninterpretedSortValuesTracker.push()
318+
}
319+
320+
fun popAssertionLevel(n: UInt) {
321+
uninterpretedSortValuesTracker.pop(n)
322+
}
323+
324+
fun registerUninterpretedSortValue(value: KUninterpretedSortValue) {
325+
uninterpretedSortValuesTracker.addToCurrentLevel(value)
326+
}
327+
328+
fun uninterpretedSortValues(sort: KUninterpretedSort) =
329+
uninterpretedSortValuesTracker.getUninterpretedSortValues(sort)
298330

299331
/**
300332
* Yices can produce different values with the same index.
@@ -339,20 +371,6 @@ open class KYicesContext : AutoCloseable {
339371
}
340372

341373
companion object {
342-
init {
343-
if (!Yices.isReady()) {
344-
NativeLibraryLoader.load { os ->
345-
when (os) {
346-
NativeLibraryLoader.OS.LINUX -> listOf("libyices", "libyices2java")
347-
NativeLibraryLoader.OS.WINDOWS -> listOf("libyices", "libyices2java")
348-
NativeLibraryLoader.OS.MACOS -> listOf("libyices", "libyices2java")
349-
}
350-
}
351-
Yices.init()
352-
Yices.setReadyFlag(true)
353-
}
354-
}
355-
356374
private const val UNINTERPRETED_SORT_VALUE_SHIFT = 1 shl 30
357375
private const val UNINTERPRETED_SORT_MAX_ALLOWED_VALUE = UNINTERPRETED_SORT_VALUE_SHIFT / 2
358376
private const val UNINTERPRETED_SORT_MIN_ALLOWED_VALUE = -UNINTERPRETED_SORT_MAX_ALLOWED_VALUE
@@ -420,7 +438,8 @@ open class KYicesContext : AutoCloseable {
420438
}
421439
}
422440

423-
private fun performGc() {
441+
@JvmStatic
442+
protected fun performGc() {
424443
// spin wait until [gcGuard] == [FREE]
425444
while (true) {
426445
if (gcGuard.compareAndSet(FREE, ON_GC)) {

‎ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesExprInternalizer.kt‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -960,7 +960,7 @@ open class KYicesExprInternalizer(
960960
yicesCtx.uninterpretedSortConst(
961961
sort.internalizeSort(),
962962
yicesCtx.uninterpretedSortValueIndex(valueIdx)
963-
)
963+
).also { yicesCtx.registerUninterpretedSortValue(expr) }
964964
}
965965
}
966966

‎ksmt-yices/src/main/kotlin/io/ksmt/solver/yices/KYicesForkingContext.kt‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,47 @@
1+
package io.ksmt.solver.yices
2+
3+
import io.ksmt.KContext
4+
5+
/**
6+
* Yices Context that allows forking and resources sharing via [KYicesForkingSolverManager].
7+
* To track resources, we have to use a unique solver specific ID, related to them.
8+
* @param [solver] is used as "specific ID" for resource tracking,
9+
* because we can't use initialized [com.sri.yices.Context] here.
10+
*/
11+
class KYicesForkingContext(
12+
ctx: KContext,
13+
manager: KYicesForkingSolverManager,
14+
solver: KYicesForkingSolver
15+
) : KYicesContext(ctx) {
16+
override val expressions = manager.findExpressionsCache(solver)
17+
override val yicesExpressions = manager.findExpressionsReversedCache(solver)
18+
19+
override val sorts = manager.findSortsCache(solver)
20+
override val yicesSorts = manager.findSortsReversedCache(solver)
21+
22+
override val decls = manager.findDeclsCache(solver)
23+
override val yicesDecls = manager.findDeclsReversedCache(solver)
24+
25+
override val vars = manager.findVarsCache(solver)
26+
override val yicesVars = manager.findVarsReversedCache(solver)
27+
28+
override val yicesTypes = manager.findTypesCache(solver)
29+
override val yicesTerms = manager.findTermsCache(solver)
30+
31+
private val maxValueIndexAtomic = manager.findMaxUninterpretedSortValueIdx(solver)
32+
33+
override var maxValueIndex: Int
34+
get() = maxValueIndexAtomic.get()
35+
set(value) {
36+
maxValueIndexAtomic.set(value)
37+
}
38+
39+
override val uninterpretedSortValuesTracker = manager.createUninterpretedValuesTracker(solver)
40+
41+
override fun close() {
42+
if (isClosed) return
43+
isClosed = true
44+
45+
performGc()
46+
}
47+
}

0 commit comments

Comments
 (0)