Skip to content

Commit

Permalink
Add more methods for Minisat/Glucose, fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@Lipen
Lipen committed Mar 1, 2024
1 parent ad295ed commit 7583ba4
Show file tree
Hide file tree
Showing 4 changed files with 130 additions and 18 deletions.
10 changes: 10 additions & 0 deletions kotlin-satlib-jna/src/main/kotlin/com/github/lipen/satlib/jna/LibGlucose.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,11 +7,21 @@ import com.sun.jna.Library
import com.sun.jna.Pointer
import com.sun.jna.PointerType

// Note: `glucose_Var` and `glucose_Lit` could be "inline classes",
// but JNA does not support mapping them.
data class glucose_Var(val value: Int) {
init {
require(value >= 0)
}

override fun toString(): String = "Var($value)"
}

data class glucose_Lit(val value: Int) {
init {
require(value >= 0)
}

override fun toString(): String = "Lit($value)"
}

Expand Down
10 changes: 8 additions & 2 deletions kotlin-satlib-jna/src/main/kotlin/com/github/lipen/satlib/jna/LibMiniSat.kt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,15 +7,21 @@ import com.sun.jna.Library
import com.sun.jna.Pointer
import com.sun.jna.PointerType

// TODO: Rename these classes to PascalCase:

// Note: `minisat_Var` and `minisat_Lit` could be "inline classes",
// but JNA does not support mapping them.
data class minisat_Var(val value: Int) {
init {
require(value >= 0)
}

override fun toString(): String = "Var($value)"
}

data class minisat_Lit(val value: Int) {
init {
require(value >= 0)
}

override fun toString(): String = "Lit($value)"
}

Expand Down
64 changes: 56 additions & 8 deletions ...in-satlib-solvers-jna/src/main/kotlin/com/github/lipen/satlib/solver/jna/GlucoseSolver.kt
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
@file:Suppress("MemberVisibilityCanBePrivate", "LocalVariableName")

package com.github.lipen.satlib.solver.jna

import com.github.lipen.satlib.core.Context
Expand All @@ -6,8 +8,10 @@ import com.github.lipen.satlib.core.Model
import com.github.lipen.satlib.core.newContext
import com.github.lipen.satlib.jna.LibGlucose
import com.github.lipen.satlib.jna.glucose_Lit
import com.github.lipen.satlib.jna.glucose_Var
import com.github.lipen.satlib.jna.glucose_addClause
import com.github.lipen.satlib.jna.glucose_lbool
import com.github.lipen.satlib.jna.glucose_limited_solve
import com.github.lipen.satlib.jna.glucose_solve
import com.github.lipen.satlib.solver.Solver
import com.github.lipen.satlib.solver.solve
Expand All @@ -19,7 +23,6 @@ import kotlin.math.absoluteValue

private val logger = KotlinLogging.logger {}

