我试图重现这种行为，但我不能.如果我不将 MiniSat 二进制文件添加到 LD_LIBRARY_PATH 环境变量，我会收到您在第一次调用 execute_command 时提到的异常.配置 LD_LIBRARY_PATH 后，异常不会发生.

I tried to reproduce this behavior, but I couldn't. If I don't add MiniSat binaries to the LD_LIBRARY_PATH environment variable, I get the exception you mentioned the very first time I invoke execute_command. After configuring LD_LIBRARY_PATH, the exception doesn't happen.

配置 LD_LIBRARY_PATH:

To configure LD_LIBRARY_PATH:

(1) 如果使用 Eclipse，您可以右键单击源文件夹之一，选择 Build Path -> Configure Build Path，然后在Source"选项卡上确保Native library location"指向一个文件夹MiniSat 二进制文件所在的位置.

(1) if using Eclipse, you can right-click on one of your source folders, choose Build Path -> Configure Build Path, then on the "Source" tab make sure that "Native library location" points to a folder in which MiniSat binaries reside.

(2) 如果从 shell 运行，只需将包含 MiniSat 二进制文件的文件夹的路径添加到 LD_LIBRARY_PATH，例如，类似于 export LD_LIBARRY_PATH=alloy/extra/x86-linux:$LD_LIBRARY_PATH.

(2) if running from the shell, just add the path to a folder with MiniSat binaries to LD_LIBRARY_PATH, e.g., something like export LD_LIBARRY_PATH=alloy/extra/x86-linux:$LD_LIBRARY_PATH.

这是我正在运行的确切代码，一切正常

Here is the exact code that I was running, and everything worked

public static void main(String[] args) throws Exception {
    A4Reporter rep = new A4Reporter();

    A4Options options = new A4Options();
    options.solver = A4Options.SatSolver.MiniSatProverJNI;

    Module someWorld = CompUtil.parseEverything_fromFile(rep, null, "someFile.als");
    Command command = someWorld.getAllCommands().get(0);
    A4Solution ans = TranslateAlloyToKodkod.execute_command(rep, someWorld.getAllReachableSigs(), command, options);
    System.out.println(ans);

    Module someOtherWorld = CompUtil.parseEverything_fromFile(rep, null, "someOtherFile.als");
    Command commandTwo = someOtherWorld.getAllCommands().get(0);
    A4Solution ansTwo = TranslateAlloyToKodkod.execute_command(rep, someOtherWorld.getAllReachableSigs(), commandTwo, options);
    System.out.println(ansTwo);
}

someFile.als"是

with "someFile.als" being

sig A {}
run { some A } for 4

和someOtherFile.als"

and "someOtherFile.als"

sig A {}
run { no A } for 4