title: Purpose of z3::tactic and z3::goal
body: <p>I see that I can create goals, add them to a tactic, and create a solver from the tactic.</p>
  
  <p>What is the advantage of this approach over simply creating a z3::solver instance and adding my expressions to it?</p>