Подтвердить что ты не робот

Упрощенная библиотека линейной формулы С++

Какова наилучшая (с точки зрения простоты использования и производительности) библиотека С++/С++ 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. Я написал это как вызов метода только для того, чтобы показать, что я ожидаю быть основным механизмом - подчеркнуть, что мне не нужен источник для исходного компилятора или этот вопрос не связан с оптимизацией исходной компиляции.

4b9b3361

ОТВЕТЫ

Ответ 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

Лучшим инструментом для упрощения этого выражения является ваш оптимизатор компилятора.

Насколько я знаю, библиотека С++ не перезапишет такое выражение для вас (хотя было бы технически возможно написать одно с помощью шаблонов выражений).

Я бы предложил посмотреть на код сборки, созданный вашим компилятором, с высокой оптимизацией. Это может дать вам намек. Другая альтернатива предоставляется инструментами статического анализа.