I have a tool which is implemented in Java.
We have interfaced Z3 Sat Solver C-API using Java JNI.
I am using Z3 version 4.1
Given this situation I do the following experiments -
Experiment 1 -
- I assert some Constraints in the Solver.
- I check the result if it is sat or unsat.
Experiment 2 -
- I assert a subset of same Constraints in the Solver.
- I push the context of the solver using
Z3_solver_push()API. - I assert remaining constraints.
- I check the result if it is sat or unsat.
The reason I am doing experiment 2 is the need to backtrack.
Now in experiment 1, I get the amount of time required for the query always less than 5 seconds consistently. I have checked so far around 20-30 times. Sometimes it is even less than 2 seconds.
Now with the experiment 2, noting the fact the constraints are exactly the same, I get the query time sometimes 5 seconds, sometimes 10 seconds, sometimes 50 seconds. I also saw the query being "Timeout" with a timeout of 60 seconds.
In order to remove some doubts, I executed the same experiments from the command line.
With experiment 1, I find that the query time is always between 2.3 - 2.7 seconds.
However with experiment 2, (I put a push statement manually), the time became variable as mentioned. It varied between 10-60 seconds.
I want to know if pushing the context will cause such variation in query?
Ideally it should not. But is there a chance?
How can we avoid this randomness and get a stable behaviour similar to without push statement?
Update
I have added the example constraints, which I would like to find out which tactic to use. Please note that, it cannot reproduce the problem mentioned in the experiment. However, we use multiple such constraints such as given below, which can reproduce the problem -
(set-option :produce-models true) ; enable model generation
(set-option :print-success false)
(declare-const goal1 Int)
(declare-const goal2 Int)
(declare-const goal3 Int)
(declare-const kmax Int)
(declare-const ordA0_A0 Bool)
(declare-const ordA0_B0 Bool)
(declare-const ordB0_B0 Bool)
(declare-const ordB0_A0 Bool)
(declare-const stA0 Int)
(declare-const stB0 Int)
(declare-const stPA_0 Int)
(declare-const enPA_0 Int)
(declare-const stPB_0 Int)
(declare-const enPB_0 Int)
(declare-const kstA0 Int)
(declare-const kyA_0 Int)
(declare-const kstB0 Int)
(declare-const kyB_0 Int)
(declare-const resA_0 Int)
(declare-const resB_0 Int)
(assert (if (>= stPA_0 enPA_0) (= ordA0_A0 true) (= ordA0_A0 false)))
(assert (if (>= stPB_0 enPB_0) (= ordB0_B0 true) (= ordB0_B0 false)))
(assert (if (>= stPA_0 enPB_0) (= ordB0_A0 true) (= ordB0_A0 false)))
(assert (if (>= stPB_0 enPA_0) (= ordA0_B0 true) (= ordA0_B0 false)))
(assert (and (>= stA0 0) (<= stA0 goal2)))
(assert (and (>= stB0 0) (<= stB0 goal2)))
(assert (or (= stA0 0) (= stB0 0)))
(assert (>= stB0 (+ stA0 1)))
(assert (=> (and (= resA_0 resB_0) (= ordA0_A0 false) (= ordB0_B0 false)) (or (= ordA0_B0 true) (= ordB0_A0 true))))
(assert (=> (and (= resA_0 resB_0) (or (= ordA0_A0 true) (= ordB0_B0 true))) (and (= ordA0_B0 true) (= ordB0_A0 true))))
(assert (and (>= resA_0 0) (< resA_0 goal3)))
(assert (and (>= resB_0 0) (< resB_0 goal3)))
(assert (=> (= resA_0 resB_0) (or (= ordA0_A0 false) (= ordB0_B0 false))))
(assert (= stPA_0 (- stA0 (* goal1 kstA0))))
(assert (= enPA_0 (- (+ stA0 1) (* goal1 kyA_0))))
(assert (= stPB_0 (- stB0 (* goal1 kstB0))))
(assert (= enPB_0 (- (+ stB0 2) (* goal1 kyB_0))))
(assert (= kstA0 (div stA0 goal1)))
(assert (= kyA_0 (div (+ stA0 1) goal1)))
(assert (= kstB0 (div stB0 goal1)))
(assert (= kyB_0 (div (+ stB0 2) goal1)))
(assert (= goal2 (+ stB0 1)))
(assert (>= goal1 1))
(assert (<= goal2 6))
(assert (= kmax (div 6 goal1)))
(assert (<= goal2 6))
(assert (<= goal3 5))
(assert (= goal1 3))
(check-sat)
(get-model)
