Open wadoon opened 5 years ago
Hi Alexander,
thank you implementing a dlang interface. Let me address your comments: 1, you can build any single app-solver pair using the scripts/mkone.sh script, it is described in the readme file. 2, ipasir_signature is specified to only return name+version, if minisat does otherwise it is a bug in the minisat implementation of ipasir. But I looked at the code and it seems to be correct. Are you sure signature prints statistics? I have noticed that release prints them, which is not forbidden. 3, the idea of ipasir is that you do not know which sat solver you will use. If you want to use minisat then you can use it directly without bothering with ipasir. Linking against multiple different sat solver is indeed impossible, but you should not need that, because an ipasir user should not care or need to know which sat solver is being used. Ipasir is designed to abstract the user away from any particular sat solver.
I solved (1) by creating an own make file. The shell script has the disadvantage of recompiling everything.
import std.stdio;
import std.conv;
import ipasir;
unittest {
auto s = new Solver();
writeln(s.signature());
}
results into
minisat220
c [minisat220]
c [minisat220] calls 0 0.0 per second
c [minisat220] restarts 0 0.0 per second
c [minisat220] conflicts 0 0.0 per second
c [minisat220] decisions 0 0.0 per second
c [minisat220] propagations 0 0.0 per second
c [minisat220]
and for picosat
picosat961
c [picosat961] 0 iterations
c [picosat961] 0 restarts
c [picosat961] 0 failed literals
c [picosat961] 0 conflicts
c [picosat961] 0 decisions
c [picosat961] 0 fixed variables
c [picosat961] 0 learned literals
c [picosat961] 0.0% deleted literals
c [picosat961] 0 propagations
c [picosat961] 0 visits
c [picosat961] 0.0% variables used
c [picosat961] 0.0 seconds in library
c [picosat961] 0.0 megaprops/second
c [picosat961] 0.0 megavisits/second
c [picosat961] probing 0.0 seconds 0%
c [picosat961] 0 simplifications
c [picosat961] 0 reductions
c [picosat961] 0.0 MB recycled
c [picosat961] 0.0 MB maximally allocated
dlopen
.Hi Alexander,
1: thank you, could you share that makefile? I would include it in the project 2: Yeah, that's because the destructor is also called in your sample program and that prints the statistics
The Makefile is available: https://github.com/wadoon/ipasir-d/blob/master/Makefile but is is a minimal version for building minisat+picosat with ipasir-interface.
That surprised me. Putting such information in an interface method would be nice:
struct entry_t { char* key, value; }
void ipasir_statistics(void* solver, entry_t* ptr, size_t* num);
Hi Alexander,
1: thank you, could you share that makefile? I would include it in the project 2: Yeah, that's because the destructor is also called in your sample program and that prints the statistics
I wonder if this is the intention. Sounds rather confusing.
I like the proposal of @wadoon to have an additional ipasir_statistics
that return the statistics into the provided buffer. However, I think we should go further and at least describe some encoding for this, e.g. JSON encoding or DIMACS-like encoding so that the caller can more easily decode the statistical information.
Hi Tomas,
I implemented an ipasir adapter for dlang.
I have several requests for enhancements:
ipasir_signature
should only return the signature (name + version) and not the statistics (seen for minisat). Here a separate extension would be nice:ipasir_statistics()
.ipasir
-declaration foreach solver, e.g.ipasir_minisat_signature
, and then I can configureipasir.h
to control to whichipasir_XXX_signature
function the functionipasir_signature
should point to.char* ipasir_signature() { return ipasir ## SOLVER ## signature ();} //not guarantee for syntax.