Extend synthesis solver to handle single invocation with additional universal quantif...

Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.