0

I'm trying to do a slightly odd thing with z3. I'm trying to see if I can use z3 to get something like an "apply" tactic from an interactive theorem prover. I have a theorem like ForAll([x], Implies(a(x),b(x)), and a goal c that is syntactically equal to b(x) for the appropriate choice of x. If I could instantiate x correctly, I can replace the goal c with a(inst_x). Is there a way to use z3 the get the appropriate x? I can't use just a model, because c might contain free variables.

I've been trying seeing if I could find it in z3 proof terms for a query like Implies(ForAll([x],b(x)), c), or somehow use the E-matching pattern facilities, but I'm stumped.

z3 internally must have sophisticated matching and unification capabilities, but I don't see where they might be exposed in the python interface.

Suggestions? Thanks

1 Answer 1

0

None of this is available via any API z3 currently supports, and definitely not the Python layer either. Your best bet would be to directly use the source code of z3 itself and add the necessary hooks. Needless to say, that’ll require studying the source code in considerable depth and making sure it stays current as z3 itself moves on.

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.