Skip to main content

Weighted Model Integration PA (Predicate Abstraction) solver.

Project description

SA-WMI-PA-SK

Build Status

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

Base version:

pip install wmipa

Version with support for NRA:

pip install "wmipa[nra]"

Additional requirements

At least one following integration backend is needed:

  • LattE integrale - Exact integration (recommended):

    sudo apt install -y libntl-dev libcdd-dev libcdd-tools
    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" CXX="g++ -std=c++11" --prefix=$HOME/latte && make && make install
    cd ..
    

    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

Project details


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

wmipa-0.1.7.tar.gz (40.4 kB view hashes)

Uploaded source

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page