CODEWITHSUNDEEP
z3py
Sombrero
Sombrero

Reputation: 45

Is there a way to use range with Z3ints in z3py?

I'm relatively new to Z3 and experimenting with it in python. I've coded a program which returns the order in which different actions is performed, represented with a number. Z3 returns an integer representing the second the action starts.

Now I want to look at the model and see if there is an instance of time where nothing happens. To do this I made a list with only 0's and I want to change the index at the times where each action is being executed, to 1. For instance, if an action start at the 5th second and takes 8 seconds to be executed, the index 5 to 12 would be set to 1. Doing this with all the actions and then look for 0's in the list would hopefully give me the instances where nothing happens.

The problem is: I would like to write something like this for coding the problem

list_for_check = [0]*total_time
m = s.model()
for action in actions: 
    for index in range(m.evaluate(action.number) , m.evaluate(action.number) + action.time_it_takes):
        list_for_check[index] = 1

But I get the error:

'IntNumRef' object cannot be interpreted as an integer

I've understood that Z3 isn't returning normal ints or bools in their models, but writing

if m.evaluate(action.boolean):

works, so I'm assuming the if is overwritten in a way, but this doesn't seem to be the case with range. So my question is: Is there a way to use range with Z3 ints? Or is there another way to do this?

The problem might also be that action.time_it_takes is an integer and adding a Z3int with a "normal" int doesn't work. (Done in the second part of the range).

I've also tried using int(m.evaluate(action.number)), but it doesn't work.

Thanks in advance :)

Upvotes: 0

Views: 438

Answers (1)

alias
alias

Reputation: 30428

When you call evaluate it returns an IntNumRef, which is an internal z3 representation of an integer number inside z3. You need to call as_long() method of it to convert it to a Python number. Here's an example:

from z3 import *

s = Solver()
a = Int('a')

s.add(a > 4);
s.add(a < 7);

if s.check() == sat:
    m = s.model()
    print("a is %s" % m.evaluate(a))
    print("Iterating from a to a+5:")
    av = m.evaluate(a).as_long()
    for index in range(av, av + 5):
        print(index)

When I run this, I get:

a is 5
Iterating from a to a+5:
5
6
7
8
9

which is exactly what you're trying to achieve.

The method as_long() is defined here. Note that there are similar conversion functions from bit-vectors and rationals as well. You can search the z3py api using the interface at: https://z3prover.github.io/api/html/namespacez3py.html

Upvotes: 1

Related Questions