如何將之和與積約束轉化爲SMT-LIB2（對於Z3）

Question

我不知道什麼是最好的方式來一筆轉換文件

或類似產品

成爲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超過三個表達式的總和（下界，上界，和累加器）？

Answer 1

明顯的選擇是使用數組作爲您的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解算器。如果不是，你最好使用交互式定理證明，即允許你表達遞歸函數和歸納證明的系統;如伊莎貝爾，科克等。