Bug #1786
closed
Integrate the latest CSIsat
Added by Pavel Shved over 12 years ago.
Updated over 12 years ago.
Description
Misha (and the original team) has made a lot of improvements into CSIsat, including, but not limited to, improvement of parser. Some interpolation queries we meet in drivers may only be solved with the newer CSIsat.
Besides, the CSIsat included in BLAST 2.6 is for 32bit architecture, and can't cope with large numbers that exceed 2^32.
Files
There's one more task to do for CSIsat integration except for the integration itself.
In source:blast/psrc/fe/theoremProver.ml#L1200 with a comment from Mr. Jhala: (* some RANDOM number I made up at 1am -- RJ *). As far as I remember, the piece of code there replaces numbers larger than one million with smaller numbers, because provers can't deal with them. This is unsound. If the CSIsat will be compiled alongside the BLAST, this restriction will be easily overcome: if BLAST is capable to understand a large number, CSIsat should understand it too, and no architecture discrepancy will prevent this.
Note that this prevents BLAST from verifying some training set files! Here's one of them.
Here's an update, with a formula BLAST makes crippled enough for CSIsat to not yield an interpolant:
[INF0] 48 : 2805: Block(ntStatus@FloppyDeviceControl =-2147483643;* (Irp@FloppyDeviceControl ).IoStatus.Information = 256;)
[INF0] 50 : 3118: Pred(ntStatus@FloppyDeviceControl == 259)
In the branch `csisat-integration' CSIsat is compiled alongside with BLAST and accepts 64-bit integer numbers. But BLAST still can't verify the training file attached in previous update (fails with no new predicates discovered), CSIsat can yield an interpolant in the example case, though.
There's still a problem interpolating formulae like this:
< a 5; ~ < a 12345678901234
CSIsat gives the answer `true', obviously it's incorrect. CSIsat is compiled in 64 bit and uses 64-bit GLPK version, though.
- Status changed from Open to Resolved
I'll mark this as resolved; however, the way we distribute CSIsat should be revamped, as its repository weighs hundreds of megabytes as it contains some large binary files.
Perhaps, we'll have to retreat to a smaller source repository...
- Status changed from Resolved to Closed
We chose to ship compiled CSIsat binaries for two architectures until the CSIsat repository reaches a good, publishing-ready state.
Also available in: Atom
PDF