Массивы и типы данных в Z3py

На самом деле я использую Z3py для планирования решения проблем и пытаюсь представить двухпроцессорную систему, в которой должны выполняться четыре процесса с разным временем выполнения.

Мои фактические данные: Процесс 1: Прибытие в 0 и время выполнения 4 Процесс 2: Прибытие в 1 и время выполнения 3 Процесс 3: Прибытие в 3 и время выполнения 5 Процесс 4: Прибытие в 1 и время выполнения 2

Я на самом деле пытаюсь представить каждый процесс, разлагая каждый в подпроцессе равного времени, поэтому мои типы данных выглядят следующим образом:

Pn = Datatype('Pn')
Pn.declare('1')
Pn.declare('2')
Pn.declare('3')
Pn.declare('4')
Pt = Datatype('Pt')
Pt.declare('1')
Pt.declare('2')
Pt.declare('3')
Pt.declare('4')
Pt.declare('5')
Process = Datatype('Process')
Process.declare('cons' , ('name',Pn) , ('time', Pt))
Process.declare('idle')

где pn и pt - имя процесса и часть процесса (процесс 1 состоит из 4 частей, ...)

Но теперь я не знаю, как я могу представить свои процессоры, чтобы добавить 3 правила, которые мне нужны: уникальность (каждый подпроцесс должен выполняться 1 и только 1 раз только 1 процессором) проверка прибытия (первая часть процесса не может обрабатываться до того, как он прибыл) и порядок (каждая часть процесса должна обрабатываться после прецедента) Итак, я думал об использовании массивов для представления моих двух процессоров с таким объявлением:

P = Array('P', IntSort() , Process)

Но когда я попытался выполнить это, я получил сообщение об ошибке:

Traceback (most recent call last):
  File "C:\Users\Alexis\Desktop\test.py", line 16, in <module>
    P = Array('P', IntSort() , Process)
  File "src/api/python\z3.py", line 3887, in Array
  File "src/api/python\z3.py", line 3873, in ArraySort
  File "src/api/python\z3.py", line 56, in _z3_assert
Z3Exception: 'Z3 sort expected'

И знаю, я не знаю, как с этим справиться ... должен ли я создать новый тип данных и найти способ добавить свои правила? или Есть ли способ добавить типы данных в массив, который позволил бы мне создавать такие правила:

unicity = ForAll([x,y] , (Implies(x!=y,P[x]!=P[y])))

заранее спасибо


z3 z3py
person a.fossart    schedule 16.05.2013    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Существует руководство по использованию типов данных из Python API. Ссылка на учебник: http://rise4fun.com/Z3Py/tutorialcontent/advanced#h22 Он показывает, как создать тип данных списка и использовать метод create () для создания экземпляра объекта Sort из объекта, используемого при объявлении типа данных. Для вашего примера достаточно добавить вызовы create () в тех местах, где вы хотите использовать объявленный тип в качестве сортировки. См .: http://rise4fun.com/Z3Py/rQ7t

Что касается остальной части рассматриваемого вами тематического исследования: определенно можно выразить описываемые вами константы с помощью квантификаторов и массивов. Вы также можете рассмотреть несколько более эффективные кодировки:

  • Вместо использования массива используйте объявление функции. Таким образом, P будет объявлен как унарная функция: P = Function ('P', IntSort (), Process.create ()).
  • Использование кванторов для небольших задач с конечной областью может быть больше накладными расходами, чем преимуществом. Запись ограничений напрямую в виде конечной конъюнкции позволяет сэкономить накладные расходы на создание экземпляров кванторов, возможно, многократно. Тем не менее, некоторые количественные аксиомы также могут быть оптимизированы. Z3 автоматически компилирует аксиомы вида: ForAll ([x, y], Implies (x! = Y, P (x)! = P (y))) в аксиомы вида Forall ([x], Pinv (P (x)) == x), где «Pinv» - новая функция. Новая аксиома по-прежнему требует, чтобы P инъективен, но требует только линейного числа экземпляров, линейного по количеству вхождений P (t) для некоторого члена 't'.

Повеселись!

person Nikolaj Bjorner    schedule 16.05.2013
comment
Спасибо, это помогло мне продолжить (я не видел метод create () в учебнике ...) Но теперь я застрял, потому что, когда я пытаюсь получить модель с уникальностью (я адаптировал ее к 2 массивам), я получить только массивы, которые для всех индексов мы будем простаивать ... (0- ›idle, else-› idle), и я не знаю, как это изменить ... Так что мне еще предстоит пройти долгий путь ^^ - person a.fossart; 17.05.2013