Fix formula interpretation, clean up interface, add higher level functions

including dnf_of_version_subset and could_satisfy
Do proper reverse dependency analysis and version range inference