如何将序列中的元素提取到基本类型，以便以下内容正常工作？
(define-sort ISeq () (Seq Int))
(define-const x ISeq (seq.unit 5))
(define-const y ISeq (seq.unit 6))
(assert (>= (seq.at x 0) (seq.at y 0)))
在实现合适的功能（或者向我们揭示其存在）之前，您可以使用以下解决方法：
(define-sort ISeq () (Seq Int))
(define-const x ISeq (seq.unit 5))
(define-const y ISeq (seq.unit 6))
(declare-const e1 Int)
(declare-const e2 Int)
(push)
(assert (= (seq.unit e1) (seq.at x 0)))
(assert (= (seq.unit e2) (seq.at y 0)))
(assert (not (>= e2 e1)))
(check-sat)
(pop)
(push) ;; or alternatively
(assert (not
(implies
(and
(= (seq.unit e1) (seq.at x 0))
(= (seq.unit e2) (seq.at y 0)))
(>= e2 e1))))
(check-sat)
(pop)
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
