Non deterministic statistics

[majidfeyzi]

Hi, I confront with non deterministic statistics in z3py. I want to solve below smt (smt2 file):

(set-info :smt-lib-version 2.6)
(set-logic QF_NIA)
(set-info :category "industrial")
(set-info :status sat)
(declare-fun a__4 () Int)
(declare-fun a__2 () Int)
(assert (and (>= (+ (* a__4 a__2) (* (- 0 1) a__2)) 0) (>= (+ a__2 (- 0 1)) 0) (>= a__4 0) (>= a__2 0)))
(check-sat)
(exit)

after each run I get rlimit using statistics of solver, and I expected to get same rlimit in each run, but I get different rlimit values.

I set these options in z3 to make it results and statistics non-random:

z3.set_option("parallel.enable", False)
z3.set_option("parallel.threads.max", 1)
z3.set_option("fixedpoint.spacer.random_seed", 0)
z3.set_option("sat.random_seed", 0)
z3.set_option("nlsat.seed", 0)
z3.set_option("fp.spacer.random_seed", 0)
z3.set_option("smt.random_seed", 0)
z3.set_option("sls.random_seed", 0)

But it seems this options doesn't affect on the results or statistics. This is my code:

def get_rlimit(solver):
    statistics = solver.statistics()
    for i in range(len(statistics)):
        if statistics[i][0] == 'rlimit count':
            return statistics[i][1]
    return 0

solver = z3.Solver()
solver.reset()
solver.set("timeout", timeout)
rlimit_before = get_rlimit(solver)
solver.add(goal.as_expr())
satisfiability = solver.check()
rlimit_after = get_rlimit(solver)
final_rlimit = rlimit_after - rlimit_before
print(str(final_rlimit))

But final_rlimit in above code has different value in each run. I'm not using any tactic. I want to get deterministic results and statistics (specially for rlimit), everytime I run my code. How can I do it? z3py version that I'm using is 4.8.12.0.

[NikolajBjorner]

you set a timeout and expect the same rlimit to return? Furthermore, the solver may use built-in tactics with timeouts. The only way to ensure it is deterministic is to specify the solver on your own to have control. You can use SimpleSolver or a solver from a tactic.

[majidfeyzi]

I can't understand, How and why setting timeout for z3 cause non-deterministic rlimit? I set timeout to 120 second. Also using SimpleSolver instead of Solver doesn't produce same rlimit inside the loop. For example I created a test file with below code in it:

import z3

def get_rlimit(solver):
    statistics = solver.statistics()
    for i in range(len(statistics)):
        if statistics[i][0] == 'rlimit count':
            return statistics[i][1]
    return 0

for i in range(0, 10):
    solver = z3.SimpleSolver()
    solver.reset()
    solver.set("timeout", 120000)

    formula = z3.parse_smt2_file("smt_file.smt2")
    formula_goal = z3.Goal()
    formula_goal.add(formula)

    rlimit_before = get_rlimit(solver)
    solver.add(formula_goal.as_expr())
    solver.check()
    rlimit_after = get_rlimit(solver)

    final_rlimit = rlimit_after - rlimit_before
    print(str(final_rlimit))

Everytime I run this python code, I get same rlimits as result, but not in each iteration of the loop. Actually this is output for me:

272759
1245152
401853
711066
470525
851695
741843
3328923
620070
4168956

And this is my smt_file: smt_file.zip

[NikolajBjorner]

This is exactly the point about rlimit instead of a timeout. Timeouts are triggered by the OS. It is therefore non-deterministic when it triggers. The rlimit is counted deterministically (unless z3 uses a tactic that uses a timeout internally).

[majidfeyzi]

Ok, thanks for your explanations. I commented solver.set("timeout", 120000) and run test file again, but the results are the same and rlimits are different in each loop.

[majidfeyzi]

I created some solvers at the beginning and out of the loop and use them inside the loop (one for each iteration). It seems that solvers behavior changed in this way. I get same rlimits inside the loop and in each iteration except first iteration. I don't know why this is happening! Why defining of solver inside loop cause different rlimits, but defining of solver outside of the loop cause same rlimits? Is it a bug? Or is it a normal behavior?

this is the code that I have been tested it:

import z3

def get_rlimit(solver):
    statistics = solver.statistics()
    for i in range(len(statistics)):
        if statistics[i][0] == 'rlimit count':
            return statistics[i][1]
    return 0

solvers = list()
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
solvers.append(z3.SimpleSolver())
for solver in solvers:

    formula = z3.parse_smt2_file("smt_file.smt2")
    formula_goal = z3.Goal()
    formula_goal.add(formula)

    rlimit_before = get_rlimit(solver)
    solver.add(formula_goal.as_expr())
    solver.check()
    rlimit_after = get_rlimit(solver)

    final_rlimit = rlimit_after - rlimit_before
    print(str(final_rlimit))

and this is the output that I reached:

272759
272213
272213
272213
272213
272213
272213
272213
272213
272213

[majidfeyzi]

No any explanation about this problem? or any solution? No need to reopen this issue again? @NikolajBjorner