CODEWITHSUNDEEP
z3smtz3pyquantifierscvc4
Theo Deep
Theo Deep

Reputation: 786

Is there a quantifier elimination functionality in CVC5 or CVC4 (I am using Python API)?

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?

Upvotes: 0

Views: 130

Answers (0)

Related Questions