(Created page with " The current versions of ProB can make use of the new B2SAT backend as an alternate way of solving constraints. It translates a subset of B formulas to SAT and for solving by an external SAT solver. == Using B2SAT == === B2SAT in the REPL === === B2SAT for PROPERTIES === The new preference SOLVER_FOR_PROPERTIES can be used to specify solver for PROPERTIES (axioms) when setting up constants. The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt...") |
No edit summary |
||
| Line 2: | Line 2: | ||
The current versions of ProB can make use of the new B2SAT backend as an alternate way of solving constraints. | The current versions of ProB can make use of the new B2SAT backend as an alternate way of solving constraints. | ||
It translates a subset of B formulas to SAT and for solving by an external SAT solver. | It translates a subset of B formulas to SAT and for solving by an external SAT solver. | ||
The new backend interleaves low-level SAT solving with high-level constraint solving performed by the default solver of ProB. | |||
| Line 7: | Line 8: | ||
=== B2SAT in the REPL === | === B2SAT in the REPL === | ||
The following four commands are now available in REPL of probcli (start with <tt>probcli --repl</tt>): | |||
* :sat PRED | |||
* :sat-z3 PRED | |||
* :sat-double-check PRED | |||
* :sat-z3-double-check PRED | |||
<pre> | |||
:sat f:1..n --> BOOL & n=3 & f(1)=TRUE & !i.(i:2..n => f(i) /= f(i-1)) | |||
PREDICATE is TRUE | |||
Solution: | |||
f = {(1|->TRUE),(2|->FALSE),(3|->TRUE)} & | |||
n = 3 | |||
</pre> | |||
=== B2SAT for PROPERTIES === | === B2SAT for PROPERTIES === | ||
The current versions of ProB can make use of the new B2SAT backend as an alternate way of solving constraints. It translates a subset of B formulas to SAT and for solving by an external SAT solver. The new backend interleaves low-level SAT solving with high-level constraint solving performed by the default solver of ProB.
The following four commands are now available in REPL of probcli (start with probcli --repl):
:sat f:1..n --> BOOL & n=3 & f(1)=TRUE & !i.(i:2..n => f(i) /= f(i-1))
PREDICATE is TRUE
Solution:
f = {(1|->TRUE),(2|->FALSE),(3|->TRUE)} &
n = 3
The new preference SOLVER_FOR_PROPERTIES can be used to specify solver for PROPERTIES (axioms) when setting up constants. The valid settings are: prob (the default), kodkod, z3, z3cns, z3axm, cdclt, sat, sat-z3.