kosat/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt at 56e00025f545cc683fdbc95e0c7b411810cd32ae · UnitTestBot/kosat · GitHub

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
import kotlin.test.Test
import kotlin.test.assertEquals
import kotlin.test.assertFailsWith
import kotlin.test.assertFalse
import kotlin.test.assertTrue

class KotlinApiTest {
    @Test
    fun tieShirtVarargs() {
        val solver = Kosat()

        assertFailsWith(IllegalArgumentException::class) { solver.newClause(1, 2) }

        solver.newVariable()
        solver.newVariable()

        solver.newClause(-1, 2)
        solver.newClause(1, 2)
        solver.newClause(-1, -2)

        assertFailsWith(IllegalStateException::class) { solver.getModel() }
        assertFailsWith(IllegalStateException::class) { solver.value(1) }
        assertFailsWith(IllegalArgumentException::class) { solver.value(0) }
        assertFailsWith(IllegalArgumentException::class) { solver.value(-5) }

        assertTrue(solver.solve())

        assertFalse(solver.value(1))
        assertTrue(solver.value(-1))
        assertTrue(solver.value(2))
        assertFalse(solver.value(-2))

        assertFailsWith(IllegalArgumentException::class) { solver.value(0) }
        assertFailsWith(IllegalArgumentException::class) { solver.value(-5) }

        assertEquals(listOf(false, true), solver.getModel())

        assertTrue(solver.solve(-1))
        assertFalse(solver.solve(1))
        assertTrue(solver.solve(-1, 2))
        assertFalse(solver.solve(-1, -2))

        solver.newClause(1, -2)
        assertFalse(solver.solve())

        assertFailsWith(IllegalStateException::class) { solver.getModel() }

        solver.reset()

        assertFailsWith(IllegalStateException::class) { solver.getModel() }

        solver.newVariable()
        solver.newVariable()
        solver.newVariable()

        assertTrue(solver.solve())

        assertEquals(3, solver.numberOfVariables())
        assertEquals(0, solver.numberOfClauses())
        assertEquals(3, solver.getModel().size)
    }

    @Test
    fun tieShirtIterables() {
        val solver = Kosat()

        solver.newVariable()
        solver.newVariable()

        solver.newClause(listOf(-1, 2))
        solver.newClause(setOf(1, 2))
        solver.newClause(listOf(-1, -2))

        assertTrue(solver.solve())

        assertEquals(listOf(false, true), solver.getModel())

        assertTrue(solver.solve(setOf(-1)))
        assertFalse(solver.solve(listOf(1)))
        assertTrue(solver.solve(listOf(-1, 2)))
        assertFalse(solver.solve(setOf(-1, -2)))

        solver.newClause(listOf(1, -2))
        assertFalse(solver.solve())
    }
}