search

GaloisInc / cryptol

Cryptol: The Language of Cryptography
https://galoisinc.github.io/cryptol/master/RefMan.html
BSD 3-Clause "New" or "Revised" License
1.14k stars 123 forks source link

Support multiple solvers for double-checking #118

Closed atomb closed 3 years ago

atomb commented 9 years ago

This is a bifurcation of #7, since it covered multiple tasks. It would be nice to run all supported solvers to attempt to prove a property, and then check their results against one another for compatibility. Results of "unknown" or "error" would be compatible with any other result, but "sat" and "unsat" would be incompatible. Multiple "unsat" results would be compatible. Multiple "sat" results could use the approach proposed for allsat, returning a list of satisfying assignments.

dylanmc commented 8 years ago

:set prover=any comes close to this, but doesn't do the cross-checking.