生成模型值的 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)
)

看起来可能还有另一个地方没有正确传递此选项(例如，当使用 set-logic 而不是直接调用 qflra 策略时)，我们仍在调查中。