JP6572668B2

JP6572668B2 - 検査方法

Info

Publication number: JP6572668B2
Application number: JP2015156088A
Authority: JP
Inventors: 吉田　浩章; 浩章吉田; グエン・クオン; ゴーシュ・インドラディープ
Original assignee: Fujitsu Ltd
Current assignee: Fujitsu Ltd
Priority date: 2014-09-04
Filing date: 2015-08-06
Publication date: 2019-09-11
Anticipated expiration: 2035-08-06
Also published as: US9767412B2; US20160071012A1; JP2016058073A

Description

本開示は一般にドントケア分析を利用するサイズ低減検査に関連する。

充足可能性問題モジュロ理論(Satisfiability modulo theories：SMT)を解くこと及び充足可能性問題(SAT)を解くことは、コンピュータがシステム及び演算に関して抽象的に推論することを可能にする。SMT及びSAT解法は、ソフトウェア検証、記号解析、プログラム検証、自動検査、セキュリティ検査などに使用されてもよい。SAT解法は、命題式が真(TRUE)として評価するような命題式のモデルが存在するか否かを判定することを含む。SMT解法はSAT解法を含み、SAT問題の命題変数が他の数学的理論の式で置換される。

SMT解法及びSAT解法を実行するため、ある種の方法及びシステムはデイビス・パトナム・ロッジマン・ラブランド(Davis-Putnam-Logemann-Loveland：DPLL)アルゴリズムを使用する。DPLLアルゴリズムは、命題論理式のSATを判断するための後戻りベースの探索アルゴリズム(backtracking-based search algorithm)である。SMT解法を実行するためにDPLLアルゴリズムとともにセオリソルバ(theory solver)が使用されてもよい。DPLLアルゴリズムのパフォーマンスを改善する更なる方法及びシステムが発展している。例えば、バックジャンプ、リスタート及び/又は節学習(clause learning)にDPLLが使用されてもよい。

しかしながらSMT及びSAT解法の効率については、特に、極めて大規模な問題を解こうとする場合に大きな障害が存在する。

一実施形態による方法は、
複数のSMT変数を有するSMT式をプログラミングコードから取得する工程と、
複数の簡略化されたSMT変数を含む簡略化されたSMT式を前記SMT式から取得する工程と、
複数のSAT変数を含むSAT式を前記簡略化されたSMT式から取得する工程と、
前記簡略化されたSMT式を利用して、前記複数のSMT変数のうち何れが「ドントケア」変数であるかを判定する工程と、
簡略化されたSAT式を利用して、前記複数のSMT変数のうち何れが「ドントケア」変数であるかを判定する工程と、
を有する方法である。

本願で説明される実施形態により「ドントケア」変数を見出すためのプロセスの具体的なフローチャートを示す図。本願で説明される少なくとも或る実施形態により形成される例示的なコンピュータ環境のブロック図。本願で説明される少なくとも1つの実施形態により一群の「ドントケア」SMT変数を見出すための具体的なプロセス300のフローチャートを示す図。本願で説明される少なくとも1つの実施形態により一群の「ドントケア」SMT変数を見出すための具体的なプロセス300の別のフローチャートを示す図。本願で説明される形態を実現するための機能を実行する例示的なコンピュータシステムを示す図。

＜実施形態の概要＞
プログラミングコードにおける「ドントケア(don’t care)」変数を確認するためのシステム及び方法が開示される。本方法は、複数のSMT変数を有するSMT式をプログラミングコードから取得する工程と、複数の簡略化されたSMT変数を含む簡略化されたSMT式を前記SMT式から取得する工程と、複数のSAT変数を含むSAT式を、簡略化されたSMT式から取得する工程と、前記簡略化されたSMT式により、前記複数のSMT変数のうちの何れが「ドントケア」変数であるかを判断する工程と、前記簡略化されたSAT式により、前記複数のSMT変数のうちの何れが「ドントケア」変数であるかを判断する工程とを有する。

これらの例示的な実施形態は、本開示を減縮も限定もせず、本開示の理解を促すように具体例を提供するように言及される。更なる実施形態は詳細な説明で議論され、そこでは更なる詳細な事項が示される。様々な実施形態のうちの1つ以上によりもたらされる恩恵は、本明細書を検討することにより或いは提示される1つ以上の実施形態を実施することにより更に理解される。

＜図面＞
本開示に関するこれら及び他の特徴、側面及び利点は、添付図面を参照しながら以下の詳細な説明を読むことにより更に理解される。

図1は本願で説明される実施形態により「ドントケア」変数を見出すためのプロセスの具体的なフローチャートである。

図2は本願で説明される少なくとも或る実施形態により形成される例示的なコンピュータ環境のブロック図である。

図3は本願で説明される少なくとも1つの実施形態により一群の「ドントケア」SMT変数を見出すための具体的なプロセス300のフローチャートである。

図4は本願で説明される少なくとも1つの実施形態により一群の「ドントケア」SMT変数を見出すための具体的なプロセス300の別のフローチャートである。

