Блог

Я относительно новичок в Z3 и экспериментирую с ним в python. Я закодировал программу, которая возвращает порядок, в котором выполняются различные действия, представленные числом. Z3 возвращает целое число, представляющее секунду начала действия.

Теперь я хочу взглянуть на модель и посмотреть, есть ли момент времени, когда ничего не происходит. Для этого я создал список, содержащий только 0, и я хочу изменить индекс во время выполнения каждого действия на 1. Например, если действие начинается на 5-й секунде и занимает 8 секунд для выполнения, индекс от 5 до 12 будет установлен равным 1. Выполнение этого со всеми действиями, а затем поиск 0 в списке, надеюсь, даст мне случаи, когда ничего не происходит.

Проблема в том, что я хотел бы написать что-то подобное для кодирования проблемы

 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
  

Но я получаю сообщение об ошибке:

 'IntNumRef' object cannot be interpreted as an integer
  

Я понял, что Z3 не возвращает обычные целые числа или bools в своих моделях, но пишет

 if m.evaluate(action.boolean):
  

работает, поэтому я предполагаю, что if каким-то образом перезаписан, но, похоже, это не относится к range. Итак, мой вопрос: есть ли способ использовать range с Z3 ints? Или есть другой способ сделать это?

Проблема также может заключаться в том, что action.time_it_takes является целым числом, и добавление Z3int с «обычным» int не работает. (Сделано во второй части диапазона).

Я также пробовал использовать int(m.evaluate(action.number)), но это не работает.

Заранее спасибо 🙂

При вызове evaluate он возвращает IntNumRef , которое является внутренним z3 представлением целого числа внутри z3. Вам нужно вызвать as_long() его метод, чтобы преобразовать его в число Python. Вот пример:

 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)
  

Когда я запускаю это, я получаю:

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

это именно то, чего вы пытаетесь достичь.

Метод as_long() определен здесь. Обратите внимание, что существуют аналогичные функции преобразования из битовых векторов и рациональных чисел. Вы можете выполнить поиск в API z3py, используя интерфейс по адресу: https://z3prover.github.io/api/html/namespacez3py.html