stp.solve

stp.solve(*fs, tm=None, ctx=None, show=True, **options)

Check the conjunction of fs; print the model, “no solution” or the reason (z3py) and return the result.