CUDD: преобразование переменных в выходные данные - PullRequest
0 голосов
/ 02 мая 2019

Я работаю с CUDD C ++, и я хотел бы знать, возможно ли сделать следующее:

На данный момент следующая таблица хранится в bdd:

|-----|-----|-----||-----|
|  x1 |  x2 |  x3 ||  y  |
|-----|-----|-----||-----|
|  0  |  0  |  0  ||  0  |
|-----|-----|-----||-----|
|  0  |  0  |  1  ||  0  |
|-----|-----|-----||-----|
|  0  |  1  |  0  ||  1  |
|-----|-----|-----||-----|
|  0  |  1  |  1  ||  0  |
|-----|-----|-----||-----|
|  1  |  0  |  0  ||  0  |
|-----|-----|-----||-----|
|  1  |  0  |  1  ||  1  |
|-----|-----|-----||-----|
|  1  |  1  |  0  ||  0  |
|-----|-----|-----||-----|
|  1  |  1  |  1  ||  0  |
|-----|-----|-----||-----|

Можно ли создать еще одну таблицу с двумя выходами, извлекая значение x2, x3, если значение исходного вывода равно 1?:

Желаемый вывод:

|-----||-----|-----|
|  x1 ||  x2 |  x3 |
|-----||-----|-----|
|  0  ||  1  |  0  |
|-----||-----|-----|
|  1  ||  0  |  1  |
|-----||-----|-----|

Я уже пытался использовать команду ExistAbastract() и получаю 2 bdds с правильными данными, но x2 и x3 все еще являются входными данными. Можно ли преобразовать x2 и x3 из переменных в выходные данные в соответствии со значением y?

1 Ответ

0 голосов
/ 02 мая 2019

Ваша первая таблица является таблицей значений, которая для каждой комбинации x1, x2, x3 определяет значение y и, следовательно, может быть представлена ​​в виде BDD над переменными x1, x2, x3.

Ваша таблица выходных данных имеет только y1 слева от двойной строки.Следовательно, вам нужны два BDD x2 и x3, которые находятся в диапазоне только от значения x1.

Обратите внимание, что ваш вопрос неоднозначен, если для некоторого значения x1 существует несколько комбинаций x2, x3, таких что y (x1, x2, x3) = True.Но вот решение, которое работает, если это не так.

Давайте рассмотрим только тот случай, когда вам нужна функция для x2 (другой случай аналогичен).Вы экзистенциально абстрагируете x3 и получаете:

|-----|-----||-----|
|  x1 |  x2 ||  y  |
|-----|-----||-----|
|  0  |  0  ||  0  |
|-----|-----||-----|
|  0  |  1  ||  1  |
|-----|-----||-----|
|  1  |  0  ||  1  |
|-----|-----||-----|
|  1  |  1  ||  0  |
|-----|-----||-----|

Неплохое начало.Теперь, что вы хотите в качестве конечной функции, это значение для x2 в строке, для которой у истинно.Разобьем это:

  • Для всех значений для x1, если выходные данные конечной функции имеют значение true, тогда y (x1, true) равно true
  • Для всех значений для x1,если вывод конечной функции равен false, то y1 (x1, false) равен true.

мы можем построить первый случай как:

(y & x2).ExistAbstract(x2)

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

...