Причина, по которой почти нет документации по интерфейсу C ++ библиотеки CUDD, заключается в том, что это просто оболочка для функций C, для которых имеется множество документации.
Оболочка C ++ в основном полезна для избавления от всех вызовов Cudd_Ref (...) и Cudd_RecursiveDeref (...), которые должен выполнять код с использованием интерфейса C.Обратите внимание, что вы также можете использовать интерфейс C из кода C ++, если хотите.
Чтобы сделать то, что вы хотите, вы должны объединить логические операторы, предлагаемые CUDD, таким образом, чтобы вы получили новыйБулева функция с требуемыми свойствами.
Первый шаг - ограничить s случаем x = 0 и x = 1:
BDD s0 = s & !x;
BDD s1 = s & x;
Как вы заметили, новые BDD(пока) не забывает о значении переменной x.Вы хотите, чтобы они были «пофиг» на значение х.Поскольку вы уже знаете, что x ограничен одним конкретным значением в s0 и s1, вы можете использовать оператор экзистенциальной абстракции:
s0 = s0.ExistAbstract(x);
s1 = s1.ExistAbstract(x);
Обратите внимание, что x используется здесь как так называемый куб (см. ниже).
Теперь это нужные вам BDD.
Объяснение куба: Если вы абстрагируетесь от нескольких переменных одновременно, вы должны вычислить такой куб из всехпеременные, которые будут абстрагированы от первого.Куб в основном используется для представления набора переменных.Из математической логики известно, что если вы экзистенциально или универсально абстрагируете несколько переменных, то порядок абстрагирования этих переменных не имеет значения.Поскольку рекурсивные операции BDD в CUDD по возможности реализуются через пары (или тройки) BDD, CUDD внутренне представляет набор переменных также в виде куба, так что операция экзистенциальной абстракции может работать только с (1) BDD, для которогонеобходимо выполнить экзистенциальную абстракцию и (2) BDD, представляющий набор переменных, от которых необходимо абстрагироваться.Внутреннее представление куба как BDD не должно иметь отношения к разработчику, использующему только CUDD (вместо расширения CUDD), за исключением того, что BDDD, представляющий переменную, также может использоваться в качестве куба.