12. A method for providing symbolic query exploration using one or more processing devices, the method comprising: receiving input information, the input information including query information that describes a query for presenting to a database; translating the query into a formula based on a background theory, wherein the formula is expressed within the background theory; and preprocessing the formula to render the formula in a form suitable for processing by satisfiability modulo theories (SMT) solver logic, wherein the preprocessing includes using an eager expansion approach to expand the formula before submitting the formula to the SMT solver logic, wherein at least one of the translating or the preprocessing is performed by the one or more processing devices.
14. The method of claim 12 , wherein the background theory encodes one or more of: arithmetic, Booleans, tuples, sets, and algebraic data types.