コマンドラインからSATソルバを選択する

Question

クラスedu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompilerは、コマンドラインからAlloyコマンドを実行する方法の例を提供します。この例で使用されるバックエンドソルバは、Sat4Jです。私はソルバーをより速いものの1つに変更したいと思っていますPlingeling。残念ながら、私はこれを達成する方法を考えることができません。単に

options.solver = A4Options.SatSolver.PLingelingJNI; 

にライン

options.solver = A4Options.SatSolver.SAT4J; 

を変更することはできません。

Exception in thread "main" Fatal error: 
Unknown exception occurred: kodkod.engine.AbortedException: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory 
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.executeCommand(TranslateAlloyToKodkod.java:1079) 
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.executeCommand(TranslateAlloyToKodkod.java:1065) 
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:381) 
    at edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler.main(ExampleUsingTheCompiler.java:72) 
Caused by: kodkod.engine.AbortedException: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory 
    at kodkod.engine.Solver.solve(Solver.java:147) 
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(A4Solution.java:1058) 
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.executeCommand(TranslateAlloyToKodkod.java:1070) 
    ... 3 more 
Caused by: kodkod.engine.satlab.SATAbortedException: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory 
    at kodkod.engine.satlab.ExternalSolver.solve(ExternalSolver.java:255) 
    at kodkod.engine.Solver.solve(Solver.java:140) 
    ... 5 more 
Caused by: java.io.IOException: Cannot run program "plingeling": error=2, No such file or directory 
    at java.lang.ProcessBuilder.start(ProcessBuilder.java:1048) 
    at java.lang.Runtime.exec(Runtime.java:620) 
    at java.lang.Runtime.exec(Runtime.java:485) 
    at kodkod.engine.satlab.ExternalSolver.solve(ExternalSolver.java:221) 
    ... 6 more 
Caused by: java.io.IOException: error=2, No such file or directory 
    at java.lang.UNIXProcess.forkAndExec(Native Method) 
    at java.lang.UNIXProcess.<init>(UNIXProcess.java:248) 
    at java.lang.ProcessImpl.start(ProcessImpl.java:134) 
    at java.lang.ProcessBuilder.start(ProcessBuilder.java:1029) 
    ... 9 more 

合金GUIは、それが実行される前に、適切な場所に（plingeling実行ファイルを含む）いくつかのファイルをコピーすることによってこの問題を回避するようだ：私は、次のエラーメッセージが表示されます。

Answer 1

Tarciana's answerからリンクされた質問のおかげで、私は正常に私のマシン（Mac）でこれを稼働させました。 実行ファイルとして配布されているPlingelingのようなソルバーを使用するためには

• 、一つはjavaを実行する前に、

  export PATH=<path_to_solver_binaries_and_libraries>:$PATH 
  

  を実行する必要があります。 javaを実行するとき 動的ライブラリとして分散さにおいてMiniSATようなソルバーを使用するために

は、一つは引数

-Djava.library.path=<path_to_solver_binaries_and_libraries> 

を追加しなければなりません。

Answer 2

私は私の質問のようにあなたと同じ問題にしていました： Execution Error when change the SATSolver from SAT4J to MiniSAT

前の質問に@Aleksandarによって指さソリューション、 Alloy API resulting in java.lang.UnsatisfiedLinkError

を参照して、古いUbuntuの中で私の作品バージョン（10.0.0）でも以前のバージョンのubuntuでは動作しません（14.04や16.04など）。

などzchaffやminisatproverなどの別のソルバーを選択するとき、私は観察し、そのインスタンスのエラーの変更、：

「必要なJNIライブラリが見つからない：ます。java.lang.UnsatisfiedLinkError：java.library.pathにではありませんzchaffx5 "

他のすべてのソルバーでは、探しているライブラリ（例：zchaffx5）はx86-linuxフォルダ内の既存のもの（合金4.2.jar内）よりも更新されているようです：zchaffx1 。私は、他のソルバーのための既存のライブラリは時代遅れだと思います。この問題の解決策を見つけることができたら、私たちに知らせてください。