如何将之和与积约束转化为SMT-LIB2（对于Z3）

问题描述：

我不知道什么是最好的方式来一笔转换文件如何将之和与积约束转化为SMT-LIB2（对于Z3）

或类似产品

成为SMT-lib2表达式，专门用于解决与Z3（或甚至metitarski）。

我认为会有一个量词的显而易见的方法，但我在创建它时遇到了麻烦，并且在许多使用情况下，这样的总和可能具有exprLB和exprUB的常量，这意味着我希望某种策略会简单地将其展开成为一个长长的添加序列，使用量词可能会使这变得更加困难。

例如，一个相当微不足道的战术

转换成

其既平凡表示为（和平凡解决了最SMT求解器）作为

(+ 
    (/ 2 x1) 
    (/ 2 x2) 
    (/ 2 x3) 
)

yielding

sat (model (define-fun x1() Real 1.0) (define-fun x2() Real 1.0) (define-fun x3() Real (/ 1.0 4.0)))

如何可以通常表达在优雅SMT-LIB2超过三个表达式的总和（下界，上界，和累加器）？

答

明显的选择是使用数组作为您的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解算器。如果不是，你最好使用交互式定理证明，即允许你表达递归函数和归纳证明的系统;如伊莎贝尔，科克等。

如何将之和与积约束转化为SMT-LIB2（对于Z3）

相关推荐