控制 Z3 中的随机性

Question

与this SO question相似（但有些相反），我确实希望尽可能公开随机性。也就是说，我希望两个连续的查询提供 不同的 结果。那可能吗？这是我的代码：

void oren_example()
{
    int i;

    // context + solver
    context ctx;
    solver solver(ctx);

    // sorts
    sort int_sort     = ctx.int_sort();
    sort seq_int_sort = ctx.seq_sort(int_sort);
    sort bool_sort    = ctx.bool_sort();

    // constants
    expr two   = ctx.int_val(2);
    expr five  = ctx.int_val(5);
    expr four  = ctx.int_val(4);
    expr three = ctx.int_val(3);

    // define State sort
    const char *names[4]={"x","A","b","n"};
    sort sorts[4]={int_sort,seq_int_sort,bool_sort,int_sort};
    func_decl_vector projs(ctx);
    sort state_sort = ctx.tuple_sort("State",4,names,sorts,projs).range();

    // define an arbitrary state sigma
    expr sigma = ctx.constant("sigma",state_sort);

    // define some predicate on the state
    func_decl init = function("init",state_sort,bool_sort);
    solver.add(forall(sigma,
        init(sigma) == (
            ((projs[0](sigma))          == two  ) &&
            ((projs[1](sigma).length()) == three) &&
            ((projs[1](sigma).nth(two)) == five ) &&
            ((projs[3](sigma))          == five ))));

    for (int k=0;k<2;k++)
    {
        // create a snapshot
        solver.push();

        // find an initial state
        solver.add(init(sigma));

        // check sat + get model
        if (solver.check() == sat)
        {
            model m = solver.get_model();
            std::cout << "x = " << m.eval(projs[0](sigma)) << "\n";
            std::cout << "A = " << m.eval(projs[1](sigma)) << "\n";
            std::cout << "b = " << m.eval(projs[2](sigma)) << "\n";
            std::cout << "n = " << m.eval(projs[3](sigma)) << "\n";

            int size = m.eval(projs[1](sigma).length()).get_numeral_int();
            std::vector<int> A;
            for (i=0;i<size;i++)
            {
                A.push_back(
                    m.eval(
                        projs[1](sigma).nth(
                            ctx.int_val(i))).get_numeral_int());
            }
            std::cout << "A = { ";
            for (i=0;i<size;i++)
            {
                std::cout << A[i] << " ";
            }
            std::cout << "}\n";
        }

        // restore snapshot
        solver.pop();
    }
}

结果是一样的：

x = 2
A = (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 5))
b = false
n = 5
A = { 6 7 5 }
x = 2
A = (seq.++ (seq.unit 6) (seq.unit 7) (seq.unit 5))
b = false
n = 5
A = { 6 7 5 } // ideally this would be different than { 6 7 5 } ...

现在发布到 GitHub/Z3/issues

Answer 1

这通常是通过对以前的模型添加约束来实现的。请注意，除非您添加新的约束，否则您不会得到新的解决方案。

如果您只是想在从头开始解决后依赖随机性，请尝试设置 z3 使用的随机种子。有几个：

$ z3 -pd | grep seed
    random_seed (unsigned int) random seed (default: 0)
    seed (unsigned int) random seed. (default: 0)
    spacer.random_seed (unsigned int) Random seed to be used by SMT solver (default: 0)
    random_seed (unsigned int) random seed for the smt solver (default: 0)
    random_seed (unsigned int) random seed (default: 0)

改变这些是否会给你一个显着不同（或完全不同）的模型将取决于你的初始约束集以及哪些理论求解器发挥作用。

要从 C++ API 设置这些，请使用 set_param 函数。以下是您如何设置它们：

set_param("sat.random_seed", 50);
set_param("smt.random_seed", 50);

如果您运行 z3 -pd 它会列出每个模块您可以提供的所有设置。您可以将其转储到一个文件 (z3 -pd > settings)，然后查看创建的 settings 文件中包含 seed 的名称，以查找存在哪些名称。请注意，您必须在实际名称前加上它们所在的模块，如上例中的 sat 和 smt。您还可以在 z3 -pd 输出中找到模块名称。

控制 Z3 中的随机性

Controlling randomness in Z3

c++

random

z3