Allow power user to have access to temporary generated files

[GoogleCodeExporter]

In some cases, it is important to follow the steps of the translation from
the A4 model into the CNF.

Several temporary files are created during that process.

It would be nice to allow the power user to run A4E in debug mode in order
to allow him to check the temp files that have been created.

So far, the following elements have been identified:
* kodkod calls
* CNF given to the SAT solver

Original issue reported on code.google.com by daniel.l...@gmail.com on 17 Nov 2008 at 8:16

[GoogleCodeExporter]

Hi: Just a clarification on how to get the Alloy4 API to capture these info,
and also two cautionary notes:

1) Currently, to capture the resulting Kodkod AST, we pass 
A4Options.SatSolver.KK as
the solver.
Then after Alloy4 finishes the typechecking and bounds optimizations,
it will immediately serialize out the Kodkod input into a file,
pass the filename to the A4 reporter, then end the entire solve.
If you still want the answer, you'll have to change the solver back to SAT4J 
then do
it again.
This is not so bad, because the typechecking and bounds optimizations usually
take one second or less.

However, this flattened out serialized text file can be very HUGE if the user
specified a large bound or has many sigs and fields (since each sig and each 
field's
possible tuple values are written out in cross products); since I have to
faithfully reproduce all subexpression sharing, that means I have to keep a map
of the generated text in memory as I generate it... so for large universe/model
it will fail with OutOfMemoryException.  That's why in Alloy4, the Kodkod input
is no longer captured everytime, but only when the user asks. (It's intended
for postmortem debugging).  And we force the user to have to consciously change
the solver back to SAT4J if he wants the answer, rather than always 
automatically
capture the Kodkod Input in parallel every time... (because once he/she sets
the scope too high, then the program dies, and the user forgot he/she had
enabled CaptureKodkod input)

2) To capture the resulting CNF, we pass A4Options.SatSolver.CNF as the solver.
Then after Kodkod generates the full CNF, Kodkod will stop processing,
then Alloy will stop processing, then we will hand the CNF filename to the 
reporter.
If you still want the answer, you'll have to change the solver back to SAT4J 
then do
it again. 

Here this is a problem because for complicated models it can take minutes (or 
longer)
to generate the CNF. So we can't afford to do the CNF generation twice.
So once again, it will have to be a conscious decision on the user's part:
either he wants the CNF or wants the Answer, but can't have both by default.

- Felix

Original comment by felix2...@gmail.com on 17 Nov 2008 at 12:46