Weighted Model Integration PA (Predicate Abstraction) solver.
Project description
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
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
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.