Module Z3cfg.MakeSource

add pred add the predicate cstr to the solver

solve mk_theory call the solver and returns the mimimum number of universes needed to solve the constraints as long as the model. The theory used by solver depends on the number of universes needed. Hence one needs to provide a function mk_theory that builds a theory when at most i are used.