Project

General

Profile

Actions
Copy link

Bug #1786

closed

Integrate the latest CSIsat

Added by Pavel Shved over 12 years ago. Updated over 12 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Mikhail Mandrykin
Category:
-
Target version:
2.7
Start date:
09/16/2011
Due date:
10/04/2011
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

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

BLAST_AUTO.i (261 KB) BLAST_AUTO.i file to check if CSIsat works Pavel Shved, 09/21/2011 09:08 PM
Actions
Copy link
 #1

Updated by Pavel Shved over 12 years ago

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.

Actions
Copy link
 #2

Updated by Pavel Shved over 12 years ago

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)
Actions
Copy link
 #3

Updated by Mikhail Mandrykin over 12 years ago

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.

Actions
Copy link
 #4

Updated by Pavel Shved over 12 years ago

  • 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...

Actions
Copy link
 #5

Updated by Pavel Shved over 12 years ago

  • 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.

Actions
Copy link

Also available in: Atom PDF