cvc5 Python API是否支持解析SMTLIB格式字符串？

在Z3中，可直接传入SMTLIB格式字符串完成可满足性检查并获取模型，示例代码如下：

from z3 import Solver

s = Solver()

s.from_string("""
(declare-const x Int)
(declare-const y Int)

(assert (> x 2))
(assert (< y 10)) 
(assert (= (+ x y) 7))
""")

s.check()
s.model() # 返回结果为 [y = 0, x = 7]

问题 #

能否通过cvc5的Python API传入SMTLIB格式字符串，执行可满足性检查并获取模型？

结论 #

根据cvc5官方文档说明，cvc5不支持解析SMT2文件，因此也不支持直接解析SMTLIB格式的字符串。

内容的提问来源于stack exchange，提问作者Tilo RC