控制Z3中的随机性

Question

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

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输出中找到模块名称。