明显的选择是使用数组作为您的x值,并使用递归函数来对总和/产品进行建模。
Z3确实支持递归函数,但它不是傻瓜式的。充其量,你最好得到unknown,
,因为大多数这样的公式需要归纳证明; SMT解决者不擅长的东西。最糟糕的是,你会得到一个无益的答案,或者如果你碰到一个bug,甚至可能是一个假的答案。
这里有一个好的工作了一个例子:
(declare-fun xs() (Array Int Real))
(define-fun-rec sum ((lb Int) (ub Int)) Real
(ite (> lb ub)
0
(+ (select xs lb)
(sum (+ lb 1) ub))))
(declare-fun lb() Int)
(declare-fun ub() Int)
(assert (= (sum lb ub) 12.34))
(check-sat)
(get-value (lb ub xs))
Z3回应:
sat
((lb 0)
(ub 0)
(xs ((as const (Array Int Real)) (/ 617.0 50.0))))
这是很酷实际上,虽然也许不是令人印象深刻,你的预期。你可以将它强制在一定范围内,以及:
(declare-fun xs() (Array Int Real))
(define-fun-rec sum ((lb Int) (ub Int)) Real
(ite (> lb ub)
0
(+ (select xs lb)
(sum (+ lb 1) ub))))
(declare-fun lb() Int)
(declare-fun ub() Int)
(assert (= 1 lb))
(assert (= 3 ub))
(assert (= (sum lb ub) 12.34))
(check-sat)
(get-value (lb ub))
(eval (select xs 1))
(eval (select xs 2))
(eval (select xs 3))
这将产生:
sat
((lb 1)
(ub 3))
0.0
(- (/ 121233.0 50.0))
2437.0
这是一个正确的模型。不幸的是,对公式/断言的轻微更改会导致无用的答案。如果我尝试:
(declare-fun xs() (Array Int Real))
(define-fun-rec sum ((lb Int) (ub Int)) Real
(ite (> lb ub)
0
(+ (/ 2.0 (select xs lb))
(sum (+ lb 1) ub))))
(assert (= (sum 1 3) 12.34))
(check-sat)
然后我得到:
unknown
解算器在他们的递归函数的支持成熟的,你一定能指望他们成功地回答更多的查询。就短期而言,您很可能经常看到unknown
的回复。
就我个人而言,当您不知道您的总和/产品中有多少条款并不是最好的想法时,我认为使用SMT解算器。如果您知道术语的数量,请务必使用SMT解算器。如果不是,你最好使用交互式定理证明,即允许你表达递归函数和归纳证明的系统;如伊莎贝尔,科克等。