[isabelle-dev] isabelle dimacs2hol

[Makarius]

On Tue, 9 Jul 2013, Tjark Weber wrote:

> On Mon, 2013-07-08 at 11:09 +0200, Makarius wrote:
>> Does the Isabelle tool "dimacs2hol" from 2004 still have a purpose?
>>
>> The DIMACS CNF format appears to be an old proposal for SAT, predating
>> newer things like SMT-LIB.  So this looks like a candidate for deletion.
>
> DIMACS CNF remains the standard input format for SAT solvers. Describing
> it as outdated wouldn't do justice to the SAT research community.

You have a link there from 2004, pointing to a paper from 1993, which 
seems to predate what they call the "official" DIMACS CNF format. (On Mac 
OS X I even failed to open that DVI file on the spot.)

So at first sight it looks unmaintained, and the usual reaction is either 
to brush it up, or keep the history in the history (via "hg rm").


> I used the tool in order to benchmark the Isabelle/HOL integration of 
> SAT solvers. This requires a full round trip, i.e., not just export of 
> propositional Isabelle/HOL formulae into DIMACS CNF, but also import of 
> DIMACS CNF benchmarks into Isabelle/HOL.

I vaguely remember a private discussion about the performance of inner 
syntax parsing in this respect.  For a realistic import one would bypass 
that anyway, i.e. not generate source files to parse them again, but read 
things directly via some Isabelle/ML functions.  Incidently, this recent 
thread on isabelle-users 
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2013-May/msg00118.html 
shows that the inner syntax parser is not the only bottle-neck, due to so 
many add-on layers in the term-check phase (and repeated term certify).


Anyway, shall I do the "hg rm" of the two relevant files now?


 	Makarius