B2SAT

Revision as of 09:08, 23 April 2024 by Michael Leuschel (talk | contribs) (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...")
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

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

B2SAT in Jupyter Notebooks