Add local theory extensions instantiation strategy (incomplete). Refactor how defaul...

Add local theory extensions instantiation strategy (incomplete).  Refactor how default options are set for quantifiers.  Minor improvement to datatypes.  Add unsat co-datatype regression.  Clean up instantiation engine.  Set inst level 0 on introduced constants for types with no ground terms.  Return introduced constant for variable trigger when no ground terms exist.