@Suppress("MemberVisibilityCanBePrivate")
class GlucoseSolver(
val initialSeed: Double? = null, // internal default is 0
) : Solver {
Expand Down Expand Up @@ -47,7 +50,7 @@ class GlucoseSolver(

if (ptr.pointer != Pointer.NULL) native.glucose_release(ptr)
ptr.pointer = native.glucose_init().pointer
// if (ptr.pointer == Pointer.NULL) throw OutOfMemoryError("glucose_init returned NULL")
if (ptr.pointer == Pointer.NULL) throw OutOfMemoryError("glucose_init returned NULL")
if (initialSeed != null) native.glucose_set_random_seed(ptr, initialSeed)
}

Expand Down Expand Up @@ -77,11 +80,35 @@ class GlucoseSolver(

override fun newLiteral(): Lit {
val lit = ++numberOfVariables
val ms = native.glucose_newLit(ptr)
check(lit == fromGlucose(ms))
val glucoseLit = native.glucose_newLit(ptr)
check(lit == fromGlucose(glucoseLit))
return lit
}

fun setPolarity(v: Int, b: Boolean) {
require(v > 0)
native.glucose_setPolarity(ptr, glucose_Var(v - 1), if (b) 1 else 0)
}

fun setDecision(v: Int, b: Boolean) {
require(v > 0)
native.glucose_setDecisionVar(ptr, glucose_Var(v - 1), if (b) 1 else 0)
}

fun setFrozen(v: Int, b: Boolean) {
require(v > 0)
native.glucose_setFrozen(ptr, glucose_Var(v - 1), b)
}

fun isEliminated(v: Int): Boolean {
require(v > 0)
return native.glucose_isEliminated(ptr, glucose_Var(v - 1))
}

fun eliminate(turn_off_elim: Boolean = false): Boolean {
return native.glucose_eliminate(ptr, turn_off_elim)
}

override fun addClause(literals: List<Lit>) {
++numberOfClauses
native.glucose_addClause(ptr, literals.map { toGlucose(it) })
Expand All @@ -93,28 +120,49 @@ class GlucoseSolver(
return res
}

override fun getValue(lit: Lit): Boolean {
fun solve_limited(): Boolean? {
val res = native.glucose_limited_solve(ptr, assumptions.map { toGlucose(it) })
assumptions.clear()
return when (res) {
glucose_lbool.True -> true
glucose_lbool.False -> false
glucose_lbool.Undef -> null
}
}

fun getAssignedValue(lit: Lit): Boolean? {
return when (native.glucose_value_Lit(ptr, toGlucose(lit))) {
glucose_lbool.True -> true
glucose_lbool.False -> false
glucose_lbool.Undef -> null
}
}

override fun getValue(lit: Lit): Boolean {
return when (native.glucose_modelValue_Lit(ptr, toGlucose(lit))) {
glucose_lbool.True -> true
glucose_lbool.False -> false
glucose_lbool.Undef -> false // FIXME?
}
}

override fun getModel(): Model {
// TODO: more efficient model extraction.
val data = List(numberOfVariables) { getValue(it + 1) }
return Model.from(data, zerobased = true)
}
}

// External Lit to internal glucose_Lit
fun toGlucose(lit: Lit): glucose_Lit {
require(lit != 0)
val v = lit.absoluteValue - 1
val sign = if (lit > 0) 1 else 0
return glucose_Lit(2 * v + sign)
val sign = if (lit < 0) 1 else 0
return glucose_Lit((v shl 1) + sign)
}

// Internal glucose_Lit to external Lit
fun fromGlucose(lit: glucose_Lit): Lit {
require(lit.value >= 0)
val v = (lit.value shr 1) + 1 // 1-based variable index
return if (lit.value and 1 == 1) -v else v
}
Expand Down
64 changes: 56 additions & 8 deletions ...in-satlib-solvers-jna/src/main/kotlin/com/github/lipen/satlib/solver/jna/MiniSatSolver.kt
View file
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
@file:Suppress("MemberVisibilityCanBePrivate", "LocalVariableName")

package com.github.lipen.satlib.solver.jna

import com.github.lipen.satlib.core.Context
Expand All @@ -6,8 +8,10 @@ import com.github.lipen.satlib.core.Model
import com.github.lipen.satlib.core.newContext
import com.github.lipen.satlib.jna.LibMiniSat
import com.github.lipen.satlib.jna.minisat_Lit
import com.github.lipen.satlib.jna.minisat_Var
import com.github.lipen.satlib.jna.minisat_addClause
import com.github.lipen.satlib.jna.minisat_lbool
import com.github.lipen.satlib.jna.minisat_limited_solve
import com.github.lipen.satlib.jna.minisat_solve
import com.github.lipen.satlib.solver.Solver
import com.github.lipen.satlib.solver.solve
Expand All @@ -19,7 +23,6 @@ import kotlin.math.absoluteValue

private val logger = KotlinLogging.logger {}

@Suppress("MemberVisibilityCanBePrivate")
class MiniSatSolver(
val initialSeed: Double? = null, // internal default is 0
) : Solver {
Expand Down Expand Up @@ -47,7 +50,7 @@ class MiniSatSolver(

if (ptr.pointer != Pointer.NULL) native.minisat_release(ptr)
ptr.pointer = native.minisat_init().pointer
// if (ptr.pointer == Pointer.NULL) throw OutOfMemoryError("minisat_init returned NULL")
if (ptr.pointer == Pointer.NULL) throw OutOfMemoryError("minisat_init returned NULL")
if (initialSeed != null) native.minisat_set_random_seed(ptr, initialSeed)
}

Expand Down Expand Up @@ -77,11 +80,35 @@ class MiniSatSolver(

override fun newLiteral(): Lit {
val lit = ++numberOfVariables
val ms = native.minisat_newLit(ptr)
check(lit == fromMinisat(ms))
val minisatLit = native.minisat_newLit(ptr)
check(lit == fromMinisat(minisatLit))
return lit
}

fun setPolarity(v: Int, b: Boolean) {
require(v > 0)
native.minisat_setPolarity(ptr, minisat_Var(v - 1), if (b) 1 else 0)
}

fun setDecision(v: Int, b: Boolean) {
require(v > 0)
native.minisat_setDecisionVar(ptr, minisat_Var(v - 1), if (b) 1 else 0)
}

fun setFrozen(v: Int, b: Boolean) {
require(v > 0)
native.minisat_setFrozen(ptr, minisat_Var(v - 1), b)
}

fun isEliminated(v: Int): Boolean {
require(v > 0)
return native.minisat_isEliminated(ptr, minisat_Var(v - 1))
}

fun eliminate(turn_off_elim: Boolean = false): Boolean {
return native.minisat_eliminate(ptr, turn_off_elim)
}

override fun addClause(literals: List<Lit>) {
++numberOfClauses
native.minisat_addClause(ptr, literals.map { toMinisat(it) })
Expand All @@ -93,28 +120,49 @@ class MiniSatSolver(
return res
}

override fun getValue(lit: Lit): Boolean {
fun solve_limited(): Boolean? {
val res = native.minisat_limited_solve(ptr, assumptions.map { toMinisat(it) })
assumptions.clear()
return when (res) {
minisat_lbool.True -> true
minisat_lbool.False -> false
minisat_lbool.Undef -> null
}
}

fun getAssignedValue(lit: Lit): Boolean? {
return when (native.minisat_value_Lit(ptr, toMinisat(lit))) {
minisat_lbool.True -> true
minisat_lbool.False -> false
minisat_lbool.Undef -> null
}
}

override fun getValue(lit: Lit): Boolean {
return when (native.minisat_modelValue_Lit(ptr, toMinisat(lit))) {
minisat_lbool.True -> true
minisat_lbool.False -> false
minisat_lbool.Undef -> false // FIXME?
}
}

override fun getModel(): Model {
// TODO: more efficient model extraction.
val data = List(numberOfVariables) { getValue(it + 1) }
return Model.from(data, zerobased = true)
}
}

// External Lit to internal minisat_Lit
fun toMinisat(lit: Lit): minisat_Lit {
require(lit != 0)
val v = lit.absoluteValue - 1
val sign = if (lit > 0) 1 else 0
return minisat_Lit(2 * v + sign)
val sign = if (lit < 0) 1 else 0
return minisat_Lit((v shl 1) + sign)
}

// Internal minisat_Lit to external Lit
fun fromMinisat(lit: minisat_Lit): Lit {
require(lit.value >= 0)
val v = (lit.value shr 1) + 1 // 1-based variable index
return if (lit.value and 1 == 1) -v else v
}
Expand Down

0 comments on commit 7583ba4

Please sign in to comment.