Z3 SMT-LIB2.0 Codependent for loops

Question

I'm a little lost using Z3, the goal is model 2 processes both running the same loop in parallel. As long as not both processes have been finished, an unfinished process is chosen and the next of its 10 steps is executed:

for i := 1 to 10 do
if x < 8 then x := x + i else x := i − 2x

x is a global variable, i is local in both instances.

Also I would like to initialize x to be 0, is this possible in Z3?

So far I'm getting unsat as a result, with this code:

(declare-const c Int)

(push)
(declare-const i1 Int)
(assert
(and
(>= i1 1)
(<= i1 20)
(ite (< c 5) (and (= c (+ c i1)) (>= i1 1) (<= i1 20)) (and (= c (- i1 (* 2 c))) (>= i1 1) (<= i1 20)))
))

(push)
(declare-const i2 Int)
(assert
(and
(>= i2 1)
(<= i2 20)
(ite (< c 5) (and (= c (+ c i2)) (>= i2 1) (<= i2 20)) (and (= c (- i2 (* 2 c))) (>= i2 1) (<= i2 20)))
))

(assert (= c -24))

(check-sat)
(get-model)
(pop)
(pop)

Thanks in advance!

Not quite clear what you are asking. You say "As long as not both processes have been finished." When do they finish? Also, what is your goal? Compute the final value of x under all interleavings? — alias

Patrick Trentin Patrick Trentin · Accepted Answer · 2017-11-24T17:29:49

The constraint

(= c (+ c i1))

is always unsat unless i1 is equal to 0, which is never the case.

Similar considerations hold for

(= c (- i1 (* 2 c)))

in this case, this would be satisfiable only if 3c = i1 for some choice of value for i1 and c s.t. c > 8 and i1 in 1..20, but some lines below you require c to be equal to -24:

(assert (= c -24))

Since i1 must be positive, it follows that c cannot be negative, hence this branch is also unsat. Given that both branches of the ite are unsat, there is no value for c s.t. the formula is satisfiable and therefore the solver correctly answers unsat.

note: you might have some fun playing with unsat cores.

Consider this pseudo-code:

int x = 0;
x = x + 1;
if (x == 1) {
    x = 2;
} else {
    x = -1;
}
assert(x == 2);

This is a possible (not very efficient) encoding:

(set-option:produce-models true)
(declare-fun x0 () Int)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(assert (= x0 0))                       ;; initial condition
(assert (= x1 (+ x0 1)))                ;; assignment to x
(assert (and
        (or (not (= x1 1)) (= x2 2))    ;; then branch
        (or (= x1 1) (= x2 (- 1)))      ;; else branch
))
(assert (= x2 2))                       ;; assertion
(check-sat)
(get-model)

The output is:

$ ./z3 test.smt2 
sat
(model 
  (define-fun x2 () Int
    2)
  (define-fun x1 () Int
    1)
  (define-fun x0 () Int
    0)
)

Observe that I declare a fresh new variable for each assignment to the original variable x in order to hold the new value.

On your example, I would perform a complete loop unrolling first, and then apply the same transformation as above.

EDIT: as mentioned in the comments by Levent Erkok, you might want to consider higher-level tools for solving that problem. For example, using NuSMV or Spin it becomes trivial to encode it.

Z3 SMT-LIB2.0 Codependent for loops

1 Answers