In my Java code, when i change the SATSolver from SAT4J to MiniSatJNI or MiniSatProverJNI in:
A4Options options = new A4Options();
options.solver = A4Options.SatSolver.SAT4J;
For instance, to:
A4Options options = new A4Options();
options.solver = A4Options.SatSolver.MiniSatProverJNI;
And then call:
A4Solution currentAns = TranslateAlloyToKodkod.execute_command(null,
javaMetamodel.getAllReachableSigs(), command, options);
I receive the following execution error:
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)
Any help?