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)

（来源：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

（来源：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)

由于缺少括号，第二个实际上是声明一个LEN带有两个参数（数组和整数）的函数，然后 Z3 在找到此声明的结果排序时会生成错误。

这是完整示例的链接：http ://rise4fun.com/Z3/TjNS

于 2012-12-04T15:27:02.307 回答