Improvements of CDCL public interface #59
Conversation
| /** | ||
| * Solves the CNF problem using the CDCL algorithm. | ||
| */ | ||
| // Overload for Java |
There was a problem hiding this comment.
Overloads for Java can be automatically generated via @JvmOverloads
There was a problem hiding this comment.
However, I agree that if we make two different solve methods (with List<Lit> and with vararg Int args), we should create a separate solve() no-arg method, since annotating both methods with @JvmOverloads would produce slashing methods. Alternatively, since solve(List<Lit> = emptyList) method could be (arguably) considered the main one, only it should be annotated with JvmOverloads, so that solve() is not needed at all.
| /** | ||
| * Solves the CNF problem using the CDCL algorithm. | ||
| */ | ||
| fun solve(vararg assumptions: Int): SolveResult { |
There was a problem hiding this comment.
This is very misleading interface, since it uses DIMACS numeration (1-based signed literals). Currently (after my CNF rework), this is probably the only place when CDCL uses anything dimacs-related. Ultimately, this should not be the case -- it is better to stick to one Lit-numeration everywhere.
If you still want dimacs-lit solve method, make an extension, probably even call it solveWithDimacsAssumptions(vararg assumptions: Int).
| @@ -43,10 +43,6 @@ fun main() { | |||
| // Create the instance of KoSAT solver: | |||
| val solver = CDCL() | |||
|
|
|||
| // Allocate two variables: | |||
There was a problem hiding this comment.
Auto-allocation of variable in newClause is an implementation detail, as newVariable docs clearly say. Do not teach users to rely on such behavior, but do teach them to safely pre-allocate all the used variables.
|
|
||
| internal class Example { | ||
| @Test | ||
| fun testExample() { |
There was a problem hiding this comment.
Have you removed this test from smoke tests?
|
"Java-centric interface improvements" are postponed until we have a proper API. Superseded by #63 |
Makes CDCL more accessible, especially from Java.