2

我在使用 SMTlib2 格式的排序时遇到了一些问题。例如，我将 Interval 定义为：

(declare-sort Pair 2)
(define-sort Interval () (Pair Int Int))

现在如何从函数返回一个新的间隔？例如：

(define-fun getInterval ((a Int) (b Int)) Interval
  (Interval a b))

这行不通。我的问题是：如何构造和实例化给定类型的对象，以及如何访问它们的字段？

现在我正在使用我创建的 2 个 UF 作为字段获取器，但我仍然不知道如何拥有一个构造函数：

(declare-fun L (Interval) Int)
(declare-fun H (Interval) Int)

谢谢，努诺

4

1 回答 1

0

您应该查看Z3 SMT 指南中的记录小节、数据类型部分。mk-pair基本上，您可以使用构造函数和两个选择器创建记录类型first并second访问其字段。

这是一个示例rise4fun链接：

(set-option :macro-finder true)

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

(define-sort Interval () (Pair Int Int))
(define-fun getInterval ((a Int) (b Int)) Interval
  (mk-pair a b))

(declare-const p1 Interval)
(declare-const p2 Interval)

;construct objects of a give sort
(assert (= p1 (getInterval 2 2)))

;accessing their fields
(assert (= (first p1) (second p2)))

(check-sat)
(get-model)
于 2012-11-21T10:36:43.867 回答