You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I assume this is because repeated invocations of minisat via the Process.system is slow. (Or it may be that writing and reading files is slow) My feeling is that the underlying code should figure out if invocation is going to be worth it. Many uses of minisat will be on totally trivial problems that the built-in SML code will perform well on.
There are many invocations of minisat just when loading things like bossLib (and in the course of a build, bossLib is loaded a great deal). Another alternative would be to cache minisat's output on disk so that subsequent theory builds would be quicker (this would at least test if the disk was the problem).
I assume this is because repeated invocations of minisat via the
Process.system
is slow. (Or it may be that writing and reading files is slow) My feeling is that the underlying code should figure out if invocation is going to be worth it. Many uses of minisat will be on totally trivial problems that the built-in SML code will perform well on.There are many invocations of minisat just when loading things like
bossLib
(and in the course of a build,bossLib
is loaded a great deal). Another alternative would be to cache minisat's output on disk so that subsequent theory builds would be quicker (this would at least test if the disk was the problem).Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.
The text was updated successfully, but these errors were encountered: