1

我目前正在尝试使用define-fun-rec 编写SMT 脚本。我已经使用 Z3 4.4.2 版和 CVC4 1.4 版进行了测试。据我所知，这些是两者的最新版本，并且都支持该功能*。但是，两者似乎都不认识该命令。

（我根据 Nikolaj 的回复对此进行了一些更改。它仍然给出错误消息。）具体来说，给定：

(define-fun-rec 
    fac ((x Int)) Int
    (
        ite (<= x 1) 
            1 
            (* x (fac (- x 1)))
    )
)

(assert (= (fac 4) 24))

(check-sat)

Z3 输出：

unsupported
; define-fun-rec
(error "line 10 column 17: unknown function/constant fac")
sat

CVC4 输出：

(error "Parse Error: fac.smt2:1.15: expected SMT-LIBv2 command, got `define-fun-rec'.

  (define-fun-rec 
   ^
")

我最好的猜测是我需要设置某种标志，或者我需要使用一些特定的逻辑，但是我在使用 define-fun-rec 找到任何类型的详细说明或示例时遇到了很多麻烦。任何意见，将不胜感激。谢谢！

*Z3 支持：Z3 中如何处理递归函数？

CVC4 支持：http ://lara.epfl.ch/~reynolds/pres-smt15.pdf

4

2 回答 2

2

CVC4 的最新版本可以在http://cvc4.cs.nyu.edu/downloads/的“开发版本”（右侧）下下载

最新的开发版本支持递归函数定义。您可以使用 cvc4 命令行选项“--fmf-fun”来启用一种技术，该技术可以为涉及递归函数应用程序的问题找到小模型，假设定义是可接受的。

（尽管不幸的是，您的阶乘示例还需要非线性算术，而 CVC4 尚不支持。）

于 2016-07-26T15:58:24.833 回答
1
  1. 不要将逻辑设置为 LIA。这不在 LIA 片段中，Z3 将使用错误的策略来解决问题。只需删除 set-logic 行。
  2. 它有助于不在“fib”的定义中使用未定义的函数“f”。
  3. 我建议您将函数称为“fac”而不是“fib”，因为您正在定义阶乘函数。

因此，

(define-fun-rec 
   fac ((x Int)) Int
   (
    ite (<= x 1) 
        1 
        (* x (fac (- x 1)))
   )
)

(assert (= (fac 4) 24))

(check-sat)

z3-版本

Z3 版本 4.4.2

z3 fac.smt2

坐

如果您将 24 更改为 25，您将变得不满意。

于 2016-07-25T23:32:37.573 回答