Decoupling the tree structure that is internally maintained for the constraints and the solver process itself allows the struct to be cloned and used in other circumstances without a backend solver. These commits implement these changes.
There are some directory changes that better reflect the purpose of files. All solvers from here on will be a part of backends/. Some syntactic sugar that solvers expose to make its use easier will be a part of a specific backend (such as z3 exposing declare-const) while smtlib2.rs will only expose the basic functions that are defined in the standard and guaranteed to work with all SMTLIB2 compatible solvers.
Decoupling the tree structure that is internally maintained for the constraints and the solver process itself allows the struct to be cloned and used in other circumstances without a backend solver. These commits implement these changes.
There are some directory changes that better reflect the purpose of files. All solvers from here on will be a part of
backends/. Some syntactic sugar that solvers expose to make its use easier will be a part of a specific backend (such as z3 exposing declare-const) while smtlib2.rs will only expose the basic functions that are defined in the standard and guaranteed to work with all SMTLIB2 compatible solvers.