Satisfiability Modulo Theories - Reasoning and Computation