visual-c++ - ライブラリを簡略化するc++線形式

Question

次のような式を単純化できる最高の（使用の単純さとパフォーマンスの点で）C ++ / C ++ 11ライブラリは何ですか？

(a < 0 && b > 0) || (a < 0 && c > 0) || (a < 0 && c > 1) 

に（例）

a < 0 && (b > 0 || c > 0)

1つのことを説明することは非常に重要だと思います（この質問は誤解されていると思うので）。

私はC/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が含まれているでしょう。私はこれをメソッド呼び出しとして記述しましたが、これは、基盤となるメカニズムとして期待されるものを示すためだけのものです。つまり、ソースからソースへのコンパイラは必要ないこと、またはこの質問はソースコンパイルの最適化とは関係がないことを強調します。

Answer 1

ブール論理を処理できる C++ 用のシンボリック数学ライブラリを探しています。

以下に、開始するためのいくつかを示します。

• SymbolicC++ : C++ 用の強力な汎用シンボリック数学ライブラリですが、ブール演算を特に意図したものではありません。
• BoolStuff : 汎用のシンボリック数学ライブラリではなく、ブール論理に非常に焦点を当てていますが、おそらくまさにあなたが望むことを行います。
• Logic Friday : C API を使用したスタンドアロンのデジタル回路解析ツールおよびブール論理単純化ツール。

Answer 2

最初に真理値表を生成する場合（かなり些細なことです）、これは回路の最小化問題になります。これは十分に研究されています。

Answer 3

推奨手順

専用ライブラリの代わりに、問題を解決するための私の推奨手順は次のとおりです。

1. 単純化されていないブール式の真理値表を生成します。
2. 単一変数の比較式が同じ変数の他の比較式を暗示している場合を特定します。ユースケースが完全に代表的なものである場合、これは簡単なはずです。
3. 入力値が含意に違反するエントリについては、真理値表の出力に「Do Not Care」（DNC）のラベルを付けます。
4. 真理値表とDNCをサポートするブール式単純化子への入力として真理値表を使用します。Mahmoud Al-Qudsiが示唆しているように、Logic Fridayは良い候補であり、これは私が以下の例で使用したものです。

説明

与えられたユースケースが問題空間を完全に表していると仮定すると、真理値表の入力と「Do Not Care」（DNC）関数の出力仕様をサポートするブール式の単純化子を使用できます。DNCが重要である理由は、単一変数の比較式の一部が、同じ変数の他の比較式を暗示する可能性があるためです。次の単一変数比較式とブール変数マッピングについて考えてみます。

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ではなく）falseの場合、この式への入力もこの式の出力も、発生する可能性がないため、気にしません。上記の式の真理値表を生成することでこの事実を利用し、（DまたはCではなく）falseの場合に目的の出力にDNCのラベルを付けることができます。その真理値表から、ブール式の単純化子を使用して、単純化された式を生成できます。

例

上記のブール変数マッピングへの単一変数比較式を想定して、この手順を例に適用してみましょう。特に、

Output = (A && B) || (A && C) || (A && D)

これは、以下の真理値表Iにマップされます。ただし、あなたの例から、（DまたはCではなく）常に真であることがわかります。したがって、（CではなくD）のすべての出力に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をLogicFridayに接続し、そのソルバーを使用すると、最小化（CNF）式が生成されます。

A && (B || C)

または同等に、ブール変数からマッピングして戻します。

a < 0 && (b > 0 || c > 0).

Answer 4

決定木を作成することをお勧めします。

各条件は、数値空間を 2 つのセクションに分割します。たとえば、スペースをとセクションc > 1に分割します。たとえば、別の条件がある場合は、追加の分割ポイントがあり、最終的に、およびの 3 つのセクションが得られます。(-Infinity, 1][1, +Infinity)cc>00(-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  

最適化を改善するために、サブツリーの比較と同等のサブツリーを 1 つに導入できます。

c<0
   b<0: false
   b>0
      a<0: true
      a>0: false  
c>0
   a<0: true
   a>0: false  

最後に、値を受け取ったら、ツリーをたどって決定を確認します。行き止まり (削除されたパス) が発生した場合、結果はfalseです。それ以外の場合は終了までトレースし、結果は になりますtrue。

Answer 5

BDD ライブラリから必要なものを取得できる場合があります。BDD は最後に C++ 式を完全には提供しませんが、C++ 式を構築できるグラフを提供します。

使ったことはありませんが、minibdd は使いやすいと聞いたことがあります。http://www.cprover.org/miniBDD/を参照

Answer 6

その式を単純化するための最適なツールは、コンパイラのオプティマイザです。

私の知る限り、そのような式を書き直す C++ ライブラリはありません (ただし、式テンプレートを使用して式を作成することは技術的に可能ですが)。

高度に最適化されたコンパイラによって生成されたアセンブリ コードを確認することをお勧めします。ヒントになるかもしれません。別の代替手段は、静的分析ツールによって提供されます。