使用Z3和SMT-LIB獲得最多兩個值

如何使用smt-lib2獲取公式的最大值？使用Z3和SMT-LIB獲得最多兩個值

我想是這樣的：

(declare-fun x() Int) 
(declare-fun y() Int) 
(declare-fun z() Int) 
(assert (= x 2)) 
(assert (= y 4)) 
(assert (= z (max x y)) 
(check-sat) 
(get-model) 
(exit)

當然， '最大' 是未知的smtlibv2。那麼，這怎麼做呢？

來源

2011-11-28 John Smith

在Z3，你可以很容易地定義一個宏max，並用它來獲得最大的兩個值：

(define-fun max ((x Int) (y Int)) Int 
    (ite (< x y) y x))

還有一個絕招使用未解釋函數模型max，這將有利於與Z3 API的使用方法：

(declare-fun max (Int Int) Int) 
(assert (forall ((x Int) (y Int)) 
    (= (max x y) (ite (< x y) y x))))

請注意，您必須設置(set-option :macro-finder true)，因此在檢查可滿足性時，Z3能夠用函數主體替換通用量詞。

來源

2011-11-28 15:09:07 pad

快速注意：'define-fun'是SMT-LIB v2標準的一部分。 –

感謝您的更正。我相應地更新了答案。 – pad

謝謝你......這確實非常好。接下來的問題將是一個最大函數，它需要n個參數（如+）。我無法讓它與「List Int」一起工作。這是如何完成的？列表最大爲 –

你有abs，每基本的數學max(a,b) = (a+b+abs(a-b))/2

來源

2011-11-28 14:53:36 MSalters

我明白了這是怎麼回事......但最終我想在多於兩個參數（浮點數）上使用max（）而不採用這種解決方法。希望有更容易的解決方案;）謝謝。 –

使用Z3和SMT-LIB獲得最多兩個值

回答

相關問題