如何将SyGuS格式读入cvc5 Python脚本？

Question

cvc5 存储库中有许多 SyGuS 格式的示例 (https://sygus.org/language/)，例如https://github.com/cvc5/cvc5/tree/main/test/regress/cli/regress0/sygus。如何将这些文件或相应的字符串读入cvc5 Python脚本中？

我了解Python API（https://cvc5.github.io/docs/cvc5-1.0.2/api/python/python.html），它允许以编程方式定义SyGuS问题，但我想直接使用SyGuS格式。我在文档中找不到任何相关信息。

---

以下是 SyGuS 格式的问题定义示例：

(set-logic LIA)

(synth-fun max2 ((x Int) (y Int)) Int
    
    ((I Int) (B Bool))

    ((I Int (x y 0 1
             (+ I I) (- I I)
             (ite B I I)))
     (B Bool ((and B B) (or B B) (not B)
              (= I I) (<= I I) (>= I I))))
)

(declare-var x Int)
(declare-var y Int)

(constraint (>= (max2 x y) x))
(constraint (>= (max2 x y) y))
(constraint (or (= x (max2 x y)) (= y (max2 x y))))

(check-synth)

Answer 1

它对我来说效果很好：

$ cat a.sy
(set-logic LIA)

(synth-fun max2 ((x Int) (y Int)) Int

    ((I Int) (B Bool))

    ((I Int (x y 0 1
             (+ I I) (- I I)
             (ite B I I)))
     (B Bool ((and B B) (or B B) (not B)
              (= I I) (<= I I) (>= I I))))
)

(declare-var x Int)
(declare-var y Int)

(constraint (>= (max2 x y) x))
(constraint (>= (max2 x y) y))
(constraint (or (= x (max2 x y)) (= y (max2 x y))))

(check-synth)

$ cvc5 a.sy
(
(define-fun max2 ((x Int) (y Int)) Int (ite (<= x y) y x))
)

请注意，文件名必须具有扩展名

sy

。也许这让你绊倒了？