pruemmer
commented
2 years ago That's a good idea; I just did a few small changes that make it possible to reuse the abstractions computed in this step.
With the option -pHints, Eldarica will print the computed templates to stdout, you can then put them into some textfile. (TODO: direct output to a file)
The templates can be read back in later runs using the options
-abstract:manual -postHints:
This seems to work for small examples; I haven't tested it yet for the combination of theories you are using, so there might be things going wrong in the pretty-printing or parsing.
If your queries don't need interpolation abstraction, of course you can also use the option -abstract:off, that would be even faster.
In general, we are also working on an incremental solver interface using assumptions. That means that you could add flags (or also more complex predicates) to clauses, and later instantiate those predicates using different constraints. E.g., you could switch individual clauses on or off this way, assign values to constants, etc. I guess this would be useful in your use case?
This is more like something that would be really nice to have.
I have a query that has 364MB and 1633 rules. I run it multiple times with different targets, which usually just adds one extra tiny rule, and 99% of all these queries is the same. Eldarica spends quite a lot of time (as expected given the size of this thing) on "analyzing loop heads", which I assume to be the same in all instances I'm running.
So the idea would be to somehow cache that analysis and be able to restart from there in following instances, basically starting at CEGAR (after parsing). Taking it further I guess it could also cache refined counterexamples and so on.
And btw: it does find counterexamples and invariants in some of these queries which imo is pretty crazy hehe