Objectives and sum operator.
Add timeouts to tests.
Refactored unsat solver.
Test cases for tuples and either data types.
Fixed typing for objectives.