CVC5/CVC4 Python API是否支持量词消除功能？

我正在使用CVC5的Python API，需要实现与以下Z3-Py代码等价的功能：

t = Tactic("qe")
phi = Goal()
phi.add(Exists(var_list, psi))
phi_qe = t(phi)
#print(phi_qe)

即：给定公式phi、变量列表var_list以及包含var_list中变量的公式psi，应用量词消除方法t处理phi，得到简化后的公式phi_qe（可为True/False）。请问CVC5是否提供此类t函数调用的API？若CVC5没有，CVC4是否具备该功能？

• CVC5的实现方式：
  CVC5没有Z3中那种直接的Tactic类和t(phi)式调用，但可以通过API直接对公式执行量词消除操作。具体步骤如下：

  1. 创建CVC5的TermManager和Solver实例；
  2. 构造带存在量词的目标公式；
  3. 通过QuantifierEliminator工具执行量词消除，得到等价的无量词公式。

  示例代码：

  import cvc5
  from cvc5 import kinds
  
  tm = cvc5.TermManager()
  solver = cvc5.Solver(tm)
  
  # 示例：构造变量和公式psi
  x = tm.mkConst(tm.getIntegerSort(), "x")
  y = tm.mkConst(tm.getIntegerSort(), "y")
  psi = tm.mkTerm(kinds.GT, tm.mkTerm(kinds.ADD, x, y), tm.mkInteger(5))
  
  # 构造存在量词公式
  var_list = [x]
  exists_formula = tm.mkTerm(kinds.EXISTS, var_list, psi)
  
  # 执行量词消除（第二个参数控制是否简化结果）
  qe = solver.getQuantifierEliminator()
  phi_qe = qe.eliminate(exists_formula, True)
  
  print(phi_qe)
  

• CVC4的实现方式：
  CVC4支持量词消除的Python API，实现逻辑与CVC5相近，同样通过QuantifierEliminator工具完成操作，核心流程为构造带量词的公式后调用消除方法，API调用风格与CVC5基本一致。

内容的提问来源于stack exchange，提问作者Theo Deep