Conversation
| sourceSets { | ||
| commonMain { | ||
| dependencies { | ||
| implementation(project(":core")) |
There was a problem hiding this comment.
The module naming (and splitting, in the first place) is weird. API should NOT depend on the implementation, but the "implementation" should implement the public interface contract. Note that the "implementation" has a separate choice of making API dependency truly api (in Gradle terms, api vs implementation configuration), however it is not "mandatory": the implementation might choose to comply with the interface without actually letting us know about it.
One example of a "good" api/impl split is SLF4J and its implementations (e.g. slf4j-simple). The same goes for log4j, if you prefer it.
That way, ideally, if the user only wants the interface, it declares the dependency on api module and receives only that - bare interface. However, when the user wants some kinda implementation, it declares the dependency on "core"/"impl" module, and receives the working classes. If he wants to interact with this implementation via some fancy interface, it should either additionally declare a dependency on API-providing module, or force "core"/"impl" to provide it via api Gradle-configuration.
Currently, your "kosat-api" module provides a mere "fancy wrapper" for CDCL, not an actual API.
See https://github.com/Lipen/sat-nexus/blob/master/lib/wrappers/src/wrap_minisat.rs
All in all, I would suggest NOT splitting impl into "core" and "wrapper", since it requires the duplicate multiplatform setup, and does not provide any value. Simply provide both "internal solver" (CDCL) and "external solver" (KoSAT) in the same module (and even in the same package org.kosat.*).
| * indexing). All variables must be defined with [newVariable] before adding | ||
| * clauses. | ||
| */ | ||
| fun newClause(vararg literals: Int) { |
There was a problem hiding this comment.
What about the users that already have an IntArray of literals? Are we going to force them to use *-spread operator solver.newClause(*literals) ?
| * clauses. | ||
| */ | ||
| fun newClause(vararg literals: Int) { | ||
| newClause(literals.asIterable()) |
There was a problem hiding this comment.
You probably don't want to allow users override this method.
|
|
||
| /** | ||
| * Solve the SAT problem with the given assumptions, if any. Assumptions are | ||
| * literals in DIMACS format. |
There was a problem hiding this comment.
Only "vararg" version of solve has the comment about DIMACS literals. Instead, it should be noted in each method, or simply in the class docs.
| } | ||
|
|
||
| /** | ||
| * Solve the SAT problem with the given assumptions |
There was a problem hiding this comment.
Document the return type.
true = SAT (ok to query the model)
false = UNSAT or UNKNOWN (model querying is prohibited)
| /** | ||
| * Solve the SAT problem with the given assumptions | ||
| */ | ||
| fun solve(assumptions: Iterable<Int>): Boolean { |
There was a problem hiding this comment.
What about UNKNOWN results? Budget exhaustion and async interrupts might lead to the solver state with is neither SAT (has a satisfying model) nor UNSAT (truly proved unsatisfiability).
| */ | ||
| fun value(literal: Int): Boolean { | ||
| if (literal == 0) { | ||
| throw IllegalArgumentException("Literal must not be 0") |
There was a problem hiding this comment.
This can be written via require (it throws IllegalArgumentException, contrary to check which throws IllegalStateException).
| fun tieShirtVarargs() { | ||
| val solver = Kosat() | ||
|
|
||
| assertFailsWith(IllegalArgumentException::class) { solver.newClause(1, 2) } |
There was a problem hiding this comment.
What about assertFailsWith<IllegalStateException> { ... } ? No need for ::class when we have reified :)
| assertTrue(solver.solve(setOf(-1))) | ||
| assertFalse(solver.solve(listOf(1))) | ||
| assertTrue(solver.solve(listOf(-1, 2))) | ||
| assertFalse(solver.solve(setOf(-1, -2))) |
There was a problem hiding this comment.
What about testing the vararg (and IntArray, if you happen to choose to split them as such) solve method?
| myInclude("core") | ||
| myInclude("cli") | ||
| myInclude("web") | ||
| myInclude("api") |
There was a problem hiding this comment.
"wrapper", see the first comment in the review
2 participants
Depends on #62. Implements a public wrapper for solver in
Kosatclass.I have chosen to sacrifice a little bit of performance with
Iterable<Int>instead ofList<Int>and a little bit of code duplication. I don't think performance should be a concern at this point, as memory is reallocated into arrays anyway, at least twice in the solver itself.Furthermore, I have also decided to include rigorous checks into methods (like enforcing allocating variables before adding clauses) because it will be easier to undo this decision in the future (as opposed to adding the checks later and introducing a breaking change~ well, not really, it's not like it's specified anywhere, might be ok to bump patch).
Unfortunately, I still was not able to include Java tests in the same project, so I have only tested the interface from java world manually. It looks ok, but if writing tests in Java is necessary, I will figure something out.