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