run Nitpick examples if Kodkodi is available

merged

init_theory: Runtime.controlled_execution for proper exception trace etc.;

eliminated slightly odd name space grouping -- now managed by Isar toplevel;

implicit name space grouping for theory/local_theory transactions;

uniform new_group/reset_group;
tuned signature;

eliminated dead code;

fixed "expect" of Nitpick examples to reflect latest changes in Nitpick

merged

use SAT solver that's available everywhere for this example