図5は本願で説明される形態を実現するための機能を実行する例示的なコンピュータシステムを示す。

＜実施形態の詳細な説明＞
プログラミングコード内で発見される「ドントケア」変数を確認するためのシステム及び方法が開示される。例えば、検証、トラブルシューティング、最適化、品質保証、記号分析、プログラム検証、自動検査、セキュリティ検査等のような任意の様々な目的のための様々な検査が、コンピュータ又はソフトウェアプログラミングコードについて実行される。多くのプログラミングコードのサイズ及び範囲は、検査される必要がある非常に多数の変数をもたらす。ある状況では、いくつかの変数がそのプログラミングコードにとって冗長的であるかもしれない。例えば、「ドントケア」変数に対する変化は、プログラミングコードの実行経路(execution path)に対する変化を招かない結果となる。これらの変数は「ドントケア」変数と言及される。一群の「ドントケア」変数を確認することにより、様々な検査は「ドントケア」変数を無視してよく、これらの検査の効率が上昇する。本願で説明される或る実施形態のアプリケーションは、「ドントケア」変数を特定することにより変数の数を削減するために使用されてもよい。

図1は本願で説明される実施形態により「ドントケア」変数を見出すためのプロセス100の具体的なフローチャートである。プロセス100の1つ以上のステップは、一実施形態においては、図2のコンピュータ環境200及び/又は図5のコンピュータシステム500のうちの1つ以上のコンポーネントにより実現されてもよい。個別的なブロックとして描かれているが、所望の実現手段に依存して、様々なブロックは、追加的なブロックに分割されてもよいし、より少数のブロックに統合されてもよいし、或いは、省略されてもよい。

ブロック105において、SMT式(SMT formula)がコードから作成される、及び/又は、SMT式は他のシステム、プロセス、方法又はシステムから入力されてもよい。SMT式を作成又は入力するために当該技術分野において既知の任意の技術が使用されてもよい。

ブロック110において、SMT式は簡略化される。SMT式の簡略化(simplification)は、SMT式の何らかの冗長性を減らしてもよいし、新たな変数を作成してもよいし、及び/又は、変数を削除してもよい。以下に説明されるように、SMT式を簡略化するために様々なアルゴリズムが使用可能である。SMT式と簡略化されたSMT式との間でSMT代替マップ(SMT substitution map)が作成される。簡略化されたSMT式は、第1「ドントケア」分析115及び第2「ドントケア」分析125という2つの異なる「ドントケア」分析に入力されてもよい。例えば、第1「ドントケア」分析は図3に示されるプロセス300において説明される。第1「ドントケア」分析は、簡略化されたSMT変数を分析して「ドントケア」変数を判定する。

第2「ドントケア」分析125は図4に示されるプロセス400で更に詳細に説明される。第2「ドントケア」分析はSAT式及び/又はSAT変数を用いて「ドントケア」変数を判定する。ブロック120において、SAT変数を伴うSAT式を作成し及び/又はSAT式を解くために、SATソルバ(SAT solver)が使用されてもよい。第2「ドントケア」分析は、SAT変数のパターンを分析して「ドントケア」変数を判定する。ブロック130において、「ドントケア」変数が出力される。そして、「ドントケア」変数は、プログラミングコード内にエラーが存在するか否かを判断するために、プログラミングコードに関連して使用されることが可能である。

図2は本願で説明される少なくとも或る実施形態により形成される例示的なコンピュータ環境200のブロック図である。図2に示されるように、コンピュータ環境200は演算装置(又はコンピューティングエンティティ)202を含む。演算装置202は、以下において詳細に説明されるように、様々コンピュータハードウェア又はソフトウェアモジュールを含む特殊用途又は汎用のコンピュータを含んでもよい。一例として、演算装置202は、移動電話機、スマートフォン、パーソナルコンピュータ、タブレット、携帯用電子機器、ゲームコンソール及び/又はその他の内蔵システムであってもよい。図5に示されるコンピュータシステムは演算装置202の他の例である。

演算装置202は、中央処理ユニット(CPU)204と、単一命令多重データ(single instruction multiple data：SIMD)マシン206とを含んでよい。SIMDマシン206は、並列的に複数のデータ群について同一又は類似する処理を実行する複数の処理用を含む。例えば、SIMDマシン206は、演算装置202に結合される又はその一部であるディスプレイに対する出力の画像の構築を高速化するために演算装置202において使用されるグラフィックス処理ユニット(GPU)であってもよい。これら及び他の実施形態において、SIMDマシン206は、負担の重いグラフィックス処理が必要とされない場合には、しばしば、主にアイドルのままであってもよい。

