0

配列の長さをモデル化する必要があります。だから私は関数を宣言します

(declare-fun LEN ((Array Int Int)) Int)

同時に、を使用していくつかのマクロを定義したいと思いますdefine-fun。

ただし、Z3で少しテストしたところ、同じソースファイルに存在できないdefine-funようです。declare-fun

次のようなこのコードは正常に機能します。

(define-fun mymax ((a Int) (b Int)) Int
  (ite (> a b) a b))

(assert (= (mymax 100 7) 100))
(check-sat)

（src： http: //rise4fun.com/Z3/jRzs）

ただし、以下は、LEN挿入された場所に関係なく、エラーが発生します。

;(declare-fun LEN ((Array Int Int) Int) 
;unknown sort 'assert'  
(define-fun mymax ((a Int) (b Int)) Int
  (ite (> a b) a b))
; (declare-fun LEN ((Array Int Int) Int) 
;unknown sort 'assert'
(assert (= (mymax 4 7) 7))
; (declare-fun LEN ((Array Int Int) Int) 
;;unknown sort 'check-assert'
(check-sat)
;(declare-fun LEN ((Array Int Int) Int) 
 ;invalid sort, symbol, '_' or '(' expected

（src： http: //rise4fun.com/Z3/HdEy）

誰かがこれを回避する方法を知っていますか？

4

1 に答える 1

2

declare-fun一緒にdefine-fun使用できます。問題は、括弧が欠落していることです。そのはず

(declare-fun LEN ((Array Int Int)) Int)

それ以外の

(declare-fun LEN ((Array Int Int) Int)

括弧がないため、2番目は実際にはLEN2つの引数（配列と整数）で関数を宣言しています。Z3は、この宣言の結果の並べ替えを見つけることができると、エラーを生成します。

完全な例へのリンクは次のとおりです：http：//rise4fun.com/Z3/TjNS

于 2012-12-04T15:27:02.307 に答える