I am using CVC5 in Python and realize that I need something that does the equivalent to the following Z3-Py code:
t = Tactic("qe")
phi = Goal()
phi.add(Exists(var_list, psi))
phi_qe = t(phi)
#print(phi_qe)
That is: given a formula phi, a list of variables var_list and a formula psi, containing variables of var_list, I apply quantifier-elimination method t to phi to obtain phi_qe, whenever phi_qe is a simplified formula or True/False.
Is there this kind of t quantifier elimination in CVC5? I mean, I guess the tool uses quantifier elimination for performing sat/unsat queries, but I would like to know if there is such t function call from the API.
In case not, is there such functionality in CVC4?