SIMDマシン206は複数のグリッド208を含んでもよい。各々のグリッドは複数のブロック210を含んでもよい。各々のブロック210は複数のスレッド212を含んでもよい。ブロック210のグリッド208は、アルゴリズムを実行する演算装置202のカーネル(図示せず)及び/又はその他の何らかの部分により指図(又は命令又は指示)される。所与のブロック210のスレッド212は、データ群の様々な部分について同一又は類似するアルゴリズムを同時に実行してもよい。スレッド212の複数のブロックは同時に動作してもよい。一般に、あるブロック210内のスレッド212は、共用メモリ214を介して、同じブロック214内の他のスレッドと協働(又は協調又は協同)してもよい。共用メモリ214は、SIMDマシン206の処理要素とともにオンチップで配置されてもよい。一実施形態において、異なるブロック210内のスレッド212がグローバルメモリ218を介して協働(又は協調又は協同)してもよい。グローバルメモリ218はチップ外に(オフチップで)配置されてもよいし及び/又はSIMDマシン206に配置されてもよい。例えば、グローバルメモリ218は、オフチップで配置され、SIMDマシン206のダイナミックランダムアクセスメモリ(DRAM)(図示せず)に配置されてもよい。一実施形態において、CPU204はグローバルメモリ218にアクセスしてもよい。

一実施形態において、演算装置202のカーネル又は他の部分は、SIMDマシン206に、SAT及び/又はSMT検査のための式及び命令を提供してもよい。式のうちの様々な部分には、SIMDマシン206のうちの様々なスレッド212が割り当てられる(割り振られる又は指定される)。そして、SIMDマシン206は、SAT及び/又はSMT検査を実行するために、式の一部に割り当てられたスレッド212を実行する。

本願で説明される実施形態は、媒体に保存されるコンピュータ実行可能な命令又はデータ構造を担う又は有するコンピュータ読み取り可能な媒体を利用して実現されてもよい。そのようなコンピュータ読み取り可能な媒体は演算装置202によりアクセスされる利用可能な任意の媒体であってよい。限定ではない一例として、そのようなコンピュータ読み取り可能な媒体は有形のコンピュータ読み取り可能な記憶媒体を含み、記憶媒体は、ランダムアクセスメモリ(RAM)、リードオンリメモリ(ROM)、電気的に消去可能でプログラム可能なリードオンリメモリ(EEPROM)、コンパクトディスクリードオンリメモリ(CD-ROM)又はその他の光学的ディスクストレージ、磁気ディスクストレージ又はその他の磁気ストレージ装置を含み、或いは、コンピュータ実行可能な命令又はデータ構造の形式で所望のプログラムコードを担う又は保存するために使用され及び演算装置202によりアクセスされる他の任意の記憶媒体を含む。上記に列挙したものの組み合わせもコンピュータ読み取り可能な媒体の範囲に含まれてよい。

コンピュータ実行可能な命令は、例えば、演算装置202(CPU204、SIMDマシン206又は他の処理装置を含む)に、所定の機能又は一群の機能を実行させる命令及びデータを含んでよい。

本願で説明されるシステム及び方法は、ソフトウェア、ハードウェア、又は、ソフトウェア及びハードウェアの組み合わせで実現されもよい。本説明において、演算装置202は、ここで規定されるような何らかのコンピュータシステムであってもよいし、或いは、コンピュータシステムで動作する何らかのモジュール又はモジュールの組み合わせであってもよい。

図3は本願で説明される少なくとも1つの実施形態により一群の「ドントケア」SMT変数を見出すための具体的なプロセス300のフローチャートである。プロセス300の1つ以上のステップは、一実施形態においては、図2のコンピュータ環境200及び/又は図5のコンピュータシステム500のうちの1つ以上のコンポーネントにより実現されてもよい。個別的なブロックとして描かれているが、所望の実現手段に依存して、様々なブロックは、追加的なブロックに分割されてもよいし、より少数のブロックに統合されてもよいし、或いは、省略されてもよい。

プロセス300はブロック305から始まり、SMT式がプログラミングコードから作成される。プログラミングコードは、例えば、C、C++、パイソン(Python)、ベーシック(BASIC)、フォートラン(FORTRAN)等のような任意のタイプのプログラミング言語を含んでよい。プログラミング言語の実行経路の全てを進行し、プログラミング言語のうちの何れか又は全てが、解を有する制約を表現するか否かを判断することにより、SMT式は作成されてもよい。SMT式は任意のSMTソルバを利用して作成されてもよく、例えば、Ario、Barcelogic、CVC、CVC Lite、CVC3、ExtSAT、Harvey、HTP、ICS(SRI)、Jat、MathSAT、Sateen、Simplify、AProVE、STep、STP、SVC、TSAT、UCLID、Yices(SRI)、Zap(Microsoft)、Z3(Microsoft)等が利用されてもよい。

ブロック310において、SMT式は、簡略化されたSMT式を作成するために簡略化される。SMT式は、例えば、リニアソルバ及び/又はアレイリード/ライト削除などのような当該技術分野で既知の任意の技術を利用して簡略化されてもよい。簡略化されたSMT式は、SMT式の中で以前には見られない新たな変数を導入してもよいし、及び/又は、SMT式に見られる変数を削除してもよい。簡略化されたSMT式の中の新たな変数とSMT式の中の変数とを対応付けるSMT代替マップが作成されてもよい。

ブロック315において、一群のSMT変数がSMT式から取得されてもよい。この一群のSMT変数は、SMT式における変数の全体集合又は変数の部分集合を含んでもよい。

