B2SAT: Difference between revisions

(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 ===

Revision as of 09:11, 23 April 2024

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.


Using B2SAT

B2SAT in the REPL

The following four commands are now available in REPL of probcli (start with probcli --repl):

  • :sat PRED
  • :sat-z3 PRED
  • :sat-double-check PRED
  • :sat-z3-double-check PRED
 :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

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, sat, sat-z3.

B2SAT in Jupyter Notebooks