unitn-sml/wmi-pa

Efficient WMI via SMT-Based Predicate Abstraction

WMI-PA

Python 3 implementation of the methods presented in:

Efficient WMI via SMT-Based Predicate Abstraction
Paolo Morettin, Andrea Passerini, Roberto Sebastiani,
in Proceedings of IJCAI 2017

Advanced smt techniques for Weighted Model Integration
Paolo Morettin, Andrea Passerini, Roberto Sebastiani,
in Artificial Intelligence, Volume 275, 2019

SMT-based Weighted Model Integration with Structure Awareness
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani,
in UAI Conference 2022

Enhancing SMT-based Weighted Model Integration by structure awareness
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani,
in Artificial Intelligence, Volume 328, 2024

Installation

Base version:

pip install wmipa

Additional requirements

The base version of the solver requires at least one integration backend to be installed.

Additional dependencies are needed to also support NRA theory.

We provide a script that automatically installs all the requirements. The script has only been tested on Ubuntu distributions.

All-in-one installation

To install all the mandatory and optional requirements, run

wmipa-install --all

and then add the following lines to the ~/.bashrc file:

PATH=$HOME/.wmipa/latte/bin:$PATH
PATH=$HOME/.wmipa/approximate-integration/bin:$PATH

Separate installation

If you want to install the requirements separately, you can use the following commands.

At least one following integration backend is needed:

• LattE integrale - Exact integration (recommended):

  wmipa-install --latte

  Add $HOME/latte/bin to the PATH environment variable by adding the following line to the ~/.bashrc file:

  PATH=$HOME/.wmipa/latte/bin:$PATH
  

• VolEsti - Approximated integration:

  wmipa-install --volesti

  Add bin to the PATH environment variable by adding the following line to the ~/.bashrc file:

  PATH=$HOME/.wmipa/approximate-integration/bin:$PATH
  

• PyXadd - Symbolic integration:

  wmipa-install --symbolic

The MathSAT5 SMT solver is required

wmipa-install --msat

To support NRA theory (PI, Sin, Exp, ecc.), a customized version of PySMT must be installed via

wmipa-install --nra

Examples

We provide some examples that show how to write a model and evaluate weighted model integrals on it. To run the code in examples/, type:

python exampleX.py

Experiments

The code for running the experiments reported in the papers above can be found in the experiments branch.