ブロック320において、一群のSMT変数の中からSMT変数が選択される。ブロック325において、SMT変数は簡略化されたSMT式の中に見出されずかつSMT代替マップ内にも見出されない、と判断される場合には、プロセス300はブロック330に移る。ブロック330において、そのSMT変数は、SMT変数の「ドントケア」群(又は「ドントケア」セット)に追加される。そのSMT変数は、簡略化されたSMT式において使用されない、或いは、簡略化されたSMT式の中の新たな変数にSMT代替マップによって対応付けられないので、その変数は不要である。ブロック330の後、プロセス300はブロック335に進む。

ブロック325において、SMT変数が、簡略化されたSMT式の中に見出されると判断される場合及びSMT代替マップにおいて見出されると判断される場合には、プロセス300はブロック335に進む。ブロック320において、一群のSMT変数の中から何らかのSMT変数が未だ選択されていない場合、プロセス300はブロック320に戻り、別のSMT変数が一群のSMT変数の中から選択される。一群のSMT変数のうちの全てのSMT変数がブロック320で選択されている場合には、プロセス300はブロック340に進み、SMT変数の「ドントケア」群が出力される。その後、「ドントケア」変数は、プログラミングコードにおけるエラーの有無を判断するために、プログラミングコードに関連して使用されることが可能である。

図4は本願で説明される少なくとも1つの実施形態により一群の「ドントケア」SMT変数を見出すための具体的なプロセス400の別のフローチャートである。プロセス400の1つ以上のステップは、一実施形態においては、図2のコンピュータ環境200及び/又は図5のコンピュータシステム500のうちの1つ以上のコンポーネントにより実現されてもよい。個別的なブロックとして描かれているが、所望の実現手段に依存して、様々なブロックは、追加的なブロックに分割されてもよいし、より少数のブロックに統合されてもよいし、或いは、省略されてもよい。

プロセス400はブロック405から始まり、簡略化されたSMT式が取得される。簡略化されたSMT式は、例えば、図3のブロック305や310及び関連する記述で説明したようにして取得されてもよい。SMT式を簡略化するために任意の数のアルゴリズム及び/又は技術が使用されてもよい。代替的に、SMT式は簡略化されなくてもよく、プロセス400の残りの部分は簡略化されていないSMT式について実行されてもよい。

ブロック410において、SAT式が、簡略化されたSMT式から作成されてもよい。SAT式は、例えば、簡略化されたSMT式をビットブラスト(bitblasting)することにより作成されてもよい。結果のSAT式はSMT変数をブール変数(Boolean variable)に変換してもよい。例えば、32ビットSMT変数は1ビットのSAT変数32個に変換されてもよい。更に、簡略化されたSMT式における様々な関数及び/又は処理は、SAT式における論理関数に変換されてもよい。

SAT式は任意のソルバを用いて作成されもよく、例えば、bitblaster、ACL2アルゴリズム、BoolSAT、minisat-in-your-browser、SATRennesPA、MniSAT、Lingeling、PicoSAT、Sat4j、DPLL、Glucose、RSat、UBCSAT、CryptoMiniSat、Spear、HyperSAT、BASolver、ArgoSAT、FastSATソルバ、zChaff、BCSAT、WinSAT等が利用されてもよい。

ブロック415において、簡略化されたSMT式における各々の変数をSAT式における1つ以上の変数に対応付けるSAT-SMT変数マップが作成される。ブロック420において、ソリューショントレイル(solution trail)(例えば、真理値表)を作成するために、SAT式が解かれる。これは、例えば、DPLLアルゴリズム、DPLLベースのアルゴリズム又は類似するアルゴリズムのような何らかの後戻りアルゴリズムを利用して実行されてもよい。ソリューショントレイルは、例えば、各々のSAT変数に関連するブール値の順序リスト(ordered list)を返してもよい。

プロセス400の残りのブロックは、SAT変数のソリューションセットのうちの何れのSAT変数が「ドントケア」変数であるかを判定するために使用される。これは、例えば、「ドントケア」変数であるSAT変数の順序付けられたソリューションセットの中で第1の(又は始めの)「ドントケア」変数を見出し、残りのSAT変数を「ドントケア」変数として指定又はラベル付けすることにより、実行されてもよい。例えば、第1の(又は最後の)「ドントケア」変数が見出されるまで、SAT変数のソリューションセットの始めから(又は最後から)反復的に処理を行うこと等により、第1の「ドントケア」値を決定する任意の技術が使用されてもよい。

ブロック425において、何らかの反復値が設定される。例えば、「start」がSAT変数のソリューショントレイルの第1の値に対応する値に設定され(start=0)、「end」がSAT変数のソリューショントレイルの長さに等しい値に設定される(end=len(trail))。

ブロック430において、「mid」が、SAT変数のソリューショントレイルの「start」変数及び「end」の間の中間の変数に設定される(mid=(end-start)/2)。一実施形態において、「mid」は、大きい方又は小さい方の最も近い整数に丸められてもよい。

