Welcome to the WM*PY documentation

wmpy \(=\) reasoning over weighted algebraic and logical constraints in python3

\[ \begin{align}\begin{aligned}P(x \ge y \:|\: y / 2 \le \pi) = ?? \quad\quad\quad\quad \text{ (marginals)}\\P(x + y > 3/4) \le 0.01 ?? \quad\quad\quad\quad \text{ (bounds)}\\argmax_y \: P(x, y) = ?? \quad\quad \text{ (optimization)}\\x \sim P(x \: | \: x \ge y) \quad\quad\quad\quad \text{ (sampling)}\end{aligned}\end{align} \]
_images/intro-cropped.png

… pip install wmpy !

WM* (weighted model *) denotes any problem that is defined on the models (solutions) of an SMT-LRA formula, i.e. any combination of logical and linear constraints over Boolean and continuous variables.

WM*PY (wmpy) is a modular library for solving quantitative reasoning tasks over logical and algebraic constraints.

This library:

  • Facilitates the integration of state-of-the-art WM* technology into your project

  • Provides a flexible framework for the development of novel solvers

Unfamiliar with WMI or SMT? Read our theory primer first.

Eager to code? Get started now!

Curious about advanced use cases? Check out our Jupiter notebooks.

Want to be part of wmpy ? Learn how to contribute.