(57)【要約】【課題】条件式の可読性を向上できる情報処理装置、情報処理方法および情報処理プログラムを提供する。【解決手段】情報処理装置は、リスト生成部と抽出部と存否表生成部と条件表生成部と更新部と条件式生成部とを有する。リスト生成部は、第１条件式を連言節の選言の形式に展開して連言節のリストを生成する。抽出部は、比較演算子を１つ有する第２条件式を第１条件式から抽出する。存否表生成部は、連言節ごとに第２条件式の存否を管理する存否表を生成する。条件表生成部は、因数分解の因数条件と連言節とを対応させる因数条件表を生成する。更新部は、因数条件に含まれない因数条件の候補に基づいて生成した第３条件式について真偽を判定し、判定の結果が真である場合に、第３条件式に基づいて存否表を更新する。条件式生成部は、更新された存否表に基づいて、第１条件式を簡約化して第４条件式を生成する。【選択図】図１
2018195042.tif 000002
【特許請求の範囲】
【請求項１】
第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成するリスト生成部と、
論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出する抽出部と、
生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成する存否表生成部と、
生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成する条件表生成部と、
生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新する更新部と、
更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する条件式生成部と、
を有することを特徴とする情報処理装置。
【請求項２】
前記条件表生成部は、前記第２条件式および前記第２条件式の否定を前記因数条件の候補として、前記連言節のリストに含まれる前記連言節を因数分解し、前記因数条件ごとに該因数条件を有する前記連言節を対応させる前記因数条件表を生成し、
前記更新部は、前記因数条件に含まれる前記候補の個数が多い順に、前記因数条件に含まれない前記候補の連言節である第５条件式を生成し、生成した前記第５条件式を選言で結合した前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、判定した前記第３条件式に含まれる前記第２条件式が不在となるように前記存否表を更新することを特徴とする請求項１に記載の情報処理装置。
【請求項３】
前記条件表生成部は、前記因数条件を有する前記連言節が３つ以上である前記因数条件に基づいて、前記因数条件表を生成することを特徴とする請求項２に記載の情報処理装置。
【請求項４】
前記第１条件式は、プログラムをシンボリック実行した場合におけるパス、前記パスのパス条件およびパス出力を抽出して、前記パス出力の出力変数ごとに、該出力変数の出力値が同一となる前記パスの前記パス条件に基づいて生成された選言条件式であることを特徴とする請求項１〜３のいずれか１つに記載の情報処理装置。
【請求項５】
前記抽出部は、前記第１条件式に代えて、前記連言節のリストから前記第２条件式を抽出することを特徴とする請求項１〜４のいずれか１つに記載の情報処理装置。
【請求項６】
前記更新部は、前記存否表の値のパターンに基づいて、前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新することを特徴とする請求項１〜５のいずれか１つに記載の情報処理装置。
【請求項７】
第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成し、
論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出し、
生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成し、
生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成し、
生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新し、
更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する
処理をコンピュータが実行することを特徴とする情報処理方法。
【請求項８】
第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成し、
論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出し、
生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成し、
生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成し、
生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新し、
更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する
処理をコンピュータに実行させることを特徴とする情報処理プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報処理装置、情報処理方法および情報処理プログラムに関する。
【背景技術】
【０００２】
既存の情報システムの保守や再構築の際には、情報システムに関するドキュメントや情報システムの構築に関わった有識者の知識を用いることが多い。ところが、情報システムに関するドキュメントは、内容が更新されず、記載された情報が古い場合がある。また、有識者も異動や退職等により活用することが難しい場合がある。このため、運用中の既存の情報システムのプログラムを分析することで、当該情報システムの保守や再構築の際に不足する情報を補うプログラムの仕様抽出が行われている。
【０００３】
プログラムの仕様抽出には、例えば、入力変数にシンボル値を設定してプログラムの実行をエミュレートするシンボリック実行を用いる。シンボリック実行の実行結果は、実行可能なパス、パス条件およびパス出力である。これらの実行結果は、例えば、入力に関する条件とその条件が満たされた場合の出力の表であるロジック表として得ることができる。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２０１３−１４３０６７号公報
【特許文献２】特開平８−１６３７８号公報
【特許文献３】特開平４−１９６８１５号公報
【特許文献４】特開平３−１０３７７号公報
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、シンボリック実行の結果であるロジック表には、パス条件の条件式に余分な条件が含まれる。余分な条件が含まれる条件式は、例えばクワイン・マクラスキー法（以下、ＱＭ法という）を用いて真偽が逆となる２個の条件式について簡約化することができるが、関係する条件式が３個以上の場合には簡約化することが困難である。このため、ロジック表の条件式を人が読む場合における可読性を向上させることが難しい。
【０００６】
一つの側面では、本発明は、条件式の可読性を向上できる情報処理装置、情報処理方法および情報処理プログラムを提供することにある。
【課題を解決するための手段】
【０００７】
一つの態様では、情報処理装置は、リスト生成部と、抽出部と、存否表生成部と、条件表生成部と、更新部と、条件式生成部とを有する。リスト生成部は、第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成する。抽出部は、論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出する。存否表生成部は、生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成する。条件表生成部は、生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成する。更新部は、生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新する。条件式生成部は、更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する。
【発明の効果】
【０００８】
条件式の可読性を向上できる。
【図面の簡単な説明】
【０００９】
【図１】図１は、実施例の情報処理装置の構成の一例を示すブロック図である。
【図２】図２は、ロジック表記憶部の一例を示す図である。
【図３】図３は、ロジック表記憶部の他の一例を示す図である。
【図４】図４は、リスト記憶部の一例を示す図である。
【図５】図５は、リスト記憶部の他の一例を示す図である。
【図６】図６は、第２条件式記憶部の一例を示す図である。
【図７】図７は、存否表記憶部の一例を示す図である。
【図８】図８は、因数条件表記憶部の一例を示す図である。
【図９】図９は、シンボリック実行の対象となるプログラムの一例を示す図である。
【図１０】図１０は、シンボリック実行によるパスの抽出の一例を示す図である。
【図１１】図１１は、シンボリック実行の結果の一例を示す図である。
【図１２】図１２は、ロジック表の一例を示す図である。
【図１３】図１３は、シンボリック実行の対象となるプログラムの他の一例を示す図である。
【図１４】図１４は、シンボリック実行の結果の他の一例を示す図である。
【図１５】図１５は、シンボリック実行の対象となるプログラムの他の一例を示す図である。
【図１６】図１６は、シンボリック実行の結果の他の一例を示す図である。
【図１７】図１７は、条件式ツリーの構成の一例を示す図である。
【図１８】図１８は、部分存否表の生成の一例を示す図である。
【図１９】図１９は、第３条件式の真偽判定ルールに対応する存否パターンの一例を示す図である。
【図２０】図２０は、存否パターンをグラフで表した場合の一例を示す図である。
【図２１】図２１は、第３条件式の真偽判定ルールに対応する存否パターンの他の一例を示す図である。
【図２２】図２２は、存否パターンをグラフで表した場合の他の一例を示す図である。
【図２３】図２３は、存否表の更新の一例を示す図である。
【図２４】図２４は、存否表の更新の一例を示す図である。
【図２５】図２５は、存否表に基づく条件式の生成の一例を示す図である。
【図２６】図２６は、実施例の簡約化処理の一例を示すフローチャートである。
【図２７】図２７は、リスト生成処理の一例を示すフローチャートである。
【図２８】図２８は、ド・モルガンの法則適用処理の一例を示すフローチャートである。
【図２９】図２９は、ド・モルガンの法則適用処理の一例を示すフローチャートである。
【図３０】図３０は、分配法則適用処理の一例を示すフローチャートである。
【図３１】図３１は、分配法則適用処理の一例を示すフローチャートである。
【図３２】図３２は、収集処理の一例を示すフローチャートである。
【図３３】図３３は、収集処理の一例を示すフローチャートである。
【図３４】図３４は、抽出処理の一例を示すフローチャートである。
【図３５】図３５は、抽出処理の一例を示すフローチャートである。
【図３６】図３６は、存否表生成処理の一例を示すフローチャートである。
【図３７】図３７は、同値判定処理の一例を示すフローチャートである。
【図３８】図３８は、ツリー判定処理の一例を示すフローチャートである。
【図３９】図３９は、ＳＭＴソルバ判定処理の一例を示すフローチャートである。
【図４０】図４０は、条件表生成処理の一例を示すフローチャートである。
【図４１】図４１は、条件表生成処理の一例を示すフローチャートである。
【図４２】図４２は、更新処理の一例を示すフローチャートである。
【図４３】図４３は、第３条件式判定処理の一例を示すフローチャートである。
【図４４】図４４は、条件式生成処理の一例を示すフローチャートである。
【図４５】図４５は、情報処理プログラムを実行するコンピュータの一例を示す図である。
【発明を実施するための形態】
【００１０】
以下、図面に基づいて、本願の開示する情報処理装置、情報処理方法および情報処理プログラムの実施例を詳細に説明する。なお、本実施例により、開示技術が限定されるものではない。また、以下の実施例は、矛盾しない範囲で適宜組みあわせてもよい。
【実施例】
【００１１】
図１は、実施例の情報処理装置の構成の一例を示すブロック図である。図１に示す情報処理装置１００には、例えば、プログラムをシンボリック実行した場合におけるパス、パスのパス条件およびパス出力に基づいて生成された条件式が第１条件式として入力される。情報処理装置１００は、入力された第１条件式を連言節（以下、ＤＮＦ（Disjunctive  Normal  Form）項ともいう）の選言の形式に展開して、連言節のリストを生成する。また、情報処理装置１００は、論理演算子を含まずに比較演算子を１つ有する第２条件式を、第１条件式から抽出する。
【００１２】
情報処理装置１００は、生成された連言節のリストと、抽出された第２条件式とに基づいて、連言節ごとに第２条件式の存否を管理する存否表を生成する。情報処理装置１００は、生成された連言節のリストおよび存否表に基づいて、因数分解の因数条件と連言節とを対応させる因数条件表を生成する。情報処理装置１００は、生成された因数条件表および存否表に基づいて、因数条件に含まれない因数条件の候補に基づいて生成した第３条件式について真偽を判定し、判定の結果が真である場合に、第３条件式に基づいて存否表を更新する。情報処理装置１００は、更新された存否表に基づいて、第１条件式を簡約化して第４条件式を生成する。これにより、情報処理装置１００は、条件式の可読性を向上できる。
【００１３】
ここで、各条件式について説明する。第１条件式は、例えば、シンボリック実行後の条件式の簡約化処理の対象となる条件式である。第２条件式は、論理演算子を含まずに比較演算子を１つ有する条件式であり、例えば（０＜値段）といった条件式である。第２条件式は、原子比較条件式または基本比較式ともいう。第３条件式は、後述する第５条件式を選言（ＯＲ，∨）で結合した条件式であり、簡約化できるか否かの判定対象の部分条件式である。第４条件式は、簡約化されて出力される条件式である。第５条件式は、因数条件に含まれない因数条件の候補（第２条件式）の連言（ＡＮＤ，∧）である。すなわち、第５条件式は、第３条件式のうち、選言（ＯＲ，∨）で切れる１つの節の条件式であり、節の中には連言（ＡＮＤ，∧）がある場合がある。また、存否表の更新時には、第６条件式を用いる。第６条件式は、更新された存否表の行ごとに第２条件式を連言で結合した条件式である。
【００１４】
また、上述の情報処理装置１００の処理について、下記の例にて説明する。第１条件式として、下記の式（１）があるとする。
【００１５】
（（Ｘ＞１）∧（Ｙ＜０））∨（（Ｘ＞１）∧（Ｙ＞１０））
∨（（Ｘ＞１）∧（Ｙ  ＮＯＴ＜０）∧（Ｙ  ＮＯＴ＞１０））          …（１）
【００１６】
上記の式（１）はＤＮＦであるので、ＤＮＦへの展開は省略する。ＤＮＦ項は、順に、（（Ｘ＞１）∧（Ｙ＜０））、（（Ｘ＞１）∧（Ｙ＞１０））、（（Ｘ＞１）∧（Ｙ  ＮＯＴ＜０）∧（Ｙ  ＮＯＴ＞１０））となる。また、第２条件式は、（Ｘ＞１）、（Ｙ＜０）、（Ｙ＞１０）である。式（１）は、（Ｘ＞１）を因数条件として因数分解でき、下記の式（２）となる。
【００１７】
（Ｘ＞１）∧（（Ｙ＜０）∨（Ｙ＞１０）∨（（Ｙ  ＮＯＴ＜０）
∧（Ｙ  ＮＯＴ＞１０）））                                          …（２）
【００１８】
ここで、因数条件（Ｘ＞１）と連言される条件式は、下記の式（３）である。式（３）が恒真式（Ｙの値が何であっても常に真）であることを判定する。
【００１９】
（Ｙ＜０）∨（Ｙ＞１０）∨（（Ｙ  ＮＯＴ＜０）∧（Ｙ  ＮＯＴ＞１０））
＝ＴＲＵＥ                                                          …（３）
【００２０】
式（３）が恒真式である場合には、式（２）に式（３）を代入することによって、式（１）は、（Ｘ＞１）と簡約化できる。
【００２１】
次に、情報処理装置１００の構成について説明する。図１に示すように、情報処理装置１００は、入力部１１１と、出力部１１２と、表示部１１３と、操作部１１４と、記憶部１２０と、制御部１３０とを有する。なお、情報処理装置１００は、図１に示す機能部以外にも既知のコンピュータが有する各種の機能部、例えば各種の入力デバイスや音声出力デバイス等の機能部を有することとしてもかまわない。
【００２２】
入力部１１１は、例えば、媒体読取装置である。入力部１１１は、ＣＤ−ＲＯＭやＤＶＤディスク、ＵＳＢ（Universal  Serial  Bus）メモリ等の可搬型記録媒体に記憶された分析対象のプログラムを読み込む。すなわち、入力部１１１には、記録媒体から分析対象のプログラムが入力される。入力部１１１は、入力された分析対象のプログラムを制御部１３０に出力する。なお、入力部１１１は、他の情報処理装置で生成された第１条件式が入力されるようにしてもよい。この場合には、入力部１１１は、入力された第１条件式を制御部１３０に出力する。また、入力部１１１は、他の情報処理装置と通信可能な通信部とし、他の情報処理装置から分析対象のプログラム、または、第１条件式を受信して入力されるようにしてもよい。
【００２３】
出力部１１２は、例えば、媒体書込装置である。出力部１１２は、制御部１３０から入力された第４条件式を記録媒体に書き込んで出力する。また、出力部１１２は、他の情報処理装置と通信可能な通信部とし、他の情報処理装置に第４条件式を送信するようにしてもよい。なお、入力部１１１と出力部１１２は、一体化してもよい。
【００２４】
表示部１１３は、各種情報を表示するための表示デバイスである。表示部１１３は、例えば、表示デバイスとして液晶ディスプレイ等によって実現される。表示部１１３は、制御部１３０から入力された各種表示画面を表示する。各種表示画面は、例えば、分析対象のプログラム、シンボリック実行結果、ロジック表、ＤＮＦ項のリスト、第２条件式のリスト、存否表、因数条件表、第４条件式等を表示する表示画面が挙げられる。
【００２５】
操作部１１４は、ユーザから各種操作を受け付ける入力デバイスである。操作部１１４は、例えば、入力デバイスとして、キーボードやマウス等によって実現される。操作部１１４は、ユーザによって入力された操作を操作情報として制御部１３０に出力する。なお、操作部１１４は、入力デバイスとして、タッチパネル等によって実現されるようにしてもよく、表示部１１３の表示デバイスと、操作部１１４の入力デバイスとは、一体化されるようにしてもよい。
【００２６】
記憶部１２０は、例えば、ＲＡＭ（Random  Access  Memory）、フラッシュメモリ（Flash  Memory）等の半導体メモリ素子、ハードディスクや光ディスク等の記憶装置によって実現される。記憶部１２０は、ロジック表記憶部１２１と、リスト記憶部１２２と、第２条件式記憶部１２３と、存否表記憶部１２４と、因数条件表記憶部１２５とを有する。また、記憶部１２０は、制御部１３０での処理に用いる情報、例えば、条件式ツリー等を記憶する。
【００２７】
ロジック表記憶部１２１は、分析対象のプログラムをシンボリック実行した結果について、パス出力で分けたロジック表を記憶する。図２は、ロジック表記憶部の一例を示す図である。図２に示すように、ロジック表記憶部１２１は、「出力Ｎｏ．」、「条件式」、「出力」といった項目を有する。ロジック表記憶部１２１は、例えば、１つの出力ごとに１レコードとして記憶する。
【００２８】
「出力Ｎｏ．」は、出力を識別する識別子である。「条件式」は、出力が同一となるシンボリック実行結果のパス条件を選言（ＯＲ，∨）で結合した条件式を示す情報である。「出力」は、シンボリック実行結果の出力を示す情報である。図２の例では、出力Ｎｏ．「１」の条件式は、出力が「購入可否＝０」となる８個のパス条件の条件式を選言で結合した条件式である。また、出力Ｎｏ．「２」の条件式は、出力が「購入可否＝１」となる１個のパス条件の条件式を示すものである。
【００２９】
また、ロジック表記憶部１２１は、シンボリック実行した結果について、例えばＱＭ法を適用した後のロジック表を記憶してもよい。図３は、ロジック表記憶部の他の一例を示す図である。図３の例では、出力Ｎｏ．「１」の条件式は、図２の出力Ｎｏ．「１」の条件式に対してＱＭ法を適用した後のパス条件の条件式である。当該条件式は、出力が「購入可否＝０」となる１２個のパス条件の条件式を選言で結合した条件式である。なお、図３のパス条件の条件式は、図２のパス条件の条件式と比べてパス条件が増加しているが、各パス条件の条件式が選言標準形のＤＮＦ項となっている。
【００３０】
図１の説明に戻って、リスト記憶部１２２は、第１条件式を連言節の選言の形式に展開された連言節のリスト、すなわちＤＮＦ項のリストを記憶する。図４は、リスト記憶部の一例を示す図である。図４に示すように、リスト記憶部１２２は、「ＤＮＦ項Ｎｏ．」、「ＤＮＦ項」といった項目を有する。リスト記憶部１２２は、例えば、１つのＤＮＦ項ごとに１レコードとして記憶する。
【００３１】
「ＤＮＦ項Ｎｏ．」は、ＤＮＦ項を識別する識別子である。「ＤＮＦ項」は、パス条件の条件式を選言で結合した条件式の各ＤＮＦ項を示す情報である。図４の例は、図３に示す出力Ｎｏ．「１」のＱＭ法を適用した後の条件式からＤＮＦ項を抽出したもので、各ＤＮＦ項は、１２個のパス条件の各条件式に対応する。また、リスト記憶部１２２は、図２に示す出力Ｎｏ．「１」の条件式からＤＮＦ項を抽出してもよい。図５は、リスト記憶部の他の一例を示す図である。図５の例では、図２に示す８個のパス条件の条件式を連言節の選言の形式に展開した条件式からＤＮＦ項を抽出したものである。図５の例では、ＤＮＦ項は３０個となる。なお、図２に示す８個のパス条件の条件式を連言節の選言の形式に展開した条件式に対してＱＭ法を適用すると、ＤＮＦ項のリストは図４に示すＤＮＦ項のリストと同じとなる。
【００３２】
図１の説明に戻って、第２条件式記憶部１２３は、論理演算子を含まずに比較演算子を１つ有する第２条件式を記憶する。図６は、第２条件式記憶部の一例を示す図である。図６に示すように、第２条件式記憶部１２３は、「式Ｎｏ．」、「第２条件式」といった項目を有する。第２条件式記憶部１２３は、例えば、１つの式Ｎｏ．ごとに１レコードとして記憶する。
【００３３】
「式Ｎｏ．」は、第２条件式を識別する識別子である。「第２条件式」は、第１条件式から抽出された論理演算子を含まずに比較演算子を１つ有する第２条件式を示す情報である。図６の例では、第２条件式は、例えば、（０＜値段）、（値段＜＝希望金額）、（在庫ＯＫ＝１）、（購入ＣＤ（Code：コード）＝’Ａ’）、（購入ＣＤ＝’Ｂ’）、（購入ＣＤ＝’Ｃ’）等が挙げられる。
【００３４】
図１の説明に戻って、存否表記憶部１２４は、ＤＮＦ項のリストにおける、ＤＮＦ項ごとの第２条件式の存否を記憶する。図７は、存否表記憶部の一例を示す図である。図７に示すように、存否表記憶部１２４は、「ＤＮＦ項Ｎｏ．」、「第２条件式」といった項目を有する。図７の例は、図４に示すＤＮＦ項のリストに対応するＤＮＦ項ごとの第２条件式の存否を記憶する場合である。「第２条件式」は、例えば、「０＜値段」、「値段＜＝希望金額」、「在庫ＯＫ＝１」、「購入ＣＤ＝’Ａ’」、「購入ＣＤ＝’Ｂ’」、「購入ＣＤ＝’Ｃ’」といった項目を有する。存否表記憶部１２４は、例えば、１つのＤＮＦ項Ｎｏ．ごとに１レコードとして記憶する。
【００３５】
「ＤＮＦ項Ｎｏ．」は、ＤＮＦ項を識別する識別子である。「第２条件式」の各項目は、ＤＮＦ項ごとの、それぞれの第２条件式の存否を示す情報である。「第２条件式」の各項目には、ＤＮＦ項に当該第２条件式が含まれる場合には「１」が入力され、当該第２条件式の否定が含まれる場合には「０」が入力される。また、「第２条件式」の各項目は、ＤＮＦ項に当該第２条件式が含まれない場合には、「−」（don't  care）とされる。図４に示すＤＮＦ項のリストの例では、ＤＮＦ項Ｎｏ．「１」のＤＮＦ項は、（（０＜値段）∧（値段＜＝希望金額）∧（購入ＣＤ  ＮＯＴ＝’Ａ’）∧（購入ＣＤ  ＮＯＴ＝’Ｂ’）∧（購入ＣＤ  ＮＯＴ＝’Ｃ’））である。これに対応する図７の存否表のＤＮＦ項Ｎｏ．「１」は、「０＜値段」が「１」、「値段＜＝希望金額」が「１」、「在庫ＯＫ＝１」が「−」、「購入ＣＤ＝’Ａ’」が「０」、「購入ＣＤ＝’Ｂ’」が「０」、「購入ＣＤ＝’Ｃ’」が「０」となる。
【００３６】
図１の説明に戻って、因数条件表記憶部１２５は、第２条件式および第２条件式の否定を因数条件の候補として、ＤＮＦ項のリストに含まれるＤＮＦ項を因数分解した場合における、因数条件と対応するＤＮＦ項Ｎｏ．とを記憶する。図８は、因数条件表記憶部の一例を示す図である。図８に示すように、因数条件表記憶部１２５は、「因数条件Ｎｏ．」、「因数条件」、「ＤＮＦ項Ｎｏ．」といった項目を有する。因数条件表記憶部１２５は、例えば、１つの因数条件Ｎｏ．ごとに１レコードとして記憶する。
【００３７】
「因数条件Ｎｏ．」は、因数条件を識別する識別子である。「因数条件」は、ＤＮＦ項のリストに含まれるＤＮＦ項を因数分解する因数条件を示す情報である。「ＤＮＦ項Ｎｏ．」は、対応する因数条件を含むＤＮＦ項Ｎｏ．を示す情報である。図８の１行目の例では、因数条件Ｎｏ．「１」は、因数条件「（０＜値段）」を含むＤＮＦ項Ｎｏ．が「１，４，５，６」であることを示している。
【００３８】
図１の説明に戻って、制御部１３０は、例えば、ＣＰＵ（Central  Processing  Unit）やＭＰＵ（Micro  Processing  Unit）等によって、内部の記憶装置に記憶されているプログラムがＲＡＭを作業領域として実行されることにより実現される。また、制御部１３０は、例えば、ＡＳＩＣ（Application  Specific  Integrated  Circuit）やＦＰＧＡ（Field  Programmable  Gate  Array）等の集積回路により実現されるようにしてもよい。制御部１３０は、記号実行部１３１と、リスト生成部１３２と、抽出部１３３と、存否表生成部１３４と、条件表生成部１３５と、更新部１３６と、条件式生成部１３７とを有し、以下に説明する情報処理の機能や作用を実現または実行する。なお、制御部１３０の内部構成は、図１に示した構成に限られず、後述する情報処理を行う構成であれば他の構成であってもよい。また、制御部１３０は、各処理工程の入出力や処理結果を各種表示画面として表示部１１３に出力するようにしてもよい。
【００３９】
記号実行部１３１は、入力部１１１から分析対象のプログラムが入力されると、当該プログラムをシンボリック実行する。記号実行部１３１は、分析対象のプログラムをシンボリック実行した結果について、パス出力で分けたロジック表を生成する。記号実行部１３１は、生成したロジック表をロジック表記憶部１２１に記憶する。なお、ロジック表には、簡約化したい条件式である第１条件式が含まれる。
【００４０】
ここで、図９から図１２を用いてロジック表の生成について説明する。図９は、シンボリック実行の対象となるプログラムの一例を示す図である。図９に示すプログラム１１は、シンボリック実行の対象となるプログラムであり、２つのＩＦ文１１ａ、１１ｂを有する。図１０は、シンボリック実行によるパスの抽出の一例を示す図である。図１０は、プログラム１１のフローチャートとパスの抽出の一例を示す。記号実行部１３１は、プログラム１１についてシンボリック実行を行うと、パス「１」、「２」、「３」の３つの実行可能なパスおよびパスごとのパス条件を抽出する。なお、パスは、実行された命令文の系列であり、パス条件は、パスが終了するまでに経由する条件のうち不定な変数値に関する条件式である。また、パスが実行可能とは、パス条件が充足可能である場合、すなわち条件式が真となりうる場合である。
【００４１】
図１１は、シンボリック実行の結果の一例を示す図である。図１１に示すシンボリック実行結果１２は、図１０のパス「１」、「２」、「３」に、それぞれ対応するパスＮｏ．「１」、「２」、「３」についてのパス条件およびパス出力を示す。また、パスＮｏ．「不可」は、パス条件が充足不能、すなわち成立不可能であることを示す。パス条件は、プログラムに記述されたＩＦ文等の条件式から単純に抽出されるものではなく、条件文の間に実行された変数の更新結果も取り込んだ条件式である。パス出力は、パスが実行された結果の出力を示す。
【００４２】
図１２は、ロジック表の一例を示す図である。図１２に示すロジック表１３は、図１１のパス出力の出力変数ごとに、出力変数の出力値が同一となるパスのパス条件に基づいて生成される。図１１の例では、パスＮｏ．「１」のパス条件は、（性別＝’男性’）∧（性別  ＮＯＴ＝’女性’）であり、図１２の出力Ｎｏ．「１」の例では、パス出力が「出力＝’Ｍ’」となる条件式は（性別＝’男性’）である。図１１と図１２とを比較すると、図１１の（性別＝’男性’）∧（性別  ＮＯＴ＝’女性’）は、図１２の（性別＝’男性’）と同値であるが、（性別  ＮＯＴ＝’女性’）という余分な条件が連言されている。なお、図１２の例では、簡単であるため人の手で（性別  ＮＯＴ＝’女性’）を削除して容易に簡約化できるが、複雑な条件式となると人の手で簡約化することは困難となる。このため、記号実行部１３１は、例えば、図１１のパスＮｏ．「１」、「２」、「３」のパス条件を条件式としたロジック表を生成する。
【００４３】
また、図１３および図１４を用いてシンボリック実行結果の他の一例について説明する。図１３は、シンボリック実行の対象となるプログラムの他の一例を示す図である。図１３に示すプログラム１４は、シンボリック実行の対象となるプログラムであり、３つの入力変数１４ａと、３つの出力変数１４ｂと、３つのＩＦ文１４ｃ、１４ｄ、１４ｅとを有する。図１４は、シンボリック実行の結果の他の一例を示す図である。図１４に示すシンボリック実行結果１５は、８本のパスを有し、それぞれのパス条件とパス出力とが対応付けられている。
【００４４】
図１４のシンボリック実行結果１５のうち、例えば、“出力３＝（入力３＋３）”となるのは、パスＮｏ．「１」、「３」、「５」、「７」の４つのパスである。従って、“出力３＝（入力３＋３）”となる入力の条件は、上記の４つのパスのパス条件の選言（ＯＲ，∨）である。すなわち、“出力３＝（入力３＋３）”となる入力の条件は、下記の式（４）となる。
【００４５】
パスＮｏ．「１」∨「３」∨「５」∨「７」＝
（（（０＜入力１）∧（入力１＜＝１０））∧（入力２＝１）∧（入力３＞１））
∨
（（（０＜入力１）∧（入力１＜＝１０））∧（入力２  ＮＯＴ＝１）
∧（入力３＞１））
∨
（（（０  ＮＯＴ＜入力１）∨（入力１  ＮＯＴ＜＝１０））∧（入力２＝１）
∧（入力３＞１））
∨
（（（０  ＮＯＴ＜入力１）∨（入力１  ＮＯＴ＜＝１０））
∧（入力２  ＮＯＴ＝１）∧（入力３＞１））                        …（４）
【００４６】
一方、図１３のプログラム１４では、“出力３＝（入力３＋３）”は、ＩＦ文１４ｅにおいてＴＨＥＮの場合であるので、入力の条件は、（入力３＞１）である。従って、上記の式（４）の右辺は、パス条件の選言の条件式を同値のまま簡約化して（入力３＞１）を得ることが求められる。
【００４７】
なお、上記の式（４）の右辺をＱＭ法で簡約化すると次の様になる。まず、パスＮｏ．「１」、「３」のパス条件の選言は、下記の式（５）となる。
【００４８】
（（０＜入力１）∧（入力１＜＝１０）∧（入力２＝１）∧（入力３＞１））
∨
（（（０＜入力１）∧（入力１＜＝１０））∧（入力２  ＮＯＴ＝１）
∧（入力３＞１））                                            …（５）
【００４９】
上記の式（５）は、（入力２＝１）および（入力２  ＮＯＴ＝１）の部分にＱＭ法を適用すれば、下記の式（６）に示すように簡約化できる。
【００５０】
（（０＜入力１）∧（入力１＜＝１０）∧（入力３＞１））        …（６）
【００５１】
同様に、パスＮｏ．「５」、「７」のパス条件は、ＱＭ法を用いて下記の式（７）に示すように簡約化できる。
【００５２】
（（（０  ＮＯＴ＜入力１）∨（入力１  ＮＯＴ＜＝１０））∧（入力３＞１））
…（７）
【００５３】
ここで、上記の式（６）および（７）は、さらにＱＭ法を適用して（入力３＞１）を得ることは困難である。これは、ＱＭ法が、真偽が逆となる２個の条件式の選言が真であることを利用して条件を簡約化できるが、３個以上の条件式には適用できないためである。また、他の簡約化の手法としてカルノー図法を用いても、ＱＭ法と同様に３個以上の条件式には適用できないため、上記の式（６）および（７）を簡約化することは困難である。
【００５４】
さらに、図１５および図１６を用いてシンボリック実行結果の他の一例について説明する。図１５は、シンボリック実行の対象となるプログラムの他の一例を示す図である。図１５に示すプログラム１６は、シンボリック実行の対象となるプログラムであり、２つの入力変数１６ａと、１つの出力変数１６ｂと、４つのＩＦ文とを有する。ここで、４つのＩＦ文のうち、ＩＦ文１６ｃは、条件を２つ有する。また、プログラム１６は、購入ＣＤ（ｃｏｄｅ：コード）と希望金額とが入力されると、購入可否を判定するプログラムである。購入可否の判定は、商品ＣＤ（ｃｏｄｅ：コード）チェック、在庫チェックおよび金額上限チェックの順に処理される。図１６は、シンボリック実行の結果の他の一例を示す図である。図１６に示すシンボリック実行結果１７は、９本のパスを有し、それぞれのパス条件とパス出力とが対応付けられている。図１６に示すシンボリック実行結果１７について、パス出力が“購入可否＝０”の場合と、“購入可否＝１”の場合とに分けたロジック表は、図２に示すロジック表記憶部１２１のロジック表となる。図２のロジック表では、“購入可否＝０”に対応するパスが８つであるので、“購入可否＝０”の条件は、８個のパス条件の選言となる。つまり、この８個のパス条件の選言は、第１条件式である。
【００５５】
図１の説明に戻って、リスト生成部１３２は、記号実行部１３１がロジック表を生成すると、ロジック表記憶部１２１を参照して、条件式（第１条件式）のＤＮＦ項のリストを生成する。まず、リスト生成部１３２は、ロジック表記憶部１２１を参照して、条件式（第１条件式）の文字列を取得する。リスト生成部１３２は、取得した条件式（第１条件式）の文字列から条件式ツリーを構成する。リスト生成部１３２は、構成した第１条件式に対応する条件式ツリーを記憶部１２０に記憶する。
【００５６】
図１７は、条件式ツリーの構成の一例を示す図である。図１７に示すように、リスト生成部１３２は、公知の文字列パーザ技術を用いて条件式ツリーを構成する。図１７の例は、条件式の文字列１８から、条件式ツリー１９を構成した場合である。条件式ツリー１９は、二分木での表現であり、各ノードは、論理演算子、関係演算子、算術演算子、および、項（変数とリテラル）である。また、二分木の左側は、演算子の左辺に該当し、二分木の右側は、演算子の右辺に該当する。
【００５７】
リスト生成部１３２は、条件式ツリーを構成すると、ド・モルガンの法則適用処理を実行する。リスト生成部１３２は、記憶部１２０から条件式ツリーを取得する。リスト生成部１３２は、取得した条件式ツリーに対して、再帰処理である全部ド・モルガン処理を実行する。リスト生成部１３２は、ド・モルガンの法則適用処理を実行した条件式ツリーを記憶部１２０に記憶する。
【００５８】
ここで、全部ド・モルガン処理について説明する。リスト生成部１３２は、まず、全部ド・モルガン処理を条件式ツリーの根元ノードに対して実行し、その後、再帰処理により左辺ノード以下のツリー、および、右辺ノード以下のツリーに対して全部ド・モルガン処理を実行する。
【００５９】
リスト生成部１３２は、指定ノードが論理演算子であるか否かを判定する。リスト生成部１３２は、指定ノードが論理演算子でない場合には、全部ド・モルガン処理を終了する。リスト生成部１３２は、指定ノードが論理演算子である場合には、指定ノードにド・モルガンの法則を適用する。また、リスト生成部１３２は、左辺ノードが論理演算子であるか否かを判定する。リスト生成部１３２は、左辺ノードが論理演算子である場合には、左辺ノード以下のツリーに対して全部ド・モルガン処理を実行、すなわち再帰処理を実行する。リスト生成部１３２は、左辺ノードが論理演算子でない場合、または、左辺ノード以下のツリーに対する全部ド・モルガン処理が完了した場合には、右辺ノードが論理演算子であるか否かを判定する。
【００６０】
リスト生成部１３２は、右辺ノードが論理演算子である場合には、右辺ノード以下のツリーに対して全部ド・モルガン処理を実行、すなわち再帰処理を実行して、全部ド・モルガン処理を終了する。リスト生成部１３２は、右辺ノードが論理演算子でない場合には、全部ド・モルガン処理を終了する。なお、条件式ツリーは、指定ノードにド・モルガンの法則を適用すると、例えば、ＮＯＴ（条件式Ａ  ＯＲ  条件式Ｂ）ならば、ＮＯＴ（条件式Ａ）  ＡＮＤ  ＮＯＴ（条件式Ｂ）と変形される。また、条件式ツリーは、例えば、ＮＯＴ（条件式Ａ  ＡＮＤ  条件式Ｂ）ならば、ＮＯＴ（条件式Ａ）  ＯＲ  ＮＯＴ（条件式Ｂ）と変形される。
【００６１】
次に、リスト生成部１３２は、条件式ツリーに対して分配法則適用処理を実行する。リスト生成部１３２は、記憶部１２０から条件式ツリーを取得する。リスト生成部１３２は、取得した条件式ツリーに対して、再帰処理である全部分配法則処理を実行する。リスト生成部１３２は、分配法則適用処理を実行した条件式ツリーを記憶部１２０に記憶する。
【００６２】
ここで、全部分配法則処理について説明する。リスト生成部１３２は、まず、全部分配法則処理を条件式ツリーの根元ノードに対して実行し、その後、再帰処理により親ノード以下のツリー、左辺ノード以下のツリー、および、右辺ノード以下のツリーに対して全部分配法則処理を実行する。
【００６３】
リスト生成部１３２は、指定ノードが論理演算子であるか否かを判定する。リスト生成部１３２は、指定ノードが論理演算子でない場合には、全部分配法則処理を終了する。リスト生成部１３２は、指定ノードが論理演算子である場合には、指定ノードに分配法則を適用する。また、リスト生成部１３２は、親ノードが論理演算子∧であるか否かを判定する。リスト生成部１３２は、親ノードが論理演算子∧である場合には、親ノード以下のツリーに対して全部分配法則処理を実行、すなわち再帰処理を実行する。リスト生成部１３２は、親ノードが論理演算子∧でない場合、または、親ノード以下のツリーに対する全部分配法則処理が完了した場合には、左辺ノードが論理演算子であるか否かを判定する。
【００６４】
リスト生成部１３２は、左辺ノードが論理演算子である場合には、左辺ノード以下のツリーに対して全部分配法則処理を実行、すなわち再帰処理を実行する。リスト生成部１３２は、左辺ノードが論理演算子でない場合、または、左辺ノード以下のツリーに対する全部分配法則処理が完了した場合には、右辺ノードが論理演算子であるか否かを判定する。
【００６５】
リスト生成部１３２は、右辺ノードが論理演算子である場合には、右辺ノード以下のツリーに対して全部分配法則処理を実行、すなわち再帰処理を実行して、全部分配法則処理を終了する。リスト生成部１３２は、右辺ノードが論理演算子でない場合には、全部分配法則処理を終了する。なお、第１条件式は、分配法則適用処理まで実行されると、選言標準形（ＤＮＦ）に展開される。
【００６６】
続いて、リスト生成部１３２は、条件式ツリーに対して収集処理を実行する。リスト生成部１３２は、記憶部１２０から条件式ツリーを取得する。リスト生成部１３２は、取得した条件式ツリーに対して、再帰処理であるＤＮＦ項収集処理を実行する。リスト生成部１３２は、条件式から収集されたＤＮＦ項にＤＮＦ項Ｎｏ．を付与してＤＮＦ項のリストを生成し、生成したＤＮＦ項のリストをリスト記憶部１２２に記憶する。
【００６７】
ここで、ＤＮＦ項収集処理について説明する。リスト生成部１３２は、まず、ＤＮＦ項収集処理を条件式ツリーの根元ノードに対して実行し、その後、再帰処理により左辺ノード以下のツリー、および、右辺ノード以下のツリーに対してＤＮＦ項収集処理を実行する。
【００６８】
リスト生成部１３２は、指定ノードが論理演算子∨であるか否かを判定する。リスト生成部１３２は、指定ノードが論理演算子∨でない場合には、指定ノードの条件式を収集して、ＤＮＦ項収集処理を終了する。リスト生成部１３２は、指定ノードが論理演算子∨である場合には、左辺ノードが論理演算子∨であるか否かを判定する。リスト生成部１３２は、左辺ノードが論理演算子∨でない場合には、左辺ノードの条件式を収集する。リスト生成部１３２は、左辺ノードが論理演算子∨である場合には、左辺ノード以下のツリーに対してＤＮＦ項収集処理を実行、すなわち再帰処理を実行する。
【００６９】
また、リスト生成部１３２は、左辺ノードの条件式を収集した場合、または、左辺ノード以下のツリーに対するＤＮＦ項収集処理が完了した場合には、右辺ノードが論理演算子∨であるか否かを判定する。リスト生成部１３２は、右辺ノードが論理演算子∨でない場合には、右辺ノードの条件式を収集する。リスト生成部１３２は、右辺ノードが論理演算子∨である場合には、右辺ノード以下のツリーに対してＤＮＦ項収集処理を実行、すなわち再帰処理を実行する。
【００７０】
図１の説明に戻って、抽出部１３３は、第１条件式から第２条件式を抽出し、抽出した第２条件式を第２条件式記憶部１２３に記憶する。抽出部１３３は、リスト生成部１３２が構成した第１条件式に対応する条件式ツリーを記憶部１２０から取得する。抽出部１３３は、取得した条件式ツリーに対して、再帰処理である第２条件式収集処理を実行する。抽出部１３３は、第２条件式収集処理によって収集、すなわち抽出した第２条件式を第２条件式記憶部１２３に記憶する。
【００７１】
ここで、第２条件式収集処理について説明する。抽出部１３３は、まず、第２条件式収集処理を条件式ツリーの根元ノードに対して実行し、その後、再帰処理により左辺ノード以下のツリー、および、右辺ノード以下のツリーに対して第２条件式収集処理を実行する。
【００７２】
抽出部１３３は、指定ノードが比較演算子であるか否かを判定する。抽出部１３３は、指定ノードが比較演算子である場合には、比較演算子にＮＯＴがあるか否かを判定する。抽出部１３３は、比較演算子にＮＯＴがある場合には、ＮＯＴを除去する。抽出部１３３は、比較演算子にＮＯＴがない場合、または、ＮＯＴを除去した場合には、条件式が抽出済みであるか否かを判定する。抽出部１３３は、条件式が抽出済みでない場合には、現条件式を第２条件式として、第２条件式記憶部１２３に記憶する。抽出部１３３は、条件式が抽出済みである場合には、第２条件式収集処理を終了する。
【００７３】
抽出部１３３は、指定ノードが比較演算子でない場合には、左辺ノードがあるか否かを判定する。抽出部１３３は、左辺ノードがある場合には、左辺ノード以下のツリーに対して第２条件式収集処理を実行する。抽出部１３３は、左辺ノードがない場合、または、左辺ノード以下のツリーに対する第２条件式収集処理が完了した場合には、右辺ノードがあるか否かを判定する。抽出部１３３は、右辺ノードがある場合には、右辺ノード以下のツリーに対して第２条件式収集処理を実行する。抽出部１３３は、右辺ノードがない場合、または、右辺ノード以下のツリーに対する第２条件式収集処理が完了した場合には、第２条件式収集処理を終了する。
【００７４】
なお、抽出部１３３は、第１条件式に代えて、連言節（ＤＮＦ項）のリストから第２条件式を抽出してもよい。これにより、抽出部１３３の第２条件式の抽出と、存否表生成部１３４の存否表の生成とを１つの処理として実行できる。
【００７５】
存否表生成部１３４は、ＤＮＦ項のリストと第２条件式とに基づいて、ＤＮＦ項ごとに第２条件式の存否を管理する存否表を生成する。存否表生成部１３４は、リスト記憶部１２２および第２条件式記憶部１２３を参照して、ＤＮＦ項（ＤＮＦ＿ｉ，ｉ＝１，．．．，ｍ）と、第２条件式（ＥＣ＿ｊ，ｊ＝１，．．．，ｎ）とを取得する。存否表生成部１３４は、ＤＮＦ項と第２条件式とを取得すると、ｉに「１」を設定する。存否表生成部１３４は、ｉがｍより大きいか否かを判定する。存否表生成部１３４は、ｉがｍより大きい場合には、存否表を出力して存否表記憶部１２４に記憶する。存否表生成部１３４は、ｉがｍ以下である場合には、ＤＮＦ＿ｉから条件式（ＲＣ＿ｋ，．．．，Ｎ）を取得する。すなわち、存否表生成部１３４は、ＤＮＦ項に含まれる第２条件式である条件式ＲＣ＿ｋを、ＤＮＦ項から抽出して取得する。なお、存否表生成部１３４は、取得したＤＮＦ項であるＤＮＦ＿ｉ、第２条件式ＥＣ＿ｊ、および、条件式ＲＣ＿ｋを記憶部１２０に記憶する。また、存否表生成部１３４は、ＤＮＦ＿ｉ、第２条件式ＥＣ＿ｊ、および、条件式ＲＣ＿ｋについて、それぞれ条件式ツリーを生成して記憶部１２０に記憶する。
【００７６】
存否表生成部１３４は、ＤＮＦ＿ｉから条件式ＲＣ＿ｋを取得すると、ｋに「１」を設定する。存否表生成部１３４は、ｋがＮより大きいか否かを判定する。存否表生成部１３４は、ｋがＮより大きい場合には、ｉをインクリメントする。存否表生成部１３４は、ｋがＮ以下の場合には、ｊに「１」を設定する。存否表生成部１３４は、ｊがｎより大きいか否かを判定する。存否表生成部１３４は、ｊがｎより大きい場合には、ｋをインクリメントする。存否表生成部１３４は、ｊがｎ以下の場合には、同値判定処理を実行する。
【００７７】
ここで、同値判定処理について説明する。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊについて、同値であるか否かを判定する。まず、存否表生成部１３４は、２つの条件式ツリー、すなわち、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊの条件式ツリーを記憶部１２０から取得する。存否表生成部１３４は、２つの条件式、つまり２つの条件式ツリーの同値は既に判定済みであるか否かを判定する。存否表生成部１３４は、例えば、２つの条件式の文字列を連列した文字列をキーとし、判定結果を値としたマップを利用して、当該判定を行うことができる。存否表生成部１３４は、２つの条件式の同値は既に判定済みである場合には、既存の判定結果を利用する。存否表生成部１３４は、２つの条件式の同値は既に判定済みでない場合には、ツリー判定処理を実行する。
【００７８】
ここで、ツリー判定処理について説明する。存否表生成部１３４は、同値判定処理から２つの条件式ツリーを取得する。存否表生成部１３４は、２つの条件式ツリーの比較演算子が同じであるか否かを判定する。存否表生成部１３４は、２つの条件式ツリーの比較演算子が同じである場合には、２つの条件式ツリーの左辺同士、右辺同士が同じであるか否かを判定する。存否表生成部１３４は、２つの条件式ツリーの左辺同士、右辺同士が同じである場合には、２つの条件式ツリーは同値であると判定する。存否表生成部１３４は、２つの条件式ツリーの左辺同士、右辺同士が異なる場合には、ツリー判定処理を終了する。
【００７９】
存否表生成部１３４は、２つの条件式ツリーの比較演算子が異なる場合には、判定した２つの比較演算子が逆であるか否かを判定する。存否表生成部１３４は、判定した２つの比較演算子が逆でない場合には、ツリー判定処理を終了する。存否表生成部１３４は、判定した２つの比較演算子が逆である場合には、２つの条件式ツリーの右辺左辺が逆であるか否かを判定する。存否表生成部１３４は、２つの条件式ツリーの右辺左辺が逆である場合には、２つの条件式ツリーは同値であると判定する。存否表生成部１３４は、２つの条件式ツリーの右辺左辺が逆でない場合には、ツリー判定処理を終了する。
【００８０】
同値判定処理の説明に戻って、存否表生成部１３４は、ツリー判定処理の判定結果がツリーとして同値であるか否かを判定する。存否表生成部１３４は、ツリー判定処理の判定結果がツリーとして同値である場合には、２つの条件式が同値である判定結果を生成する。存否表生成部１３４は、ツリー判定処理の判定結果がツリーとして同値でない場合には、ＳＭＴ（Satisfiability  Modulo  Theories）ソルバ判定処理を実行する。
【００８１】
ここで、ＳＭＴソルバ判定処理について説明する。存否表生成部１３４は、同値判定処理から２つの条件式をＣ１、Ｃ２として取得する。存否表生成部１３４は、取得したＣ１、Ｃ２に基づいて、Ｃ１∧Ｃ２、¬Ｃ１∧Ｃ２を生成する。存否表生成部１３４は、ＳＭＴソルバを用いて、Ｃ１∧Ｃ２、¬Ｃ１∧Ｃ２の充足可能性を判定する。存否表生成部１３４は、充足可能性の判定の結果について、Ｃ１∧Ｃ２が充足可能、かつ、¬Ｃ１∧Ｃ２が充足不可能であるか否かを判定する。存否表生成部１３４は、Ｃ１∧Ｃ２が充足可能、かつ、¬Ｃ１∧Ｃ２が充足不可能である場合には、２つの条件式が同値であると判定する。存否表生成部１３４は、Ｃ１∧Ｃ２が充足可能、かつ、¬Ｃ１∧Ｃ２が充足不可能でない場合には、ＳＭＴソルバ判定処理を終了する。
【００８２】
同値判定処理の説明に戻って、存否表生成部１３４は、ＳＭＴソルバ判定処理の判定結果が同値であるか否かを判定する。存否表生成部１３４は、ＳＭＴソルバ判定処理の判定結果が同値である場合には、２つの条件式が同値である判定結果を生成する。存否表生成部１３４は、ＳＭＴソルバ判定処理の判定結果が同値でない場合には、同値でない判定結果を生成する。
【００８３】
存否表を生成する処理の説明に戻って、存否表生成部１３４は、同値判定処理の判定結果に基づいて、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが同値であるか否かを判定する。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが同値である場合には、ＤＮＦ＿ｉに第２条件式ＥＣ＿ｊが同値で存在するとして、存否表の対応するセルに「１」を記憶する。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが同値でない場合には、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係であるか否かを判定する。なお、存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係であるか否かの判定は、第２条件式ＥＣ＿ｊの否定であるＮＯＴ（ＥＣ＿ｊ）を生成し、条件式ＲＣ＿ｋと、ＮＯＴ（ＥＣ＿ｊ）とが同値であるか否かを判定すればよい。
【００８４】
存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係である場合には、ＤＮＦ＿ｉに第２条件式ＥＣ＿ｊが否定で存在するとして、存否表の対応するセルに「０」を記憶する。存否表生成部１３４は、存否表の対応するセルに「１」または「０」を記憶すると、ｋをインクリメントして、次の条件式ＲＣ＿ｋについて、第２条件式ＥＣ＿ｊとの同値判定処理を繰り返す。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係でない場合には、存否表の対応するセルは「−（Don't  Care）」であるとして、ｊをインクリメントして同値判定処理を繰り返す。
【００８５】
条件表生成部１３５は、存否表が生成されると、ＤＮＦ項のリストおよび存否表に基づいて、因数分解の因数条件とＤＮＦ項とを対応させる因数条件表を生成する。すなわち、条件表生成部１３５は、第２条件式および第２条件式の否定を因数条件の候補として、ＤＮＦ項のリストに含まれるＤＮＦ項を因数分解し、因数条件ごとに該因数条件を有するＤＮＦ項を対応させる因数条件表を生成する。
【００８６】
条件表生成部１３５は、存否表記憶部１２４を参照して、存否表を取得する。条件表生成部１３５は、取得した存否表に対して、再帰処理である因数条件表生成処理を実行する。条件表生成部１３５は、因数条件表生成処理で生成された因数条件表を因数条件表記憶部１２５に記憶する。
【００８７】
ここで、因数条件表生成処理について説明する。条件表生成部１３５は、第２条件式記憶部１２３を参照して第２条件式を取得する。条件表生成部１３５は、取得した第２条件式のうち、先頭の第２条件式を選択する。条件表生成部１３５は、変数ｅに「１」を設定する。なお、変数ｅは、存否表の各セルに記憶されている「１」または「０」を選択するために用いる変数である。
【００８８】
条件表生成部１３５は、変数ｅが「０」未満であるか否かを判定する。条件表生成部１３５は、変数ｅが「０」未満である場合には、因数条件表生成処理を終了する。条件表生成部１３５は、変数ｅが「０」未満でない場合には、存否表のうち選択された第２条件式の存否がｅであるＤＮＦ項の行を選択する。条件表生成部１３５は、選択されたＤＮＦ項の行、つまり選択行の個数が３個以上であるか否かを判定する。条件表生成部１３５は、選択行の個数が３個未満である場合には、次の第２条件式を選択する。条件表生成部１３５は、選択行の個数が３個以上である場合には、因数条件表に先頭の第２条件式および選択行のＤＮＦ項Ｎｏ．を対応付けて、因数条件表記憶部１２５に記憶する。なお、条件表生成部１３５は、選択行の個数が３個未満となる因数条件しかない場合には、ＱＭ法を用いて簡約化することができる。
【００８９】
条件表生成部１３５は、存否表から選択行のＤＮＦ項Ｎｏ．に対応する行を抽出し、先頭の第２条件式の列を削除して部分存否表を生成する。条件表生成部１３５は、生成した部分存否表に対して因数条件表生成処理を実行、すなわち再帰処理を実行する。条件表生成部１３５は、再帰処理が終了するとｅをデクリメントする。
【００９０】
ここで、図１８を用いて部分存否表の生成について説明する。図１８は、部分存否表の生成の一例を示す図である。図１８の例では、条件表生成部１３５は、存否表２０から部分存否表２１ａ、２２ａを生成する。部分存否表２１ａは、「０＜値段」を選択した第２条件式とし、存否を「１」とした場合における部分存否表である。すなわち、部分存否表２１ａは、存否表２０から「０＜値段」の存否が「１」である行を抽出し、「０＜値段」の列を削除したものである。部分存否表２１ａでは、選択行がＤＮＦ項Ｎｏ．「１、４、５、６」であるので、因数条件の第２条件式「０＜値段」に、図１８中の枠２１ｂで囲った選択行のＤＮＦ項Ｎｏ．「１、４、５、６」が対応付けられて、因数条件表記憶部１２５に記憶される。
【００９１】
同様に、部分存否表２２ａは、「０＜値段」を選択した第２条件式とし、存否を「０」とした場合における部分存否表である。部分存否表２２ａでは、選択行がＤＮＦ項Ｎｏ．「２、７、８、９」であるので、因数条件の第２条件式「０＜値段」の否定に、図１８中の枠２２ｂで囲った選択行のＤＮＦ項Ｎｏ．「２、７、８、９」が対応付けられて、因数条件表記憶部１２５に記憶される。
【００９２】
図１の説明に戻って、更新部１３６は、因数条件表が生成されると、因数条件表および存否表に基づいて、因数条件に含まれない因数条件の候補に基づいて生成した第３条件式について真偽を判定する。更新部１３６は、判定の結果が真である場合に、第３条件式に基づいて存否表を更新する。すなわち、更新部１３６は、因数条件に含まれる候補の個数が多い順に、因数条件に含まれない候補の連言節である第５条件式を生成する。更新部１３６は、生成した第５条件式を選言（ＯＲ，∨）で結合した第３条件式について真偽を判定する。更新部１３６は、判定の結果が真である場合に、判定した第３条件式に含まれる第２条件式が不在となるように存否表を更新する。
【００９３】
更新部１３６の更新処理について、より詳細に説明する。更新部１３６は、存否表記憶部１２４および因数条件表記憶部１２５を参照して、存否表と因数条件表とを取得する。更新部１３６は、因数条件表で因数条件に含まれる第２条件式の数が多い順に行を選択し、対応するＤＮＦ項Ｎｏ．を取得する。更新部１３６は、因数条件表に未処理の行があるか否かを判定する。
【００９４】
更新部１３６は、因数条件表に未処理の行がない場合には、更新処理を終了する。更新部１３６は、因数条件表に未処理の行がある場合には、因数条件に含まれない因数条件の候補、すなわち第２条件式を連言（ＡＮＤ，∧）で結合し、存否表のＤＮＦ項Ｎｏ．ごとに第５条件式を生成する。更新部１３６は、生成した第５条件式を選言（ＯＲ，∨）で結合して第３条件式を生成する。更新部１３６は、生成した第３条件式について真偽を判定する第３条件式判定処理を実行する。
【００９５】
ここで、第３条件式判定処理について説明する。更新部１３６は、更新処理から第３条件式を取得する。更新部１３６は、第３条件式の真偽判定ルールが成立するか否かを判定する。第３条件式の真偽判定ルールは、存否表の第２条件式の存否パターン、つまり「１」と「０」の配置パターンが規定のパターンと一致するか否かを判定し、一致した場合に真と判定できるようなルールである。なお、第３条件式の真偽判定ルールは、ＳＭＴソルバを利用しないので、ＳＭＴソルバの制限や性能に依存せずに第３条件式の真偽判定を行うことができる。
【００９６】
第３条件式の真偽判定ルールについて、図１９から図２２を用いて説明する。図１９は、第３条件式の真偽判定ルールに対応する存否パターンの一例を示す図である。図１９に示すルールＮｏ．「１」は、第３条件式の真偽判定ルールとして、第３条件式に２個の変数と１個の値があり、該当する存否表の部分の存否パターンが存否パターン２３、２４、２５のうちいずれか１つの存否パターンを満たす場合である。
【００９７】
ここで、図２０を用いて存否パターン２３、２４、２５をグラフで表す場合について説明する。図２０は、存否パターンをグラフで表した場合の一例を示す図である。図２０に示すグラフ２６は、横軸を変数α、縦軸を変数βとしたグラフである。また、グラフ２６には、値γに対応する直線、および、変数β＝変数αに対応する直線が引かれている。このとき、存否パターン２３は、ＤＮＦ項＿Ｐの（値γ＜変数α）ＡＮＤ（変数α＜＝変数β）に対応する領域２７と、ＤＮＦ項＿ＱのＮＯＴ（値γ＜変数α）に対応する領域２８と、ＤＮＦ項＿ＲのＮＯＴ（変数α＜＝変数β）に対応する領域２９とで表すことができる。なお、グラフ２６の領域３０は、領域２８と領域２９とが重複している。すなわち、存否パターン２３は、３つの領域２７、２８、２９で平面全体をカバーできるので、（（値γ＜変数α）ＡＮＤ（変数α＜＝変数β））ＯＲ（ＮＯＴ（値γ＜変数α））ＯＲ（ＮＯＴ（変数α＜＝変数β））は真となる。また、存否パターン２４、２５は、グラフ２６の領域の重複をなくした状態に対応する存否パターンである。
【００９８】
図２１は、第３条件式の真偽判定ルールに対応する存否パターンの他の一例を示す図である。図２１に示すルールＮｏ．「２」は、第３条件式の真偽判定ルールとして、第３条件式に１個の変数と２個の値（ただし、値γ＜値δ）があり、該当する存否表の部分の存否パターンが存否パターン３１を満たす場合である。また、図２１に示すルールＮｏ．「３」は、第３条件式の真偽判定ルールとして、第３条件式に１個の変数と２個の値（ただし、値γ＜値δ）があり、該当する存否表の部分の存否パターンが存否パターン３２を満たす場合である。
【００９９】
ここで、図２２を用いて存否パターン３１をグラフで表す場合について説明する。図２２は、存否パターンをグラフで表した場合の他の一例を示す図である。図２２に示すグラフ３３は、横軸を変数とした数直線で表されたグラフである。また、グラフ３３には、値γおよび値δが数直線上に配置されている。このとき、存否パターン３１は、ＤＮＦ項＿Ｐの（値γ＜変数）ＡＮＤ（変数＜＝値δ）と、ＤＮＦ項＿ＱのＮＯＴ（値γ＜変数）と、ＤＮＦ項＿ＲのＮＯＴ（変数＜＝値δ）とで、数直線上に表すことができる。存否パターン３１は、数直線上の全ての領域をカバーするので、（（値γ＜変数）ＡＮＤ（変数＜＝値δ））ＯＲ（ＮＯＴ（値γ＜変数））ＯＲ（ＮＯＴ（変数＜＝値δ））は真となる。なお、存否パターン３２をグラフで表す場合には、グラフ３３と同様に、数直線で表されたグラフとなるが、存否パターン３１の場合と同様であるので、その説明は省略する。
【０１００】
第３条件式判定処理の説明に戻って、更新部１３６は、第３条件式の真偽判定ルールが成立すると判定した場合には、第３条件式が真であると判定する。更新部１３６は、第３条件式の真偽判定ルールが成立しないと判定した場合には、ＳＭＴソルバを利用して、（第３条件式）およびＮＯＴ（第３条件式）の充足可能性を判定する。更新部１３６は、充足可能性の判定の結果について、（第３条件式）が充足可能、かつ、ＮＯＴ（第３条件式）が充足不可能であるか否かを判定する。更新部１３６は、（第３条件式）が充足可能、かつ、ＮＯＴ（第３条件式）が充足不可能である場合には、第３条件式が真であると判定する。更新部１３６は、（第３条件式）が充足可能、かつ、ＮＯＴ（第３条件式）が充足不可能でない場合には、第３条件式が偽であると判定する。
【０１０１】
更新処理の説明に戻って、更新部１３６は、第３条件式判定処理の判定結果に基づいて、第３条件式が真であるか否かを判定する。更新部１３６は、第３条件式が真である場合には、存否表の対応するＤＮＦ項Ｎｏ．の行について、１つの行の第５条件式に含まれる第２条件式、および、他の行の全ての第２条件式の存否を不在（−：Don't  Care）に更新する。すなわち、更新部１３６は、存否表記憶部１２４に記憶されている存否表を更新する。更新部１３６は、第３条件式が真でない場合には、次の行の処理を実行する。
【０１０２】
更新処理について図２３および図２４を用いて説明する。図２３および図２４は、存否表の更新の一例を示す図である。図２３に示すように、更新部１３６は、因数条件表記憶部１２５に記憶されている因数条件表のうち、第２条件式の数が最も多い因数条件Ｎｏ．１５の行を選択し、図２３中の枠３４で囲まれた、対応するＤＮＦ項Ｎｏ．「１、２、３」を取得する。
【０１０３】
次に、更新部１３６は、存否表記憶部１２４に記憶されている存否表の対応するＤＮＦ項Ｎｏ．について、因数条件に含まれない第２条件式を連言（ＡＮＤ，∧）で結合して第５条件式を生成する。図２３では、枠３５で囲まれた範囲について、ＤＮＦ項Ｎｏ．ごとに第５条件式を生成すると、ＤＮＦ項Ｎｏ．「１」は、（（０＜値段）∧（値段＜＝希望金額））が第５条件式となる。また、ＤＮＦ項Ｎｏ．「２」は、ＮＯＴ（０＜値段）が第５条件式となり、ＤＮＦ項Ｎｏ．「３」は、ＮＯＴ（値段＜＝希望金額）が第５条件式となる。
【０１０４】
更新部１３６は、生成した各第５条件式を選言で結合し、第３条件式３６を生成する。また、更新部１３６は、枠３５で囲まれた範囲について、第３条件式の存否パターン２３〜２５、３１、３２のうち、いずれか１つを満たすか否かを判定する。図２３の例では、枠３５で囲まれた範囲は、値が１つ、変数が２つであり、存否パターン２３を満たすので、第３条件式３６は真であると判定する。更新部１３６は、存否表のＤＮＦ項Ｎｏ．「１、２、３」の行について、枠３７で囲まれた範囲の存否を不在（−）に更新する。更新部１３６は、存否表の他の部分についても同様に更新する。
【０１０５】
更新後の存否表１２４ａを図２４に示す。図２４に示すように、更新後の存否表１２４ａは、第３条件式の真偽判定ルールおよびＳＭＴソルバに基づいて、簡約化される。なお、図２４中、「−（１）」は、当該セルの値が「１」から「−」となったことを示し、「−（０）」は、当該セルの値が「０」から「−」となったことを示す。
【０１０６】
図１の説明に戻って、条件式生成部１３７は、存否表記憶部１２４に記憶されている存否表が更新されると、更新された存否表に基づいて、第１条件式を簡約化した第４条件式を生成する。条件式生成部１３７は、まず、存否表記憶部１２４を参照して、更新された存否表を取得する。条件式生成部１３７は、取得した存否表の行を１行ずつ順に選択する。また、条件式生成部１３７は、存否表に未処理の行があるか否かを判定する。条件式生成部１３７は、存否表に未処理の行がある場合には、選択した行について、第２条件式の存否に「１」か「０」が存在するか否かを判定する。条件式生成部１３７は、第２条件式の存否に「１」か「０」が存在する場合には、「１」ならば第２条件式、「０」ならば第２条件式の否定として連言（ＡＮＤ，∧）で結合して、第６条件式を生成する。条件式生成部１３７は、第２条件式の存否に「１」か「０」が存在しない場合には、存否表の次の行の処理に移る。
【０１０７】
また、条件式生成部１３７は、存否表に未処理の行がない場合には、生成された第６条件式を選言（ＯＲ，∨）で結合して第４条件式を生成する。条件式生成部１３７は、生成した第４条件式を、出力部１１２に出力する。また、条件式生成部１３７は、生成した第４条件式を、表示部１１３に表示する。
【０１０８】
図２５は、存否表に基づく条件式の生成の一例を示す図である。図２５に示すように、条件式生成部１３７は、例えば、更新された存否表１２４ａのＤＮＦ項Ｎｏ．「１、４、５、６、７、１０」のそれぞれに対応する第６条件式を生成する。条件式生成部１３７は、生成された第６条件式を選言（ＯＲ，∨）で結合して第４条件式３８を生成し、生成した第４条件式３８を出力部１１２に出力する。
【０１０９】
次に、実施例の情報処理装置１００の動作について説明する。図２６は、実施例の簡約化処理の一例を示すフローチャートである。
【０１１０】
記号実行部１３１は、入力部１１１から分析対象のプログラムが入力されると、当該プログラムをシンボリック実行する。記号実行部１３１は、分析対象のプログラムをシンボリック実行した結果からパス、パスの条件およびパス出力を抽出する（ステップＳ１）。記号実行部１３１は、抽出したパス、パスの条件およびパス出力に基づいて、第１条件式を生成する（ステップＳ２）。すなわち、記号実行部１３１は、抽出したパス、パスの条件およびパス出力に基づいて、パス出力で分けた第１条件式を含むロジック表を生成する。記号実行部１３１は、生成したロジック表をロジック表記憶部１２１に記憶する。
【０１１１】
リスト生成部１３２は、記号実行部１３１がロジック表を生成すると、リスト生成処理を実行する（ステップＳ３）。ここで、図２７を用いてリスト生成処理を説明する。図２７は、リスト生成処理の一例を示すフローチャートである。リスト生成部１３２は、ロジック表記憶部１２１を参照して、条件式（第１条件式）の文字列を取得する（ステップＳ３１）。リスト生成部１３２は、取得した条件式（第１条件式）の文字列から条件式ツリーを構成する（ステップＳ３２）。リスト生成部１３２は、構成した第１条件式に対応する条件式ツリーを記憶部１２０に記憶する。リスト生成部１３２は、条件式ツリーを構成すると、ド・モルガンの法則適用処理を実行する（ステップＳ３３）。
【０１１２】
ここで、図２８および図２９を用いてド・モルガンの法則適用処理を説明する。図２８および図２９は、ド・モルガンの法則適用処理の一例を示すフローチャートである。リスト生成部１３２は、記憶部１２０から条件式ツリーを取得する（ステップＳ３３１）。リスト生成部１３２は、取得した条件式ツリーの根元ノードに対して、再帰処理である全部ド・モルガン処理を実行する（ステップＳ３３２）。リスト生成部１３２は、ド・モルガンの法則適用処理を実行した条件式ツリーを記憶部１２０に記憶する。
【０１１３】
全部ド・モルガン処理について説明する。リスト生成部１３２は、指定ノードが論理演算子であるか否かを判定する（ステップＳ３３２１）。リスト生成部１３２は、指定ノードが論理演算子でない場合には（ステップＳ３３２１：否定）、全部ド・モルガン処理を終了する。リスト生成部１３２は、指定ノードが論理演算子である場合には（ステップＳ３３２１：肯定）、指定ノードにド・モルガンの法則を適用する（ステップＳ３３２２）。また、リスト生成部１３２は、左辺ノードが論理演算子であるか否かを判定する（ステップＳ３３２３）。リスト生成部１３２は、左辺ノードが論理演算子である場合には（ステップＳ３３２３：肯定）、左辺ノード以下のツリーに対して全部ド・モルガン処理を実行、すなわち再帰処理を実行する（ステップＳ３３２４）。
【０１１４】
リスト生成部１３２は、左辺ノードが論理演算子でない場合（ステップＳ３３２３：否定）、または、左辺ノード以下のツリーに対する全部ド・モルガン処理が完了した場合には、右辺ノードが論理演算子であるか否かを判定する（ステップＳ３３２５）。リスト生成部１３２は、右辺ノードが論理演算子である場合には（ステップＳ３３２５：肯定）、右辺ノード以下のツリーに対して全部ド・モルガン処理を実行、すなわち再帰処理を実行して（ステップＳ３３２６）、全部ド・モルガン処理を終了する。リスト生成部１３２は、右辺ノードが論理演算子でない場合には（ステップＳ３３２５：否定）、全部ド・モルガン処理を終了する。これにより、情報処理装置１００は、条件式を簡約化できる。
【０１１５】
図２７の説明に戻って、次に、リスト生成部１３２は、条件式ツリーに対して分配法則適用処理を実行する（ステップＳ３４）。ここで、図３０および図３１を用いて分配法則適用処理を説明する。図３０および図３１は、分配法則適用処理の一例を示すフローチャートである。リスト生成部１３２は、記憶部１２０から条件式ツリーを取得する（ステップＳ３４１）。リスト生成部１３２は、取得した条件式ツリーの根元ノードに対して、再帰処理である全部分配法則処理を実行する（ステップＳ３４２）。リスト生成部１３２は、分配法則適用処理を実行した条件式ツリーを記憶部１２０に記憶する。
【０１１６】
全部分配法則処理について説明する。リスト生成部１３２は、指定ノードが論理演算子であるか否かを判定する（ステップＳ３４２１）。リスト生成部１３２は、指定ノードが論理演算子でない場合には（ステップＳ３４２１：否定）、全部分配法則処理を終了する。リスト生成部１３２は、指定ノードが論理演算子である場合には（ステップＳ３４２１：肯定）、指定ノードに分配法則を適用する（ステップＳ３４２２）。また、リスト生成部１３２は、親ノードが論理演算子∧であるか否かを判定する（ステップＳ３４２３）。リスト生成部１３２は、親ノードが論理演算子∧である場合には（ステップＳ３４２３：肯定）、親ノード以下のツリーに対して全部分配法則処理を実行、すなわち再帰処理を実行する（ステップＳ３４２４）。リスト生成部１３２は、親ノードが論理演算子∧でない場合（ステップＳ３４２３：否定）、または、親ノード以下のツリーに対する全部分配法則処理が完了した場合には、左辺ノードが論理演算子であるか否かを判定する（ステップＳ３４２５）。
【０１１７】
リスト生成部１３２は、左辺ノードが論理演算子である場合には（ステップＳ３４２５：肯定）、左辺ノード以下のツリーに対して全部分配法則処理を実行、すなわち再帰処理を実行する（ステップＳ３４２６）。リスト生成部１３２は、左辺ノードが論理演算子でない場合（ステップＳ３４２５：否定）、または、左辺ノード以下のツリーに対する全部分配法則処理が完了した場合には、右辺ノードが論理演算子であるか否かを判定する（ステップＳ３４２７）。リスト生成部１３２は、右辺ノードが論理演算子である場合には（ステップＳ３４２７：肯定）、右辺ノード以下のツリーに対して全部分配法則処理を実行、すなわち再帰処理を実行して（ステップＳ３４２８）、全部分配法則処理を終了する。リスト生成部１３２は、右辺ノードが論理演算子でない場合には（ステップＳ３４２７：否定）、全部分配法則処理を終了する。これにより、情報処理装置１００は、条件式を簡約化できる。
【０１１８】
図２７の説明に戻って、続いて、リスト生成部１３２は、条件式ツリーに対して収集処理を実行する（ステップＳ３５）。ここで、図３２および図３３を用いて収集処理を説明する。図３２および図３３は、収集処理の一例を示すフローチャートである。リスト生成部１３２は、記憶部１２０から条件式ツリーを取得する（ステップＳ３５１）。リスト生成部１３２は、取得した条件式ツリーの根元ノードに対して、再帰処理であるＤＮＦ項収集処理を実行する（ステップＳ３５２）。リスト生成部１３２は、条件式から収集されたＤＮＦ項にＤＮＦ項Ｎｏ．を付与してＤＮＦ項のリストを生成し、生成したＤＮＦ項のリストをリスト記憶部１２２に記憶する。
【０１１９】
ＤＮＦ項収集処理について説明する。リスト生成部１３２は、指定ノードが論理演算子∨であるか否かを判定する（ステップＳ３５２１）。リスト生成部１３２は、指定ノードが論理演算子∨でない場合には（ステップＳ３５２１：否定）、指定ノードの条件式を収集して（ステップＳ３５２２）、ＤＮＦ項収集処理を終了する。リスト生成部１３２は、指定ノードが論理演算子∨である場合には（ステップＳ３５２１：肯定）、左辺ノードが論理演算子∨であるか否かを判定する（ステップＳ３５２３）。リスト生成部１３２は、左辺ノードが論理演算子∨でない場合には（ステップＳ３５２３：否定）、左辺ノードの条件式を収集する（ステップＳ３５２４）。リスト生成部１３２は、左辺ノードが論理演算子∨である場合には（ステップＳ３５２３：肯定）、左辺ノード以下のツリーに対してＤＮＦ項収集処理を実行、すなわち再帰処理を実行する（ステップＳ３５２５）。
【０１２０】
また、リスト生成部１３２は、左辺ノードの条件式を収集した場合、または、左辺ノード以下のツリーに対するＤＮＦ項収集処理が完了した場合には、右辺ノードが論理演算子∨であるか否かを判定する（ステップＳ３５２６）。リスト生成部１３２は、右辺ノードが論理演算子∨でない場合には（ステップＳ３５２６：否定）、右辺ノードの条件式を収集して（ステップＳ３５２７）、ＤＮＦ項収集処理を終了する。リスト生成部１３２は、右辺ノードが論理演算子∨である場合には（ステップＳ３５２６：肯定）、右辺ノード以下のツリーに対してＤＮＦ項収集処理を実行、すなわち再帰処理を実行して（ステップＳ３５２８）、ＤＮＦ項収集処理を終了する。これにより、情報処理装置１００は、ＤＮＦ項を収集できる。
【０１２１】
図２７の説明に戻って、リスト生成部１３２は、条件式から収集されたＤＮＦ項にＤＮＦ項Ｎｏ．を付与してＤＮＦ項のリストを生成し（ステップＳ３６）、生成したＤＮＦ項のリストをリスト記憶部１２２に記憶する。これにより、情報処理装置１００は、ＤＮＦ項のリストを生成できる。
【０１２２】
図２６の説明に戻って、抽出部１３３は、第１条件式から第２条件式を抽出する抽出処理を実行する（ステップＳ４）。ここで、図３４および図３５を用いて抽出処理を説明する。図３４および図３５は、抽出処理の一例を示すフローチャートである。抽出部１３３は、リスト生成部１３２が構成した第１条件式に対応する条件式ツリーを記憶部１２０から取得する（ステップＳ４１）。抽出部１３３は、取得した条件式ツリーの根元ノードに対して、再帰処理である第２条件式収集処理を実行する（ステップＳ４２）。抽出部１３３は、第２条件式収集処理によって収集、すなわち抽出した第２条件式を第２条件式記憶部１２３に記憶する。
【０１２３】
第２条件式収集処理について説明する。抽出部１３３は、指定ノードが比較演算子であるか否かを判定する（ステップＳ４２１）。抽出部１３３は、指定ノードが比較演算子である場合には（ステップＳ４２１：肯定）、比較演算子にＮＯＴがあるか否かを判定する（ステップＳ４２２）。抽出部１３３は、比較演算子にＮＯＴがある場合には（ステップＳ４２２：肯定）、ＮＯＴを除去する（ステップＳ４２３）。抽出部１３３は、比較演算子にＮＯＴがない場合（ステップＳ４２２：否定）、または、ＮＯＴを除去した場合には、条件式が抽出済みであるか否かを判定する（ステップＳ４２４）。抽出部１３３は、条件式が抽出済みでない場合には（ステップＳ４２４：否定）、現条件式を第２条件式として、第２条件式記憶部１２３に記憶し（ステップＳ４２５）、第２条件式収集処理を終了する。抽出部１３３は、条件式が抽出済みである場合には（ステップＳ４２４：肯定）、第２条件式収集処理を終了する。
【０１２４】
ステップＳ４２１の説明に戻る。抽出部１３３は、指定ノードが比較演算子でない場合には（ステップＳ４２１：否定）、左辺ノードがあるか否かを判定する（ステップＳ４２６）。抽出部１３３は、左辺ノードがある場合には（ステップＳ４２６：肯定）、左辺ノード以下のツリーに対して第２条件式収集処理を実行する（ステップＳ４２７）。抽出部１３３は、左辺ノードがない場合（ステップＳ４２６：否定）、または、左辺ノード以下のツリーに対する第２条件式収集処理が完了した場合には、右辺ノードがあるか否かを判定する（ステップＳ４２８）。抽出部１３３は、右辺ノードがある場合には（ステップＳ４２８：肯定）、右辺ノード以下のツリーに対して第２条件式収集処理を実行し（ステップＳ４２９）、第２条件式収集処理を終了する。抽出部１３３は、右辺ノードがない場合（ステップＳ４２８：否定）、または、右辺ノード以下のツリーに対する第２条件式収集処理が完了した場合には、第２条件式収集処理を終了する。これにより、情報処理装置１００は、第２条件式を収集できる。
【０１２５】
図２６の説明に戻って、存否表生成部１３４は、ＤＮＦ項ごとに第２条件式の存否を管理する存否表を生成する存否表生成処理を実行する（ステップＳ５）。ここで、図３６から図３９を用いて存否表生成処理を説明する。図３６は、存否表生成処理の一例を示すフローチャートである。存否表生成部１３４は、リスト記憶部１２２および第２条件式記憶部１２３を参照して、ＤＮＦ項（ＤＮＦ＿ｉ，ｉ＝１，．．．，ｍ）と、第２条件式（ＥＣ＿ｊ，ｊ＝１，．．．，ｎ）とを取得する（ステップＳ５１１）。
【０１２６】
存否表生成部１３４は、ＤＮＦ項と第２条件式とを取得すると、ｉに「１」を設定する（ステップＳ５１２）。存否表生成部１３４は、ｉがｍより大きいか否かを判定する（ステップＳ５１３）。存否表生成部１３４は、ｉがｍより大きい場合には（ステップＳ５１３：肯定）、存否表を出力して存否表記憶部１２４に記憶し（ステップＳ５２７）、存否表生成処理を終了する。
【０１２７】
存否表生成部１３４は、ｉがｍ以下である場合には（ステップＳ５１３：否定）、ＤＮＦ＿ｉから条件式（ＲＣ＿ｋ，．．．，Ｎ）を取得する（ステップＳ５１４）。存否表生成部１３４は、取得したＤＮＦ項であるＤＮＦ＿ｉ、第２条件式ＥＣ＿ｊ、および、条件式ＲＣ＿ｋを記憶部１２０に記憶する。また、存否表生成部１３４は、ＤＮＦ＿ｉ、第２条件式ＥＣ＿ｊ、および、条件式ＲＣ＿ｋについて、それぞれ条件式ツリーを生成して記憶部１２０に記憶する。
【０１２８】
存否表生成部１３４は、ＤＮＦ＿ｉから条件式ＲＣ＿ｋを取得すると、ｋに「１」を設定する（ステップＳ５１５）。存否表生成部１３４は、ｋがＮより大きいか否かを判定する（ステップＳ５１６）。存否表生成部１３４は、ｋがＮより大きい場合には（ステップＳ５１６：肯定）、ｉをインクリメントして（ステップＳ５１７）、ステップＳ５１３に戻る。存否表生成部１３４は、ｋがＮ以下の場合には（ステップＳ５１６：否定）、ｊに「１」を設定する（ステップＳ５１８）。存否表生成部１３４は、ｊがｎより大きいか否かを判定する（ステップＳ５１９）。存否表生成部１３４は、ｊがｎより大きい場合には（ステップＳ５１９：肯定）、ｋをインクリメントして（ステップＳ５２６）、ステップＳ５１６に戻る。存否表生成部１３４は、ｊがｎ以下の場合には（ステップＳ５１９：否定）、同値判定処理を実行する（ステップＳ５２０）。
【０１２９】
図３７を用いて、同値判定処理について説明する。図３７は、同値判定処理の一例を示すフローチャートである。存否表生成部１３４は、２つの条件式ツリー、すなわち、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊの条件式ツリーを記憶部１２０から取得する（ステップＳ５２０１）。存否表生成部１３４は、２つの条件式、つまり２つの条件式ツリーの同値は既に判定済みであるか否かを判定する（ステップＳ５２０２）。存否表生成部１３４は、２つの条件式の同値は既に判定済みである場合には（ステップＳ５２０２：肯定）、既存の判定結果を利用して（ステップＳ５２１０）、同値判定処理を終了する。存否表生成部１３４は、２つの条件式の同値は既に判定済みでない場合には（ステップＳ５２０２：否定）、ツリー判定処理を実行する（ステップＳ５２０３）。
【０１３０】
図３８を用いて、ツリー判定処理について説明する。図３８は、ツリー判定処理の一例を示すフローチャートである。存否表生成部１３４は、同値判定処理から２つの条件式ツリーを取得する（ステップＳ５２０３１）。存否表生成部１３４は、２つの条件式ツリーの比較演算子が同じであるか否かを判定する（ステップＳ５２０３２）。存否表生成部１３４は、２つの条件式ツリーの比較演算子が同じである場合には（ステップＳ５２０３２：肯定）、２つの条件式ツリーの左辺同士、右辺同士が同じであるか否かを判定する（ステップＳ５２０３３）。存否表生成部１３４は、２つの条件式ツリーの左辺同士、右辺同士が同じである場合には（ステップＳ５２０３３：肯定）、２つの条件式ツリーは同値であると判定して（ステップＳ５２０３４）、ツリー判定処理を終了する。存否表生成部１３４は、２つの条件式ツリーの左辺同士、右辺同士が異なる場合には（ステップＳ５２０３３：否定）、ツリー判定処理を終了する。
【０１３１】
ステップＳ５２０３２の説明に戻る。存否表生成部１３４は、２つの条件式ツリーの比較演算子が異なる場合には（ステップＳ５２０３２：否定）、判定した２つの比較演算子が逆であるか否かを判定する（ステップＳ５２０３５）。存否表生成部１３４は、判定した２つの比較演算子が逆でない場合には（ステップＳ５２０３５：否定）、ツリー判定処理を終了する。存否表生成部１３４は、判定した２つの比較演算子が逆である場合には（ステップＳ５２０３５：肯定）、２つの条件式ツリーの右辺左辺が逆であるか否かを判定する（ステップＳ５２０３６）。存否表生成部１３４は、２つの条件式ツリーの右辺左辺が逆である場合には（ステップＳ５２０３６：肯定）、２つの条件式ツリーは同値であると判定して（ステップＳ５２０３４）、ツリー判定処理を終了する。存否表生成部１３４は、２つの条件式ツリーの右辺左辺が逆でない場合には（ステップＳ５２０３６：否定）、ツリー判定処理を終了する。これにより、情報処理装置１００は、２つの条件式ツリーが同値であるか否かを判定できる。
【０１３２】
図３７の説明に戻って、存否表生成部１３４は、ツリー判定処理の判定結果がツリーとして同値であるか否かを判定する（ステップＳ５２０４）。存否表生成部１３４は、ツリー判定処理の判定結果がツリーとして同値である場合には（ステップＳ５２０４：肯定）、２つの条件式が同値である判定結果を生成して（ステップＳ５２０８）、同値判定処理を終了する。存否表生成部１３４は、ツリー判定処理の判定結果がツリーとして同値でない場合には（ステップＳ５２０４：否定）、ＳＭＴソルバ判定処理を実行する（ステップＳ５２０５）。
【０１３３】
図３９を用いて、ＳＭＴソルバ判定処理について説明する。図３９は、ＳＭＴソルバ判定処理の一例を示すフローチャートである。存否表生成部１３４は、同値判定処理から２つの条件式をＣ１、Ｃ２として取得する（ステップＳ５２０５１）。存否表生成部１３４は、取得したＣ１、Ｃ２に基づいて、Ｃ１∧Ｃ２、¬Ｃ１∧Ｃ２を生成する（ステップＳ５２０５２）。存否表生成部１３４は、ＳＭＴソルバを用いて、Ｃ１∧Ｃ２、¬Ｃ１∧Ｃ２の充足可能性を判定する（ステップＳ５２０５３）。存否表生成部１３４は、充足可能性の判定の結果について、Ｃ１∧Ｃ２が充足可能、かつ、¬Ｃ１∧Ｃ２が充足不可能であるか否かを判定する（ステップＳ５２０５４）。存否表生成部１３４は、Ｃ１∧Ｃ２が充足可能、かつ、¬Ｃ１∧Ｃ２が充足不可能である場合には（ステップＳ５２０５４：肯定）、２つの条件式が同値であると判定して（ステップＳ５２０５５）、ＳＭＴソルバ判定処理を終了する。存否表生成部１３４は、Ｃ１∧Ｃ２が充足可能、かつ、¬Ｃ１∧Ｃ２が充足不可能でない場合には（ステップＳ５２０５４：否定）、ＳＭＴソルバ判定処理を終了する。これにより、情報処理装置１００は、２つの条件式ツリーが同値であるか否かを判定できる。
【０１３４】
図３７の説明に戻って、存否表生成部１３４は、ＳＭＴソルバ判定処理の判定結果が同値であるか否かを判定する（ステップＳ５２０６）。存否表生成部１３４は、ＳＭＴソルバ判定処理の判定結果が同値である場合には（ステップＳ５２０６：肯定）、２つの条件式が同値である判定結果を生成して（ステップＳ５２０８）、同値判定処理を終了する。存否表生成部１３４は、ＳＭＴソルバ判定処理の判定結果が同値でない場合には（ステップＳ５２０６：否定）、同値でない判定結果を生成して（ステップＳ５２０７）、同値判定処理を終了する。これにより、情報処理装置１００は、２つの条件式ツリーが同値であるか否かを判定できる。
【０１３５】
図３６の説明に戻って、存否表生成部１３４は、同値判定処理の判定結果に基づいて、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが同値であるか否かを判定する（ステップＳ５２１）。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが同値である場合には（ステップＳ５２１：肯定）、ＤＮＦ＿ｉに第２条件式ＥＣ＿ｊが同値で存在するとする（ステップＳ５２２）。存否表生成部１３４は、ＤＮＦ＿ｉに第２条件式ＥＣ＿ｊが同値で存在するとした場合には、存否表の対応するセルに「１」を記憶し、ステップＳ５２６に進む。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが同値でない場合には（ステップＳ５２１：否定）、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係であるか否かを判定する（ステップＳ５２３）。
【０１３６】
存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係である場合には（ステップＳ５２３：肯定）、ＤＮＦ＿ｉに第２条件式ＥＣ＿ｊが否定で存在するとする（ステップＳ５２５）。存否表生成部１３４は、ＤＮＦ＿ｉに第２条件式ＥＣ＿ｊが否定で存在するとした場合には、存否表の対応するセルに「０」を記憶し、ステップＳ５２６に進む。存否表生成部１３４は、条件式ＲＣ＿ｋ、および、第２条件式ＥＣ＿ｊが否定の関係でない場合には（ステップＳ５２３：否定）、存否表の対応するセルは「−」であるとして、ｊをインクリメントして（ステップＳ５２４）、ステップＳ５１９に戻る。これにより、情報処理装置１００は、存否表を生成できる。
【０１３７】
図２６の説明に戻って、条件表生成部１３５は、存否表が生成されると、因数条件表を生成する条件表生成処理を実行する（ステップＳ６）。ここで、図４０および図４１を用いて条件表生成処理を説明する。図４０および図４１は、条件表生成処理の一例を示すフローチャートである。条件表生成部１３５は、存否表記憶部１２４を参照して、存否表を取得する（ステップＳ６１）。条件表生成部１３５は、取得した存否表に対して、再帰処理である因数条件表生成処理を実行する（ステップＳ６２）。条件表生成部１３５は、因数条件表生成処理で生成された因数条件表を因数条件表記憶部１２５に記憶する。
【０１３８】
因数条件表生成処理について説明する。条件表生成部１３５は、第２条件式記憶部１２３を参照して第２条件式を取得する。条件表生成部１３５は、取得した第２条件式のうち、先頭の第２条件式を選択する（ステップＳ６２１）。条件表生成部１３５は、変数ｅに「１」を設定する（ステップＳ６２２）。条件表生成部１３５は、変数ｅが「０」未満であるか否かを判定する（ステップＳ６２３）。条件表生成部１３５は、変数ｅが「０」未満である場合には（ステップＳ６２３：肯定）、因数条件表生成処理を終了する。
【０１３９】
条件表生成部１３５は、変数ｅが「０」未満でない場合には（ステップＳ６２３：否定）、存否表のうち選択された第２条件式の存否がｅであるＤＮＦ項の行を選択する（ステップＳ６２４）。条件表生成部１３５は、選択行の個数が３個以上であるか否かを判定する（ステップＳ６２５）。条件表生成部１３５は、選択行の個数が３個未満である場合には（ステップＳ６２５：否定）、次の第２条件式を選択して（ステップＳ６３０）、ステップＳ６２３に戻る。条件表生成部１３５は、選択行の個数が３個以上である場合には（ステップＳ６２５：肯定）、因数条件表に先頭の第２条件式および選択行のＤＮＦ項Ｎｏ．を対応付けて、因数条件表記憶部１２５に記憶する（ステップＳ６２６）。
【０１４０】
条件表生成部１３５は、存否表から選択行のＤＮＦ項Ｎｏ．に対応する行を抽出し、先頭の第２条件式の列を削除して部分存否表を生成する（ステップＳ６２７）。条件表生成部１３５は、生成した部分存否表に対して因数条件表生成処理を実行、すなわち再帰処理を実行する（ステップＳ６２８）。条件表生成部１３５は、再帰処理が終了するとｅをデクリメントして（ステップＳ６２９）、ステップＳ６２３に戻る。これにより、情報処理装置１００は、因数条件表を生成できる。
【０１４１】
図２６の説明に戻って、更新部１３６は、因数条件表が生成されると、更新処理を実行する（ステップＳ７）。ここで、図４２および図４３を用いて更新処理を説明する。図４２は、更新処理の一例を示すフローチャートである。更新部１３６は、存否表記憶部１２４および因数条件表記憶部１２５を参照して、存否表と因数条件表とを取得する（ステップＳ７１）。更新部１３６は、因数条件表で因数条件に含まれる第２条件式の数が多い順に行を選択し、対応するＤＮＦ項Ｎｏ．を取得する（ステップＳ７２）。更新部１３６は、因数条件表に未処理の行があるか否かを判定する（ステップＳ７３）。更新部１３６は、因数条件表に未処理の行がない場合には（ステップＳ７３：否定）、更新処理を終了する。
【０１４２】
更新部１３６は、因数条件表に未処理の行がある場合には（ステップＳ７３：肯定）、因数条件に含まれない第２条件式を連言で結合して存否表のＤＮＦ項Ｎｏ．ごとに第５条件式を生成する（ステップＳ７４）。更新部１３６は、生成した第５条件式を選言で結合して第３条件式を生成する（ステップＳ７５）。更新部１３６は、生成した第３条件式について真偽を判定する第３条件式判定処理を実行する（ステップＳ７６）。
【０１４３】
図４３を用いて、第３条件式判定処理について説明する。図４３は、第３条件式判定処理の一例を示すフローチャートである。更新部１３６は、更新処理から第３条件式を取得する（ステップＳ７６１）。更新部１３６は、第３条件式の真偽判定ルールが成立するか否かを判定する（ステップＳ７６２）。更新部１３６は、第３条件式の真偽判定ルールが成立すると判定した場合には（ステップＳ７６２：肯定）、第３条件式が真であると判定して（ステップＳ７６３）、第３条件式判定処理を終了する。
【０１４４】
更新部１３６は、第３条件式の真偽判定ルールが成立しないと判定した場合には（ステップＳ７６２：否定）、ＳＭＴソルバを利用して、（第３条件式）およびＮＯＴ（第３条件式）の充足可能性を判定する（ステップＳ７６４）。更新部１３６は、充足可能性の判定の結果について、（第３条件式）が充足可能、かつ、ＮＯＴ（第３条件式）が充足不可能であるか否かを判定する（ステップＳ７６５）。更新部１３６は、（第３条件式）が充足可能、かつ、ＮＯＴ（第３条件式）が充足不可能である場合には（ステップＳ７６５：肯定）、第３条件式が真であると判定して（ステップＳ７６３）、第３条件式判定処理を終了する。更新部１３６は、（第３条件式）が充足可能、かつ、ＮＯＴ（第３条件式）が充足不可能でない場合には（ステップＳ７６５：否定）、第３条件式が偽であると判定して（ステップＳ７６６）、第３条件式判定処理を終了する。これにより、情報処理装置１００は、第３条件式の真偽を判定できる。
【０１４５】
図４２の説明に戻って、更新部１３６は、第３条件式判定処理の判定結果に基づいて、第３条件式が真であるか否かを判定する（ステップＳ７７）。更新部１３６は、第３条件式が真である場合には（ステップＳ７７：肯定）、存否表の対応するＤＮＦ項Ｎｏ．の行について、１つの行の第５条件式に含まれる第２条件式、および、他の行の全ての第２条件式の存否を不在（−）に更新する（ステップＳ７８）。更新部１３６は、ステップＳ７８の更新を行うと、ステップＳ７２に戻る。更新部１３６は、第３条件式が真でない場合には（ステップＳ７７：否定）、ステップＳ７２に戻る。これにより、情報処理装置１００は、存否表を更新できる。
【０１４６】
図２６の説明に戻って、条件式生成部１３７は、存否表記憶部１２４に記憶されている存否表が更新されると、条件式生成処理を実行する（ステップＳ８）。ここで、図４４を用いて条件式生成処理を説明する。図４４は、条件式生成処理の一例を示すフローチャートである。条件式生成部１３７は、存否表記憶部１２４を参照して、更新された存否表を取得する（ステップＳ８１）。条件式生成部１３７は、取得した存否表の行を１行ずつ順に選択する（ステップＳ８２）。
【０１４７】
条件式生成部１３７は、存否表に未処理の行があるか否かを判定する（ステップＳ８３）。条件式生成部１３７は、存否表に未処理の行がある場合には（ステップＳ８３：肯定）、選択した行について、第２条件式の存否に「１」か「０」が存在するか否かを判定する（ステップＳ８４）。条件式生成部１３７は、第２条件式の存否に「１」か「０」が存在する場合には（ステップＳ８４：肯定）、「１」ならば第２条件式、「０」ならば第２条件式の否定として連言で結合して、第６条件式を生成して（ステップＳ８５）、ステップＳ８２に戻る。条件式生成部１３７は、第２条件式の存否に「１」か「０」が存在しない場合には（ステップＳ８４：否定）、ステップＳ８２に戻る。
【０１４８】
ステップＳ８３の説明に戻る。条件式生成部１３７は、存否表に未処理の行がない場合には（ステップＳ８３：否定）、生成された第６条件式を選言で結合して第４条件式を生成する（ステップＳ８６）。条件式生成部１３７は、生成した第４条件式を、出力部１１２に出力する（ステップＳ８７）。また、条件式生成部１３７は、生成した第４条件式を、表示部１１３に表示する。これにより、情報処理装置１００は、第１条件式を簡約化した第４条件式を出力できる。また、情報処理装置１００は、条件式の可読性を向上できる。
【０１４９】
このように、情報処理装置１００は、第１条件式を連言節の選言の形式に展開して、連言節のリストを生成する。情報処理装置１００は、論理演算子を含まずに比較演算子を１つ有する第２条件式を、第１条件式から抽出する。情報処理装置１００は、生成された連言節のリストと、抽出された第２条件式とに基づいて、連言節ごとに第２条件式の存否を管理する存否表を生成する。情報処理装置１００は、生成された連言節のリストおよび存否表に基づいて、因数分解の因数条件と連言節とを対応させる因数条件表を生成する。情報処理装置１００は、生成された因数条件表および存否表に基づいて、因数条件に含まれない因数条件の候補に基づいて生成した第３条件式について真偽を判定し、判定の結果が真である場合に、第３条件式に基づいて存否表を更新する。情報処理装置１００は、更新された存否表に基づいて、第１条件式を簡約化して第４条件式を生成する。その結果、条件式の可読性を向上できる。
【０１５０】
また、情報処理装置１００は、第２条件式および第２条件式の否定を因数条件の候補として、連言節のリストに含まれる連言節を因数分解し、因数条件ごとに該因数条件を有する連言節を対応させる因数条件表を生成する。また、情報処理装置１００は、因数条件に含まれる候補の個数が多い順に、因数条件に含まれない候補の連言節である第５条件式を生成し、生成した第５条件式を選言で結合した第３条件式について真偽を判定する。情報処理装置１００は、判定の結果が真である場合に、判定した第３条件式に含まれる第２条件式が不在となるように存否表を更新する。その結果、条件式を簡約化できるので、条件式の可読性を向上できる。
【０１５１】
また、情報処理装置１００は、因数条件を有する連言節が３つ以上である因数条件に基づいて、因数条件表を生成する。その結果、ＱＭ法で簡約化した条件式に対しても、さらに簡約化できる。
【０１５２】
また、情報処理装置１００では、第１条件式は、プログラムをシンボリック実行した場合におけるパス、パスのパス条件およびパス出力を抽出して、パス出力の出力変数ごとに、該出力変数の出力値が同一となるパスのパス条件に基づいて生成された選言条件式である。その結果、プログラムの仕様について容易に理解できる条件式を得られる。
【０１５３】
また、情報処理装置１００は、第１条件式に代えて、連言節のリストから第２条件式を抽出する。その結果、第２条件式の抽出と存否表の生成とを１つの処理として実行できる。
【０１５４】
また、情報処理装置１００は、存否表の値のパターンに基づいて、第３条件式について真偽を判定し、判定の結果が真である場合に、第３条件式に基づいて存否表を更新する。その結果、ＳＭＴソルバの制限や性能に依存せずに第３条件式の真偽を判定できる。
【０１５５】
なお、上記実施例では、ＱＭ法を適用した後の条件式を第１条件式としたが、これに限定されない。例えば、プログラムをシンボリック実行した結果得られる条件式を第１条件式としてもよい。
【０１５６】
また、図示した各部の各構成要素は、必ずしも物理的に図示の如く構成されていることを要しない。すなわち、各部の分散・統合の具体的形態は図示のものに限られず、その全部または一部を、各種の負荷や使用状況等に応じて、任意の単位で機能的または物理的に分散・統合して構成することができる。例えば、抽出部１３３と存否表生成部１３４とを統合してもよい。
【０１５７】
さらに、各装置で行われる各種処理機能は、ＣＰＵ（またはＭＰＵ、ＭＣＵ（Micro  Controller  Unit）等のマイクロ・コンピュータ）上で、その全部または任意の一部を実行するようにしてもよい。また、各種処理機能は、ＣＰＵ（またはＭＰＵ、ＭＣＵ等のマイクロ・コンピュータ）で解析実行されるプログラム上、またはワイヤードロジックによるハードウェア上で、その全部または任意の一部を実行するようにしてもよいことは言うまでもない。
【０１５８】
ところで、上記の実施例で説明した各種の処理は、予め用意されたプログラムをコンピュータで実行することで実現できる。そこで、以下では、上記の実施例と同様の機能を有するプログラムを実行するコンピュータの一例を説明する。図４５は、情報処理プログラムを実行するコンピュータの一例を示す図である。
【０１５９】
図４５に示すように、コンピュータ２００は、各種演算処理を実行するＣＰＵ２０１と、データ入力を受け付ける入力装置２０２と、モニタ２０３とを有する。また、コンピュータ２００は、記憶媒体からプログラム等を読み取る媒体読取装置２０４と、各種装置と接続するためのインタフェース装置２０５と、他の情報処理装置等と有線または無線により接続するための通信装置２０６とを有する。また、コンピュータ２００は、各種情報を一時記憶するＲＡＭ２０７と、ハードディスク装置２０８とを有する。また、各装置２０１〜２０８は、バス２０９に接続される。
【０１６０】
ハードディスク装置２０８には、図１に示した記号実行部１３１、リスト生成部１３２、抽出部１３３、存否表生成部１３４、条件表生成部１３５、更新部１３６および条件式生成部１３７の各処理部と同様の機能を有する情報処理プログラムが記憶される。また、ハードディスク装置２０８には、ロジック表記憶部１２１、リスト記憶部１２２、第２条件式記憶部１２３、存否表記憶部１２４、因数条件表記憶部１２５、および、情報処理プログラムを実現するための各種データが記憶される。入力装置２０２は、例えば、コンピュータ２００の管理者から操作情報、管理情報等の各種情報の入力を受け付ける。モニタ２０３は、例えば、コンピュータ２００の管理者に対して表示画面、管理情報の画面および各種画面を表示する。媒体読取装置２０４は、例えば、記録媒体に記録された第１条件式を読み取る。インタフェース装置２０５は、例えば印刷装置等が接続される。通信装置２０６は、例えば、図１に示した入力部１１１の一例である通信部と同様の機能を有し図示しないネットワークと接続され、各種装置と各種情報をやりとりする。
【０１６１】
ＣＰＵ２０１は、ハードディスク装置２０８に記憶された各プログラムを読み出して、ＲＡＭ２０７に展開して実行することで、各種の処理を行う。また、これらのプログラムは、コンピュータ２００を図１に示した記号実行部１３１、リスト生成部１３２、抽出部１３３、存否表生成部１３４、条件表生成部１３５、更新部１３６および条件式生成部１３７として機能させることができる。
【０１６２】
なお、上記の情報処理プログラムは、必ずしもハードディスク装置２０８に記憶されている必要はない。例えば、コンピュータ２００が読み取り可能な記憶媒体に記憶されたプログラムを、コンピュータ２００が読み出して実行するようにしてもよい。コンピュータ２００が読み取り可能な記憶媒体は、例えば、ＣＤ−ＲＯＭやＤＶＤディスク、ＵＳＢメモリ等の可搬型記録媒体、フラッシュメモリ等の半導体メモリ、ハードディスクドライブ等が対応する。また、公衆回線、インターネット、ＬＡＮ等に接続された装置にこの情報処理プログラムを記憶させておき、コンピュータ２００がこれらから情報処理プログラムを読み出して実行するようにしてもよい。
【０１６３】
以上、本実施例を含む実施の形態に関し、さらに以下の付記を開示する。
【０１６４】
（付記１）第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成するリスト生成部と、
論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出する抽出部と、
生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成する存否表生成部と、
生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成する条件表生成部と、
生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新する更新部と、
更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する条件式生成部と、
を有することを特徴とする情報処理装置。
【０１６５】
（付記２）前記条件表生成部は、前記第２条件式および前記第２条件式の否定を前記因数条件の候補として、前記連言節のリストに含まれる前記連言節を因数分解し、前記因数条件ごとに該因数条件を有する前記連言節を対応させる前記因数条件表を生成し、
前記更新部は、前記因数条件に含まれる前記候補の個数が多い順に、前記因数条件に含まれない前記候補の連言節である第５条件式を生成し、生成した前記第５条件式を選言で結合した前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、判定した前記第３条件式に含まれる前記第２条件式が不在となるように前記存否表を更新することを特徴とする付記１に記載の情報処理装置。
【０１６６】
（付記３）前記条件表生成部は、前記因数条件を有する前記連言節が３つ以上である前記因数条件に基づいて、前記因数条件表を生成することを特徴とする付記２に記載の情報処理装置。
【０１６７】
（付記４）前記第１条件式は、プログラムをシンボリック実行した場合におけるパス、前記パスのパス条件およびパス出力を抽出して、前記パス出力の出力変数ごとに、該出力変数の出力値が同一となる前記パスの前記パス条件に基づいて生成された選言条件式であることを特徴とする付記１〜３のいずれか１つに記載の情報処理装置。
【０１６８】
（付記５）前記抽出部は、前記第１条件式に代えて、前記連言節のリストから前記第２条件式を抽出することを特徴とする付記１〜４のいずれか１つに記載の情報処理装置。
【０１６９】
（付記６）前記更新部は、前記存否表の値のパターンに基づいて、前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新することを特徴とする付記１〜５のいずれか１つに記載の情報処理装置。
【０１７０】
（付記７）第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成し、
論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出し、
生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成し、
生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成し、
生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新し、
更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する
処理をコンピュータが実行することを特徴とする情報処理方法。
【０１７１】
（付記８）前記因数条件表を生成する処理は、前記第２条件式および前記第２条件式の否定を前記因数条件の候補として、前記連言節のリストに含まれる前記連言節を因数分解し、前記因数条件ごとに該因数条件を有する前記連言節を対応させる前記因数条件表を生成し、
前記更新する処理は、前記因数条件に含まれる前記候補の個数が多い順に、前記因数条件に含まれない前記候補の連言節である第５条件式を生成し、生成した前記第５条件式を選言で結合した前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、判定した前記第３条件式に含まれる前記第２条件式が不在となるように前記存否表を更新することを特徴とする付記７に記載の情報処理方法。
【０１７２】
（付記９）前記因数条件表を生成する処理は、前記因数条件を有する前記連言節が３つ以上である前記因数条件に基づいて、前記因数条件表を生成することを特徴とする付記８に記載の情報処理方法。
【０１７３】
（付記１０）前記第１条件式は、プログラムをシンボリック実行した場合におけるパス、前記パスのパス条件およびパス出力を抽出して、前記パス出力の出力変数ごとに、該出力変数の出力値が同一となる前記パスの前記パス条件に基づいて生成された選言条件式であることを特徴とする付記７〜９のいずれか１つに記載の情報処理方法。
【０１７４】
（付記１１）前記抽出する処理は、前記第１条件式に代えて、前記連言節のリストから前記第２条件式を抽出することを特徴とする付記７〜１０のいずれか１つに記載の情報処理方法。
【０１７５】
（付記１２）前記更新する処理は、前記存否表の値のパターンに基づいて、前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新することを特徴とする付記７〜１１のいずれか１つに記載の情報処理方法。
【０１７６】
（付記１３）第１条件式を連言節の選言の形式に展開して、前記連言節のリストを生成し、
論理演算子を含まずに比較演算子を１つ有する第２条件式を、前記第１条件式から抽出し、
生成された前記連言節のリストと、抽出された前記第２条件式とに基づいて、前記連言節ごとに前記第２条件式の存否を管理する存否表を生成し、
生成された前記連言節のリストおよび前記存否表に基づいて、因数分解の因数条件と前記連言節とを対応させる因数条件表を生成し、
生成された前記因数条件表および前記存否表に基づいて、前記因数条件に含まれない前記因数条件の候補に基づいて生成した第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新し、
更新された前記存否表に基づいて、前記第１条件式を簡約化して第４条件式を生成する
処理をコンピュータに実行させることを特徴とする情報処理プログラム。
【０１７７】
（付記１４）前記因数条件表を生成する処理は、前記第２条件式および前記第２条件式の否定を前記因数条件の候補として、前記連言節のリストに含まれる前記連言節を因数分解し、前記因数条件ごとに該因数条件を有する前記連言節を対応させる前記因数条件表を生成し、
前記更新する処理は、前記因数条件に含まれる前記候補の個数が多い順に、前記因数条件に含まれない前記候補の連言節である第５条件式を生成し、生成した前記第５条件式を選言で結合した前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、判定した前記第３条件式に含まれる前記第２条件式が不在となるように前記存否表を更新することを特徴とする付記１３に記載の情報処理プログラム。
【０１７８】
（付記１５）前記因数条件表を生成する処理は、前記因数条件を有する前記連言節が３つ以上である前記因数条件に基づいて、前記因数条件表を生成することを特徴とする付記１４に記載の情報処理プログラム。
【０１７９】
（付記１６）前記第１条件式は、プログラムをシンボリック実行した場合におけるパス、前記パスのパス条件およびパス出力を抽出して、前記パス出力の出力変数ごとに、該出力変数の出力値が同一となる前記パスの前記パス条件に基づいて生成された選言条件式であることを特徴とする付記１３〜１５のいずれか１つに記載の情報処理プログラム。
【０１８０】
（付記１７）前記抽出する処理は、前記第１条件式に代えて、前記連言節のリストから前記第２条件式を抽出することを特徴とする付記１３〜１６のいずれか１つに記載の情報処理プログラム。
【０１８１】
（付記１８）前記更新する処理は、前記存否表の値のパターンに基づいて、前記第３条件式について真偽を判定し、前記判定の結果が真である場合に、前記第３条件式に基づいて前記存否表を更新することを特徴とする付記１３〜１７のいずれか１つに記載の情報処理プログラム。
【符号の説明】
【０１８２】
１００  情報処理装置
１１１  入力部
１１２  出力部
１１３  表示部
１１４  操作部
１２０  記憶部
１２１  ロジック表記憶部
１２２  リスト記憶部
１２３  第２条件式記憶部
１２４  存否表記憶部
１２５  因数条件表記憶部
１３０  制御部
１３１  記号実行部
１３２  リスト生成部
１３３  抽出部
１３４  存否表生成部
１３５  条件表生成部
１３６  更新部
１３７  条件式生成部
【図１】
2018195042.tif 000003
【図２】
2018195042.tif 000004
【図３】
2018195042.tif 000005
【図４】
2018195042.tif 000006
【図５】
2018195042.tif 000007
【図６】
2018195042.tif 000008
【図７】
2018195042.tif 000009
【図８】
2018195042.tif 000010
【図９】
2018195042.tif 000011
【図１０】
2018195042.tif 000012
【図１１】
2018195042.tif 000013
【図１２】
2018195042.tif 000014
【図１３】
2018195042.tif 000015
【図１４】
2018195042.tif 000016
【図１５】
2018195042.tif 000017
【図１６】
2018195042.tif 000018
【図１７】
2018195042.tif 000019
【図１８】
2018195042.tif 000020
【図１９】
2018195042.tif 000021
【図２０】
2018195042.tif 000022
【図２１】
2018195042.tif 000023
【図２２】
2018195042.tif 000024
【図２３】
2018195042.tif 000025
【図２４】
2018195042.tif 000026
【図２５】
2018195042.tif 000027
【図２６】
2018195042.tif 000028
【図２７】
2018195042.tif 000029
【図２８】
2018195042.tif 000030
【図２９】
2018195042.tif 000031
【図３０】
2018195042.tif 000032
【図３１】
2018195042.tif 000033
【図３２】
2018195042.tif 000034
【図３３】
2018195042.tif 000035
【図３４】
2018195042.tif 000036
【図３５】
2018195042.tif 000037
【図３６】
2018195042.tif 000038
【図３７】
2018195042.tif 000039
【図３８】
2018195042.tif 000040
【図３９】
2018195042.tif 000041
【図４０】
2018195042.tif 000042
【図４１】
2018195042.tif 000043
【図４２】
2018195042.tif 000044
【図４３】
2018195042.tif 000045
【図４４】
2018195042.tif 000046
【図４５】
2018195042.tif 000047