ブロック435において、SAT変数のソリューショントレイルを利用してSAT式が充足たされるか否かが判定される。例えば、全ての制約が充足たされる場合に、SAT式は充足たされると判断されてもよい。

ブロック435においてSAT式が充足たされる場合、ブロック440において「end」は「mid」に設定され、プロセス400はブロック450に進む。ブロック435においてSAT式が充足たされない場合、「mid」から「end」までの変数は解の値にリセットされ、ブロック445において「start」は「mid」に設定される。

ブロック450において、「start」及び「end」の間の差分が1以下である場合(end-start≦1)、プロセス400はブロック455に移る。そうでない場合、プロセス400はブロック430に移る。プロセス400は、ブロック450に示されるエグジット条件(ループを抜け出る条件)が満たされるまで、任意の回数だけ反復されてもよい。

ブロック455において、SMT-SATソリューションマップを用いて、未定のSAT変数から、「ドントケア」SMT変数が推定される。例えば、SATソリューションマップにおける未定のSAT変数に関連するSMT変数は、「ドントケア」SMT変数と考えられてもよい。ブロック460において、「ドントケア」SMT変数が出力される。「ドントケア」変数は、以後、プログラムコードにおけるエラーの有無を確認するためにプログラムコードに関連して使用されることが可能である。

特定の具体例として、SAT変数のソリューションセットが次のように書けたとする：
ｐｃｎｆ１４１０
２ −７ −８ −９ −３０
−２３０
−２７０
−２９０
−２８０
３５ −６０
−３ −５０
−３６０
１４０
２０
この特定の具体例において、以下は、DPLLアルゴリズムから作成された具体的なSATソリューションである：
２：真
１４：真
３：真
７：真
９：真
８：真
５：偽
６：真
１：真
４：真
１０：真
１１：真
１２：真
１３：真
ソリューションマップは順序リストである。この例では、ブロック425及びブロック430の開始の際に、start=0, end=14, 及び mid=7 である。SATソリューションマップにおけるmid及びendの間のSAT変数のソリューショントレイルのSAT変数は、次のように、未定(undefined)に設定される。

２：真
１４：真
３：真
７：真
９：真
８：真
５：偽
６：未定
１：未定
４：未定
１０：未定
１１：未定
１２：未定
１３：未定
この特定の具体例において、SAT変数のソリューションセットは、SAT変数のソリューションセットによっては充足されない。例えば、SAT変数のソリューションセットは変数6を必要とするが、この変数はSAT変数のソリューションセットにおいては未定として掲げられている。従って、ブロック435において、プロセス400はブロック445に移り、startはmidに等しくなるように設定される(start=7)。プロセス400はブロック450に進み、プロセス400はブロック430に進み、その理由は、end-start=15-7=7は1より大きいからである。ブロック430において、mid=(14+7)/2=10が設定され、SATソリューションマップにおけるmid及びendの間のSAT変数のソリューショントレイルのSAT変数は、次のように、未定に設定される。

２：真
１４：真
３：真
７：真
９：真
８：真
５：偽
６：真
１：真
４：真
１０：未定
１１：未定
１２：未定
１３：未定
この例の場合、ブロック435において、SAT式は充足される。例えば、SAT式において、未定の項は使用されない。しかしながら、第1のSAT変数の位置はそれでも未知である。プロセス400はブロック440に進み、end=mid=10に設定される。次に、プロセス400はブロック450に進み、プロセスは終了すべきか否かが判定される。この場合、end-start=10-7=3は1より大きい。従って、プロセス400はブロック430に続く。ブロック430において、mid=(end+start)/2=(10+7)/2=8が設定される。SATソリューションマップにおけるmid及びendの間のSAT変数のソリューショントレイルのSAT変数は、次のように、未定に設定される。

２：真
１４：真
３：真
７：真
９：真
８：真
５：偽
６：真
１：未定
４：未定
１０：未定
１１：未定
１２：未定
１３：未定
ブロック435において、SAT式において未定の項は必要とされていないので、SAT式は充足される、と判断されるべきである。そして、プロセス400はブロック445に移り、startはmidに等しくなるように設定される(start=8)。そして、プロセス400はブロック450に進み、プロセスは終了すべきか否かが判断される。この場合、end-start=10-8=2は1より大きい。従って、プロセス400はブロック430に続く。ブロック430において、mid=(end+start)/2=(10+8)/2=9が設定される。SATソリューションマップにおけるmid及びendの間のSAT変数のソリューショントレイルのSAT変数は、次のように、未定に設定される。

２：真
１４：真
３：真
７：真
９：真
８：真
５：偽
６：真
１：真
４：未定
１０：未定
１１：真
１２：真
１３：真
ブロック435において、SAT式において未定の項は必要とされていないので、SAT式は充足される、と判断される。プロセス400はブロック445に移り、startはmidに等しくなるように設定される(start=9)。そして、プロセス400はブロック450に進み、プロセスは終了すべきか否かが判断される。この場合、end-start=10-9=1は1に等しいので、プロセス400はブロック455に移る。

