Is there a way to check satisfiability of a python string like 'p or p -> p' in Z3 if you do not know the variable names before hand? For example I have seen this:
p = Bool('p')
solve(Implies(Or(p, p), p))
However I cannot define the variables in Z3 in advance because the proposition is given to me as a string. How can I do this with z3?
I have also seen python's eval function but it seems I need to have the variable names defined in z3 of that prior too
Some questions to ponder: What would be the meaning of that string? What if it has syntax-errors in it? How do you discern what are the valid operators/variables? Do you allow just booleans, or other sorts as well? What about grouping, precedence, and associativity of operators?
Bottom line, if you want to go directly from a string, you really have no choice but to agree on a syntax and a semantics of what those strings mean. And the only way to do that is to write a parser for those strings, and "interpret" that result in the z3 context.
One choice is to "stick" to SMTLib, i.e., ask your input to be well-formatted SMTLib scripts. If you go with this choice, then z3 already have a built-in parser for them that you can readily use. See here: https://z3prover.github.io/api/html/namespacez3py.html#a09fe122cbfbc6d3fa30a79850b2a2414 But I'm pretty sure you'll find this rather ugly and not quite what you wanted. But this is the only "out-of-the-box" solution.
The proper way to handle this issue is to write a basic parser over boolean-expressions, whose syntax (and to some extent semantics) you'll have freedom to define however way you want. Also, this isn't a particularly difficult thing to do. If you're doing this in Python, you can use ply (https://www.dabeaz.com/ply/), or go with a hand-written recursive-descent parser (https://www.booleanworld.com/building-recursive-descent-parsers-definitive-guide/).
Feel free to explore and ask further questions; though make sure to tag them appropriately if it's about parsing strings in Python; which really have nothing to do with z3/z3py.