[isabelle-dev] SMT components and environment variables

[Sascha Boehme]

Hi,

With changeset 3214c39777ab, the SMT solvers have been turned into
components.

As a consequence, the now obsolete environment variables
(in settings files) CVC3_SOLVER, YICES_SOLVER, and Z3_SOLVER should be
removed.  This only applies if you have used the smt method so before.

Prior to their usage, SMT solvers need to be added to the components
list -- more precisely, the paths to SMT solver bundles need to be
added to $ISABELLE_HOME_USER/etc/components.  SMT solver bundles can
be found at TU Muenchen servers in the directories ~isabelle/cvc3
(without support for Darwin-based systems for now, this will be fixed
within the next days) and ~isabelle/z3.  Note the provided LICENSE
files (e.g., Z3 is restricted for non-commercial usage only).  The
reward for this rather clumsy setup is a more powerful sledgehammer
command.

Sascha