Enums
Result returned by the
final_check call.Traits
Main interface for a solver: it makes it possible to add clauses,
allocate variables, and check for satisfiability
Theory that parametrizes the solver and can react on events
Interface provided to the theory