1

我试图影响 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]。即使是在给定约束中未使用的变量的模型完成似乎总是会产生确定性的结果。

关于此选项如何工作的任何想法或提示？

4

1 回答 1

1

谢谢你抓住它！确实有一个错误导致随机种子无法传递给算术理论。这现在已在不稳定分支中修复（在此处修复）。

这个例子：

(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 策略时），我们仍在调查中。

于 2014-06-23T14:55:01.850 回答