我目前正在尝试使用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找到任何详细的说明或示例时遇到了很多麻烦 . 任何意见,将不胜感激 . 谢谢!
2 回答
不要将逻辑设置为LIA . 这不在LIA片段中,Z3将使用错误的策略来解决问题 . 只需删除set-logic line .
有助于在"fib"的定义中不使用未定义的函数"f" .
我建议您调用函数"fac"而不是"fib",因为您正在定义阶乘函数 .
从而,
Z3版本4.4.2
SAT
如果你改变24到25你就会变得不满意 .
最新版本的CVC4可以在"Development versions"(右侧)下载:http://cvc4.cs.nyu.edu/downloads/
最新的开发版本支持递归函数定义 . 您可以使用cvc4命令行选项“--fmf-fun”来启用一种技术,该技术可以查找涉及递归函数应用程序的问题的小模型,假设定义是可接受的 .
(虽然,不幸的是你的factorial例子也需要非线性算术,CVC4还不支持 . )