(57)【要約】【課題】処理実行判定の判定条件の簡約化を高速に行う情報処理プログラム、情報処理装置及び情報処理方法を提供する。【解決手段】入力に対して所定の処理を実行するか否かを判定条件を用いて判定するプログラムを基に生成された、選言で接続される複数の条件群から未選択の条件群を１つ選択し、選択した条件群において連言で接続される変数を含む要素条件を抽出し、既に実行した判定結果を基に、抽出した要素条件の全てを充足可能か否か判定することを特徴とする。【選択図】図４０
2018205969.tif 000002
【特許請求の範囲】
【請求項１】
入力に対して所定の処理を実行するか否かを判定条件を用いて判定するプログラムを基に生成された、選言で接続される複数の条件群から未選択の条件群を１つ選択し、選択した条件群において連言で接続される変数を含む要素条件を抽出し、
既に実行した充足可能性の判定結果を基に、抽出した前記要素条件の全てを充足可能か否か判定する
処理をコンピュータに実行させることを特徴とする情報処理プログラム。
【請求項２】
前記判定の処理は、選択した条件群に含まれる前記要素条件をグループ化し、前記グループ毎に前記要素条件が充足可能か否かを判定し、且つ前記グループにおいて既に前記要素条件が充足可能か否かの判定が実行されている場合、既存の判定結果を用いて判定を行い、全てのグループにおいて前記要素条件の充足が可能な場合に選択した条件群が充足可能と判定することを特徴とする請求項１に記載の情報処理プログラム。
【請求項３】
各前記要素条件に含まれる変数毎に前記要素条件をグループ化することを特徴とする請求項２に記載の情報処理プログラム。
【請求項４】
前記プログラムに対するシンボリック実行の結果を加法標準形に展開して中間データを生成することを特徴とする請求項１〜３のいずれか一つに記載の情報処理プログラム。
【請求項５】
入力に対して所定の処理を実行するか否かを判定条件を用いて判定するプログラムを基に生成された、選言で接続される複数の条件群から未選択の条件群を１つ選択する条件群選択部と、
前記条件群選択部により選択された前記条件群において連言で接続される変数を含む要素条件を抽出する要素条件抽出部と、
前記要素条件抽出部により抽出された前記要素条件の全てが充足可能か否かを、既に実行した充足可能性の判定結果を基に判定する充足可能性判定部と
を備えたことを特徴とする情報処理装置。
【請求項６】
サーバが、
入力に対して所定の処理を実行するか否かを判定条件を用いて判定するプログラムを基に生成された、選言で接続される複数の条件群から未選択の条件群を１つ選択し、選択した条件群において連言で接続される変数を含む要素条件を抽出し、
既に実行した充足可能性の判定結果を基に、抽出した前記要素条件の全てを充足可能か否か判定する
ことを特徴とする情報処理方法。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、情報処理プログラム、情報処理装置及び情報処理方法に関する。
【背景技術】
【０００２】
「ある実行条件Ａを満たせば業務処理Ｂを実施する。」という形でアプリケーション上のビジネスルールを管理し、実行するＢＲＭＳ（Business  Rule  Management  System）が普及してきている。ＢＲＭＳを導入する場合、既存システムのＢＲＭＳへの移行が行われる。
【０００３】
既存システムをＢＲＭＳへ移行するためには、既存システムが有する既存プログラムからのビジネスルールの抽出を行うことになるが、このビジネスルールの抽出を人手で行うことは困難である。そのため、既存プログラムからビジネスルールを自動的に抽出することが望まれる。
【０００４】
従来、シンボリック実行を用いて、既存プログラムのソースコードから業務処理を実行するか否かを判定するための条件（パス条件）を自動抽出する技術がある。シンボリック実行とは、入力変数にシンボル値を設定してプログラムの実行をエミュレートする技術である。シンボリック実行の実行結果は、実行可能なパス、パス条件およびパス出力である。これらの実行結果は、例えば、入力に関する条件とその条件が満たされた場合の出力の表であるロジック表として得ることができる。
【０００５】
ただし、シンボリック実行を用いて自動抽出したパス条件は非常に長い文字列となる場合があり、目視での検証は困難である。例えば、既存プログラムのあるソースコードから抽出される業務処理を実行するためのパス条件は、それぞれが複数の比較式で構成される分岐条件を１５個連ねたものとなる場合がある。このように分岐条件が１５個もあるプログラムを人の手によって解釈することは困難である。
【０００６】
そこで、自動抽出したパス条件を簡約化することが望まれる。このように、既存のプログラムから抽出した条件を簡約化することは、ＢＲＭＳへの移行時だけでなくシステムの移行時にも、実行されることが多い。
【０００７】
既存のプログラムから抽出した条件を簡約化する技術としては、例えば、入力された条件を加法標準形へ展開し、それぞれの連言型について充足可能か否か判定し、充足不要な条件を除去する従来技術がある。また、解析対象のモジュールの分割を行い、生成されるパス条件そのものを減らし、充足可能性判定の負荷を減らす従来技術がある。
【先行技術文献】
【特許文献】
【０００８】
【特許文献１】特開２０１４−１８６４７７号公報
【発明の概要】
【発明が解決しようとする課題】
【０００９】
しかしながら、複雑なパス条件を加法標準形へ展開した場合、膨大な数の連言形の論理式が生成される可能性がある。このように膨大な数の論理式が生成された場合、簡約化のため充足不要な論理式を除去するために従来の方法で各論理式の充足可能性の判定を行うと、充足可能性の判定処理を生成された論理式の数以上行うことになるおそれがある。また、解析対象のモジュールの分割を行い生成されるパス条件そのものを減らす従来技術は、ビジネスルールを対象とする場合のようにパス条件そのものが入力として与えられる場合には適用することができない。
【００１０】
開示の技術は、上記に鑑みてなされたものであって、処理実行判定の判定条件の簡約化を高速に行う情報処理プログラム、情報処理装置及び情報処理方法を提供することを目的とする。
【課題を解決するための手段】
【００１１】
本願の開示する情報処理プログラム、情報処理装置及び情報処理方法は、一つの態様において、以下の処理を実行する。入力に対して所定の処理を実行するか否かを判定条件を用いて判定するプログラムを基に生成された、選言で接続される複数の条件群から未選択の条件群を１つ選択し、選択した条件群において連言で接続される変数を含む要素条件を抽出する。また、既に実行した充足可能性の判定結果を基に、抽出した前記要素条件の全てを充足可能か否か判定する。
【発明の効果】
【００１２】
本願の開示する情報処理プログラム、情報処理装置及び情報処理方法の一つの態様によれば、入力に対する処理実行判定の判定条件の簡約化を高速に行うことができるという効果を奏する。
【図面の簡単な説明】
【００１３】
【図１】図１は、実施例１に係る条件簡約化装置のブロック図である。
【図２】図２は、プログラム簡約化処理の概要を説明するための図である。
【図３】図３は、シンボリック実行装置によるシンボリック実行の概要を説明するための図である。
【図４】図４は、ＤＮＦ展開を説明するための図である。
【図５】図５は、連言節と識別子との対応を表すテーブルの作成を説明するための図である。
【図６】図６は、連言節判定結果リストの作成を説明するための図である。
【図７】図７は、１回目の要素条件の抽出を説明するための図である。
【図８】図８は、１回目のグループの作成を説明するための図である。
【図９】図９は、１回目の各グループの充足可能性判定を説明するための図である。
【図１０】図１０は、１回目の連言節判定結果リストへの登録を説明するための図である。
【図１１】図１１は、１回目のグループ判定結果リストへの登録を説明するための図である。
【図１２】図１２は、２回目の要素条件の抽出を説明するための図である。
【図１３】図１３は、２回目のグループの作成を説明するための図である。
【図１４】図１４は、グループ５１に対する充足可能性判定の処理を説明するための図である。
【図１５】図１５は、グループ５２に対する充足可能性判定の処理を説明するための図である。
【図１６】図１６は、グループ５３に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。
【図１７】図１７は、グループ５３に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。
【図１８】図１８は、グループ５４に対する充足可能性判定の処理を説明するための図である。
【図１９】図１９は、グループ５５に対する充足可能性判定の処理を説明するための図である。
【図２０】図２０は、グループ５６に対する充足可能性判定の処理を説明するための図である。
【図２１】図２１は、グループ５７に対する充足可能性判定の処理を説明するための図である。
【図２２】図２２は、２回目の連言節判定結果リストへの登録を説明するための図である。
【図２３】図２３は、２回目のグループ判定結果リストへの登録を説明するための図である。
【図２４】図２４は、３５７４回目の要素条件の抽出を説明するための図である。
【図２５】図２５は、３５７４回目のグループの作成を説明するための図である。
【図２６】図２６は、グループ７１に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。
【図２７】図２７は、グループ７１に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。
【図２８】図２８は、グループ７２に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。
【図２９】図２９は、グループ７２に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。
【図３０】図３０は、グループ７３に対する充足可能性判定の処理を説明するための図である。
【図３１】図３１は、グループ７４に対する充足可能性判定の処理を説明するための図である。
【図３２】図３２は、グループ７５に対する充足可能性判定の処理を説明するための図である。
【図３３】図３３は、グループ７６に対する充足可能性判定の処理を説明するための図である。
【図３４】図３４は、グループ７７に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。
【図３５】図３５は、グループ７７に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。
【図３６】図３６は、３５７４回目の連言節判定結果リストへの登録を説明するための図である。
【図３７】図３７は、充足可能な連言節の抽出を説明するための図である。
【図３８】図３８は、簡約化条件生成部による要素条件の抽出を説明するための図である。
【図３９】図３９は、簡約化連言節の生成を説明するための図である。
【図４０】図４０は、実施例１に係る条件簡約化装置による簡約化条件の生成処理のフローチャートである。
【図４１】図４１は、実施例１に係る条件簡約化装置による要素条件の充足可能性判定の処理のフローチャートである。
【図４２】図４２は、加法標準形に展開された状態の中間データを表す図である。
【図４３】図４３は、グループを用いた１回目の充足可能性判定処理を表す図である。
【図４４】図４４は、グループを用いた２回目の充足可能性判定処理を表す図である。
【図４５】図４５は、グループを用いた充足可能性判定処理完了後の状態を表す図である。
【図４６】図４６は、実施例２に係る条件簡約化装置のブロック図である。
【図４７】図４７は、実施例２に係る条件簡約化装置による簡約化条件の生成処理のフローチャートである。
【図４８】図４８は、実施例２に係る条件簡約化装置による要素条件の充足可能性判定の処理のフローチャートである。
【図４９】図４９は、情報処理プログラムを実行するコンピュータの一例を示す図である。
【発明を実施するための形態】
【００１４】
以下に、本願の開示する情報処理プログラム、情報処理装置及び情報処理方法の実施例を図面に基づいて詳細に説明する。なお、以下の実施例により本願の開示する情報処理プログラム、情報処理装置及び情報処理方法が限定されるものではない。
【実施例１】
【００１５】
図１は、実施例１に係る条件簡約化装置のブロック図である。図１の条件簡約化装置１が、情報処理装置の一例にあたる。条件簡約化装置１は、シンボリック実行装置３と接続される。また、入力端末２は、シンボリック実行装置３と接続される。
【００１６】
シンボリック実行装置３は、解析を行うプログラムの入力を入力端末２から受ける。さらに、シンボリック実行装置３は、シンボリック実行に用いる入力データ項目群の入力を入力端末２から受ける。
【００１７】
まず、図２を参照して、本実施例におけるプログラムの簡約化処理の概要を説明する。図２は、プログラム簡約化処理の概要を説明するための図である。ここでは、解析を行うプログラム１００は、少なくとも加工処理Ａ及び業務処理Ｂを実行するプログラムである。そして、プログラム１００は、例えば、業務処理Ｂ実行パス１０１に示すように、業務処理Ｂを実行するに至るまでに分岐条件＃１〜＃１５という１５個の分岐条件（パス条件）を有する。すなわち、業務処理Ｂ実行パス１０１では、分岐条件＃１〜＃１５の全てを充足する場合に業務処理Ｂが実行される。図２では、分岐条件＃１〜＃１５が充足される場合を「真」とし、充足されない場合を「偽」として表している。
【００１８】
シンボリック実行装置３は、プログラム１００に入力データ項目群を用いてシンボリック実行を実施し、加工処理Ａ及び業務処理Ｂを含む各処理毎に、各処理を実施するに至るまでの分岐条件を連言（ＡＮＤ連結）で接続した形式で抽出する。例えば、シンボリック実行装置３は、業務処理Ｂを実施するに至るまでの分岐条件をパス条件１２０として抽出する。ここで、ＢＲＭＳへの移行の場合、各処理を実施するに至るまでの分岐条件がビジネスルールにあたる。
【００１９】
そして、条件簡約化装置１は、シンボリック実行装置３が抽出した各処理毎の分岐条件を簡約化する。例えば、条件簡約化装置１は、パス条件１２０を簡約化して、簡約化条件２００を生成する。
【００２０】
次に、プログラム簡約化処理における、シンボリック実行装置３の処理の概要及び条件簡約化装置１の処理の詳細を説明する。以下では、各装置で実施される処理の具体的な説明を行う場合、図２に示したプログラム１００、業務処理Ｂ実行パス１０１及びパス条件１２０を用いて説明する。
【００２１】
シンボリック実行装置３は、入力されたプログラムに対して、入力データ項目群を入力としてシンボリック実行を行う。これによりシンボリック実行装置３は、プログラムにおいて実行される処理毎に、処理の実行にいたるまでの各分岐条件を連言で接続した形式で抽出する。
【００２２】
図３は、シンボリック実行装置によるシンボリック実行の概要を説明するための図である。シンボリック実行装置３は、業務処理Ｂ実行パス１０１の分岐条件＃１を論理式１１１として抽出する。また、シンボリック実行装置３は、業務処理Ｂ実行パス１０１の分岐条件＃２を論理式１１２として抽出する。シンボリック実行装置３は、業務処理Ｂ実行パス１０１の分岐条件＃３〜＃１５も同様に、論理式として抽出する。そして、シンボリック実行装置３は、論理式１１１及び１１２を含む分岐条件＃１〜＃１５を表す論理式を連言で接続し、業務処理Ｂ実行パス１０１を表すパス条件１２０を生成する。
【００２３】
ここで、シンボリック実行装置３により生成されたパス条件１２０は、人がそのまま理解することは困難である。また、シンボリック実行装置３により生成されたパス条件１２０は、そのままでは長いため、機械で処理するとしても読み込みに時間がかかってしまう。そこで、業務処理Ｂ実行パス１０１を表すパス条件１２０を簡約化することで、人が理解しやすくすることができ、その条件式を用いて処理を行う場合にも処理時間を短縮することができる。そのため、シンボリック実行装置３が生成したパス条件１２０は、本実施例に係る条件簡約化装置１により簡約化されることが好ましい。パス条件１２０の簡約化を実施するため、シンボリック実行装置３は、生成したパス条件１２０を条件簡約化装置１へ出力する。
【００２４】
図１に戻って説明を続ける。図１に示すように、条件簡約化装置１は、ＤＮＦ（Disjunctive  Normal  Form）展開部１１、統括制御部１２、要素条件抽出部１３、グルーピング部１４、充足可能性判定部１５、グループ判定結果記憶部１６、判定結果記憶部１７及び簡約化条件生成部１８を有する。
【００２５】
ＤＮＦ展開部１１、統括制御部１２、要素条件抽出部１３、グルーピング部１４、充足可能性判定部１５及び簡約化条件生成部１８は、以下のように実現される。例えば、ＣＰＵ（Central  Processing  Unit）やＭＰＵ（Micro  Processing  Unit）等によって、内部の記憶装置に記憶されているプログラムがＲＡＭ（Random  Access  Memory）を作業領域として実行されることにより各部の機能が実現される。また、各部の機能は、例えば、ＡＳＩＣ（Application  Specific  Integrated  Circuit）やＦＰＧＡ（Field  Programmable  Gate  Array）等の集積回路により実現されるようにしてもよい。また、グループ判定結果記憶部１６及び判定結果記憶部１７は、ハードディスクやメモリなどで実現される。
【００２６】
ＤＮＦ展開部１１は、シンボリック実行装置３が生成したパス条件１２０の入力を受ける。そして、ＤＮＦ展開部１１は、入力されたパス条件１２０をＤＮＦ展開して加法標準形で表される中間データを生成する。中間データは、複数の連言節が選言で接続された形式を有する。ここで、「選言」とは、命題と命題とを「または」「あるいは」に相当する論理で結合する形式を有する論理式である。また、「連言」とは、命題と命題とを「そして」「および」に相当する論理で結合する論理式である。また、「連言節」とは、複数の命題がそれぞれ連言で接続された論理式である。さらに、「充足可能性判定」とは、連言及び選言の何れか一方もしくは双方を用いて生成された論理式が、ある入力データが与えられた場合に、成立するか否かを判定する処理を指す。すなわち、ある入力データが与えられた場合に、特定の論理式が成立する場合、その入力データが、その特定の論理式を充足可能であるという。
【００２７】
ここで、ＤＮＦ展開部１１がＤＮＦ展開を行うと、非常に多くの連言節が生成されるおそれがある。この点、ＤＮＦ展開部１１が生成する全ての連言節に対して個別に充足可能性判定を行えば充足可能な連言節の抽出が行えるので、パス条件１２０の簡約化が行える。しかし、連言節の数が非常に多いため簡約化に時間がかかってしまう。そこで、本実施例に係る条件簡約化装置１の各部は、簡約化を高速に行うために、以下の処理を実施する。ＤＮＦ展開部１１は、中間データを統括制御部１２へ出力する。
【００２８】
統括制御部１２は、加法標準形で表される中間データの入力をＤＮＦ展開部１１から受ける。そして、統括制御部１２は、取得した中間データから連言節を抽出し、各連言節に識別子（ＩＤ：Identifier）を与え、連言節と識別子とが登録されたテーブルを生成する。
【００２９】
次に、統括制御部１２は、生成したテーブルに対応させて充足可能性の欄を生成し、連言節判定結果リスト１４０を作成する。連言節判定結果リスト１４０は、各連言節に対する充足可能性の判定結果を登録するためのリストである。統括制御部１２は、作成した連言節判定結果リスト１４０を判定結果記憶部１７へ格納する。
【００３０】
さらに、統括制御部１２は、グループ判定結果記憶部１６に格納されているグループ判定結果リスト１５０を初期化する。グループ判定結果リスト１５０は、後述するようにグループ分けした条件式のグループ毎の充足可能性の判定結果を登録するためのリストである。
【００３１】
次に、統括制御部１２は、連言節判定結果リスト１４０から連言節を１つ選択する。ここで、本実施例では、統括制御部１２は、連言節に割り当てた識別子の小さい順に連言節を選択していくものとする。そして、統括制御部１２は、選択した連言節を要素条件抽出部１３へ出力する。
【００３２】
その後、統括制御部１２は、選択した連言節の判定完了の通知を充足可能性判定部１５から受信する。判定完了の通知を受信すると、統括制御部１２は、次に識別子の値が大きい連言節を選択し、選択した連言節を要素条件抽出部１３へ出力する。
【００３３】
統括制御部１２は、充足可能性判定部１５による充足可能性判定が終了する度に連言節判定結果リスト１４０から順次連言節を選択し、要素条件抽出部１３に選択した連言節を送信することを、連言節判定結果リスト１４０の全ての連言節に対して行うまで繰り返す。連言節判定結果リスト１４０の全ての連言節に対する選択及び送信が完了すると、統括制御部１２は、簡約化条件の生成を簡約化条件生成部１８に指示する。
【００３４】
要素条件抽出部１３は、統括制御部１２から１つずつ連言節の入力を受ける。そして、要素条件抽出部１３は、入力された連言節の中から条件の一番小さいくくりである要素条件を抽出する。要素条件とは、例えば、連言節の中で連言によって接続される変数を含む個々の条件式である。要素条件抽出部１３は、抽出した要素条件をグルーピング部１４へ出力する。
【００３５】
グルーピング部１４は、要素条件抽出部１３により抽出された要素条件、すなわち１つの連言節に含まれる全ての種類の要素条件の入力を要素条件抽出部１３から受ける。そして、グルーピング部１４は、入力された要素条件を予め決められた規則にしたがいグループ分けする。ここで、本実施例では、グルーピング部１４は、各要素条件の中に含まれる変数によってグループ分けを行う。ここで、本実施例では、変数を用いてグループ分けをしているが、グループ分けの規則はこれに限らないしグループ分けを行わなくてもよい。さらに、本実施例では、グルーピング部１４は、同じグループの中に重複する要素条件がある場合、重複する要素条件を削除して重複を無くす。次に、グルーピング部１４は、グループ分けした要素条件を充足可能性判定部１５へ出力する。
【００３６】
グループ判定結果記憶部１６は、充足可能性判定部１５による各グループの充足可能性判定の結果が登録されるグループ判定結果リスト１５０を記憶する。グループ判定結果リスト１５０には、後述するように、グループ毎にそのグループに含まれる要素条件のハッシュ値が充足可能性判定部１５による充足可能性判定の結果に対応させて登録される。
【００３７】
充足可能性判定部１５は、グループ分けされた要素条件の入力をグルーピング部１４から受ける。そして、充足可能性判定部１５は、グループ毎にそのグループに含まれる要素条件に対して予め決められたハッシュ関数を用いてハッシュ値を求めグループのキーとする。ここで、充足可能性判定部１５は、ハッシュ関数として、例えばＭＤ（Message  Digest）５又はＳＨＡ（Secure  Hash  Algorithm）などを用いることができる。ここで、要素条件の順序が変わっても、連言で結ばれる場合同じ条件となる。そのため、要素条件の順序が変わっても同じキーとなることが好ましい。そこで、充足可能性判定部１５は、グループに含まれる要素条件を所定の順番に整列させてからグループのキーを作成する。
【００３８】
そして、充足可能性判定部１５は、算出したハッシュ関数でグループ判定結果リスト１５０を検索し、一致するグループの充足可能性の判定結果が有るか否かを判定する。一致するグループの充足可能性の判定結果が有る場合、充足可能性判定部１５は、グループ判定結果リスト１５０に登録された充足可能性の判定結果を取得する。そして、充足可能性判定部１５は、取得した充足可能性の判定結果を記憶し、次のグループの選択に移る。
【００３９】
これに対して、一致するグループの充足可能性の判定結果がグループ判定結果リスト１５０に無い場合、充足可能性判定部１５は、そのグループに含まれる要素条件を連言で接続し、例えば、ＳＭＴ（Satisfiability  Modulo  Theories）ソルバを用いて充足可能性判定を行う。そして、充足可能性判定部１５は、取得した充足可能性の判定結果を記憶するとともに、グループ判定結果リスト１５０に新たに求めたグループの充足可能性の判定結果をグループのハッシュ値とともに登録する。その後、充足可能性判定部１５は、次のグループの選択に移る。
【００４０】
充足可能性判定部１５は、グルーピング部１４から入力された全てのグループの充足可能性の判定結果を取得するまで、グループを選択し、選択したグループに対してグループ判定結果リスト１５０又はＳＭＴソルバによる充足可能性の判定結果の取得を繰り返す。
【００４１】
充足可能性判定部１５は、グルーピング部１４から入力された全てのグループの充足可能性の判定結果の取得が完了すると、判定結果の中に充足不能なグループが有るか否かを検索する。充足不能なグループが有る場合、充足可能性判定部１５は、それらグループが属する連言節は充足不能であると判定する。これに対して、判定結果の中に充足不能なグループが無い場合、すなわち、全てのグループが充足可能である場合、充足可能性判定部１５は、それらのグループが属する連言節は充足可能であると判定する。そして、充足可能性判定部１５は、判定結果記憶部１７に格納された連言節判定結果リスト１４０に各連言節の充足可能性の判定結果を順次登録する。
【００４２】
簡約化条件生成部１８は、簡約化条件の生成の指示を統括制御部１２から受ける。そして、簡約化条件生成部１８は、連言節判定結果リスト１４０を判定結果記憶部１７から取得する。
【００４３】
次に、簡約化条件生成部１８は、連言節判定結果リスト１４０から充足可能な連言節を抽出する。そして、簡約化条件生成部１８は、抽出した各連言節から要素条件を取り出し、重複する要素条件は１つにまとめて要素条件リストを連言節毎に作成する。
【００４４】
次に、簡約化条件生成部１８は、作成した要素条件リストに含まれる各要素条件を連言で接続し、各連言節に対応する簡約化連言節を生成する。そして、簡約化条件生成部１８は、生成した各簡約化連言節を選言で接続し、簡約化条件２００を生成する。
【００４５】
ここで、具体的な例を用いて中間データのＤＮＦ展開から簡約化条件２００の生成までの処理についてさらに具体的に説明する。以下は、図２及び３で例示したパス条件１２０の簡約化条件２００の生成についてより詳細に説明する。
【００４６】
ＤＮＦ展開部１１は、シンボリック実行装置３が生成したパス条件１２０の入力を受ける。そして、ＤＮＦ展開部１１は、図４に示すように、入力されたパス条件１２０をＤＮＦ展開して加法標準形で表される中間データ１３０を生成する。図４は、ＤＮＦ展開を説明するための図である。中間データ１３０は、図４に示すように、連言節１３１及び１３２を含む複数の連言節が選言で接続された形式を有する。ここで、ＤＮＦ展開部１１は、例えばパス条件１２０に対して１２３２０個の連言節を有する中間データ１３０を生成する。そして、ＤＮＦ展開部１１は、中間データ１３０を統括制御部１２へ出力する。
【００４７】
統括制御部１２は、加法標準形で表される中間データ１３０の入力をＤＮＦ展開部１１から受ける。そして、統括制御部１２は、図５に示すように、取得した中間データ１３０から連言節を抽出し、各連言節に識別子（ＩＤ）を与え、連言節と識別子とが登録されたテーブル１３３を生成する。図５は、連言節と識別子との対応を表すテーブルの作成を説明するための図である。
【００４８】
次に、統括制御部１２は、図６に示すように、テーブル１３３の各連言節に対応させて充足可能性の欄を生成し、連言節判定結果リスト１４０を作成する。図６は、連言節判定結果リストの作成を説明するための図である。統括制御部１２は、作成した連言節判定結果リスト１４０を判定結果記憶部１７へ格納する。
【００４９】
統括制御部１２は、図６に示す連言節判定結果リスト１４０を生成した後、１回目の選択として、連言節判定結果リスト１４０から最もＩＤの小さい連言節１４１を選択する。そして、統括制御部１２は、選択した連言節１４１を要素条件抽出部１３へ出力する。
【００５０】
要素条件抽出部１３は、連言節１４１の入力を統括制御部１２から受ける。そして、要素条件抽出部１３は、図７に示すように、連言節１４１から要素条件を抽出し、抽出した要素条件を並べたデータ４１１を取得する。ここで、図７は、１回目の要素条件の抽出を説明するための図である。そして、要素条件抽出部１３は、連言節１４１に対応するデータ４１１をグルーピング部１４へ出力する。
【００５１】
グルーピング部１４は、データ４１１の入力を要素条件抽出部１３から受ける。そして、グルーピング部１４は、データ４１１の各要素条件に含まれる変数毎に要素条件を分類する。ここで、要素条件の中に複数の変数が含まれる場合、含まれる変数のいずれかを含む要素条件を統合したグループを作成する。たとえば、図８では、要素条件４２は、２つの変数ｖａｒ６及びｖａｒ７を含む。この場合、グルーピング部１４は、ｖａｒ６又はｖａｒ７を含む他の要素条件４１と要素条件４２とを統合して｛ｖａｒ６，ｖａｒ７｝という１つのグループを作成する。図８は、１回目のグループの作成を説明するための図である。このように、グルーピング部１４は、変数毎に要素条件を分類し、グループデータ４１２を作成する。そして、グルーピング部１４は、連言節１４１に対応するグループデータ４１２を充足可能性判定部１５へ出力する。
【００５２】
充足可能性判定部１５は、グループデータ４１２の入力をグルーピング部１４から受ける。そして、充足可能性判定部１５は、グループデータ４１２の各グループに対して、１回目の充足可能性判定を行う。この場合、最初の充足可能性判定であるため、グループ判定結果リスト１５０にはどのグループの充足可能性の判定結果も登録されていない。そこで、この場合、充足可能性判定部１５は、図９に示すように、グループデータ４１２の全てのグループに対して、ＳＭＴソルバを用いて充足可能性判定を行い、各グループに充足可能性の判定結果を対応させたデータ４１３を取得する。ここでは、｛ｖａｒ１｝及び｛ｖａｒ２｝のグループが充足不能である場合で説明する。図９は、１回目の各グループの充足可能性判定を説明するための図である。
【００５３】
次に、充足可能性判定部１５は、データ４１３に示される記憶した充足可能性の判定結果から連言節１４１の充足可能性判定を行う。図１０は、１回目の連言節判定結果リストへの登録を説明するための図である。ここでは、｛ｖａｒ１｝及び｛ｖａｒ２｝のグループが充足不能であるので、充足可能性判定部１５は、連言節１４１は充足不能であると判定する。そして、充足可能性判定部１５は、図１０に示すように、連言節１４１の充足可能性の判定結果として充足不能を判定結果記憶部１７に格納された連言節判定結果リスト１４０に登録する。
【００５４】
さらに、充足可能性判定部１５は、データ４１３の各グループの要素条件のハッシュ値を求める。そして、充足可能性判定部１５は、図１１に示すように、各グループのハッシュ値をキーとして、各キーに対応させて充足可能性の判定結果をグループ判定結果記憶部１６に格納されるグループ判定結果リスト１５０に登録する。図１１は、１回目のグループ判定結果リストへの登録を説明するための図である。
【００５５】
次に、統括制御部１２は、２回目の選択として、連言節判定結果リスト１４０から連言節１４１の次のＩＤを有する連言節１４２を選択する。そして、統括制御部１２は、選択した連言節１４２を要素条件抽出部１３へ出力する。
【００５６】
要素条件抽出部１３は、連言節１４２の入力を統括制御部１２から受ける。そして、要素条件抽出部１３は、図１２に示すように、連言節１４２から要素条件を抽出し、抽出した要素条件を並べたデータ４２１を取得する。ここで、図１２は、２回目の要素条件の抽出を説明するための図である。そして、要素条件抽出部１３は、連言節１４２に対応するデータ４２１をグルーピング部１４へ出力する。
【００５７】
グルーピング部１４は、データ４２１の入力を要素条件抽出部１３から受ける。そして、グルーピング部１４は、図１３に示すように、データ４２１の各要素条件に含まれる変数毎に要素条件を分類し、グループ５１〜５７を有するグループデータ４２２を作成する。そして、グルーピング部１４は、連言節１４２に対応するグループデータ４２２を充足可能性判定部１５へ出力する。図１３は、２回目のグループの作成を説明するための図である。
【００５８】
充足可能性判定部１５は、グループデータ４２２の入力をグルーピング部１４から受ける。そして、充足可能性判定部１５は、グループデータ４２２からグループ５１を選択する。充足可能性判定部１５は、グループ５１の充足可能性判定を行う。図１４は、グループ５１に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５１のキーを求める。そして、充足可能性判定部１５は、図１４に示すように、グループ５１のキーを用いてグループ判定結果リスト１５０を検索する。ここで、図１４では、分かり易いようにグループ判定結果リスト１５０のキーの欄に要素条件を並べて記載しているが実際には、ハッシュ値が格納される。そして、矢印Ｐ１は、充足可能性判定部１５による矢印の向かう先のグループのキーでのグループ判定結果リスト１５０の検索処理を示す。この場合、グループ５１のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ５１の充足可能性の判定結果６１として充足不能を取得する。そして、充足可能性判定部１５は、グループ５１の充足可能性の判定結果６１である充足不能を記憶する。矢印Ｐ２は、充足可能性判定部１５による矢印Ｐ１の検索により取得した充足可能性の判定結果を取得し記憶する処理を示す。以下の説明でも、Ｐ１及びＰ２と同様の矢印は同様の処理を表すものとする。
【００５９】
次に、充足可能性判定部１５は、グループデータ４２２からグループ５２を選択する。そして、充足可能性判定部１５は、グループ５２の充足可能性判定を行う。図１５は、グループ５２に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５２のキーを求める。そして、充足可能性判定部１５は、図１５に示すように、グループ５２のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ５２のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ５２の充足可能性の判定結果６２として充足不能を取得する。そして、充足可能性判定部１５は、グループ５２の充足可能性の判定結果６２である充足不能を記憶する。
【００６０】
次に、充足可能性判定部１５は、グループデータ４２２からグループ５３を選択する。そして、充足可能性判定部１５は、グループ５３の充足可能性判定を行う。図１６は、グループ５３に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５３のキーを求める。そして、充足可能性判定部１５は、図１６に示すように、グループ５３のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ５３のキーがグループ判定結果リスト１５０においてヒットしないので、充足可能性判定部１５は、グループ５３の充足可能性の判定結果６３を未判定とする。
【００６１】
グループ判定結果リスト１５０を用いた場合のグループ５３の充足可能性の判定結果６３が未判定となったため、充足可能性判定部１５は、ＳＭＴソルバを用いた充足可能性判定に移行する。図１７は、グループ５３に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５３の充足可能性の判定結果６３が未判定であるので、グループ判定結果リスト１５０を用いた判定を行った段階では、図１７のデータ４２３を保持する。そして、充足可能性判定部１５は、未判定であるグループ５３に対してＳＭＴソルバを用いて充足可能性判定を行う。本実施例では、充足可能性判定部１５は、グループ５３の充足可能性の判定結果６３として充足可能を取得し、図１７のデータ４２４を保持する。
【００６２】
次に、充足可能性判定部１５は、グループデータ４２２からグループ５４を選択する。そして、充足可能性判定部１５は、グループ５４の充足可能性判定を行う。図１８は、グループ５４に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５４のキーを求める。そして、充足可能性判定部１５は、図１８に示すように、グループ５４のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ５４のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ５４の充足可能性の判定結果６４として充足可能を取得する。そして、充足可能性判定部１５は、グループ５４の充足可能性の判定結果６４である充足可能を記憶する。
【００６３】
次に、充足可能性判定部１５は、グループデータ４２２からグループ５５を選択する。そして、充足可能性判定部１５は、グループ５５の充足可能性判定を行う。図１９は、グループ５５に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５５のキーを求める。そして、充足可能性判定部１５は、図１９に示すように、グループ５５のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ５５のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ５５の充足可能性の判定結果６５として充足可能を取得する。そして、充足可能性判定部１５は、グループ５５の充足可能性の判定結果６５である充足可能を記憶する。
【００６４】
次に、充足可能性判定部１５は、グループデータ４２２からグループ５６を選択する。そして、充足可能性判定部１５は、グループ５７の充足可能性判定を行う。図２０は、グループ５６に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５６のキーを求める。そして、充足可能性判定部１５は、図２０に示すように、グループ５６のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ５６のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ５６の充足可能性の判定結果６６として充足可能を取得する。そして、充足可能性判定部１５は、グループ５６の充足可能性の判定結果６６である充足可能を記憶する。
【００６５】
次に、充足可能性判定部１５は、グループデータ４２２からグループ５７を選択する。そして、充足可能性判定部１５は、グループ５６の充足可能性判定を行う。図２１は、グループ５７に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ５７のキーを求める。そして、充足可能性判定部１５は、図２１に示すように、グループ５７のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ５７のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ５７の充足可能性の判定結果６７として充足可能を取得する。そして、充足可能性判定部１５は、グループ５７の充足可能性の判定結果６７である充足可能を記憶する。これにより、充足可能性判定部１５は、２回目の充足可能性判定である連言節１４２に対応するグループの充足可能性判定を完了する。
【００６６】
次に、充足可能性判定部１５は、記憶したグループ５１〜５７の充足可能性の判定結果６１〜６７から連言節１４２の充足可能性判定を行う。図２２は、２回目の連言節判定結果リストへの登録を説明するための図である。ここでは、｛ｖａｒ１｝及び｛ｖａｒ２｝のグループが充足不能であるので、充足可能性判定部１５は、連言節１４２は充足不能であると判定する。そして、充足可能性判定部１５は、図２２に示すように、連言節１４２の充足可能性の判定結果として充足不能を判定結果記憶部１７に格納される連言節判定結果リスト１４０に登録する。
【００６７】
さらに、充足可能性判定部１５は、連言節１４２において新たに充足可能性の判定結果を取得したグループの充足可能性の判定結果をグループ判定結果リスト１５０に登録する。図２３は、２回目のグループ判定結果リストへの登録を説明するための図である。充足可能性判定部１５は、図２３に示すように、連言節１４２の各グループの充足可能性の判定結果を含むデータ４２５から、新たに求めたグループ５３の充足可能性の判定結果６３を取得する。そして、充足可能性判定部１５は、グループ５３のキーに充足可能性の判定結果を対応させたエントリ１５１をグループ判定結果記憶部１６に格納されるグループ判定結果リスト１５０に登録する。
【００６８】
その後、統括制御部１２は、連言節判定結果リスト１４０から連言節の選択を順次行っていく。また、要素条件抽出部１３は、入力された連言節に対する要素条件の抽出を繰り返す。また、グルーピング部１４は、入力された要素条件のグルーピングを繰り返す。そして、充足可能性判定部１５は、入力されたグループの充足可能性判定及びそれらのグループに対応する連言節の充足可能性判定を繰り返す。
【００６９】
次に、本実施例における３５７４回目の充足可能性判定について説明する。図２４は、３５７４回目の要素条件の抽出を説明するための図である。統括制御部１２は、３５７４回目の選択として、連言節判定結果リスト１４０から連言節１４３を選択する。そして、統括制御部１２は、選択した連言節１４３を要素条件抽出部１３へ出力する。
【００７０】
要素条件抽出部１３は、連言節１４３の入力を統括制御部１２から受ける。そして、要素条件抽出部１３は、図２４に示すように、連言節１４３から要素条件を抽出し、抽出した要素条件を並べたデータ４３１を取得する。そして、要素条件抽出部１３は、連言節１４３に対応するデータ４３１をグルーピング部１４へ出力する。
【００７１】
グルーピング部１４は、データ４３１の入力を要素条件抽出部１３から受ける。そして、グルーピング部１４は、図２５に示すように、データ４３１の各要素条件に含まれる変数毎に要素条件を分類し、グループ７１〜７７を有するグループデータ４３２を作成する。そして、グルーピング部１４は、連言節１４３に対応するグループデータ４３２を充足可能性判定部１５へ出力する。図２５は、３５７４回目のグループの作成を説明するための図である。
【００７２】
充足可能性判定部１５は、グループデータ４３２からグループ７１を選択する。そして、充足可能性判定部１５は、グループ７１の充足可能性判定を行う。図２６は、グループ７１に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７１のキーを求める。そして、充足可能性判定部１５は、図２６に示すように、グループ７１のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７１のキーがグループ判定結果リスト１５０においてヒットしないので、充足可能性判定部１５は、グループ７１の充足可能性の判定結果８１を未判定とする。
【００７３】
グループ判定結果リスト１５０を用いた場合のグループ７１の充足可能性の判定結果８１が未判定となったため、充足可能性判定部１５は、ＳＭＴソルバを用いた充足可能性判定に移行する。図２７は、グループ７１に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７１の充足可能性の判定結果８１が未判定であるので、グループ判定結果リスト１５０を用いた判定を行った段階では、図２７のデータ４３３を保持する。そして、充足可能性判定部１５は、未判定であるグループ７１に対してＳＭＴソルバを用いて充足可能性判定を行う。本実施例では、充足可能性判定部１５は、グループ７１の充足可能性の判定結果８１として充足可能を取得し、図２７のデータ４３４を保持する。
【００７４】
次に、充足可能性判定部１５は、グループデータ４３２からグループ７２を選択する。そして、充足可能性判定部１５は、グループ７２の充足可能性判定を行う。図２８は、グループ７２に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７２のキーを求める。そして、充足可能性判定部１５は、図２８に示すように、グループ７２のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７２のキーがグループ判定結果リスト１５０においてヒットしないので、充足可能性判定部１５は、グループ７２の充足可能性の判定結果８２を未判定とする。
【００７５】
グループ判定結果リスト１５０を用いた場合のグループ７２の充足可能性の判定結果８２が未判定となったため、充足可能性判定部１５は、ＳＭＴソルバを用いた充足可能性判定に移行する。図２９は、グループ７２に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７２の充足可能性の判定結果８２が未判定であるので、グループ判定結果リスト１５０を用いた判定を行った段階では、図２９のデータ４３５を保持する。そして、充足可能性判定部１５は、未判定であるグループ７２に対してＳＭＴソルバを用いて充足可能性判定を行う。本実施例では、充足可能性判定部１５は、グループ７２の充足可能性の判定結果８２として充足可能を取得し、図２９のデータ４３６を保持する。
【００７６】
次に、充足可能性判定部１５は、グループデータ４３２からグループ７３を選択する。そして、充足可能性判定部１５は、グループ７３の充足可能性判定を行う。図３０は、グループ７３に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７３のキーを求める。そして、充足可能性判定部１５は、図３０に示すように、グループ７３のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７３のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ７３の充足可能性の判定結果８３として充足可能を取得する。そして、充足可能性判定部１５は、グループ７３の充足可能性の判定結果８３である充足可能を記憶する。
【００７７】
次に、充足可能性判定部１５は、グループデータ４３２からグループ７４を選択する。そして、充足可能性判定部１５は、グループ７４の充足可能性判定を行う。図３１は、グループ７４に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７４のキーを求める。そして、充足可能性判定部１５は、図３１に示すように、グループ７４のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７４のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ７４の充足可能性の判定結果８４として充足可能を取得する。そして、充足可能性判定部１５は、グループ７４の充足可能性の判定結果８４である充足可能を記憶する。
【００７８】
次に、充足可能性判定部１５は、グループデータ４３２からグループ７５を選択する。そして、充足可能性判定部１５は、グループ７５の充足可能性判定を行う。図３２は、グループ７５に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７５のキーを求める。そして、充足可能性判定部１５は、図３２に示すように、グループ７５のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７５のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ７５の充足可能性の判定結果８５として充足可能を取得する。そして、充足可能性判定部１５は、グループ７５の充足可能性の判定結果８５である充足可能を記憶する。
【００７９】
次に、充足可能性判定部１５は、グループデータ４３２からグループ７６を選択する。そして、充足可能性判定部１５は、グループ７６の充足可能性判定を行う。図３３は、グループ７６に対する充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７６のキーを求める。そして、充足可能性判定部１５は、図３３に示すように、グループ７６のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７６のキーがグループ判定結果リスト１５０においてヒットするので、充足可能性判定部１５は、ヒットしたキーに対応する充足可能性の判定結果を取得する。本実施例では、充足可能性判定部１５は、グループ７６の充足可能性の判定結果８６として充足可能を取得する。そして、充足可能性判定部１５は、グループ７６の充足可能性の判定結果８６である充足可能を記憶する。
【００８０】
充足可能性判定部１５は、グループデータ４３２からグループ７７を選択する。そして、充足可能性判定部１５は、グループ７７の充足可能性判定を行う。図３４は、グループ７７に対するグループ判定結果リストを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７７のキーを求める。そして、充足可能性判定部１５は、図３４に示すように、グループ７７のキーを用いてグループ判定結果リスト１５０を検索する。この場合、グループ７７のキーがグループ判定結果リスト１５０においてヒットしないので、充足可能性判定部１５は、グループ７７の充足可能性の判定結果８７を未判定とする。
【００８１】
グループ判定結果リスト１５０を用いた場合のグループ７７の充足可能性の判定結果８７が未判定となったため、充足可能性判定部１５は、ＳＭＴソルバを用いた充足可能性判定に移行する。図３５は、グループ７７に対するＳＭＴソルバを用いた充足可能性判定の処理を説明するための図である。充足可能性判定部１５は、グループ７７の充足可能性の判定結果８７が未判定であるので、グループ判定結果リスト１５０を用いた判定を行った段階では、図３５のデータ４３７を保持する。そして、充足可能性判定部１５は、未判定であるグループ７７に対してＳＭＴソルバを用いて充足可能性判定を行う。本実施例では、充足可能性判定部１５は、グループ７７の充足可能性の判定結果８７として充足可能を取得し、図３５のデータ４３８を保持する。
【００８２】
次に、充足可能性判定部１５は、記憶したグループ７１〜７７の充足可能性の判定結果８１〜８７から連言節１４３の充足可能性判定を行う。図３６は、３５７４回目の連言節判定結果リストへの登録を説明するための図である。ここでは、グループ７１〜７７の全てが充足可能であるので、充足可能性判定部１５は、連言節１４３は充足可能であると判定する。そして、充足可能性判定部１５は、図３６に示すように、連言節１４３の充足可能性の判定結果として充足可能を判定結果記憶部１７に格納される連言節判定結果リスト１４０に登録する。さらに、充足可能性判定部１５は、グループ７１、７２及び７７の各キーにそれぞれの充足可能性の判定結果を対応させたエントリをグループ判定結果記憶部１６に格納されるグループ判定結果リスト１５０に登録する。
【００８３】
その後、統括制御部１２、要素条件抽出部１３、グルーピング部１４及び充足可能性判定部１５は、連言節判定結果リスト１４０に記載された全ての連言節に対する充足可能性判定処理を繰り返す。本実施例では、連言節１４３以外の連言節は、全て充足可能性の判定結果が充足不能であるものとする。連言節判定結果リスト１４０に記載された全ての連言節の充足可能性判定が完了すると、統括制御部１２は、簡約化条件生成部１８に簡約化条件の作成を指示する。
【００８４】
簡約化条件生成部１８は、図３７に示すように、判定結果記憶部１７に格納された連言節判定結果リスト１４０に登録された連言節の中から充足可能性の判定結果が充足可能である連言節を抽出する。本実施例では、充足可能である連言節は連言節１４３のみであるので、簡約化条件生成部１８は、図３７に示すように、連言節判定結果リスト１４０から連言節１４３のみを抽出する。図３７は、充足可能な連言節の抽出を説明するための図である。
【００８５】
次に、簡約化条件生成部１８は、図３８に示すように、抽出した連言節１４３から要素条件を抽出し、抽出した要素条件の中で重複する要素条件を１つにまとめて要素条件を並べた要素条件リスト４４１を取得する。図３８は、簡約化条件生成部による要素条件の抽出を説明するための図である。
【００８６】
次に、簡約化条件生成部１８は、図３９に示すように、要素条件リスト４４１に含まれる各要素を連言で接続し、連言節１４３に対応する簡約化連言節１６０を生成する。図３９は、簡約化連言節の生成を説明するための図である。
【００８７】
その後、簡約化条件生成部１８は、生成した簡約化連言節を選言で接続して簡約化条件２００を生成する。ただし、本実施例では、簡約化連言節１６０のみが生成されたので、簡約化条件生成部１８は、簡約化連言節１６０をそのまま簡約化条件２００とする。
【００８８】
次に、図４０を参照して、本実施例に係る条件簡約化装置１による簡約化条件の生成の全体的な流れについて説明する。図４０は、実施例１に係る条件簡約化装置による簡約化条件の生成処理のフローチャートである。
【００８９】
ＤＮＦ展開部１１は、シンボリック実行装置３が生成したパス条件の入力を受ける。そして、ＤＮＦ展開部１１は、取得したパス条件をＤＮＦ展開し中間データ１３０を生成する（ステップＳ１）。その後、ＤＮＦ展開部１１は、生成した中間データ１３０を統括制御部１２へ出力する。
【００９０】
統括制御部１２は、加法標準形で表される中間データ１３０の入力をＤＮＦ展開部１１から受ける。次に、統括制御部１２は、取得した中間データ１３０から連言節を抽出し識別子を与える。そして、統括制御部１２は、ＩＤが割り当てられた各連言節の充足可能性の判定結果を登録するための連言節判定結果リスト１４０を生成する（ステップＳ２）。そして、統括制御部１２は、生成した連言節判定結果リスト１４０を判定結果記憶部１７へ格納する。
【００９１】
次に、統括制御部１２は、グループ判定結果記憶部１６に格納されているグループ判定結果リスト１５０を初期化する（ステップＳ３）。
【００９２】
統括制御部１２は、連言節判定結果リスト１４０に登録された連言節の中から未判定の連言節を１つ選択する（ステップＳ４）。そして、統括制御部１２は、選択した連言節を要素条件抽出部１３へ出力する。
【００９３】
要素条件抽出部１３は、連言節の入力を統括制御部１２から受ける。そして、要素条件抽出部１３は、取得した連言節から要素条件を抽出する（ステップＳ５）。この時、要素条件抽出部１３は、重複する連言節を１つにまとめる。その後、要素条件抽出部１３は、抽出した要素条件を、グルーピング部１４へ出力する。
【００９４】
グルーピング部１４は、連言節に含まれる要素条件の入力を要素条件抽出部１３から受ける。そして、グルーピング部１４は、各要素条件に含まれる変数を基準として要素条件を分類してグループを生成する（ステップＳ６）。そして、グルーピング部１４は、グループ化した要素条件を充足可能性判定部１５へ出力する。
【００９５】
次に、充足可能性判定部１５は、グループ化された要素条件の入力をグルーピング部１４から受ける。そして、充足可能性判定部１５は、グループ毎に要素条件の充足可能性判定を行う（ステップＳ７）。
【００９６】
次に、充足可能性判定部１５は、各グループの要素条件の充足可能性の判定結果を基に、連言節の充足可能性判定を行う。そして、充足可能性判定部１５は、連言節の充足可能性の判定結果を判定結果記憶部１７に格納された連言節判定結果リスト１４０に登録する（ステップＳ８）。そして、充足可能性判定部１５は、選択された連言節の充足可能性判定の完了を統括制御部１２に通知する。
【００９７】
統括制御部１２は、充足可能性判定部１５からの充足可能性判定の完了通知を受けて、連言節判定結果リスト１４０に登録された全ての連言節の充足可能性判定が完了したか否かを判定する（ステップＳ９）。充足可能性判定を行っていない連言節が残っている場合（ステップＳ９：否定）、統括制御部１２は、ステップＳ４へ戻る。
【００９８】
これに対して、連言節判定結果リスト１４０に登録された全ての連言節の充足可能性判定が完了した場合（ステップＳ９：肯定）、統括制御部１２は、簡約化条件の生成を簡約化条件生成部１８に指示する。簡約化条件生成部１８は、統括制御部１２からの指示を受けて、連言節判定結果リスト１４０から充足可能な連言節を抽出する（ステップＳ１０）。
【００９９】
次に、簡約化条件生成部１８は、抽出した各連言節から要素条件を抽出し、重複する要素条件を１つにまとめて、要素条件リストを作成する（ステップＳ１１）。
【０１００】
次に、簡約化条件生成部１８は、要素条件リストに含まれる各要素条件を連言で接続し簡約化連言節１６０を生成する（ステップＳ１２）。
【０１０１】
次に、簡約化条件生成部１８は、簡約化連言節１６０を選言で接続し、簡約化条件２００を生成する（ステップＳ１３）。
【０１０２】
次に、図４１を参照して、本実施例に係る条件簡約化装置１による要素条件の充足可能性判定の処理の流れについて説明する。図４１は、実施例１に係る条件簡約化装置による要素条件の充足可能性判定の処理のフローチャートである。図４１に示すフローは、図４０のステップＳ７で実行される処理の一例にあたる。
【０１０３】
充足可能性判定部１５は、要素条件のグループの中から未選択のグループを１つ選択する（ステップＳ２１）。
【０１０４】
次に、充足可能性判定部１５は、グループに含まれる要素条件に対して予め決められたハッシュ関数を用いてハッシュを行い、グループのキーを作成する（ステップＳ２２）。
【０１０５】
次に、充足可能性判定部１５は、作成したキーでグループ判定結果リスト１５０を検索し、グループ判定結果リスト１５０にキーが存在するか否かを判定する（ステップＳ２３）。キーが存在している場合（ステップＳ２３：肯定）、充足可能性判定部１５は、グループ判定結果リスト１５０に登録されている充足可能性を取得し、ステップＳ２８へ進む。
【０１０６】
これに対して、キーが存在していない場合（ステップＳ２３：否定）、充足可能性判定部１５は、ＳＭＴソルバによる充足可能性判定を実行する（ステップＳ２４）。そして、充足可能性判定部１５は、そのグループが充足可能か否かを判定する（ステップＳ２５）。
【０１０７】
充足可能な場合（ステップＳ２５：肯定）、充足可能性判定部１５は、グループの充足可能をグループ判定結果リスト１５０に登録する（ステップＳ２６）。これに対して、充足不能な場合（ステップＳ２５：否定）、充足可能性判定部１５は、グループの充足不能をグループ判定結果リスト１５０に登録する（ステップＳ２７）。ここで、図４１のフローでは、ＳＭＴソルバによる充足可能判定をした場合に、新たにグループ判定結果リスト１５０への登録が行われることを明確にするため、充足可能性判定部１５は、グループの判定毎に登録を行っている。ただし、上述したように、充足可能性判定部１５は、連言節に含まれる全てのグループの充足可能性判定を行った後に、グループ判定結果リスト１５０への登録を行ってもよい。
【０１０８】
そして、充足可能性判定部１５は、グループの充足可能性の判定結果を記憶する（ステップＳ２８）。
【０１０９】
次に、充足可能性判定部１５は、要素条件のグループの中の全てのグループの充足可能性判定を完了したか否かを判定する（ステップＳ２９）。充足可能性判定を行っていないグループが残っている場合（ステップＳ２９：否定）、充足可能性判定部１５は、ステップＳ２１へ戻る。
【０１１０】
これに対して、要素条件のグループの中の全てのグループの充足可能性判定が完了した場合（ステップＳ２９：肯定）、充足可能性判定部１５は、１つの連言節に対応する要素条件の充足可能性判定処理を終了する。
【０１１１】
ここで、図４２〜４５を参照して、条件簡約化装置１による充足可能性判定処理の高速化の効果について説明する。図４２は、加法標準形に展開された状態の中間データを表す図である。図４３は、グループを用いた１回目の充足可能性判定処理を表す図である。図４４は、グループを用いた２回目の充足可能性判定処理を表す図である。図４５は、グループを用いた充足可能性判定処理完了後の状態を表す図である。
【０１１２】
図４２に示すように、ＤＮＦ展開により生成された中間データ１３０は、連言節１３１及び１３２を含む１２３２０種類の連言節を有する。ここで、連言節１３１に対しての充足可能性判定、連言節１３２に対しての充足可能性判定、というように各連言節に対して充足可能性判定を行った場合、１２３２０回の充足可能性判定を行うことになる。
【０１１３】
これに対して、本実施例では、図４３に示すように、連言節１３１をグループ化し充足可能性判定を行う。１回目は未だどのグループに対しても充足可能性の判定結果は出ていないので、充足可能性判定部１５は、各グループに対してＳＭＴソルバを用いた充足可能性判定を行う。
【０１１４】
しかし、２回目の連言節１３２の充足可能性判定においては、図４４に示すように、既にグループ群５０１に含まれるグループに関しては充足可能性判定が行われており、充足可能性判定部１５は、単にその結果を取得するだけである。そして、この場合、グループ５０２に対してのみ、充足可能性判定部１５は、ＳＭＴソルバを用いた充足可能性判定を行う。
【０１１５】
最終的に、図４５に示すように、充足可能性判定部１５は、１６９４種類のグループに対してＳＭＴソルバを用いた充足可能性判定を行うことで、中間データ１３０に含まれる全ての連言節の充足可能性判定を完了する。すなわち、条件簡約化装置１は、要素条件をグループ化し、同じ要素条件の組には既存の充足可能性の判定結果を用いることで、ＳＭＴソルバを用いた判定回数を、連言節毎に別個に充足可能性判定を行う場合に比べて、１６９４／１２３２０に低減することができる。
【０１１６】
以上に説明したように、本実施例に係る条件簡約化装置は、グループ毎の充足可能性の判定結果を記憶しておき、１度判定を行った要素条件の組み合わせのグループに対しては判定結果を再利用する。これにより、本実施例に係る条件簡約化装置は、プログラムにおける処理実行判定の判定条件の簡約化を高速に行うことができる。
【０１１７】
また、本実施例に係る条件簡約化装置は、充足可能性判定の対象となる連言節を、関連する要素条件でグループ化し、グループ毎に充足可能性判定を行う。これにより、充足可能性判定を行う対象のバリエーションを少なくすることができる。特に、連言形へ変形された条件の場合、同じ要素条件の組み合わせが複数回出現する性質があるため、グループ化による高速化の効果が大きくなる。
【実施例２】
【０１１８】
図４６は、実施例２に係る条件簡約化装置のブロック図である。本実施例に係る条件簡約化装置１は、ある連言節におけるグループの充足可能性判定を行う際に、充足不能と判定された場合、その連言節を充足不能と判定し、その後のグループの判定を行わないことが実施例１と異なる。以下では、グループの充足可能性判定及び連言節の充足可能性判定を主に説明する。以下の説明では、実施例１と同じ各部の機能については説明を省略する。
【０１１９】
本実施例に係る充足可能性判定部１５は、連言節の要素条件を登録するための要素条件リストを有する。充足可能性判定部１５は、充足可能性判定の対象とする連言節に含まれるグループの情報をグルーピング部１４から受ける。そして、充足可能性判定部１５は、要素条件リストを初期化し、未だ要素条件が登録されていない状態にする。
【０１２０】
次に、充足可能性判定部１５は、グループを１つ選択する。そして、充足可能性判定部１５は、選択したグループの要素条件に対して予め決められたハッシュ関数を用いてハッシュを行いグループのキーを作成する。さらに、充足可能性判定部１５は、作成したキーを用いてグループ判定結果リスト１５０を検索する。
【０１２１】
作成したキーがグループ判定結果リスト１５０でヒットした場合、充足可能性判定部１５は、グループ判定結果リスト１５０を用いてそのグループが充足可能か否かを判定する。そのグループが充足可能な場合、充足可能性判定部１５は、グループに含まれる要素条件を要素条件リストへ追加する。この場合、充足可能性判定部１５は、重複する要素条件は１つにまとめて登録する。これに対して、そのグループが充足不能の場合、充足可能性判定部１５は、判定対象の連言節を充足不能と判定して、その連言節の充足可能性判定を終了する。
【０１２２】
また、作成したキーがグループ判定結果リスト１５０でヒットしない場合、充足可能性判定部１５は、そのグループに対してＳＭＴソルバによる充足可能性判定を実行する。そして、そのグループが充足可能な場合、充足可能性判定部１５は、グループ判定結果リスト１５０にそのグループの充足可能性である充足不能を登録する。そして、充足可能性判定部１５は、判定対象の連言節を充足不能と判定して、その連言節の充足可能性判定を終了する。
【０１２３】
これに対して、そのグループが充足可能な場合、充足可能性判定部１５は、グループ判定結果リスト１５０にそのグループの充足可能性として充足可能を登録する。さらに、充足可能性判定部１５は、グループに含まれる要素条件を要素条件リストへ追加する。
【０１２４】
グループ判定結果リスト１５０に各グループの充足可能性を登録することにより、充足可能性判定部１５は、同じ要素条件を有するグループに対するＳＭＴソルバによる充足判定を回避することができる。
【０１２５】
さらに、充足可能性判定部１５は、充足可能性判定の対象とする連言節の全てのグループの判定が完了したか否かを判定する。充足可能性の判定が完了していないグループがある場合、充足可能性判定部１５は、次のグループの判定に進む。このように、充足可能性判定部１５は、充足可能性判定の対象とする連言節の全てのグループの判定が完了する、又はグループが充足不能と判定されるまで充足可能性判定を繰り返す。
【０１２６】
充足可能性判定部１５は、連言節の全てのグループが充足可能と判定された場合、その連言節の要素条件リストを判定結果記憶部１７に格納する。さらに、充足可能性判定部１５は、連言節の充足可能を統括制御部１２に通知する。このように、充足可能性判定部１５は、各連言節の充足可能性判定を行い、全てのグループが充足可能とされた連言節毎に要素条件リストを判定結果記憶部１７に格納する。
【０１２７】
簡約化条件生成部１８は、簡約化連言節の作成の指示を統括制御部１２から受ける。次に、簡約化条件生成部１８は、判定結果記憶部１７の中から指定された連言節の要素条件リストを取得する。そして、簡約化条件生成部１８は、取得した要素条件リストに記載された要素条件を連言で接続し簡約化連言節を作成する。その後、簡約化条件生成部１８は、判定結果記憶部１７に格納された簡約化連言節リスト１７０に作成した簡約化連言節を登録する。
【０１２８】
その後、簡約化条件生成部１８は、簡約化条件２００の生成の指示を統括制御部１２から受ける。そして、簡約化条件生成部１８は、簡約化連言節リスト１７０に登録された簡約化連言節を選言で接続し、簡約化条件２００を生成する。
【０１２９】
統括制御部１２は、連言節の充足可能の通知を充足可能性判定部１５から受けると、その連言節に対する簡約化連言節の作成の指示を簡約化条件生成部１８に指示する。また、統括制御部１２は、全ての連言節の充足可能性判定の終了の通知を充足可能性判定部１５から受けると、簡約化条件の生成を簡約化条件生成部１８に指示する。
【０１３０】
次に、図４７を参照して、本実施例に係る条件簡約化装置１による簡約化条件の生成の全体的な流れについて説明する。図４７は、実施例２に係る条件簡約化装置による簡約化条件の生成処理のフローチャートである。
【０１３１】
ＤＮＦ展開部１１は、シンボリック実行装置３が生成したパス条件の入力を受ける。そして、ＤＮＦ展開部１１は、取得したパス条件をＤＮＦ展開し中間データを生成する（ステップＳ１０１）。その後、ＤＮＦ展開部１１は、生成した中間データを統括制御部１２へ出力する。
【０１３２】
統括制御部１２は、加法標準形で表される中間データの入力をＤＮＦ展開部１１から受ける。次に、統括制御部１２は、取得した中間データから連言節を抽出し識別子を与える。さらに、統括制御部１２は、判定結果記憶部１７に格納された簡約化連言節リスト１７０を初期化する（ステップＳ１０２）。
【０１３３】
次に、統括制御部１２は、グループ判定結果記憶部１６に格納されているグループ判定結果リスト１５０を初期化する（ステップＳ１０３）。
【０１３４】
統括制御部１２は、中間データから抽出した連言節の中から未判定の連言節を１つ選択する（ステップＳ１０４）。そして、統括制御部１２は、選択した連言節を要素条件抽出部１３へ出力する。
【０１３５】
要素条件抽出部１３は、連言節の入力を統括制御部１２から受ける。そして、要素条件抽出部１３は、取得した連言節から要素条件を抽出する（ステップＳ１０５）。この時、要素条件抽出部１３は、重複する連言節を１つにまとめる。その後、要素条件抽出部１３は、抽出した要素条件を、グルーピング部１４へ出力する。
【０１３６】
グルーピング部１４は、連言節に含まれる要素条件の入力を要素条件抽出部１３から受ける。そして、グルーピング部１４は、各要素条件に含まれる変数を基準として要素条件を分類してグループを生成する（ステップＳ１０６）。そして、グルーピング部１４は、グループ化した要素条件を充足可能性判定部１５へ出力する。
【０１３７】
次に、充足可能性判定部１５は、グループ化された要素条件の入力をグルーピング部１４から受ける。そして、充足可能性判定部１５は、グループ毎に要素条件リストを作成しながら連言節の充足可能性判定を行う（ステップＳ１０７）。この処理については次に詳細に説明する。
【０１３８】
そして、充足可能性判定部１５は、連言節が充足可能か否かを判定する（ステップＳ１０８）。連言節が充足不能の場合（ステップＳ１０８：否定）、充足可能性判定部１５は、選択された連言節の充足可能性判定の完了を統括制御部１２に通知し、処理はステップＳ１１１へ進む。
【０１３９】
これに対して、連言節が充足可能の場合（ステップＳ１０８：肯定）、充足可能性判定部１５は、連言節の充足可能を統括制御部１２に通知する。その後、簡約化条件生成部１８は、簡約化連言節の作成の指示を統括制御部１２から受けて、指定された連言節に対応する要素条件リストに記載された要素条件を連言で接続し、簡約化連言節を生成する（ステップＳ１０９）。
【０１４０】
次に、簡約化条件生成部１８は、生成した簡約化連言節を簡約化連言節リスト１７０へ追加する（ステップＳ１１０）。充足可能性判定部１５は、選択された連言節の充足可能性判定の完了を統括制御部１２に通知する。
【０１４１】
統括制御部１２は、充足可能性判定部１５からの充足可能性判定の完了通知を受けて、中間データから抽出した全ての連言節の充足可能性判定が完了したか否かを判定する（ステップＳ１１１）。充足可能性判定を行っていない連言節が残っている場合（ステップＳ１１１：否定）、統括制御部１２は、ステップＳ１０４へ戻る。
【０１４２】
これに対して、中間データから抽出した全ての連言節の充足可能性判定が完了した場合（ステップＳ１１１：肯定）、統括制御部１２は、簡約化条件２００の生成を簡約化条件生成部１８に指示する。簡約化条件生成部１８は、判定結果記憶部１７に格納された簡約化連言節リスト１７０に登録された簡約化連言節を取得する。そして、簡約化条件生成部１８は、取得した簡約化連言節を選言で接続し、簡約化条件２００を生成する（ステップＳ１１２）。
【０１４３】
次に、図４８を参照して、本実施例に係る条件簡約化装置１による連言節の充足判定の処理の流れについて説明する。図４８は、実施例２に係る条件簡約化装置による要素条件の充足判定の処理のフローチャートである。図４８に示すフローは、図４７のステップＳ１０７で実行される処理の一例にあたる。
【０１４４】
充足可能性判定部１５は、要素条件リストを初期化する（ステップＳ１２１）。次に、充足可能性判定部１５は、要素条件のグループの中から未選択のグループを１つ選択する（ステップＳ１２２）。
【０１４５】
次に、充足可能性判定部１５は、グループに含まれる要素条件に対して予め決められたハッシュ関数を用いてハッシュを行い、グループのキーを作成する（ステップＳ１２３）。
【０１４６】
次に、充足可能性判定部１５は、作成したキーでグループ判定結果リスト１５０を検索し、グループ判定結果リスト１５０にキーが存在するか否かを判定する（ステップＳ１２４）。キーが存在している場合（ステップＳ１２４：肯定）、充足可能性判定部１５は、グループ判定結果リスト１５０に登録されている充足可能性の判定結果から、そのグループが充足可能か否かを判定する（ステップＳ１２５）。
【０１４７】
そのグループが充足可能な場合（ステップＳ１２５：肯定）、充足可能性判定部１５は、ステップＳ１３０へ進む。これに対して、そのグループが充足不能な場合（ステップＳ１２５：否定）、充足可能性判定部１５は、充足可能性判定の対象とした連言節を充足不能と判定し、連言節の充足可能性判定を終了する。
【０１４８】
これに対して、キーが存在していない場合（ステップＳ１２４：否定）、充足可能性判定部１５は、ＳＭＴソルバによる充足可能性判定を実行する（ステップＳ１２６）。そして、充足可能性判定部１５は、そのグループが充足可能か否かを判定する（ステップＳ１２７）。
【０１４９】
充足不能な場合（ステップＳ１２７：否定）、充足可能性判定部１５は、グループの充足不能をグループ判定結果リスト１５０に登録する（ステップＳ１２８）。そして、充足可能性判定部１５は、充足可能性判定の対象とした連言節を充足不能と判定し、連言節の充足可能性判定を終了する。
【０１５０】
これに対して、充足可能な場合（ステップＳ１２７：肯定）、充足可能性判定部１５は、グループの充足可能をグループ判定結果リスト１５０に登録する（ステップＳ１２９）。
【０１５１】
そして、充足可能性判定部１５は、そのグループに含まれる要素条件を要素条件リストへ登録する（ステップＳ１３０）。
【０１５２】
次に、充足可能性判定部１５は、要素条件のグループの中の全てのグループの充足可能性判定を完了したか否かを判定する（ステップＳ１３１）。充足可能性判定を行っていないグループが残っている場合（ステップＳ１３１：否定）、充足可能性判定部１５は、ステップＳ１２２へ戻る。
【０１５３】
これに対して、要素条件のグループの中の全てのグループの充足可能性判定が完了した場合（ステップＳ１３１：肯定）、充足可能性判定部１５は、充足可能性判定の対象とした連言節を充足可能と判定し、連言節の充足可能性判定を終了する。
【０１５４】
以上に説明したように、本実施例に係る条件簡約化装置は、グループが充足不能な場合に、そのグループが属する連言節を充足不能と判定し、次の連言節の判定に移る。これにより、不要なグループの充足可能性の判定を抑制することができ、より高速に簡約化条件を生成することができる。
【０１５５】
ここで、各実施例で図示した各部の各構成要素は、必ずしも物理的に図示の如く構成されていることを要しない。すなわち、各部の分散・統合の具体的形態は図示のものに限られず、その全部または一部を、各種の負荷や使用状況等に応じて、任意の単位で機能的または物理的に分散・統合して構成することができる。
【０１５６】
さらに、各装置で行われる各種処理機能は、ＣＰＵ（またはＭＰＵ、ＭＣＵ（Micro  Controller  Unit）等のマイクロ・コンピュータ）上で、その全部または任意の一部を実行するようにしてもよい。また、各種処理機能は、ＣＰＵ（またはＭＰＵ、ＭＣＵ等のマイクロ・コンピュータ）で解析実行されるプログラム上、またはワイヤードロジックによるハードウェア上で、その全部または任意の一部を実行するようにしてもよいことは言うまでもない。
【０１５７】
ところで、上記の実施例で説明した各種の処理は、予め用意されたプログラムをコンピュータで実行することで実現できる。そこで、以下では、上記の実施例と同様の機能を有するプログラムを実行するコンピュータの一例を説明する。図４９は、情報処理プログラムを実行するコンピュータの一例を示す図である。
【０１５８】
図４９に示すように、コンピュータ９００は、各種演算処理を実行するＣＰＵ９０１と、データ入力を受け付ける入力装置９０２と、モニタ９０３とを有する。また、コンピュータ９００は、記憶媒体からプログラム等を読み取る媒体読取装置９０４と、各種装置と接続するためのインタフェース装置９０５と、他の情報処理装置等と有線または無線により接続するための通信装置９０６とを有する。また、コンピュータ９００は、各種情報を一時記憶するＲＡＭ９０７と、ハードディスク装置９０８とを有する。また、各装置９０１〜９０８は、バス９０９に接続される。
【０１５９】
ハードディスク装置９０８には、図１及び４６に示したＤＮＦ展開部１１、統括制御部１２、要素条件抽出部１３、グルーピング部１４、充足可能性判定部１５及び簡約化条件生成部１８の各処理部と同様の機能を有する情報処理プログラムが記憶される。また、ハードディスク装置９０８には、グループ判定結果記憶部１６及び判定結果記憶部１７、並びに、情報処理プログラムを実現するための各種データが記憶される。入力装置９０２は、例えば、コンピュータ９００の管理者から操作情報、管理情報等の各種情報の入力を受け付ける。モニタ９０３は、例えば、コンピュータ９００の管理者に対して表示画面、管理情報の画面および各種画面を表示する。媒体読取装置９０４は、例えば、記録媒体に記録された情報を読み取る。インタフェース装置９０５は、例えば印刷装置等が接続される。通信装置９０６は、例えば、図示しないネットワークと接続され、各種装置と各種情報をやりとりする。
【０１６０】
ＣＰＵ９０１は、ハードディスク装置９０８に記憶された各プログラムを読み出して、ＲＡＭ９０７に展開して実行することで、各種の処理を行う。また、これらのプログラムは、コンピュータ９００を図１及び４６に示したＤＮＦ展開部１１、統括制御部１２、要素条件抽出部１３、グルーピング部１４、充足可能性判定部１５及び簡約化条件生成部１８として機能させることができる。
【０１６１】
なお、上記の情報処理プログラムは、必ずしもハードディスク装置９０８に記憶されている必要はない。例えば、コンピュータ９００が読み取り可能な記憶媒体に記憶されたプログラムを、コンピュータ９００が読み出して実行するようにしてもよい。コンピュータ９００が読み取り可能な記憶媒体は、例えば、ＣＤ−ＲＯＭやＤＶＤディスク、ＵＳＢメモリ等の可搬型記録媒体、フラッシュメモリ等の半導体メモリ、ハードディスクドライブ等が対応する。また、公衆回線、インターネット、ＬＡＮ等に接続された装置にこの情報処理プログラムを記憶させておき、コンピュータ９００がこれらから情報処理プログラムを読み出して実行するようにしてもよい。
【０１６２】
さらに、以上の各実施例に係る条件簡約化装置を用いた場合の効果についてまとめて説明する。
【０１６３】
まず、１つの適用方法として例えば以下の方法がある。あるプログラムを改修した場合に、改修前のプログラムから抽出したパス条件と改修後のプログラムから抽出したパス条件とを比較する。そして、改修前後で同じ入力値を与えて出力値が等価でない場合に真となるパス条件を抽出する。そして、そのパス条件に対して各実施例に係る条件簡約化装置を用いて簡約化条件を生成することで、利用者は改修前後でパス条件の挙動がどうして変わるのかを理解することが容易となる。さらに、その後、生成した簡易条件に対してＳＭＴソルバなどの制約ソルバを用いて充足可能性判定を行い、改修後で挙動が変わる入力データを取得することができる。この時に、各実施例に係る条件簡約化装置により生成された簡約化条件を用いることで、制約ソルバを実行する情報処理装置にデータを読み込ます時間を短縮することができる。
【０１６４】
さらに、他の適用方法として例えば以下の方法がある。あるプログラムを改修した場合に、改修前後のプログラムのそれぞれから抽出したパス条件に対して各実施例に係る条件簡約化装置を用いて簡約化条件をそれぞれ生成する。これにより、利用者はパス条件が容易に理解できる形となり、利用者が人手でプログラムを改修する際の手がかりとすることができる。その後、簡約化条件を手掛かりとして改修されたプログラムの改修前後のパス条件を比較し、同じ入力値を与えて出力値が等価でない場合に真となるパス条件を抽出する。その後、生成した簡易条件に対してＳＭＴソルバなどの制約ソルバを用いて充足可能性判定を行い、改修後で挙動が変わる入力データを取得することができる。
【符号の説明】
【０１６５】
１  条件簡約化装置
２  入力端末
３  シンボリック実行装置
１１  ＤＮＦ展開部
１２  統括制御部
１３  要素条件抽出部
１４  グルーピング部
１５  充足可能性判定部
１６  グループ判定結果記憶部
１７  判定結果記憶部
１８  簡約化条件生成部
１００  プログラム
１２０  パス条件
１３０  中間データ
１４０  連言節判定結果リスト
１５０  グループ判定結果リスト
１６０  簡約化連言節
【図１】
2018205969.tif 000003
【図２】
2018205969.tif 000004
【図３】
2018205969.tif 000005
【図４】
2018205969.tif 000006
【図５】
2018205969.tif 000007
【図６】
2018205969.tif 000008
【図７】
2018205969.tif 000009
【図８】
2018205969.tif 000010
【図９】
2018205969.tif 000011
【図１０】
2018205969.tif 000012
【図１１】
2018205969.tif 000013
【図１２】
2018205969.tif 000014
【図１３】
2018205969.tif 000015
【図１４】
2018205969.tif 000016
【図１５】
2018205969.tif 000017
【図１６】
2018205969.tif 000018
【図１７】
2018205969.tif 000019
【図１８】
2018205969.tif 000020
【図１９】
2018205969.tif 000021
【図２０】
2018205969.tif 000022
【図２１】
2018205969.tif 000023
【図２２】
2018205969.tif 000024
【図２３】
2018205969.tif 000025
【図２４】
2018205969.tif 000026
【図２５】
2018205969.tif 000027
【図２６】
2018205969.tif 000028
【図２７】
2018205969.tif 000029
【図２８】
2018205969.tif 000030
【図２９】
2018205969.tif 000031
【図３０】
2018205969.tif 000032
【図３１】
2018205969.tif 000033
【図３２】
2018205969.tif 000034
【図３３】
2018205969.tif 000035
【図３４】
2018205969.tif 000036
【図３５】
2018205969.tif 000037
【図３６】
2018205969.tif 000038
【図３７】
2018205969.tif 000039
【図３８】
2018205969.tif 000040
【図３９】
2018205969.tif 000041
【図４０】
2018205969.tif 000042
【図４１】
2018205969.tif 000043
【図４２】
2018205969.tif 000044
【図４３】
2018205969.tif 000045
【図４４】
2018205969.tif 000046
【図４５】
2018205969.tif 000047
【図４６】
2018205969.tif 000048
【図４７】
2018205969.tif 000049
【図４８】
2018205969.tif 000050
【図４９】
2018205969.tif 000051