2016-08-19 11 views
1

z3コードを複数のスレッドで並列に実行したい。私のプログラム構造では、Z3ソルバをまずすべてのアサーションで初期化し、次に満足できる解決策を求めます。Microsoft Z3 Dot Net API、クローンソルバー

私は複数のクローンを作成し、複数のスレッドにクローンを渡すことができるように、Z3ソルバーをクローンする方法はありますか?私はoffcourse自身がソルバーの配列を作成し、アサーション・プロセス中にそれらのそれぞれに主張私のクローンを作成することができますが、私はそれを行うにしたくない

Solver slvr1; 
//initialize and add all assertions on solver 1. 
//then create N number of clone solvers. 
//Finally run each solver clone on each thread. 

私の考えがあります...効率的でない可能性があります。

私はdot net APIを使用しています。だから誰でもドットネットapiの文脈で私に答えることができれば、もっと役立つだろう。

答えて

3

コンテキスト間でソルバーを翻訳する方法があります。これを使って。

https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/Solver.cs

コンテキストはスレッドセーフではありませんことを覚えておいて、その別のスレッドで異なるコンテキストを使用しています。

関連する問題