Ошибка выполнения при изменении SATSolver с SAT4J на MiniSAT

Question

В моем коде Java, когда я меняю SATSolver с SAT4J на MiniSatJNI или MiniSatProverJNI в:

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

Например, чтобы:

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

А затем позвоните:

A4Solution currentAns = TranslateAlloyToKodkod.execute_command(null,
                        javaMetamodel.getAllReachableSigs(), command, options);

Я получаю следующую ошибку выполнения:

Fatal error:
The required JNI library cannot be found: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:390)
    at ejdolly.JDollyImp.initializeAlloyAnalyzer(JDollyImp.java:128)
    at ejdolly.JDolly.hasNext(JDolly.java:181)
    at org.testorrery.ForLoopIterator.hasNext(ForLoopIterator.java:40)
    at refactoringTest.RefactoringTest.runTests(RefactoringTest.java:145)
    at refactoringTest.MainRunner.main(MainRunner.java:83)
Caused by: java.lang.UnsatisfiedLinkError: no minisatproverx5 in java.library.path
    at java.lang.ClassLoader.loadLibrary(Unknown Source)
    at java.lang.Runtime.loadLibrary0(Unknown Source)
    at java.lang.System.loadLibrary(Unknown Source)
    at kodkod.engine.satlab.NativeSolver.loadLibrary(NativeSolver.java:73)
    at kodkod.engine.satlab.MiniSatProver.<clinit>(MiniSatProver.java:148)
    at kodkod.engine.satlab.SATFactory$5.instance(SATFactory.java:106)
    at kodkod.engine.fol2sat.Bool2CNFTranslator.translate(Bool2CNFTranslator.java:55)
    at kodkod.engine.fol2sat.Translator.toCNF(Translator.java:426)
    at kodkod.engine.fol2sat.Translator.generateSBP(Translator.java:365)
    at kodkod.engine.fol2sat.Translator.toBoolean(Translator.java:343)
    at kodkod.engine.fol2sat.Translator.translate(Translator.java:189)
    at kodkod.engine.fol2sat.Translator.translate(Translator.java:143)
    at kodkod.engine.Solver$SolutionIterator.next(Solver.java:495)
    at kodkod.engine.Solver$SolutionIterator.next(Solver.java:1)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.<init>(A4Solution.java:719)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution$Peeker.<init>(A4Solution.java:709)
    at edu.mit.csail.sdg.alloy4compiler.translator.A4Solution.solve(A4Solution.java:941)
    at edu.mit.csail.sdg.alloy4compiler.translator.TranslateAlloyToKodkod.execute_command(TranslateAlloyToKodkod.java:388)
    ... 5 more
java.lang.NullPointerException
    at ejdolly.JDolly.hasNext(JDolly.java:182)
    at org.testorrery.ForLoopIterator.hasNext(ForLoopIterator.java:40)
    at refactoringTest.RefactoringTest.runTests(RefactoringTest.java:145)
    at refactoringTest.MainRunner.main(MainRunner.java:83)

Любая помощь?

Answer 1

Alloy вызывает собственные решатели (такие как MiniSAT) с использованием JNDI/JNI. Это означает, что собственные библиотеки должны быть правильно настроены ранее. Если у вас не настроена корректность библиотеки, Java выдаст исключение "java.lang.UnsatisfiedLinkError".

Распространяемый jar Alloy включает в себя правильно настроенные библиотеки для Windows "x86" и для Linux и Mac в "x86" и "x64". Это означает, что jar будет работать в Windows без какой-либо дополнительной настройки, если вы используете 32-битную версию Java, но не 64-битную версию Java. В других операционных системах вы можете использовать обе версии Java (32 и 64 бит).

Вы можете проверить другие вопросы в Stackru для того же объяснения.

Answer 2

Решение, на которое указал @Aleksandar: Alloy API, приводящий к java.lang.UnsatisfiedLinkError

у меня работало на linux!!! Но это не работает на окнах.

Спасибо за помощь!