Re: [isabelle] SAT solver problem



Dear Omar,

> I have problem with using nitpick even for trivial lemma such as:  lemma "P
> â Q ".
> in the output panel, I've got this kodkod warning:
> Kodkod warning: cannot launch SAT solver, falling back on "DefaultSAT4J"
> 
> I'm using Isabelle 2016 64-bit windows version. Any suggestion?

This seems to be a low-level issue. There are hard to debug; let's see if there's a workaround first.

In the Nitpick documentation (isabelle doc nitpick), there's a list of SAT solvers that can be tried. You can choose one by setting

   nitpick_params [sat_solver = <name_of_solver>]

Could you try e.g. MiniSat as the solver and see if the issue goes away?

Cheers,

Jasmin





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