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と 2 つのセレクター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 に答える