Re: [isabelle] Difficulties with "setsum" (Alfio Martini)



Hi Makarius,

> I've tried this with Isabelle2015-RC2.  It is generally better to test sledgehammer with these parameters:
> 
>  sledgehammer_params [dont_try0]
> 
> Doing that, it basically works for me (on 12 cores), but cvc4 breaks down as follows:
> 
>  SMT: Result:
>    (error "Error in option parsing: option `produce-unsat-cores' requires a proofs-enabled build of CVC4; this binary was not built with proof support")
>  "cvc4": A prover error occurred:
>  Solver "cvc4" failed -- enable tracing using the "smt_trace" option for details
> 
> This means there is something wrong with the bundled cvc4 component, and Jasmin needs to look at it.

It turns out the Windows binary is compiled without proof output. CVC4âs predecessor, CVC3, used to only work in that mode, but CVC4 now supports unsat core output (i.e. it can print the list of used axioms for a proof, which is useful to Sledgehammer). Unfortunately, the CVC4 developers compile out proof output from CVC4.

The ultimate solution will be to build a proper binary for CVC4 for Windows, but Iâm currently not in a position to do it. (I need to get a Windows license first etc., and Iâm not at the lab next week.)

What I have to offer instead is less efficient: brute-force minimization. This is what we used to do with CVC3 and Yices. It works surprisingly well, esp. that CVC4 is blindingly fast. Please apply the following exported patch to âisabelle-releaseâ.

Thanks,

Jasmin

Attachment: cvc4.export
Description: Binary data



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.