Enhancement for ipasir.h

[wadoon]

Hi Tomas,

I implemented an ipasir adapter for dlang.

I have several requests for enhancements:

• The makefile should allow to build only minisat or picosat static objects.
• The 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().
• Currently it is only possible to link against one sat at the same time (w/o using ld).
  It would be nice to have a several ipasir-declaration foreach solver, e.g. ipasir_minisat_signature,
  and then I can configure ipasir.h to control to which ipasir_XXX_signature function the function ipasir_signature should point to.

#ifndef SOLVER
#error "..."
#endif

char* ipasir_signature() { return ipasir ## SOLVER ## signature ();} //not guarantee for syntax.

Usage:

#include "ipasir_minisat.h" // defines SOLVER as "minisat"
#include "ipasir.h" // defines SOLVER 
...

[biotomas]

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.

[wadoon]

I solved (1) by creating an own make file. The shell script has the disadvantage of recompiling everything.
2. The program

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

3. Then I need to work around with dlopen.

[biotomas]

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

[wadoon]

1. 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.

2. 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);

[Robbepop]

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.