I want to take mathematical functions as input and algorithmically change the values before checking with z3 if the new manipulated formulas are satisfiable. I am hoping there is some tree structure I can use. I do not want to make my own because I would like to use an existing parser to convert the formulas to z3 format. Is there such a thing? Or can I manipulate SMT 2.0 formulas? Thanks!
You can use Z3's ASTs via it's API. The SMT2 format is relatively simple though, so writing your own parser and/or serialiser isn't that hard (it's very close to Lisp).