Упрощенная библиотека линейной формулы С++
Какова наилучшая (с точки зрения простоты использования и производительности) библиотека С++/С++ 11, которая упрощает такие формулы, как следующее?
(a < 0 && b > 0) || (a < 0 && c > 0) || (a < 0 && c > 1)
до (например)
a < 0 && (b > 0 || c > 0)
Я думаю, что очень важно объяснить одно (потому что я вижу, что этот вопрос неправильно понял).
Я не хочу упрощать выражения C/С++ - я знаю, компилятор может это сделать.
Я делаю инструмент обработки графа. На ребрах графика есть некоторые условия относительно его вершин (допустим, вершины a, b, c, и эти условия похожи на a<b, b>0 и т.д. - Обратите внимание, что эти условия не выражаются как "строки", они могут быть любым вызовом функции или библиотеки). Во время обработки я собираю выражения вместе, и перед дальнейшей обработкой графика я хочу упростить их.
Условия и выражения будут созданы во время выполнения.
Я хочу иметь возможность вводить некоторые выражения в эту библиотеку, например:
[...]
a = new Variable();
b = new Variable();
expr1 = lib.addExpr(a,0, lib.LESS);
expr2 = lib.addExpr(b,0, lib.MORE);
expr3 = lib.addExpr(expr1, expr2, lib.AND);
[...]
cout << lib.solve(exprn).getConditionsOf(a);
Конечно, эта библиотека, вероятно, будет иметь гораздо более красивый API. Я написал это как вызов метода только для того, чтобы показать, что я ожидаю быть основным механизмом - подчеркнуть, что мне не нужен источник для исходного компилятора или этот вопрос не связан с оптимизацией исходной компиляции.
Ответы
Ответ 1
Вы ищете символическую математическую библиотеку для С++, которая может обрабатывать логическую логику.
Вот некоторые из них, которые нужно начать с:
- SymbolicC++: мощная символическая математическая библиотека общего назначения для С++, но не предназначена для булевой математики.
- BoolStuff: не символическая математическая библиотека общего назначения, очень ориентированная на логическую логику, но, вероятно, именно то, что вы хотите.
- Logic Friday: автономный инструмент для анализа цифровых схем и упрощенная логическая логика с API C.
Ответ 2
Если вы сначала генерируете таблицу истинности (довольно тривиальную), это сводится к проблеме минимизации схемы, которая хорошо изучена.
Ответ 3
Предлагаемая процедура
Вместо выделенной библиотеки моя предлагаемая процедура для решения вашей проблемы такова:
- Сгенерировать таблицу истинности для несимметричного булева выражения.
- Определите случаи, когда выражения сравнения с одной переменной подразумевают другие выражения сравнения одной и той же переменной. Это должно быть простым, если ваш прецедент является полностью представительным.
- Обозначьте выходы таблицы истинности как "Не заботьтесь" (DNC) для тех записей, где входные значения нарушают последствия.
- Используйте таблицу истинности как вход в булевское упрощение выражений, которое поддерживает таблицы истинности и DNC. Как говорит Махмуд Аль-Кудси, логика Пятница - хороший кандидат, и это то, что я использовал в приведенном ниже примере.
Объяснение
Предполагая, что ваш прецедент полностью отражает пространство проблем, вы можете использовать любое упрощенное выражение для булевых выражений, которое поддерживает входы таблицы истинности и характеристики вывода функции "Не заботьтесь" (DNC). Причина, по которой DNC важны, заключается в том, что некоторые из ваших выражений сравнения с одной переменной могут подразумевать другие выражения сравнения одной и той же переменной. Рассмотрим следующее выражение сравнения с одной переменной для сопоставления переменных Boolean:
A = (a < 0); B = (b > 0); C = (c > 0); D = (c > 1);
D подразумевает C или эквивалентно (не D или C) всегда истинно. Поэтому при рассмотрении входных данных в выражение вашего примера (заменяя нашу новую определенную логическую переменную)
Output = (A && B) || (A && C) || (A && D)
мы не заботимся о вводе этого выражения или выходе этого выражения, когда (а не D или C) является ложным, потому что это никогда не произойдет. Мы можем воспользоваться этим фактом, создав таблицу истинности для вышеуказанного выражения и назовите желаемые выходы как DNC в случаях, когда (а не D или C) является ложным. Из этой таблицы истинности вы можете использовать упрощенное выражение Boolean для создания упрощенного выражения.
Пример
Позвольте применить процедуру к вашему примеру, если предположить, что выражение сравнения с одной переменной для Boolean mapping mapping приведено выше. В частности, имеем
Output = (A && B) || (A && C) || (A && D)
который сопоставляется с таблицей истинности я ниже. Однако из вашего примера мы знаем, что (а не D или C) всегда истинно; поэтому мы можем обозначить все выходы, где (D, а не C), как DNC, что приводит к таблице истинности II ниже.
Truth Table I Truth Table II
============= ==============
A B C D Output A B C D Output
0 0 0 0 0 0 0 0 0 0
0 0 0 1 0 0 0 0 1 DNC
0 0 1 0 0 0 0 1 0 0
0 0 1 1 0 0 0 1 1 0
0 1 0 0 0 0 1 0 0 0
0 1 0 1 0 0 1 0 1 DNC
0 1 1 0 0 0 1 1 0 0
0 1 1 1 0 0 1 1 1 0
1 0 0 0 0 1 0 0 0 0
1 0 0 1 1 1 0 0 1 DNC
1 0 1 0 1 1 0 1 0 1
1 0 1 1 1 1 0 1 1 1
1 1 0 0 1 1 1 0 0 1
1 1 0 1 1 1 1 0 1 DNC
1 1 1 0 1 1 1 1 0 1
1 1 1 1 1 1 1 1 1 1
Включение таблицы истинности II в Logic Friday и использование ее решателя приводит к минимизированному выражению (CNF):
A && (B || C)
или, что эквивалентно, отображение из булевых переменных,
a < 0 && (b > 0 || c > 0).
Ответ 4
Я предлагаю вам построить дерево решений.
Каждое из ваших условий делит числовое пространство на два раздела. Например, c > 1 делит пространство на разделы (-Infinity, 1] и [1, +Infinity). Если у вас есть другое условие с c, например c>0, то у вас есть дополнительная точка деления 0 и, наконец, вы получите 3 раздела: (-Infinity, 0], [0,1] и [1, +Infinity).
Итак, каждый уровень дерева будет содержать соответствующее ветвление:
c<0
b<0
a<0
a>0
b>0
a<0
a>0
0<c<1
b<0
a<0
a>0
b>0
a<0
a>0
c>1
b<0
a<0
a>0
b>0
a<0
a>0
Теперь вы должны оставить только те пути, которые существуют в вашем выражении. Это будет ваша оптимизация. Не уверен, что он на 100% эффективен, но он как-то эффективен.
В вашем случае это будет
c<0
b<0: false
b>0
a<0: true
a>0: false
0<c<1
b<0
a<0: true
a>0: false
b>0
a<0: true
a>0: false
c>1
b<0
a<0: true
a>0: false
b>0
a<0: true
a>0: false
Чтобы улучшить оптимизацию, вы можете ввести сравнение поддерева и унифицированные эквивалентные поддеревья в один
c<0
b<0: false
b>0
a<0: true
a>0: false
c>0
a<0: true
a>0: false
Наконец, когда вы получаете свои значения, просто проследите дерево и проверьте свое решение. Если вы получаете тупик (удаленный путь), тогда результат false. В противном случае трассировка для выхода и результат будет true.
Ответ 5
Возможно, вы сможете получить то, что хотите от библиотеки BDD. BDD не дают вам выражения С++ в конце, но они дают вам график, из которого вы можете преобразовать выражение С++.
Я никогда не использовал его, но я слышал, что minibdd прост в использовании. См. http://www.cprover.org/miniBDD/
Ответ 6
Лучшим инструментом для упрощения этого выражения является ваш оптимизатор компилятора.
Насколько я знаю, библиотека С++ не перезапишет такое выражение для вас (хотя было бы технически возможно написать одно с помощью шаблонов выражений).
Я бы предложил посмотреть на код сборки, созданный вашим компилятором, с высокой оптимизацией. Это может дать вам намек. Другая альтернатива предоставляется инструментами статического анализа.
