SA-WMI-PA-SK

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

SMT-based Weighted Model Integration with Structure Awareness and Multiple Integration Approaches
Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, Roberto Sebastiani

pywmi

WMI-PA is now part of pywmi, a general framework for Weighted Model Integration that offers a number of different solvers, a command-line interface, etc.

Installation

pip install wmipa

Additional requirements

At least one following integration backend is needed:

• LattE integrale - Exact integration (recommended):

  wget https://github.com/latte-int/latte/releases/download/version_1_7_6/latte-int-1.7.6.tar.gz
  tar -xzf latte-int-1.7.6.tar.gz
  cd latte-int-1.7.6
  ./configure GXX="g++ -std=c++11" --prefix=$HOME/latte && make && make install
  

  Add $HOME/latte/bin to the PATH environment variable:

  export PATH=$HOME/latte/bin:$PATH
  

• VolEsti - Approximated integration:

  ```[bash]
  git clone https://github.com/masinag/approximate-integration
  cd approximate-integration
  make
  

  Add bin to the PATH environment variable:

  export PATH=$PWD/bin:$PATH
  

MathSAT5

pysmt-install --msat

For the SA-WMI-PA-SK mode, a slightly customized version of MathSAT5 is needed. In order to install it, you need to substitute the file <venv>/lib/python3.8/site-packages/_mathsat.cpython-38-x86_64-linux-gnu.so with the one provided in the bin/ folder of this repository (Python3.8 under Linux x86_64 is required).

Support for other OS and Python versions will be added in the near future.

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