[isabelle-dev] sledgehammer / yices

[Sascha Boehme]

>> I am sure this is already in the pipeline. It seems that the  
>> variable YICES_INSTALLED (and the analogue for other solvers)  
>> should be mentioned in the documentation of sledgehammer (since  
>> what is currently given as installation instructions in `isabelle  
>> doc sledgehammer` of changeset 3060e6343953 does not work without  
>> setting YICES_INSTALLED="yes").
>
> Thanks for the report. I wasn't aware of this variable -- it seems  
> like this was introduced in January 2011, after I wrote the  
> documentation in Sledgehammer.
>
> The variable seems superfluous to me. It should be sufficient to  
> check whether "YICES_SOLVER" is set. Sascha, any thoughts?

I don't know for sure. It might be that YICES_INSTALLED and friends  
were added as a sanity check to avoid errors when invoking the solver  
locally and it doesn't exist. If that's the case, it's probably better  
to remove YICES_INSTALLED and just test if the file pointed to by  
YICES_SOLVER does exist.

Cheers,
Sascha