ブロック455において、変数のリストのうちのmidないしendにおけるSATソリューションマップにリストされるSAT変数が、特定される。この特定の例では、これらの変数は、変数4、10、11、12、13を含む。ステップ460において、SAT-SMT変数マップを利用して、SAT変数に関連するSMT変数が特定され出力される。そして、プログラミングコードにおいてエラーが存在するか否かを確認するためにプログラミングコードとともに「ドントケア」変数が使用されることが可能である。

プロセス400及び/又はプロセス300の他の様々な具体例も予想されることが可能である。

図5に示されるコンピュータシステム(又は演算システム)500は本願で説明される任意の実施形態による処理を実行及び/又は制御するために使用されてよい。例えば、コンピュータシステム500は単独で使用されてもよいし或いは他のコンポーネントに関連して使用されてもよい。別の例として、コンピュータシステム500は、任意の計算を実行し、任意の方程式を解き、任意の識別を実行し、及び/又は、本願で説明される任意の判断を行うために使用されてよい。

コンピュータシステム500は図面に示され本願で説明されるハードウェア要素の全部又は何れからを含んでよい。コンピュータシステム500はバス505を介して電気的に結合されるハードウェア要素を含んでもよい(或いは、必要に応じて通信を行ってもよい)。ハードウェア要素は、限定ではないが1つ以上の汎用プロセッサ及び/又は1つ以上の特殊目的のプロセッサを含む1つ以上のプロセッサ510(例えば、ディジタル信号処理チップ、グラフィクス高速化チップ等)と、限定ではないがマウス、キーボード等を含んでよい1つ以上の入力デバイス515と、限定ではないがディスプレイデバイス、プリンタ等を含んでよい1つ以上の出力デバイス520とを含んでよい。

コンピュータシステム500は1つ以上のストレージデバイス525を更に含んでもよく(及び/又は1つ以上のストレージデバイス525と通信を行ってもよく)、ストレージデバイスは、限定ではないがローカルのストレージ及び/又はネットワークアクセス可能なストレージを含み、限定ではないが、ディスクドライブ、ドライブアレイ、光ストレージデバイス、ソリッドステートストレージデバイス、例えばランダムアクセスメモリ(RAM)及び/又はリードオンリメモリ(ROM)等を含み、これらはプログラム可能であってもよいし、フラッシュ更新等が可能であってもよい。コンピュータシステム500は通信サブシステム530も含み、通信サブシステム530は、限定ではないが、モデム、(無線又は有線による)ネットワークカード、赤外線通信装置、無線通信装置及び/又はチップセット(例えば、ブルートゥース(登録商標)デバイス、802.6デバイス、WiFiデバイス、WiMAXデバイス、セルラ通信設備)等を含んでもよい。通信サブシステム530は、データが、ネットワーク(例えば、一例として以下に説明されるようなネットワーク)及び/又は本願で説明される他の任意の装置と送受信されることを可能にする。多くの実施形態において、通信システム500は、上述したようなRAM又はROMを含んでよいワーキングメモリ535を更に含むであろう。

コンピュータシステム500は、オペレーティングシステム540及び/又は1つ以上のアプリケーションプログラム545のような他のコードを含むワーキングメモリ535内に現在位置するように示されるソフトウェア要素を含んでもよく、ソフトウェア要素は、本発明のコンピュータプログラムを含んでもよく、及び/又は、本願で説明されるように、本発明の方法を実行するように及び/又は本発明のシステムを構成するように設計されてもよい。例えば、上述した方法に関連して説明される1つ以上のプロシジャは、コンピュータ(及び/又はコンピュータ内のプロセッサ)により実行可能なコード及び/又は命令として実現されてもよい。これらの命令及び/又はコードのセットは、上述したストレージデバイス525のようなコンピュータ読み取り可能なストレージ媒体に保存されてもよい。

場合によっては、ストレージ媒体は、コンピュータシステム500内に組み込まれてもよいし、或いは、コンピュータシステム500と通信してもよい。他の実施形態では、ストレージ媒体は、コンピュータシステム500から分離していてもよいし(例えば、コンパクトディスクのように取り外し可能な媒体など)、及び/又は、インストレーションパッケージに設けられてもよく、そのようなストレージ媒体がそこに保存される命令/コードとともに汎用コンピュータをプログラムするのに使用されるようにする。これらの命令は、コンピュータシステム500により実行可能な実行可能コードの形態をとってもよいし、及び/又は、(例えば、コンパイラ、インストレーションプログラム、圧縮/解凍ユーティリティ等のような一般的に利用可能な様々な任意のものを利用して)コンピュータシステム500にコンパイル及び/又はインストールされる場合に、ソース及び/又はインストール可能なコードの形態をとり、その後に実行可能なコードの形態をとってもよい。

請求項に記載される事項の十分な理解をもたらすために多くの具体的な詳細が本願では説明されている。しかしながら、当業者は、請求項に記載される事項はこれらの具体的な詳細によらずに実施されてもよいことを理解するであろう。それ以外の点に関し、当業者に知られている方法、装置又はシステムは、請求項に記載される事項を曖昧にしないように詳細には説明されていない。

