Z3生成模型值的隨機性

Question

我試圖影響由Z3生成的模型值的結果隨機性。據我瞭解，這個選項是非常有限的：在線性算術的情況下，單純形求解器不允許仍然滿足給定約束的隨機結果。然而，有一個選項smt.arith.random_initial_value（「使用線性運算（默認情況下，基於單面程序隨機初始值：FALSE）」），我似乎這並沒有得到工作：

from z3 import * 
set_option('smt.arith.random_initial_value',True) 
x = Int('x') 
y = Int('y') 
s = Solver() 
s.add(x+y > 0) 
s.check() 
s.model() 

這似乎總是產生[y = 0，x = 1]。即使在給定約束條件下未使用的變量的模型完成似乎始終會產生確定性結果。

有關這個選項如何工作的任何想法或提示？

Answer 1

感謝您的支持！確實有一個錯誤導致隨機種子不能傳遞到算術理論。現在已在不穩定分支中修復（修復here）。

這個例子：

(set-option :smt.arith.random_initial_value true) 
(declare-const x Int) 
(declare-const y Int) 
(assert (> (+ x y) 0)) 
(check-sat-using (using-params qflra :random_seed 1)) 
(get-model) 
(check-sat-using (using-params qflra :random_seed 2)) 
(get-model) 
(check-sat-using (using-params qflra :random_seed 3)) 
(get-model) 

現可生產三種不同的模式：

sat 
model 
    (define-fun y() Int 
    4294966763) 
    (define-fun x() Int 
    4294966337) 
) 
sat 
(model 
    (define-fun y() Int 
    216) 
    (define-fun x() Int 
    4294966341) 
) 
sat 
(model 
    (define-fun y() Int 
    196) 
    (define-fun x() Int 
    4294966344) 
) 

看起來可能存在這個選項不是通過正確傳遞（另一個地方例如，使用集時 - 而不是直接調用qflra策略），我們仍在研究這一點。