B2SAT: Difference between revisions

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

Here is a simple example:

 >>> :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.

The last two will use B2SAT.

B2SAT in Jupyter Notebooks