ある説明部分は、コンピュータメモリのようなコンピュータシステムメモリに保存されるバイナリディジタル信号又はデータビットに対する処理の抽象的表現又はアルゴリズムの観点から提供される。アルゴリズム的な記述又は表現は、データ処理の技術分野における通常の知識を有する者(当業者)が当該技術分野の他の当業者に彼らの仕事内容を伝えるために使用する技術的手段である。アルゴリズムは、所望の結果を導く一貫した処理シーケンス又は同様なプロセスである。この文脈において、処理又はプロセスは物理量の物理的な操作に関わる。必須ではないが、典型的には、そのような量は、保存、転送、統合、比較又はその他の操作をすることが可能な電気的又は磁気的な信号の形態をとってもよい。しばしば、主に慣用的な理由により、そのような信号を、ビット、データ、値、要素、シンボル、キャラクタ、文字、数、数値などと言及することが便利である。しかしながら、これら及び類似する全ての用語は、適切な物理量に関連し、単なる便宜的なラベルにすぎないことが、理解されるべきである。明示的にそうでないと言及しない限り、本明細書を通じて、「処理」、「演算」、「計算」、「判断」、「特定」等のような用語を用いる説明は、1つ以上のコンピュータ又は類似する電子コンピュータ装置又はデバイスのようなコンピュータ装置のアクション又は処理に関連することが認められ、そのアクション等は、メモリ、レジスタ、その他の情報ストレージデバイス、送信装置又はディスプレイ装置などのコンピュータプラットフォームにおけるものの中で物理的、電子的又は磁気的な量として表現されるデータを操作又は変換する。

本願で説明される1つ又は複数のシステムは何らかの特定のハードウェアアーキテクチャや構成に限定されない。コンピュータ装置又は演算装置は、1つ以上の入力により条件付けられる結果をもたらすコンポーネントの適切な任意の配置を含んでもよい。適切なコンピュータ装置は、保存されたソフトウェアにアクセスする多目的マイクロプロセッサベースのコンピュータシステムを含み、ソフトウェアは、汎用コンピュータ装置から、本願の対象の1つ以上の形態を実現するように特化されるコンピュータ装置へ、コンピュータシステムをプログラム又は構築する。適切な任意のプログラミング言語、スクリプト言語、その他のタイプの言語又は言語の組み合わせを利用して、コンピュータ装置をプログラミングする又は構成するのに使用されるソフトウェアで、本願に含まれる教示内容を実現してもよい。

本願で開示される方法の実施形態は、そのようなコンピュータ装置の処理において実行されてもよい。上記の例で示されるブロックの順番は変更されてもよく、例えば、ブロックは、並べ替えられてもよいし、統合されてもよいし、及び/又は、サブブロックに分断されてもよい。所定のブロック又はプロセスは並列的に実行されてもよい。

本願において「構成される」又は「設定される」のように使用される用語は、開放的な包含する言葉を意味し、追加的なタスクやステップ(又は工程)を実行するように構成又は設定される装置を排除しない。更に、「基づく」のように使用される用語は、開放的で包含的であるように意図され、1つ以上の言及される条件又は値に「基づく」プロセス、ステップ(又は工程)、計算又は他の処理は、実際には、言及されたもの以外の追加的な条件又は値に基づいてもよい。本願に含まれる見出し、リスト及び番号付けは、説明を簡易にするだけのためであり、限定することを意図していない。

本願の対象の事項が具体的な実施形態に関連して詳細に説明されてきたが、当業者は、上記の内容を把握すれば、そのような実施形態に対する代替例、変形例及び均等物を容易に生成できることが認められるであろう。従って、本開示は限定ではなく例示を目的として与えられており、本願の対象事項に対する当業者にとって自明であるような修正、変形及び/又は付加を包含することを排除しないことが、理解されるべきである。

５００コンピュータシステム
５１０プロセッサ
５２５ストレージデバイス
５１５入力デバイス
５２０出力デバイス
５３０通信サブシステム
５３５ワーキングメモリ
５４０オペレーティングシステム
５４５アプリケーション

Claims

