No edit summary |
|||
(2 intermediate revisions by the same user not shown) | |||
Line 2: | Line 2: | ||
[[Category:Stubs]] | [[Category:Stubs]] | ||
As of version 1.3.5 ProB can make use of [ | As of version 1.3.5 ProB can make use of [https://emina.github.io/kodkod/ Kodkod] as an alternate way of solving constraints. | ||
Kodkod provides a relational interface to SAT solvers and is | Kodkod provides a relational interface to SAT solvers and is the heart of the [https://alloytools.org Alloy] tool. | ||
= How to enable Kodkod = | = How to enable Kodkod = | ||
Line 54: | Line 54: | ||
You can control the solver being used using the <tt>KODKOD_SAT_SOLVER</tt> preference (which has four possible values: sat4j, minisat, lingeling, glucose). | You can control the solver being used using the <tt>KODKOD_SAT_SOLVER</tt> preference (which has four possible values: sat4j, minisat, lingeling, glucose). | ||
These files can be downloaded from the [ | These files can be downloaded from the [https://emina.github.io/kodkod/ Kodkod download site]. | ||
= More Preferences = | = More Preferences = | ||
Line 76: | Line 76: | ||
You can also have a look at these Wiki pages: | You can also have a look at these Wiki pages: | ||
* [[Proving_Theorems_in_the_ProB_REPL]] | * [[Proving_Theorems_in_the_ProB_REPL]] | ||
* [[Argumentation_Theory Argumentation Theory Example]] | * [[Argumentation_Theory|Argumentation Theory Example]] |
As of version 1.3.5 ProB can make use of Kodkod as an alternate way of solving constraints.
Kodkod provides a relational interface to SAT solvers and is the heart of the Alloy tool.
For the command-line version you need to call prob as follows:
probcli -p KODKOD TRUE
Note: to experiment with Kodkod you may want to try out the command:
probcli -p KODKOD TRUE -repl
If in addition you want see a graphical representation of the solutions found you can use the following command and open the out.dot file using dotty or GraphViz:
probcli -p KODKOD TRUE -repl -evaldot ~/out.dot
For the ProB Tcl/Tk Version you should select the menu command "Enable Kodkod for Properties" in the Preferences menu.
Once enabled, the Kodkod translation will be used in the following circumstances:
By default Kodkod in ProB uses the bundled SAT4J solver. You can switch to using minisat by putting a current version of libminisat.jnilib into ProB's lib directory.
Similarly, as of ProB 1.6.1-beta5 you can also use the Solver lingeling or glucose by dropping liblingeling.dylib or libglucose.dylib into ProB's lib folder (for Mac OS X; for Linux the extension will be different). You can control the solver being used using the KODKOD_SAT_SOLVER preference (which has four possible values: sat4j, minisat, lingeling, glucose).
These files can be downloaded from the Kodkod download site.
If you set KODKOD_ONLY_FULL to FALSE, then the Kodkod translation can be applied to part of a predicate. In other words, the predicate (such as the PROPERTIES) are partitioned into two parts: one that can be understood by Kodkod and the rest which will be dealt with by ProB's solver.
You can also enable symmetry by using the preference KODKOD_SYMMETRY. By default, ProB will set this value to 0, i.e., symmetry is off. This means that Kodkod can also be used within set comprehensions. By setting the preference to a value higher than 0 you will enable symmetry within Kodkod, which may mean that not all solutions will be returned. Setting the value too high may be counter productive; Kodkod's recommended default is 20.
Finally, you can control the number of solutions that Kodkod computes in one go using the preference KODKOD_MAX_NR_SOLS. E.g., if you are interested in only one solution and KODKOD_ONLY_FULL is TRUE, then you should set this value to 1.
You can also have a look at these Wiki pages: