-
Notifications
You must be signed in to change notification settings - Fork 26
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Cache invariants, color PASS/FAIL/[assumed], & syntax definitions #64
base: master
Are you sure you want to change the base?
Conversation
…bout FAIL, and have not yet fully tested saving of invariants
… to work correctly when I test it with my own model.
Example contents of
|
Orthogonally, I'd like to mention that the
... then everything works correctly. |
I've rolled this other PR into mine, per our conversation @kenmcmil , so all these changes can be accepted at once. I'll make a few more changes that we discussed before this PR should be merged. |
The "PASS PASS" issue we observed wasn't a bug, I just pasted the word |
@kenmcmil you also mentioned maybe we should lock the file before writing/reading and unlock after. I'm not sure how best to do this, but will look into it some more. |
To be clear the lock feature is implemented. This is ready to be merged. |
This pull request makes the following changes.
database
parameter. Settingdatabase=my-file.txt
tells the code to usemy-file.txt
as a data-base. The database works like a cache of failed SMT formulae, namely, failed negations of invariants or assertions. The idea is to achieve a speed-up by caching computations done when checking the model before you added or removed an invariant, sort of like how in Coq some portion of your proof will be green and won't need to be re-evaluated just to check the next portion you write.PASS
green,FAIL
red, and[assumed]
blue (will behave slightly differently depending on your terminal theme). This improves overall legibility.setup.py
, as well as the requirement that you use Python 2.x as the code simply is not Python 3 compatible.