CODEWITHSUNDEEP
z3
user1458344
user1458344

Reputation: 111

Modeling array assignment in Z3

I'm working on a project for program verification. I have the following statement to be modeled in Z3:

temp = a[i];
a[i] = a[j];
a[j] = temp;

All the variables are of integer type. Would someone give me some hints on how to build constraints to model the above statements?

Upvotes: 1

Views: 256

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Here is a general "recipe".

We represent array updates using (store a i v). The result is a new array equal to a, but at position i contains the value v. An array access a[i] should be encoded as (select a i). Assignments such as i = i + 1 are usually encoded by creating Z3 variables that represent the value of i before and after the assignment. That is, we would encode it as (= i1 (+ i0 1)). Keep in mind that the formula (= i (+ i 1)) is equivalent to false.

Here is the example above encode in SMT 2.0 format.

http://www.rise4fun.com/Z3/G5Zk

Here is the script found in the link above.

(declare-const a0 (Array Int Int))
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(declare-const temp0 Int)
(declare-const temp1 Int)
(declare-const i0 Int)
(declare-const j0 Int)

(assert (= temp0 (select a0 i0)))
(assert (= a1 (store a0 i0 (select a0 j0))))
(assert (= a2 (store a1 j0 temp0)))

(check-sat)
(get-model)

Upvotes: 1

Related Questions