Controlling randomness in Z3

Question

Similar (but somewhat opposite) to this SO question, I do want to expose randomness if possible. That is, I want the two consecutive queries to provide different results. Is that possible? Here is my code:

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();
    }
}

And the results are the same:

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 } ...

Posted now to GitHub/Z3/issues

Answer 1

This is typically done by adding constraints to outlaw previous models. Note that unless you add new constraints, you will not get a new solution.

If you simply want to rely on randomness after solving from scratch, try setting random seeds used by z3. There are a few of them:

$ 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)

whether altering these will give you a significantly different (or different at all) model will depend on your initial set of constraints and which theory solvers come into play.

To set these from the C++ API, use the set_param function. Here's how you'd set them:

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

If you run z3 -pd it'll list all the settings you can give, per module. You can dump it to a file (z3 -pd > settings), then look at the created settings file for names that include seed to find which ones there are. Note that you have to prefix the actual names with the module they are in, as in the above example with sat and smt. You'll also find the module names in the z3 -pd output.