search

GaloisInc / saw-script

The SAW scripting language.
BSD 3-Clause "New" or "Revised" License
442 stars 63 forks source link

Allow parallel solvers #264

Open TomMD opened 6 years ago

TomMD commented 6 years ago

cryptol has the ability to :set prover=any. For the same reason that exists, it would be good to have multiple parallel solvers supported in saw. I'm not sure if it would be possible to have a parallel solver combinator par :: ProofScript SatResult -> ProofScript SatResult -> ProofScript SatResult or perhaps pars :: [ProofScript SatResult] -> ProofScript SatResult. If not then I could see benefit even from a blunt tool such as all :: ProofScript SatResult which implicitly uses abc, cvc4, z3, yices, mathsat, and trivial but can't allow more complex scripts such as unint_*.

Thoughts?

atomb commented 3 years ago

This exists in both SBV and What4, so we could add it pretty easily (as least in the all form, but probably also in the explicitly-specified form).