I am currently working on an description of the behavior of Red-Black-Trees in Alloy.
This is a greater project than any I have done before in Alloy (I am a beginner). I have run into some problems, which I couldn’t solve with the usual debugging methods (removing predicates and studying their effects).
I was hoping that using a solver with Unsat Core could help with that.
When opening the “options” menu, there is no option “MiniSat with Unsat Core”. I know the windows version does not contain the MiniSat solver by default, but I am using Linux (Ubuntu).
This here is my “options” menu:
The jar file itself contains these libraries:
- libcryptominisat.so
- libglucose.so
- liblingeling.so
- libminisat.so
- libminisatprover.so
- libminisatproverx1.so
- libminisatx1.so
as well as a binary called “cryptominisat”.
I have searched for an option to install a solver that would help me use the Unsat Core functions, but I wasn’t sure how to find one.
Is it common for the alloy analyser jar to come without Unsat Core options?
I have downloaded the jar from (https://github.com/AlloyTools/org.alloytools.alloy/releases/download/v6.0.0/org.alloytools.alloy.dist.jar).