Simplify Prover and Language

[Padraic Cashin]

Hello,

I apologize if this is not the correct forum but I have not been successful in finding my own solution and was hoping someone could point me in the correct direction.  

I am attempting to check implication relationships between invariants returned by Daikon but have been running into some problems with defining predicates and constructing my proof obligations.  Are there any resources which describe the correct usage of Simplify and how to construct an input file?

Thank you for your time,

Padraic 

[Michael Ernst]

Padraic-

I did a quick online search, but, unfortunately, I couldn't find documentation of Simplify's file format.  It should be out there somewhere in the Simplify source code or in an earlier release of Z3.

At the time Daikon's interface to theorem-proving was written, Simplify was state-of-the-art or nearly so.  Today, other tools such as Z3 are much better (faster and more capable).  The Daikon manual mentions this:  http://plse.cs.washington.edu/daikon/download/doc/daikon.html#Installing-Simplify .  So, if you cannot figure out the Simplify file format, or if Simplify is too fiddly, you could consider interfacing Daikon to a different theorem prover.  That is not a trivial task, but it isn't conceptually difficult since much of the work is mechanical translation from one file format to another.

Sorry I couldn't be more helpful.  Good luck!

Mike

--
You received this message because you are subscribed to the Google Groups "Daikon discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to daikon-discus...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/51f8e2af-a89e-46f5-98d9-55c751bdfb44%40googlegroups.com.

[Aniket Modi]

Hi Michael

I want to use Simplify for pruning out redundant invariants that Daikon gives (using the --suppress_redundant flag). However, the link for downloading the Simplify is no longer valid, and I couldn't find it online either. The documentation does mention that older versions of Z3 can be used instead, but it doesn't mention how. Could you please let me know possible ways forward? 

Thanks

Aniket 

[Michael Ernst]

Aniket-

As far as I can tell, the link first broke shortly before June 17, 2022.

A wonderful resource for obtaining deleted web files is the Wayback Machine.

It contains the file at

https://web.archive.org/web/20170201034825/https://www.kindsoftware.com/products/opensource/archives/Simplify-1.5.5-13-06-07-binary.zip

I have updated the Daikon Manual to use that link instead, as of the next release of Daikon.

-Mike

To view this discussion on the web visit https://groups.google.com/d/msgid/daikon-discuss/5232ac75-7539-4f31-ae36-b5bab6e7d685n%40googlegroups.com.