コンピュータにより実行される方法であって、前記方法は、前記コンピュータが、
複数のSMT変数を有するSMT式をプログラミングコードから取得する工程と、
複数の簡略化されたSMT変数を含む簡略化されたSMT式を前記SMT式から取得する工程と、
複数のSAT変数を含むSAT式を前記簡略化されたSMT式から取得する工程と、
前記簡略化されたSMT式を利用して、前記複数のSMT変数のうち何れが「ドントケア」変数であるかを判定する工程と、
前記SAT式を利用して、前記複数のSMT変数のうち何れが「ドントケア」変数であるかを判定する工程と、
を有する方法。
前記簡略化されたSMT式により、前記複数のSMT変数のうち何れが「ドントケア」変数であるかを判定する工程が、
SMT代替マップを作成する工程と、
前記簡略化されたSMT変数及び前記SMT代替マップの双方又は一方に何れのSMT変数が含まれていないかを判定する工程と、
前記簡略化されたSMT変数及び前記SMT代替マップの双方又は一方に含まれていない前記SMT変数を出力する工程と、
を更に有する請求項1に記載の方法。
前記SAT式により、前記複数のSMT変数のうち何れが「ドントケア」変数であるかを判定する工程が、
前記SAT式を解くことにより、前記SAT変数をSAT変数の順序リストに並べるSATソリューショントレイルを取得する工程と、
前記SAT式が解を有する場合に、前記SAT変数の順序リストのうち、前記SAT式から削除することが可能な第1のSAT変数を判定する工程と、
前記SAT式が解を有する場合に、前記SAT式から削除することが可能な残りのSAT変数を判定する工程と、
削除することが可能なSAT変数に関連する前記SMT変数を判定する工程と、
を有する請求項1に記載の方法。
SATソリューショントレイルを取得する工程が、DPLLアルゴリズムを前記SAT式に適用する工程を更に有する、請求項3に記載の方法。
前記SAT式を取得することが、前記簡略化されたSMT式をビットブラストすることを更に含む、請求項1に記載の方法。
前記SMT式を簡略化することが、線形アレイソルバを前記SMT式に適用すること、及び/又は、アレイリード/ライト削除を前記SMT式に適用することを更に含む、請求項1に記載の方法。
前記コンピュータが、
前記「ドントケア」変数に基づいて、前記プログラミングコードにエラーが存在するか否かを判定する工程を更に有する請求項1に記載の方法。
コンピュータにより実行される方法であって、前記方法は、前記コンピュータが、
プログラミングコードを受信する工程と、
複数のSMT変数を含むSMT式を前記プログラミングコードから取得する工程と、
前記SMT式を、複数の簡略化されたSMT変数を有する簡略化されたSMT式に簡略化する工程と、
SMT代替マップを作成する工程と、
前記簡略化されたSMT式及び前記SMT代替マップの双方又は一方に何れのSMT変数が含まれていないかを判定する工程と、
前記簡略化されたSMT式及び前記SMT代替マップの双方又は一方に含まれていない前記SMT変数を出力する工程と、
を有する方法。
前記SMT式を簡略化することが、線形アレイソルバを前記SMT式に適用すること、及び/又は、アレイリード/ライト削除を前記SMT式に適用することを更に含む、請求項8に記載の方法。
前記簡略化されたSMT式及び前記SMT代替マップの双方又は一方に何れのSMT変数が含まれていないかを判定する工程が、前記SMT変数の各々を通じて反復する反復工程を有する、請求項8に記載の方法。
前記簡略化されたSMT式及び前記SMT代替マップの双方又は一方に含まれていない前記SMT変数は、「ドントケア」変数である、請求項8に記載の方法。
前記簡略化されたSMT式及び前記SMT代替マップの双方又は一方に含まれていない前記SMT変数に基づいて、前記プログラミングコードにエラーが存在するか否かを判定する工程を更に有する請求項8に記載の方法。
コンピュータにより実行される方法であって、前記方法は、前記コンピュータが、
SMT式を取得する工程と、
複数の簡略化されたSMT変数を含む簡略化されたSMT式を前記SMT式から取得する工程と、
複数のSAT変数を含むSAT式を前記簡略化されたSMT式から取得する工程と、
前記SAT式を解くことにより、前記SAT変数をSAT変数の順序リストに並べるSATソリューショントレイルを取得する工程と、
前記SAT式が解を有する場合に、前記SAT変数の順序リストのうち、前記SAT式から削除することが可能な第1のSAT変数を判定する工程と、
前記SAT式が解を有する場合に、前記SAT式から削除することが可能な残りのSAT変数を判定する工程と、
削除することが可能なSAT変数に関連する前記SMT変数を判定する工程と、
を有し、
SMT式を取得する工程が、
プログラミングコードを受信すること、及び
前記プログラミングコードから複数のSMT変数を有する前記SMT式を作成すること
を含む、
方法。
前記SAT式を取得することが、前記簡略化されたSMT式をビットブラストすることを更に含む、請求項13に記載の方法。
SATソリューショントレイルを取得する工程が、DPLLアルゴリズムを前記SAT式に適用する工程を更に有する、請求項13に記載の方法。
前記SAT変数の順序リストのうち、前記SAT式から削除することが可能な第1のSAT変数を判定する工程が、前記SATソリューショントレイルの一部分のうち少なくとも半分の前記SAT変数を明らかにする反復工程を更に有する請求項13に記載の方法。
後の反復における前記SATソリューショントレイルの少なくとも一部分は、前の反復における前記SATソリューショントレイルの半分のサイズである、請求項16に記載の方法。
前記SMT式を簡略化することが、線形アレイソルバを前記SMT式に適用すること、及び/又は、アレイリード/ライト削除を前記SMT式に適用することを更に含む、請求項13に記載の方法。
前記コンピュータが、
削除することが可能なSAT変数に関連する前記SMT変数に基づいて、プログラミングコードにエラーが存在するか否かを判定する工程を更に有する請求項13に記載の方法。