(57)【要約】【課題】条件式を簡約化する際に長大化することを抑制できる。【解決手段】条件式簡約化装置２０は、連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得する。選言形式の条件式のリストに基づいて、選言形式の条件に含まれる各変数の代入値を取得し、代入値のリストを生成する。生成された代入値のリストに基づいて、代入値毎に、代入値を対象条件式に代入することにより、対象条件式を整理する。代入値毎に、代入値を代入して整理された対象条件式と、整理前の対象条件式とに基づいて、整理された対象条件式について、対象条件式の簡約化が成功したか否かを判定する。代入値の各々について、対象条件式で簡約化が成功したと判定された場合に、整理された対象条件式と代入値を表す等式条件式との連言の条件式を作成する。代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成する。【選択図】図８
2019021138.tif 000002
【特許請求の範囲】
【請求項１】
連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得する等式条件抽出部と、
前記選言形式の条件式のリストに基づいて、前記選言形式の条件式に含まれる各変数の代入値を取得し、前記代入値のリストを生成する代入値生成部と、
前記代入値生成部により生成された前記代入値のリストに基づいて、前記代入値毎に、前記代入値を前記対象条件式に代入することにより、前記対象条件式を整理する代入整理部と、
前記代入値毎に、前記代入値を代入して整理された前記対象条件式と、整理前の前記対象条件式とに基づいて、前記整理された前記対象条件式について、前記対象条件式の簡約化が成功したか否かを判定する簡約化判定部と、
前記代入値の各々について、前記対象条件式で簡約化が成功したと判定された場合に、前記整理された前記対象条件式と前記代入値を表す等式条件式との連言の条件式を作成し、前記代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成して出力する簡約化条件出力部と、
を有することを特徴とする条件式簡約化装置。
【請求項２】
前記代入整理部は、前記対象条件式を表す木構造において前記代入値を代入し、末端ノードから順番に各ノードに対応する条件式の真偽値を評価することにより、前記対象条件式を整理することを特徴とする請求項１に記載の条件式簡約化装置。
【請求項３】
前記簡約化判定部は、整理前の前記対象条件式と前記代入値を代入して整理された前記対象条件式とのそれぞれを連言で分割し、前記整理前の前記対象条件式の分割数と、前記整理された前記対象条件式の分割数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする請求項１又は請求項２に記載の条件式簡約化装置。
【請求項４】
整理前の前記対象条件式に含まれる原子条件式の数と前記代入値を代入して整理された前記対象条件式に含まれる原子条件式の数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする請求項３に記載の条件式簡約化装置。
【請求項５】
前記代入値生成部は、前記選言形式の条件式のリストのうち、含まれる原子条件式が多い前記選言形式の条件から順に、代入値を取得する請求項１〜４の何れか１項に記載の条件式簡約化装置。
【請求項６】
連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得し、
前記選言形式の条件式のリストに基づいて、前記選言形式の条件に含まれる各変数の代入値を取得し、前記代入値のリストを生成し、
前記生成された前記代入値のリストに基づいて、前記代入値毎に、前記代入値を前記対象条件式に代入することにより、前記対象条件式を整理し、
前記代入値毎に、前記代入値を代入して整理された前記対象条件式と、整理前の前記対象条件式とに基づいて、前記整理された前記対象条件式について、前記対象条件式の簡約化が成功したか否かを判定し、
前記代入値の各々について、前記対象条件式で簡約化が成功したと判定された場合に、前記整理された前記対象条件式と前記代入値を表す等式条件式との連言の条件式を作成し、前記代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成し、
前記簡約化条件を出力することを特徴とするプログラム。
【請求項７】
連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得し、
前記選言形式の条件式のリストに基づいて、前記選言形式の条件に含まれる各変数の代入値を取得し、前記代入値のリストを生成し、
前記生成された前記代入値のリストに基づいて、前記代入値毎に、前記代入値を前記対象条件式に代入することにより、前記対象条件式を整理し、
前記代入値毎に、前記代入値を代入して整理された前記対象条件式と、整理前の前記対象条件式とに基づいて、前記整理された前記対象条件式について、前記対象条件式の簡約化が成功したか否かを判定し、
前記代入値の各々について、前記対象条件式で簡約化が成功したと判定された場合に、前記整理された前記対象条件式と前記代入値を表す等式条件式との連言の条件式を作成し、前記代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成し、
前記簡約化条件を出力することを特徴とする条件式簡約化方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、条件式簡約化装置、プログラム、及び方法に関する。
【背景技術】
【０００２】
従来より、プログラムのロジックを抽出し、抽出結果の条件式を変換して簡約化する技術がある。
【０００３】
例えば、制約の集合を等価なＤＮＦ（Disjunctive Normal Form）の論理式に変換し、変換後の各論理式の連言項を満たす充足解を包含する解モデルを求める過程と整形整理機能をもつ技術がある。
【０００４】
また、ビット・ストリームの分析を再現する技術がある。この技術では、バックトラッキング及び先読みの両方を避けるように、ステート・マシーンで最適化を行う上で、トリガ条件の設定及び供給条件をＤＮＦ又はＣＮＦ（Conjunctive Normal Form）で単純化している。
【０００５】
また、既定の事後条件に対し、事前条件を効率よく生成する技術がある。この技術では、プログラムを論理式の形式に変換し、事後条件を表す論理式の否定との論理積をとって論理式を作成し、当該論理式を真にする解を求める過程でＣＮＦを用いて事前条件を求めている。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００７−２４１４９１号公報
【特許文献２】特開２０１６−８５７４５号公報
【特許文献３】国際公開２０１１−０５２０３０号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
条件式をＤＮＦに変形する際に適用される分配法則に起因して、条件式内の項数が多数となり条件式が長大化する場合がある。
【０００８】
本発明は、一つの側面として、条件式を簡約化する際に条件式が長大化することを抑制することを目的とする。
【課題を解決するための手段】
【０００９】
一つの態様として、連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得する。選言形式の条件式のリストに基づいて、選言形式の条件に含まれる各変数の代入値を取得し、代入値のリストを生成する。生成された代入値のリストに基づいて、代入値毎に、代入値を対象条件式に代入することにより、対象条件式を整理する。代入値毎に、代入値を代入して整理された対象条件式と、整理前の対象条件式とに基づいて、整理された対象条件式について、対象条件式の簡約化が成功したか否かを判定する。代入値の各々について、対象条件式で簡約化が成功したと判定された場合に、整理された対象条件式と代入値を表す等式条件式との連言の条件式を作成する。代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成する。
【発明の効果】
【００１０】
一つの側面として、条件式を簡約化する際に条件式が長大化することを抑制できる、という効果を有する。
【図面の簡単な説明】
【００１１】
【図１】プログラムのロジック抽出の動作例の一例を示す図である。
【図２】プログラムのフロー図における、条件による分岐構造と処理内容の一例を示す図である。
【図３】プログラムのフロー図における、パス条件を抽出する一例を示す図である。
【図４】図３のプログラムをシンボリック実行によって分析して得られた実現可能なパスのパス条件とパス出力の一覧を示す図である。
【図５】シンボリック実行結果を整理したロジック表の一例を示す図である。
【図６】COBOLプログラムの一例を示す図である。
【図７】図６のプログラムをシンボリック実行によって分析して得られた実現可能なパスのパス条件とパス出力の一覧を示す図である。
【図８】本発明の実施形態に係る条件式簡約化装置の概略構成を示すブロック図である。
【図９】条件式簡約化装置として機能するコンピュータの概略構成を示すブロック図である。
【図１０】条件式簡約化処理の一例を示すフローチャートである。
【図１１】等式条件取得処理の一例を示すフローチャートである。
【図１２】対象条件式を木構造にした場合の一例を示す図である。
【図１３】連言で木構造を分割する処理の一例を示すフローチャートである。
【図１４】等式条件の収集方法の処理の一例を示すフローチャートである。
【図１５】選言で木構造を分割する処理の一例を示すフローチャートである。
【図１６】等式条件取得処理の動作例を示す図である。
【図１７】等式条件取得処理の動作例を示す図である。
【図１８】代入値生成処理の一例を示すフローチャートである。
【図１９】代入値生成処理の動作例を示す図である。
【図２０】代入値生成処理の動作例を示す図である。
【図２１】代入整理処理の一例を示すフローチャートである。
【図２２】代入後の対象条件式の自明部分を除去する処理の一例を示すフローチャートである。
【図２３】代入整理処理の動作例を示す図である。
【図２４】代入整理処理の動作例を示す図である。
【図２５】簡約化判定処理の一例を示すフローチャートである。
【図２６】簡約化判定処理の動作例を示す図である。
【図２７】簡約化判定処理の動作例を示す図である。
【図２８】簡約化判定処理の動作例を示す図である。
【図２９】簡約化判定処理の動作例を示す図である。
【図３０】簡約化条件保持制御処理の一例を示すフローチャートである。
【図３１】簡約化条件を生成する処理の一例を示すフローチャートである。
【図３２】簡約化条件保持制御処理の動作例を示す図である。
【図３３】パス条件を簡約化した場合の一例を示す図である。
【発明を実施するための形態】
【００１２】
本実施形態の詳細を説明する前に、プログラムのロジック抽出、及び条件式の変換について説明する。
【００１３】
まず、プログラムのロジック抽出が必要となる前提について説明する。
【００１４】
既存の情報システムの保守や再構築の作業では、既存システムの現状を理解し把握するため、既存システムに関するドキュメントや有識者の知識などの情報が必要である。しかし、長期に運用保守された情報システムでは、ドキュメントの不備や有識者の不在などの要因により、保守や再構築に作業に必要な情報が不足する事態が発生することがある。
【００１５】
このような場合に、ドキュメントや有識者から得られる情報の代替として、前述の情報システムの実装実体であるプログラムを解析することによって、不足する知識を補う対処が行われる。このようなプログラムの分析は、プログラムのロジック抽出と呼ばれる。ここで、プログラムのロジックとは、プログラムに記述された処理の内容であり、具体的には、プログラムの実行結果としての入出力関係である。
【００１６】
プログラムのロジック抽出の方式の１つに、シンボリック実行技術を利用する手法がある。
【００１７】
ここで、シンボリック実行（Symbolic Execution、記号実行）は、入力変数にシンボル値（記号値）を設定して、プログラムの実行可能なパスを抽出することによって、プログラムを分析する技術である。当該技術は、プログラムに記述された命令文に従って変数値の参照と更新を行い、条件分岐文やループ文のような制御文ではプログラム記述通りに命令文の実行を制御する。特に、条件分岐では条件式の真偽値に従って分岐を選択するが、条件式を構成する変数値にシンボル値が含まれる場合は条件式の真偽値を算出できないので、代わりに条件式の充足可能性（条件式が真となりうること）を判定して条件分岐の分岐選択を制御する。充足可能性の判定は、SMTソルバやSATソルバを利用する。条件分岐の複数の分岐が充足可能な場合は、これら複数の分岐は共に実行可能なので、複数の分岐のうち順に1つを仮定し選択することによって、実行可能パスを抽出する。
【００１８】
シンボリック実行に関しては例えば以下の非特許文献１を参照できる。
【００１９】
非特許文献１：シンボリック実行：玉井哲雄、福永光一、「シンボリック実行システム」、情報処理、pp. 18-28、1982/01/15
【００２０】
シンボリック実行の分析結果は、実行可能なパス毎の、パス条件とパス出力である。これらの結果を整理し、分析対象プログラムから仕様を抽出した結果の１つの形式がロジック表、あるいは、決定表である。ロジック表は、入力に関する条件とその条件が満たされた場合の出力を記述する。
【００２１】
以下では、シンボリック実行を利用したプログラムのロジック抽出の動作例を、図１に示したCOBOLプログラムを例として説明する。プログラム例１には２個のＩＦ文がある。図２はプログラム例１のフロー図であり、条件による分岐構造と処理内容を示す。
【００２２】
図１のプログラムをシンボリック実行で分析することによって、図３に示すように、実行可能な３個のパスとパス毎のパス条件を抽出することができる。ここで、パスは実行された命令文の系列であり、パス条件はパスが終了するまでに経由する条件のうち不定な変数値に関する条件式である。パスが実行可能とは、パス条件が充足可能（条件式が真となりうること）である場合に該当する。
【００２３】
図４は、図３に示した実現可能なパスのパス条件とパス出力である。パス条件は、プログラムに記述されたＩＦ文等の条件文の条件式から単純に抽出されるものではなく、条件文の間に実行された変数の更新結果も取り込んだものである。４番目のパスは、パス条件が充足不能（成立不可能）であるため、実行不可能なパスと判定され抽出されない。パス出力は、パスが実行された結果の出力である。
【００２４】
図５は、図４のシンボリック実行結果を整理したロジック表の例である。ロジック表は、分析対象のプログラムのロジック内容を表現するものであるから、人が理解しやすいように可読性を向上させることが必要である。
【００２５】
次に、条件式を簡略化することの必要性について説明する。
【００２６】
パス条件は、一般に、パス上で経由した分岐条件の連言、つまり、論理積の形式の条件式である。例えば、図４のパス１のパス条件は「(性別='男性')∧(性別!='女性')」である。
【００２７】
ここで、∧は論理演算子の∧である。上記パス条件は(性別=’男性’)と同値である(性別!='女性')という余分な条件が連言されている。余分な条件があると可読性が阻害される。つまり、ロジック表の可読性を向上させるため、条件式は同値のままで簡約化することが求められる。
【００２８】
次に、条件式を簡約化する手順について説明する。
【００２９】
条件式の簡約化は下記のステップ１〜３の手順で行われる。
【００３０】
ステップ１では、簡約化の対象の条件式をＤＮＦに変形する。
【００３１】
ＤＮＦは、論理式の標準化（正規化）の一種であり、連言節の選言の形式で表現される論理式である。ＤＮＦは、選言標準形、または、加法標準形と呼ばれる。
【００３２】
ステップ２では、ＤＮＦの各々の連言節を整理する。
【００３３】
ＤＮＦは連言節の選言の形式なので、偽または充足不可能な連言節は削除できる。ＤＮＦの各連言節で真偽または充足可能性を調べ、偽または充足不可能な連言節を削除することによって、ＤＮＦの連言節の個数を少なくすることができる。
【００３４】
ステップ３では、ＤＮＦに対して、既存技術の論理式の簡略化手法を適用する。既存技術としては、クワイン・マクラスキー法(Quine-McCluskey algoithm:QM法)やカルノー図による方法がある。
【００３５】
上記の既存技術の論理式の簡略化手法を簡単に説明する。
【００３６】
クワイン・マクラスキー法はブール関数を簡単化するための方法である。カルノー図と同様の目的で使われるが、コンピュータによる自動化に適しており、またブール関数が最簡形かどうか決定的に求めることができる。例えば、A、B、Cを論理式とすると、(A∧B∧C)∨(A∧B∧¬C)=A∧B、のように、論理式を簡約化することができる。
【００３７】
カルノー図法による条件式の簡略化は、カルノー図と呼ばれる表を利用して、条件式を簡略化する手法である。この手法も、クワイン・マクラスキー法と同様に、真偽が逆となる２個の論理式の選言が真であることを利用して条件を簡約化する。
【００３８】
上記の条件式の簡約化のステップ１で、簡約化対象の条件式をＤＮＦに変形する手順は、以下ステップ１−１〜１−３の手順である。
【００３９】
ステップ１−１で二重否定を除去する。ステップ１−２でド・モルガンの法則を適用する。ステップ１−３で分配法則を適用する。
【００４０】
しかしながら、ステップ１−３での分配法則の適用に起因して、対象条件式をＤＮＦへ変換した結果、条件式が長大になることがある。
【００４１】
例えば、対象条件式が、(A1∨A2∨…∨Am)∧(B1∨B2∨…∨Bn)である時、分配法則を適用すると、連言節の個数は、(m×n)個となる。
【００４２】
ＤＮＦに変形した結果の条件式が長大化すると、条件式の簡約化のステップ２と３の処理の実行において、処理時間の長大化や使用メモリ量の増大化などの悪影響が生じる。すなわち、課題のひとつは、条件簡約化でのＤＮＦへの変換において条件式が長大化することである。
【００４３】
本実施形態が対象とする条件式は、プログラムをシンボリック実行によって分析した結果のパス条件である。パス条件は、前述のように、シンボリック実行で抽出されたパス上にある条件分岐文の条件の連言である。パス上の条件分岐文の条件が選言を含む複合条件である場合に、前記の課題である「ＤＮＦへの変換での条件式の長大化」が発生する。
【００４４】
以下、図６のCOBOLプログラムの例を用いて、パス条件をＤＮＦに変換する際に、条件式が長大化することを例示する。
【００４５】
図６のプログラムの処理内容は、区分値に依存して出力値を求める処理である。15行目のIF文で、入力された区分値が所定条件を満たすかチェックし、区分値が'A1','A2','A3','A4','A5'に該当しなければエラーとして、実行を中断する。区分値が条件を満たした場合、21行目と24行目のIF文で、区分値の値に依存して、出力値を計算する。図６のような、入力チェックの後に業務内容の処理を行うプログラムは、実際の業務アプリケーション・システムにおいて一般的である。
【００４６】
図７は、図６のプログラムをシンボリック実行によって分析した結果、抽出されたパス、パス条件、及びパス出力を示す。
【００４７】
図７によると、例えば、パスNo.2のパス条件は以下である。
【００４８】
(((区分値='A1')∨(区分値='A2')∨(区分値='A3')∨(区分値='A4')∨(区分値='A5'))∧((区分値='A3')∨(区分値='A4')∨(区分値='A5')))
【００４９】
上記のパス条件には、図６の15行目と21行目のIF文の条件式の選言が含まれている。このパス条件に分配法則を単純に適用すると、以下のように、(5×3)個の連言節に展開され、条件式が長大化する。
【００５０】
((区分値='A1')∧(区分値='A3'))∨((区分値='A1')∧(区分値='A4'))∨((区分値='A1')∧(区分値='A5'))∨((区分値='A2')∧(区分値='A3'))∨((区分値='A2')∧(区分値='A4'))∨((区分値='A2')∧(区分値='A5'))∨((区分値='A3')∧(区分値='A3'))∨((区分値='A3')∧(区分値='A4'))∨((区分値='A3')∧(区分値='A5'))∨((区分値='A4')∧(区分値='A3'))∨((区分値='A4')∧(区分値='A4'))∨((区分値='A4')∧(区分値='A5'))∨((区分値='A5')∧(区分値='A3'))∨((区分値='A5')∧(区分値='A4'))∨((区分値='A5')∧(区分値='A5'))
【００５１】
以上のようにパス条件をＤＮＦに変換する際に、条件式が長大化する。
【００５２】
そこで、本実施形態では、ＤＮＦに変換する際に、条件式が長大化することを抑制する。
【００５３】
本実施形態で用いるアイデアの一例を説明する。簡約化対象の条件式が、図７のパスNo.3のパス条件である場合で説明する。
【００５４】
パス条件３は以下である。
【００５５】
((区分値='A1')∨(区分値='A2')∨(区分値='A3')∨(区分値='A4')∨(区分値='A5'))∧((区分値!='A3')∧(区分値!='A4')∧(区分値!='A5'))∧(区分値='A1')
【００５６】
パス条件３の条件は、図６のプログラム例の３個のIF文において、15行目と21行目のIFはELSE側、24行目のIFはTHEN側を通過するパスのパス条件である。上記の条件を手作業で簡約化の計算を行うと、(区分値='A1')を得ることができる。
【００５７】
一方、本実施形態のアイデアは、パス条件の連言される条件（以下連言条件と記す）に含まれる等式条件を利用することである。上記の条件式の連言条件の等式条件のひとつに、(区分値='A1')がある。
【００５８】
簡約化対象条件式に含まれる等式(区分値='A1')に注目して、以下の処理１〜４を行なう。
【００５９】
処理１では、対象条件の区分値に'A1'を代入する。処理２では、条件式の木構造をトラバースすることによって、代入後の条件の自明な部分を整理する。処理３では、代入で簡約化できるか判定する。処理４では、簡約化成功の場合、代入後整理した条件式に(区分値 = 'A1')を連言する。
【００６０】
上記の処理１〜４の結果は以下のようになる。
【００６１】
(('A1'='A1')∨('A1'='A2')∨('A1'='A3')∨('A1'='A4'))∨('A1'='A5'))∧(('A1'!='A3')∧('A1'!='A4')∧('A1'!='A5'))∧('A1'='A1')∧(区分値='A1')
=TRUE∧(区分値='A1')
=(区分値='A1')
【００６２】
上記の結果は、手作業での簡約化計算の結果と一致するので、連言条件の「等式」を利用して等号値を対象条件に代入し、複数の連言条件を真とできる時、上記の方法で条件式を簡約化できることが分かる。上記のアイデアの方法によって、図７の他のパス条件でも簡約化できる。
【００６３】
ここで、上記のアイデアの方法では、SMTソルバ等を利用した条件式の充足性判定の処理を含まないことに注意すべきである。SMTソルバでの充足可能性判定の処理は、条件式が長大で複雑な場合には実行時間が長くなるが、本アイデアの方法は、代入と条件式のトラバースだけで構成されるので、SMTソルバを使う方法より、高速な実行を期待できる利点がある。
【００６４】
以下、図面を参照して本実施形態の一例を詳細に説明する。
【００６５】
図８に示すように、本実施形態に係る条件式簡約化装置２０は、機能的には、等式条件取得部３１と、代入値生成部３２と、代入整理部３３と、簡約化判定部３４と、簡約化条件保持制御部３５と、簡約化条件出力部３６とを含む。なお、各処理部の処理の詳細については、後述する作用においてフローチャートを参照して説明する。なお、簡約化条件保持制御部３５及び簡約化条件出力部３６は、開示の技術の簡約化条件出力部の一例である
【００６６】
等式条件取得部３１は、連言形式の対象条件式に基づいて、対象条件式に含まれる条件節の各々から、原子条件式を等式条件とする選言形式の条件式を抽出することにより、原子条件式を等式条件とする選言形式の条件式のリストを取得する。
【００６７】
ここで、連言形式の条件式とは、条件節の連言により構成される条件式である。
【００６８】
原子条件式は、比較演算子と比較演算子の右辺と左辺で構成される条件式である。例えば、原子条件式は、「x=y」、「y>2」、「x+y<3」、「x+y>z*y」などのような条件式である。
【００６９】
連言形式の条件式は、選言条件節をClauseiとすると、「Clause1」、「Clause1∧Clause2」、「Clause1∧Clause2∧…∧Clausen」などのような条件式である。
【００７０】
対象とする条件式は、シンボリック実行により抽出されたパス条件である。パス条件は、抽出されたパス上にある条件分岐文の条件の連言である。よって、パス条件は、連言形式の条件式である。
【００７１】
代入値生成部３２は、等式条件取得部３１で取得した選言形式の条件式のリストに基づいて、選言形式の条件式毎に、選言形式の条件式に含まれる連言節の各々から、各変数の代入値を取得して、代入値の組とし、代入値の組のリストを生成する。
【００７２】
ここで、代入値の組のリストは、例えば、[{(X=1,Y=1),(X=2)}]や[{(X=1,Y=1),(X=2)},{(X=1)},{(Y=1)}]である。代入値は丸括弧()で括られた部分であり、同時に設定する２以上の代入値が存在する場合には、同時に設定する２以上の代入値が含まれる。例えば、(X=1,Y=1)は、「Xに1をYに1を同時に設定する」ことを意味する。中括弧{}は、代入値の組であり、{(X=1,Y=1),(X=2)}は、「Xに1をYに1を同時に設定する」または「Xに2を設定する」ことを意味する。代入値の組のリストは、代入値の組を集めたものであり、角括弧[]で表現することにする。
【００７３】
代入整理部３３は、代入値生成部３２により生成された代入値の組のリストに基づいて、代入値毎に、対象条件式を表す木構造において代入値を代入する。代入整理部３３は、代入値毎に、代入値を代入した対象条件式を表す木構造について、末端ノードから順番に各ノードに対応する条件式の真偽値を評価し、偽の条件式に対応する部分を削除することにより、対象条件式を整理する。
【００７４】
簡約化判定部３４は、代入値毎に、代入値を代入して整理された対象条件式と、整理前の対象条件式とに基づいて、整理された対象条件式について、対象条件式の簡約化が成功したか否かを判定する。例えば、整理前の対象条件式と代入値を代入して整理された対象条件式とのそれぞれを連言で分割し、整理前の対象条件式の分割数と、整理された対象条件式の分割数との差が２以上であるか否かに基づいて、成功したか否かを判定する。更に、整理前の対象条件式に含まれる原子条件式の数と代入値を代入して整理された対象条件式に含まれる原子条件式の数との差が２以上であるか否かに基づいて、成功したか否かを判定する。
【００７５】
簡約化条件保持制御部３５は、簡約化判定部３４で簡約化が成功したと判定された代入値と整理された対象条件式とを用いて、簡約化条件を生成する。具体的には、整理された対象条件式と代入値の各々を表す等式条件式との連言の条件式を、簡約化が成功したと判定された代入値の全てについて作成し、作成した条件式の連言の条件式を、簡約化条件として生成する。
【００７６】
簡約化条件出力部３６は、簡約化条件保持制御部３５で生成された簡約化条件を出力する。
【００７７】
条件式簡約化装置２０は、例えば図９に示すコンピュータ４０で実現することができる。コンピュータ４０は、Central Processing Unit（ＣＰＵ）４１と、一時記憶領域としてのメモリ４２と、不揮発性の記憶部４３とを備える。また、コンピュータ４０は、入出力装置４４と、記憶媒体４９に対するデータの読み込み及び書き込みを制御するRead/Write（Ｒ／Ｗ）部４５と、インターネット等のネットワークに接続される通信インターフェース（Ｉ／Ｆ）４６とを備える。ＣＰＵ４１、メモリ４２、記憶部４３、入出力装置４４、Ｒ／Ｗ部４５、及び通信Ｉ／Ｆ４６は、バス４７を介して互いに接続される。
【００７８】
記憶部４３は、Hard Disk Drive（ＨＤＤ）、Solid State Drive（ＳＳＤ）、フラッシュメモリ等によって実現できる。記憶媒体としての記憶部４３には、コンピュータ４０を条件式簡約化装置２０として機能させるための条件式簡約化プログラム５０が記憶される。条件式簡約化プログラム５０は、等式条件取得プロセス５２と、代入値生成プロセス５４と、代入整理プロセス５６と、簡約化判定プロセス５８と、簡約化条件式保持制御プロセス６０と、簡約化条件出力プロセス６２とを有する。
【００７９】
ＣＰＵ４１は、条件式簡約化プログラム５０を記憶部４３から読み出してメモリ４２に展開し、条件式簡約化プログラム５０が有するプロセスを順次実行する。ＣＰＵ４１は、等式条件取得プロセス５２を実行することで、図８に示す等式条件取得部３１として動作する。また、ＣＰＵ４１は、代入値生成プロセス５４を実行することで、図８に示す代入値生成部３２として動作する。また、ＣＰＵ４１は、代入整理プロセス５６を実行することで、図８に示す代入整理部３３として動作する。また、ＣＰＵ４１は、簡約化判定プロセス５８を実行することで、図８に示す簡約化判定部３４として動作する。また、ＣＰＵ４１は、簡約化条件式保持制御プロセス６０を実行することで、図８に示す簡約化条件保持制御部３５として動作する。また、ＣＰＵ４１は、簡約化条件出力プロセス６２を実行することで、図８に示す簡約化条件出力部３６として動作する。これにより、条件式簡約化プログラム５０を実行したコンピュータ４０が、条件式簡約化装置２０として機能することになる。なお、プログラムを実行するＣＰＵ４１はハードウェアである。
【００８０】
なお、条件式簡約化プログラム５０により実現される機能は、例えば半導体集積回路、より詳しくはApplication Specific Integrated Circuit（ＡＳＩＣ）等で実現することも可能である。
【００８１】
次に、本実施形態に係る条件式簡約化装置２０の作用について説明する。まず、図１０のフローチャートを参照して、条件式簡約化処理について説明する。
【００８２】
ステップＳ１００で、等式条件取得部３１が、対象条件式に基づいて、等式条件のリストを取得する。
【００８３】
ステップＳ１０２で、代入値生成部３２が、等式条件のリストに基づいて、対象条件式に代入するための代入値の組のリストを生成する。
【００８４】
ステップＳ１０４で、代入整理部３３が、代入値の組のリストに含まれる代入値の各々を対象条件式に代入し、自明な部分を除去して条件を整理する。
【００８５】
ステップＳ１０６で、簡約化判定部３４が、代入値の組のリストに含まれる代入値の各々について、整理された対象条件式の簡約化が成功したか否かを判定する。
【００８６】
ステップＳ１０８で、簡約化条件保持制御部３５が、ステップＳ１０８で簡約化が成功と判定された代入値の各々についての、整理後の対象条件式と、代入値の等式条件式の連言とに基づいて、簡約化条件を生成する。
【００８７】
ステップＳ１１０で、簡約化条件出力部３６が、簡約化条件を出力し処理を終了する。
【００８８】
次に、上記ステップＳ１００の等式条件取得部３１の処理の詳細について図１１のフローチャートを参照して説明する。
【００８９】
ステップＳ１０００で、対象条件式をパース（構文解析）して、条件式の木構造を生成する。木構造はノード及びエッジからなる。図１２は対象条件式（(X=1)∨(Y=2)）∧(X!=3)を木構造にした場合の一例である。根本ノードは論理演算子または原子条件式となる。末端ノードは原子条件式となる。図１２では、根本ノードは論理演算子∧である。論理演算子∧に対応する根本ノードを親ノードとして左エッジで接続される子ノードには、論理演算子∧の左辺の論理演算子∨が対応する。また、根本ノードを親ノードとして右エッジで接続される子ノードには、論理演算子∧の右辺の原子条件式X!=3が対応する。また、論理演算子∨に対応するノードを親ノードとして左エッジで接続される子ノードには、論理演算子∨の左辺の原子条件式X=1、右エッジで接続される子ノードには、論理演算子∨の右辺の原子条件式Y=2が対応する。
【００９０】
ステップＳ１００２で、連言で木構造を分割する。分割方法については後述する。
【００９１】
ステップＳ１００４で、分割結果の条件式の木構造をＴｉ(ｉ＝１,...，Ｎ)とする。
【００９２】
ステップＳ１００６で、ｉ←１と代入する。
【００９３】
ステップＳ１００８で、ｉ≦Ｎか否かを判定し、ｉ≦ＮであればステップＳ１０１０へ移行し、ｉ≦ＮでなければステップＳ１０１６へ移行する。
【００９４】
ステップＳ１０１０で、Ｔｉについて等式条件を収集する。収集方法については後述する。
【００９５】
ステップＳ１０１２で、Ｔｉについての等式条件の収集結果を結果セットに追加する。
【００９６】
ステップＳ１０１４で、ｉ←ｉ＋１と代入し、ステップＳ１００８に戻る。
【００９７】
ステップＳ１０１６で、結果セットを出力して、等式条件取得処理を終了する。
【００９８】
次に、上記ステップＳ１００２の連言で木構造を分割する処理の詳細について、図１３のフローチャートを参照して説明する。まず、対象条件式を示す木構造の根本ノードに着目して木構造を分割する処理を実行し、分割された木構造の各々についても、根本ノードに着目して再帰的に木構造を分割する処理を実行して、分割結果の出力リストを出力する。
【００９９】
ステップＳ１１００で、根本ノードが末端ノードか否かを判定し、末端ノードであれば、ステップＳ１１０２へ移行し、末端ノードでなければ、ステップＳ１１０４へ移行する。
【０１００】
ステップＳ１１０２で、末端ノードの原子条件式を結果セットに追加する。
【０１０１】
ステップＳ１１０４で、根本ノードが連言か否かを判定し、連言でなければステップＳ１１０６へ移行し、連言であればステップＳ１１０８へ移行する。
【０１０２】
ステップＳ１１０６で、着目している根本ノードから末端ノードまでの木構造が示す条件式を分割結果の結果セットに追加する。
【０１０３】
ステップＳ１１０８で、着目している根本ノードと子ノードとを接続するエッジを切断することで、連言の左辺に対応する木構造（以下、「左辺の木構造」という）と、右辺に対応する木構造（以下、「右辺の木構造」という）とに分割する。そして、左辺の木構造及び右辺の木構造の各々について、本フローチャートのステップＳ１１００から再帰的に連言で分割することを繰り返す。
【０１０４】
次に、ステップＳ１０１０の等式条件の収集方法の処理の詳細について、図１４のフローチャートを参照して説明する。
【０１０５】
ステップＳ１２００で、根本ノードが末端ノードであるか否かを判定し、末端ノードであれば、ステップＳ１２０２へ移行し、末端ノードでなければステップＳ１２０６へ移行する。
【０１０６】
ステップＳ１２０２で、末端ノードが等式条件式であるか否かを判定し、等式条件式であれば、ステップＳ１２０４へ移行し、等式条件式でなければステップＳ１２２０へ移行する。
【０１０７】
ステップＳ１２０４で、末端ノードの原子条件式を結果セットに追加する。
【０１０８】
ステップＳ１２０６で、選言で木構造を分割する。処理の詳細については後述する。
【０１０９】
ステップＳ１２０８で、分割結果の条件式の木構造をＴｊ(ｊ＝１,...，ｎ)とする。
【０１１０】
ステップＳ１２１０で、ｊ←１と代入する。
【０１１１】
ステップＳ１２１２で、ｊ≦ｎか否かを判定し、ｊ≦ｎであればステップＳ１２１４へ移行し、ｊ≦ｎでなければステップＳ１２２０へ移行する。
【０１１２】
ステップＳ１２１４で、Ｔｊの全ての原子条件式が等式条件式か否かを判定し、等式条件式であればステップＳ１２１６へ移行し、等式条件式でなければステップＳ１２１８へ移行する。
【０１１３】
ステップＳ１２１６で、等式条件式の結果セットに木構造Ｔｊが示す等式条件式を追加する。
【０１１４】
ステップＳ１２１８で、ｊ←ｊ＋１と代入し、ステップＳ１２１２に戻る。
【０１１５】
ステップＳ１２２０で、等式条件式の結果セットを出力し、等式条件の収集方法の処理を終了する。
【０１１６】
次に、上記ステップＳ１２０６の選言で木構造を分割する処理の詳細について、図１５のフローチャートを参照して説明する。まず、分割された木構造の根本ノードに着目して木構造を分割する処理を実行し、分割された木構造の各々についても、根本ノードに着目して再帰的に木構造を分割する処理を実行して、分割結果の出力リストを出力する。
【０１１７】
ステップＳ１３００で、根本ノードが末端ノードか否かを判定し、末端ノードであれば、ステップＳ１３０２へ移行し、末端ノードでなければ、ステップＳ１３０４へ移行する。
【０１１８】
ステップＳ１３０２で、末端ノードの原子条件式を結果セットに追加する。
【０１１９】
ステップＳ１３０４で、根本ノードが選言か否かを判定し、連言でなければステップＳ１３０６へ移行し、連言であればステップＳ１３０８へ移行する。
【０１２０】
ステップＳ１３０６で、着目している根本ノードから末端ノードまでの木構造が示す条件式を分割結果の結果セットに追加する。
【０１２１】
ステップＳ１３０８で、着目している根本ノードと子ノードとを接続するエッジを切断することで、選言の左辺の木構造と、右辺の木構造とに分割する。そして、左辺の木構造及び右辺の木構造の各々について、本フローチャートのステップＳ１３００から再帰的に選言で分割することを繰り返す。
【０１２２】
ここで、等式条件取得部３１の動作例について説明する。図１６は、入力の対象条件式を、(X!=3)∧(((X=1)∧(Y=1))∨(X=2))∧(Y!=2)とした場合の例である。まず、対象条件式をパースして木構造の表現を生成する。次に対象条件式の木構造の根本ノードから開始して、木構造を連言で分割し、選言で分割して得られた等式条件の選言形式からなる選言条件式のセットを生成する。選言条件式のセットから、全ての原子条件式が等式である選言条件式のセットを選択する。以上の処理により出力される等式条件は、((X=1)∧(Y=1))∨(X=2)となる。図１７は、入力の対象条件式を、((X=1)∨(X=2)∨(Y=3))∧(X=1)∧(Y=1)とした場合の例である。出力の等式条件は、{((X=1)∨(X=2)∨(Y=3)),(X=1),(Y=1)}となる。
【０１２３】
次に、上記ステップＳ１０２の代入値生成部３２の処理の詳細について図１８のフローチャートを参照して説明する。
【０１２４】
ステップＳ２０００で、等式条件取得部３１で取得した、全ての原子条件式が等式である選言条件式のセットを受け取り、選言条件式ごとに、Ｅｋ(ｋ＝１,...，Ｇ)とする。
【０１２５】
ステップＳ２００２で、ｋ←１と代入する。
【０１２６】
ステップＳ２００４で、ｋ≦Ｇか否かを判定し、ｋ≦ＧであればステップＳ２００６へ移行し、ｋ≦ＧでなければステップＳ２０１６へ移行する。
【０１２７】
ステップＳ２００６で、選言条件式ＥｋをＤＮＦに変形した条件式をＣｋとする。
【０１２８】
ステップＳ２００８で、選言で条件式Ｃｋの木構造を分割し、連言節を取得する。選言での分割処理は図１５のフローチャートと同様である。
【０１２９】
ステップＳ２０１０で、分割後の連言節の各々について、連言節に含まれる等式条件から代入値を生成して、代入値の組とする。連言節が単独の原子条件式でない場合は、同時設定の代入値とする。
【０１３０】
ステップＳ２０１２で、ステップＳ２０１０で生成した代入値の組を結果セットに追加する。
【０１３１】
ステップＳ２０１４で、ｋ←ｋ＋１と代入し、ステップＳ２００４に戻る。
【０１３２】
ステップＳ２０１６で、結果セットの代入値の組を、連言節に含まれる原子条件式が多い順に並び替えて、代入値の組のリストを生成する。
【０１３３】
ステップＳ２０１８で、結果セットの代入値の組のリストを出力する。
【０１３４】
ここで、代入値生成部３２の動作例について説明する。図１９は、全ての原子条件式が等式である選言条件式のセットを、{(((X=1)∧(Y=1))∨(X=2))}とした場合の例である。選言条件式を選言標準形ＤＮＦに変形し、連言節を取得する。選言標準形の連言節は同時に代入する代入値｛変数=代入値,...｝とする。出力の代入値の組のリストは、[{(X=1,Y=1),(X=2)}]となる。図２０は、全ての原子条件式が等式である選言条件式のセットを、{((X=1)∧(Y=1)∨(X=2)),(X=1),(Y=1)}とした場合の例である。選言条件式のセットに含まれる選言条件式を順に処理する。出力される代入値の組のリストは、[{(X=1,Y=1),(X=2)},{(X=1)},{(Y=1)}]となる。
【０１３５】
次に、上記ステップＳ１０４の代入整理部３３の処理の詳細について図２１のフローチャートを参照して説明する。図２１のフローチャートの処理が、代入値の組のリストに含まれる代入値毎に実行される。
【０１３６】
ステップＳ３０００で、対象条件式の木構造、及び代入値の組のリストに含まれる対象の代入値を受け付ける。
【０１３７】
ステップＳ３００２で、対象条件式の木構造の末端ノードの原子条件式に、対象の代入値に含まれる各等号値を代入する。
【０１３８】
ステップＳ３００４で、代入後の対象条件式の自明部分を除去する。処理の詳細については後述する。
【０１３９】
ステップＳ３００６で、自明部分を除去した整理後の対象条件式を出力する。
【０１４０】
次に上記ステップＳ３００４の代入後の対象条件式の自明部分を除去する処理の詳細について図２２のフローチャートを参照して説明する。なお、対象条件式の木構造の階層の深い末端ノードの親ノードから順に着目ノードに設定して処理していき、全てのノードを処理するまでリターンして処理を繰り返す。
【０１４１】
ステップＳ３１００で、着目ノードが根本ノードか否かを判定する。着目ノードが根本ノードであればステップＳ３１０２へ移行する。着目ノードが末端ノードでなければステップＳ３１１２へ移行する。
【０１４２】
ステップＳ３１０２で、根本ノードの条件式に変数が残っているか否かを判定する。変数が残っている場合には、ステップＳ３１０４で根本ノードの真偽値として不定を返す。根本ノードに変数が残っていない場合には、ステップＳ３１０６で、根本ノードの左辺及び右辺の各ノードの真偽値に基づいて真偽値を算出して、根本ノードの真偽値として返す。なお、根本ノードの真偽値は、対象条件式の真偽値を表す。
【０１４３】
ステップＳ３１１２で、着目ノードが連言か否かを判定する。連言であればステップＳ３１１４へ移行する。連言でなければステップＳ３１２８へ移行する。
【０１４４】
ステップＳ３１１４で、着目ノードの左辺及び右辺の両辺の真偽値が真か否かを判定する。両辺が真であればステップＳ３１１６へ移行する。いずれか一方でも真でなければステップＳ３１１８へ移行する。
【０１４５】
ステップＳ３１１６で、着目ノードの条件式の真偽値を真とする。
【０１４６】
ステップＳ３１１８で、着目ノードの左辺及び右辺の一方が偽か否かを判定する。一方が偽であればステップＳ３１２０へ移行する。両辺が偽であればステップＳ３１２２へ移行する。
【０１４７】
ステップＳ３１２０で、着目ノードの条件式の真偽値を偽とする。
【０１４８】
ステップＳ３１２２で、着目ノードの左辺及び右辺の一方が真かつ他方が不定であるか否かを判定する。一方が真かつ他方が不定であればステップＳ３１２４へ移行する。一方が真かつ他方が不定でなければステップＳ３１２６へ移行する。
【０１４９】
ステップＳ３１２４で、着目ノードの条件式の真偽値として不定を返す。
【０１５０】
ステップＳ３１２６で、着目ノードに対応する条件式をそのまま返す。
【０１５１】
ステップＳ３１２８で、着目ノードの左辺及び右辺の一方が真か否かを判定する。真であればステップＳ３１３０へ移行する。真でなければステップＳ３１３２へ移行する。
【０１５２】
ステップＳ３１３０で、着目ノードの条件式の真偽値を真とする。
【０１５３】
ステップＳ３１３２で、着目ノードの左辺及び右辺の両辺が偽か否かを判定する。両辺が偽であればステップＳ３１３４へ移行する。両辺が偽でなければステップＳ３１３６へ移行する。
【０１５４】
ステップＳ３１３４で、着目ノードの条件式の真偽値を偽とする。
【０１５５】
ステップＳ３１３６で、着目ノードの左辺及び右辺の一方が偽かつ他方が不定か否かを判定する。一方が偽かつ他方が不定であればステップＳ３１３８へ移行する。一方が偽かつ他方が不定でなければステップＳ３１４０へ移行する。
【０１５６】
ステップＳ３１３８で、着目ノードの条件式の真偽値として不定を返す。
【０１５７】
ステップＳ３１４０で、着目ノードの条件式をそのまま返す。
【０１５８】
ステップＳ３１４２で、着目ノードの子ノードについては自明になったものとして除去する。着目ノードの親ノードからみて、階層の深いノードの親ノードを新たな着目ノードとして設定し、右辺及び左辺のノードの条件式について、自明部分を除去することを本フローチャートのステップＳ３１００から再帰的に繰り返す。
【０１５９】
ここで、代入整理部３３の動作例について説明する。図２３は、入力の対象条件式を、(X!=3)∧(((X=1)∧(Y=1))∨(X=2))∧(Y!=2)とし、代入値を(X=1,Y=1)とした場合の例である。まず、対象条件式に代入値を代入する。条件式の木構造で、末端ノードの原子条件式の真偽値を評価する。木構造の末端ノードから、条件式の真偽値を伝播しながら自明な部分を除去していく。以上の処理により出力される整理後の対象条件式の最終的な真偽値は真となる。図２４は、入力の対象条件式を、(X!=3)∧(((X=1)∧(Y=1))∨(X=2))∧(Y!=2)とし、代入値を(X=2)とした場合の例である。出力される整理後の対象条件式の真偽値はY!=2がそのまま残っているため、真偽値として不定が出力される。
【０１６０】
次に、上記ステップＳ１０６の簡約化判定部３４の処理の詳細について図２５のフローチャートを参照して説明する。なお、簡約化の判定は、代入値の組のリストに含まれる代入値の各々について整理した整理後の対象条件式について行う。
【０１６１】
ステップＳ４０００で、対象条件式、及び代入整理部３３で整理された整理後の対象条件式を受け付け、対象条件式をC1とし、整理後の対象条件式をC2とする
【０１６２】
ステップＳ４００２で、整理後の対象条件式C2の最終的な真偽値（根本ノードの真偽値）が真か否かを判定する。真であればステップＳ４０１４へ移行する。真でなければステップＳ４００４へ移行する。
【０１６３】
ステップＳ４００４で、対象条件式C1について連言で木構造を分割する。分割する処理は上記図１３のフローチャートで説明した処理と同様である。
【０１６４】
ステップＳ４００６で、対象条件式C1について分割して得られた分割数をD1とする。
【０１６５】
ステップＳ４００８で、整理後の対象条件式C2について連言で木構造を分割する。分割する処理は上記図１３のフローチャートで説明した処理と同様である。
【０１６６】
ステップＳ４０１０で、整理後の対象条件式C2について分割して得られた分割数をD2とする。
【０１６７】
ステップＳ４０１２で、(D1-D2)が２以上であるか否かを判定する。２以上であればステップＳ４０１４へ移行する。２以上でなければステップＳ４０１６へ移行する。
【０１６８】
ステップＳ４０１４で、整理後の対象条件式C2の簡約化が成功していると判定する。このように整理前後の対象条件式の分割数又は原子条件式の差が２以上の場合に簡約化が成功すると判定できることは、検証によって得られている。
【０１６９】
ステップＳ４０１６で、対象条件式C1の原子条件式の個数をA1とし、整理後の対象条件式C2の原子条件式の個数をA2とする。
【０１７０】
ステップＳ４０１８で、(A1-A2)が２以上であるか否かを判定する。２以上であればステップＳ４０１４へ移行する。２以上でなければステップＳ４０２０へ移行する。
【０１７１】
ステップＳ４０２０で、整理後の対象条件式C2の簡約化が成功していないと判定する。
【０１７２】
ここで、簡約化判定部３４の動作例について説明する。図２６は、簡約化の対象条件式を(X!=3)∧(((X=1)∧(Y=1))∨(X=2))∧(Y!=2)とし、代入整理部３３で代入値(X=1,Y=1)を代入して整理をした整理後の対象条件式について簡約化判定する場合の例である。整理後の対象条件式の最終的な真偽値が真であるので、この場合には簡約化は成功と判定する。
【０１７３】
図２７は、簡約化の対象条件式を(X!=3)∧(((X=1)∧(Y=1))∨(X=2))∧(Y!=2)とし、代入整理部３３で代入値(X=2)を代入して整理をした整理後の対象条件式について簡約化判定する場合の例である。整理後の対象条件式は(Y!=2)となっており最終的な真偽値は真ではないため、真偽値では簡約化は成功と判定されない。次に分割数をみると、D1=3、D2=1となりD1-D2=2と差が２以上であるので、この場合には簡約化は成功と判定する。
【０１７４】
図２８は、簡約化の対象条件式を(X=1)∧(((X!=1)∧(Y!=2))∨(Y=1))とし、代入整理部３３で代入値(X=1)を代入して整理をした整理後の対象条件式について簡約化判定する場合の例である。整理後の対象条件式は(Y=1)となっており最終的な真偽値は真ではないため、真偽値では簡約化は成功と判定されない。次に分割数をみると、D1=2、D2=1となりD1-D2=1と差が２以上ないので簡約化は成功と判定されない。次に原子条件式の個数をみると、A1=3、A2=1となりA1-A2=2と差が２以上であるので、この場合には簡約化は成功と判定する。
【０１７５】
図２９は、簡約化の対象条件式を(X=1)∧(Y=1)∧(Z=1)とし、代入整理部３３で代入値(X=1)を代入して整理をした整理後の対象条件式について簡約化判定する場合の例である。整理後の対象条件式は(Y=1)∧(Z=1)となっており最終的な真偽値は真ではないため、真偽値では簡約化は成功と判定されない。次に分割数をみると、D1=3、D2=2となりD1-D2=1と差が２以上ないので簡約化は成功と判定されない。次に原子条件式の個数をみると、A1=3、A2=2となりA1-A2=1と差が２以上でないので、この場合には簡約化は成功と判定されない。
【０１７６】
次に、上記ステップＳ１０８の簡約化条件保持制御部３５の処理の詳細について図３０のフローチャートを参照して説明する。
【０１７７】
ステップＳ５０００で、簡約化の対象条件式をＣと定める。
【０１７８】
ステップＳ５００２で、対象条件式Ｃについて代入値生成部３２で生成した代入値の組のリストＳを取得する。
【０１７９】
ステップＳ５００４で、代入値の組のリストが出力として得られたか否かを判定する。得られた場合にはステップＳ５００６へ移行する。得られなかった場合には、簡約化できないものとして処理を終了する。
【０１８０】
ステップＳ５００６で、代入値の組のリストに基づいて、代入値の組のリストに含まれる代入値の各々を代入した場合の代入整理部３３の出力、及び簡約化判定部３４の出力を呼び出して、対象条件式を簡約化し、簡約化条件を生成する。処理の詳細については後述する。
【０１８１】
次に、上記ステップＳ５００６の簡約化条件を生成する処理の詳細について図３１のフローチャートを参照して説明する。ここでは対象条件式をＣｉｎ、代入値の組のリストをＳとする。
【０１８２】
ステップＳ５１００で、代入値の組のリストＳのサイズ（代入値の組の数）について、Ｓのサイズ＞０であるか否かを判定する。Ｓのサイズ＞０である場合にはステップＳ５１０２へ移行する。Ｓのサイズ＞０でない場合にはリターンする。
【０１８３】
ステップＳ５１０２で、代入値の組のリストＳから代入値の組を取り出し、代入値の組に含まれる代入値をＤｉ(i＝１,...,Ｎ)とする。
【０１８４】
ステップＳ５１０４で、ｉ←１と代入し、結果条件式Ｃｏｕｔ←ｎｕｌｌと代入する。
【０１８５】
ステップＳ５１０６で、ｉ≦Ｎか否かを判定する。ｉ≦ＮであればステップＳ５１０８へ移行する。ｉ≦ＮでなければステップＳ５１３０へ移行する。
【０１８６】
ステップＳ５１０８で、代入整理部３３から、対象条件式Ｃｉｎに代入値Ｄｉを代入して整理した結果である整理後の対象条件式Ｃｓｉｍｐを取得する。
【０１８７】
ステップＳ５１１０で、簡約化判定部３４から、整理後の対象条件式Ｃｓｉｍｐの簡約化が成功したか否かの判定結果を取得する。
【０１８８】
ステップＳ５１１２で、ステップＳ５１１０で取得した判定結果が成功か否かを判定する。成功であればステップＳ５１１４へ移行し、成功でなければステップＳ５１２８へ移行する。
【０１８９】
ステップＳ５１１４で、Ｃｔｍｐ←ｎｕｌｌと代入する。
【０１９０】
ステップＳ５１１６で、整理後の対象条件式Ｃｓｉｍｐの最終的な真偽値がＦＡＬＳＥ（偽）でないか否かを判定する。真偽値がＦＡＬＳＥでなければステップＳ５１１８へ移行し、ＦＡＬＳＥであればステップＳ５１２０へ移行する。
【０１９１】
ステップＳ５１１８で、Ｃｔｍｐ←Ｃｓｉｍｐの真偽値∧Ｄｉの等式条件を代入する。
【０１９２】
ステップＳ５１２０で、Ｃｔｍｐ＝ｎｕｌｌか否かを判定する。Ｃｔｍｐ＝ｎｕｌｌであればステップＳ５１２８へ移行する。Ｃｔｍｐ＝ｎｕｌｌでなければステップＳ５１２２へ移行する。
【０１９３】
ステップＳ５１２２で、Ｃｏｕｔ＝ｎｕｌｌか否かを判定する。Ｃｏｕｔ＝ｎｕｌｌであればステップＳ５１２４へ移行する。Ｃｏｕｔ＝ｎｕｌｌでなければステップＳ５１２６へ移行する。
【０１９４】
ステップＳ５１２４で、Ｃｏｕｔ←Ｃｔｍｐと代入する。
【０１９５】
ステップＳ５１２６で、Ｃｏｕｔ←Ｃｏｕｔ∨Ｃｔｍｐと代入する。
【０１９６】
ステップＳ５１２８で、ｉ←ｉ＋１と代入し、ステップＳ５１０６に戻る。
【０１９７】
ステップＳ５１３０で、Ｃｏｕｔ＝ｎｕｌｌか否かを判定する。Ｃｏｕｔ＝ｎｕｌｌであればステップＳ５１３２へ移行する。Ｃｏｕｔ＝ｎｕｌｌでなければステップＳ５１４０へ移行する。
【０１９８】
ステップＳ５１３２で、代入値の組のリストＳのサイズについて、Ｓのサイズ＞０であるか否かを判定する。Ｓのサイズ＞０である場合にはステップＳ５１３４へ移行する。Ｓのサイズ＞０でない場合にはステップＳ５１３８へ移行する。
【０１９９】
ステップＳ５１３４で、簡約化条件を生成する(Ｃｉｎ,Ｓ)を呼び出して本処理ルーチンを繰り返す。
【０２００】
ステップＳ５１３６で、Ｃｏｕｔに、上記ステップＳ５１３４で生成された簡約化条件を代入する。
【０２０１】
ステップＳ５１３８で、Ｃｏｕｔ←Ｃｉｎと代入する。
【０２０２】
ステップＳ５１４０で、代入値の組のリストＳのサイズ＞０であるか否かを判定する。Ｓのサイズ＞０である場合にはステップＳ５１４２へ移行する。Ｓのサイズ＞０でない場合にはリターンする。
【０２０３】
ステップＳ５１４２で、簡約化条件を生成する(Ｃｏｕｔ,Ｓ)を呼び出して本処理ルーチンを繰り返す。
【０２０４】
ステップＳ５１４４で、Ｃｏｕｔに、上記ステップＳ５１４２で生成された簡約化条件と代入する。
【０２０５】
ここで、簡約化条件保持制御部３５の動作例について説明する。図３２は、簡約化の対象条件式を(X!=3)∧(((X=1)∧(Y=1))∨(X=2))∧(Y!=2)とした場合の例である。代入値の組のリストは[{(X=1,Y=1),(X=2)}]が生成される。代入値の各々について代入整理した結果を呼び出し、整理後の対象条件式として、真、及び(Y!=2)という結果が各々得られる。簡約化判定結果を呼び出し、代入値のいずれも成功という結果が得られる。代入値の各々について、整理後の対象条件式と等式条件と連言でつないだ条件式を作成する。代入値の各々について作成した条件式を選言でつなぎ出力とする。
【０２０６】
次に上記図７のパス条件３を簡約化する場合について、上記図３０及び図３１のフローチャートに沿って説明する。
【０２０７】
ステップＳ５０００では、簡約化の対象条件式Ｃとして以下を設定する。
【０２０８】
Ｃ←(((区分値='A1')OR(区分値='A2')OR(区分値='A3')OR(区分値='A4')OR(区分値='A5'))AND((区分値NOT='A3')AND(区分値NOT='A4')AND(区分値NOT='A5'))AND(区分値='A1'))
【０２０９】
ステップＳ５００２では、以下の代入値の組のリストＳを取得する。
【０２１０】
Ｓ=[{(区分値='A1‘)},{(区分値='A1'),(区分値='A2'),(区分値='A3'),(区分値='A4‘),(区分値='A5')}]
【０２１１】
ステップＳ５００４では、代入値の組のリストがあるため、ステップＳ５００６において代入して簡約化する(Ｃ,Ｓ)を呼び出す。続いてステップＳ５００６の詳細について説明する。
【０２１２】
ステップＳ５１００は、Ｓのサイズ＝２でありＹｅｓであるからステップＳ５１０２へ移行する。ステップＳ５１０２では、代入値の組のリストＳから１つ代入値の組{(区分値='A1')}を取り出す。代入値の組に含まれる代入値が１つであるためＮ＝１である。取り出し後のＳはＳ=[{(区分値='A1'),(区分値='A2'),(区分値='A3'),(区分値='A4'),(区分値='A5')}]となる。
【０２１３】
ステップＳ５１０４〜Ｓ５１０８に進み{(区分値='A1')}を代入整理すると、Ｃｓｉｍｐ←真と代入できる。
【０２１４】
ステップＳ５１１０〜Ｓ５１１２では、簡約化判定で、簡約化が成功と判定される。
【０２１５】
ステップＳ５１１４〜Ｓ５１１８では、整理後の条件式Ｃｓｉｍｐと等式条件(区分値 = 'A1')の連言により、Ｃｔｍｐ←真∧(区分値='A1')=(区分値='A1')と代入できる。
【０２１６】
ステップＳ５１２０〜Ｓ５１２４では、Ｃｏｕｔ←(区分値='A1')と代入され、ステップＳ５１２８でｉ←１＋１＝２となり、ステップＳ５１０８に戻る。
【０２１７】
ステップＳ５１３０に進み、Ｃｏｕｔ＝ｎｕｌｌはＮｏのためステップＳ５１４０へ移行する。
【０２１８】
ステップＳ５１４２では、Ｓのサイズ＝１であるため、ＹｅｓでありステップＳ５１４４へ移行し、代入して簡約化する(Ｃｏｕｔ，Ｓ)を呼び出して、再帰的に代入して簡約化する処理を行う。
【０２１９】
ステップＳ５１００〜Ｓ５１０２では、代入値の組のリストＳから１つ代入値の組{(区分値='A1'),(区分値='A2'),(区分値='A3'),(区分値='A4'),(区分値='A5')}を取り出し、Ｓ＝[]、Ｎ＝５とする。
【０２２０】
ステップＳ５１０４〜Ｓ５１０８では、{(区分値='A1')}を代入整理すると、Ｃｓｉｍｐ←真と代入できる。
【０２２１】
ステップＳ５１１０〜Ｓ５１１２では簡約化が失敗であるためＮｏとなり、ステップＳ５１０６〜Ｓ５１１２で失敗が４回繰り返され、ステップＳ５１３０へ移行する。
【０２２２】
ステップＳ５１３０では、Ｎｏとなり、ステップＳ５１４０へ移行する。Ｓ＝０であるためＮｏとなって、リターンし、Ｃｏｕｔ=(区分値='A1')が出力として返される。
【０２２３】
図３３に示すように、パス条件３の簡約化後の条件式は、(区分値='A1')となる。
【０２２４】
以上説明したように、本実施形態に係る条件式簡約化装置によれば、条件式の等号値を利用して生成した代入値の組を条件式に代入し、代入された条件式を整理し、整理した条件式において簡約化が成功した場合に、簡約化条件を生成する。これにより、条件式を簡約化する際に長大化することを抑制できる。
【０２２５】
また、上記では、開示の技術に係る制御プログラムの一例である条件式簡約化プログラム５０が記憶部４３に予め記憶（インストール）されている態様を説明したが、これに限定されない。開示の技術に係る制御プログラムは、ＣＤ−ＲＯＭ、ＤＶＤ−ＲＯＭ、ＵＳＢメモリ等の記憶媒体に記憶された形態で提供することも可能である。
【０２２６】
以上の実施形態に関し、更に以下の付記を開示する。
【０２２７】
（付記１）
連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得する等式条件抽出部と、
前記選言形式の条件式のリストに基づいて、前記選言形式の条件に含まれる各変数の代入値を取得し、前記代入値のリストを生成する代入値生成部と、
前記代入値生成部により生成された前記代入値のリストに基づいて、前記代入値毎に、前記代入値を前記対象条件式に代入することにより、前記対象条件式を整理する代入整理部と、
前記代入値毎に、前記代入値を代入して整理された前記対象条件式と、整理前の前記対象条件式とに基づいて、前記整理された前記対象条件式について、前記対象条件式の簡約化が成功したか否かを判定する簡約化判定部と、
前記代入値の各々について、前記対象条件式で簡約化が成功したと判定された場合に、前記整理された前記対象条件式と前記代入値を表す等式条件式との連言の条件式を作成し、前記代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成して出力する簡約化条件出力部と、
を有することを特徴とする条件式簡約化装置。
【０２２８】
（付記２）
前記代入整理部は、前記対象条件式を表す木構造において前記代入値を代入し、末端ノードから順番に各ノードに対応する条件式の真偽値を評価することにより、前記対象条件式を整理することを特徴とする付記１に記載の条件式簡約化装置。
【０２２９】
（付記３）
前記簡約化判定部は、整理前の前記対象条件式と前記代入値を代入して整理された前記対象条件式とのそれぞれを連言で分割し、前記整理前の前記対象条件式の分割数と、前記整理された前記対象条件式の分割数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする付記１又は付記２に記載の条件式簡約化装置。
【０２３０】
（付記４）
整理前の前記対象条件式に含まれる原子条件式の数と前記代入値を代入して整理された前記対象条件式に含まれる原子条件式の数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする付記３に記載の条件式簡約化装置。
【０２３１】
（付記５）
前記代入値生成部は、前記選言形式の条件式のリストのうち、含まれる原子条件式が多い前記選言形式の条件から順に、代入値を取得する付記１〜４の何れかに記載の条件式簡約化装置。
【０２３２】
（付記６）
連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得しと、
前記選言形式の条件式のリストに基づいて、前記選言形式の条件に含まれる各変数の代入値を取得し、前記代入値のリストを生成しと、
前記生成された前記代入値のリストに基づいて、前記代入値毎に、前記代入値を前記対象条件式に代入することにより、前記対象条件式を整理しと、
前記代入値毎に、前記代入値を代入して整理された前記対象条件式と、整理前の前記対象条件式とに基づいて、前記整理された前記対象条件式について、前記対象条件式の簡約化が成功したか否かを判定しと、
前記代入値の各々について、前記対象条件式で簡約化が成功したと判定された場合に、前記整理された前記対象条件式と前記代入値を表す等式条件式との連言の条件式を作成し、前記代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成して出力することを特徴とするプログラム。
【０２３３】
（付記７）
前記対象条件式を表す木構造において前記代入値を代入し、末端ノードから順番に各ノードに対応する条件式の真偽値を評価することにより、前記対象条件式を整理することを特徴とする付記６に記載のプログラム。
【０２３４】
（付記８）
整理前の前記対象条件式と前記代入値を代入して整理された前記対象条件式とのそれぞれを連言で分割し、前記整理前の前記対象条件式の分割数と、前記整理された前記対象条件式の分割数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする付記６又は付記７に記載のプログラム。
【０２３５】
（付記９）
整理前の前記対象条件式に含まれる原子条件式の数と前記代入値を代入して整理された前記対象条件式に含まれる原子条件式の数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする付記８に記載のプログラム。
【０２３６】
（付記１０）
前記選言形式の条件式のリストのうち、含まれる原子条件式が多い前記選言形式の条件から順に、代入値を取得する付記６〜９の何れかに記載のプログラム。
【０２３７】
（付記１１）
連言形式の対象条件式に基づいて、原子条件式を等式条件とする選言形式の条件式のリストを取得しと、
前記選言形式の条件式のリストに基づいて、前記選言形式の条件に含まれる各変数の代入値を取得し、前記代入値のリストを生成しと、
前記生成された前記代入値のリストに基づいて、前記代入値毎に、前記代入値を前記対象条件式に代入することにより、前記対象条件式を整理しと、
前記代入値毎に、前記代入値を代入して整理された前記対象条件式と、整理前の前記対象条件式とに基づいて、前記整理された前記対象条件式について、前記対象条件式の簡約化が成功したか否かを判定しと、
前記代入値の各々について、前記対象条件式で簡約化が成功したと判定された場合に、前記整理された前記対象条件式と前記代入値を表す等式条件式との連言の条件式を作成し、前記代入値の各々について作成した条件式の連言の条件式を、簡約化条件として生成して出力することを特徴とする条件式簡約化方法。
【０２３８】
（付記１２）
前記対象条件式を表す木構造において前記代入値を代入し、末端ノードから順番に各ノードに対応する条件式の真偽値を評価することにより、前記対象条件式を整理することを特徴とする付記１１に記載の条件式簡約化方法。
【０２３９】
（付記１３）
整理前の前記対象条件式と前記代入値を代入して整理された前記対象条件式とのそれぞれを連言で分割し、前記整理前の前記対象条件式の分割数と、前記整理された前記対象条件式の分割数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする付記１１又は付記１２に条件式簡約化方法。
【０２４０】
（付記１４）
整理前の前記対象条件式に含まれる原子条件式の数と前記代入値を代入して整理された前記対象条件式に含まれる原子条件式の数との差が２以上であるか否かに基づいて、前記成功したか否かを判定することを特徴とする付記１３に記載の条件式簡約化方法。
【０２４１】
（付記１５）
前記選言形式の条件式のリストのうち、含まれる原子条件式が多い前記選言形式の条件から順に、代入値を取得する付記１１〜１４の何れかに記載の条件式簡約化方法。
【符号の説明】
【０２４２】
２０   条件式簡約化装置
３１   等式条件取得部
３２   代入値生成部
３３   代入整理部
３４   簡約化判定部
３５   簡約化条件保持制御部
３６   簡約化条件出力部
４０   コンピュータ
４１   ＣＰＵ
４２   メモリ
４３   記憶部
４９   記憶媒体
５０   条件式簡約化プログラム
【図１】
2019021138.tif 000003
【図２】
2019021138.tif 000004
【図３】
2019021138.tif 000005
【図４】
2019021138.tif 000006
【図５】
2019021138.tif 000007
【図６】
2019021138.tif 000008
【図７】
2019021138.tif 000009
【図８】
2019021138.tif 000010
【図９】
2019021138.tif 000011
【図１０】
2019021138.tif 000012
【図１１】
2019021138.tif 000013
【図１２】
2019021138.tif 000014
【図１３】
2019021138.tif 000015
【図１４】
2019021138.tif 000016
【図１５】
2019021138.tif 000017
【図１６】
2019021138.tif 000018
【図１７】
2019021138.tif 000019
【図１８】
2019021138.tif 000020
【図１９】
2019021138.tif 000021
【図２０】
2019021138.tif 000022
【図２１】
2019021138.tif 000023
【図２２】
2019021138.tif 000024
【図２３】
2019021138.tif 000025
【図２４】
2019021138.tif 000026
【図２５】
2019021138.tif 000027
【図２６】
2019021138.tif 000028
【図２７】
2019021138.tif 000029
【図２８】
2019021138.tif 000030
【図２９】
2019021138.tif 000031
【図３０】
2019021138.tif 000032
【図３１】
2019021138.tif 000033
【図３２】
2019021138.tif 000034
【図３３】
2019021138.tif 000035