Debugging overwrites generated files

[ruhler]

The debug solver works great if the solver is used for a single query. But often the debug solver with a given filename is used with multiple queries, in which case the later queries overwrite the earlier queries.

This issue is exacerbated by

• the SMT monad, which performs many, often unrelated, queries with the same solver.
• the threaded runtime, which may perform multiple queries with the same solver

Can we somehow improve the situation?

I propose the following: instead of only associating a name with the debug solver, let us associate a name with every query. The debug solver can then use the name associated with the query. How this solves things:

• the SMT monad can let you name the individual queries inside it, and further, can number each query as it is run. Then the sequence of queries is clear, and the origin of each query is clear.
• the threaded runtime can number each query as it runs, so again, the sequence of queries is clear.

In more detail:

• Change the underlying type of Solver in the runtime from (IO SolverInst) to (String -> IO SolverInst) with its name. This argument will be ignored by all but the debug solver
• Add queryd function to the SMT monad, which takes the query name as an additional argument. The query function can be built on top of queryd, giving an appropriate default name.
• Have the SMT monad keep track of the query number and add that to the query name when it calls run_symbolic.
• Add run_symbolicd function to the IO monad, which takes the query name as an additional argument. The run_symbolic function can be build on top of this, giving an appropriate default name.
• Implement run_symbolicd internally with an auxiliary function which takes an extra argument, which is the int number of the query.

Things I don't entirely like about this proposal:

• why should everyone have to care about query names, when they are only used for debugging?
• queryd and run_symbolicd are slightly unpleasant. Is there a better way to let people specify a query name? Perhaps a better name for these functions?

[ruhler]

On naming schemes:

• run_symbolic is not a consistent name. It should be runSymbolic, so that it is like runState, runReader, runList, runSMT, and friends.

Given that, perhaps the best way to add a name to a query is:

• runSymbolicNamed :: String -> Solver -> Symbolic a -> IO (Maybe a)
• runSMTNamed :: String -> Solver -> SMT a -> IO a
• queryNamed :: String -> Symbolic a -> SMT (Maybe a)

Consistant, readable, doesn't force people to add names, hopefully not too onerous, and gives what we want. I vote for this approach.

[ruhler]

I implemented this in a separate branch. Observations:

• I can now get meaningful debug info out of running sketch. And it should work well with the threaded runtime.
• It's a little strange that the 'debug' solver doesn't take any arguments. Isn't it bad the user doesn't control what the name of the output file is?
• what happens if you pass a debug solver to the debug solver? Won't that break things? Shouldn't it not break things?

This suggests an alternative to me. Maybe we shouldn't associate a debug solver with a file name, but rather a file handle. That way, if you call the solver multiple times, we can just append to the file you gave us.

Benefits of this approach:

• You get sequencing directly: the sequence of output to the given file.
• The user has full control over what file is produced
• We don't need to name queries or otherwise change the interface to using the SMT solver
• The user can write comments to the debug file in between calls to things, to keep track of where they are.
• We can print debug output to stderr and stdout easily.

I think, rather than merge the debug branch, that this is the approach we ought to take. For convenience we could provide a constructor for the Debug solver which takes a filepath.

[ruhler]

The Smten base doesn't support Handles to files currently, so as an easy way out, I just changed the debug solver to be IO Solver instead of Solver. This appears to very easily fix the problem in a nice, non-invasive way.