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

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

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-test-0.1.8.tar.gz (40.3 kB view details)

Uploaded Source

File details

Details for the file wmipa-test-0.1.8.tar.gz.

File metadata

  • Download URL: wmipa-test-0.1.8.tar.gz
  • Upload date:
  • Size: 40.3 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.10.6

File hashes

Hashes for wmipa-test-0.1.8.tar.gz
Algorithm Hash digest
SHA256 e988ff172aa434674ddca1b1ae9b681c8a3dd99bd0b92c7c3d54f9d29db88232
MD5 3190d14dcfdbb21e8a8915d2b6ed2520
BLAKE2b-256 e2fea049d2cb36335b2d839aa2ed78e335498785892ff547b92ede333781ced4

See more details on using hashes here.

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