feat(solver/context): Use new encoding for minimize
feat(solver/context): Use new encoding for minimize

Given objective functions f₁(x), ... fₙ(x) and the current
constraints ϕᵢ which involves x. this method encodes them into a
universally quantified formula ψ:

    ψ =  ∃z₁...zₙ. (z₁ = f₁(x) ∧ ... ∧ zₙ = fₙ(x)) ∧
              [∀y. (∨ᵢ ¬ϕᵢ(y)) ∨ (z₁ ≤ f₁(y) ∨ ... ∨ zₙ ≤ fₙ(y))].

Here zᵢs are new existential variables zᵢ for fᵢ(x).

soonho-tri/dreal4,dreal/dreal4,dreal/dreal4,dreal/dreal4,soonho-tri/dreal4,soonho-tri/dreal4,soonho-tri/dreal4,dreal/dreal4