%global _empty_manifest_terminate_build 0 Name: python-pywmi Version: 0.7.15 Release: 1 Summary: Essential tools and interfaces for WMI solving. License: MIT URL: http://github.com/samuelkolb/pywmi Source0: https://mirrors.nju.edu.cn/pypi/web/packages/57/ee/e6c5a32908092872b7e0f410da1d9fc989c10f6193af70a091bdc18ecdf2/pywmi-0.7.15.tar.gz BuildArch: noarch Requires: python3-pysmt Requires: python3-numpy Requires: python3-future Requires: python3-matplotlib Requires: python3-pillow Requires: python3-polytope Requires: python3-tabulate Requires: python3-graphviz Requires: python3-sympy Requires: python3-scipy Requires: python3-autodora Requires: python3-deprecated Requires: python3-networkx Requires: python3-antlr4-python3-runtime Requires: python3-pysdd %description # pywmi [![Build Status](https://travis-ci.org/weighted-model-integration/pywmi.svg?branch=master)](https://travis-ci.org/weighted-model-integration/pywmi) ## Installation pip install pywmi pywmi offers various services and engines that require additional installation steps. ### SMT solvers pywmi relies upon pysmt to interface with SMT solvers. If you want to benefit from functionality relying on SMT solvers please install an SMT solver through the pysmt-install tool that comes as part of your pywmi installation. pysmt-install --msat # example to install mathsat, more solvers are available For older versions of PySMT (older than version 0.8), you have to make sure that when you use pywmi, the SMT solvers are on your path. The pysmt-install tool can show you the necessary commands. pysmt-install --env ### XADD engine The XADD engine performs WMI using XADDs as described in [Kolb et al., 2018](https://www.ijcai.org/proceedings/2018/698). To use this engine you need [Java](https://www.oracle.com/technetwork/java/javase/downloads/index.html), [Gurobi](https://www.gurobi.com) and the xadd library JAR file. The pywmi-install tool that comes with your pywmi installation can automatically download and install the JAR file, however, you need to install Java and Gurobi manually. Once you did that, just call: pywmi-install xadd pywmi-install xadd --force # To download a new version ### Predicate abstraction engine The predicate abstraction engine (short PA engine) uses MathSAT and Latte to solve WMI using predicate abstraction, as described in [Morettin et al., 2017](https://www.ijcai.org/proceedings/2017/0100.pdf). In order to use the PA engine, you need to install the MathSAT SMT solver (see instructions above), Latte (see instructions below) and the [wmipa library](https://github.com/unitn-sml/wmi-pa). You can use the `pysmt-install` utility to download the library. pywmi-install pa pywmi-install pa --force # To download a new version **Manual installation** You can also download or clone the library manually and add it to your `PYTHONPATH` 1. Download / clone the [wmipa library](https://github.com/unitn-sml/wmi-pa) 2. Add the directory containing the library to your `PYTHONPATH` ### Native XSDD engine The native XSDD engine (and the PiecewiseXSDD class for representing piecewise functions) are implemented using the [PySDD](https://github.com/wannesm/PySDD) library. The PySDD package can be installed as follows: pip install git+https://github.com/wannesm/PySDD.git#egg=PySDD ### External XSDD engine WMI using XSDD inference is also supported by pywmi. To use the XSDD engine you need to install [HAL-ProbLog](https://bitbucket.org/pedrozudo/hal_problog) by following the instructions provided in the README file. **Summary** 1. Install the [dmd compiler v2.078.3](http://downloads.dlang.org/releases/2.x/2.078.3/) 2. `git clone https://github.com/ariovistus/pyd.git` 3. `cd pyd` 4. `python setup.py install` 5. `cd ../` 6. `git clone --recursive https://github.com/ML-KULeuven/psipy.git` 7. `cd psypi` 8. `python psipy/build_psi.py` 9. `python setup.py install` 10. Add the psi library to your path (command printed during the previous step) 11. `cd ../` 12. `git clone https://bitbucket.org/pedrozudo/hal_problog.git` 13. `cd hal_problog` 14. `python setup.py install` Take care that your code does not run in the same directory as the one you cloned the libraries, as they will pollute your namespace. ### Latte The Latte integration backend as well as the predicate abstraction solver require [Latte](https://www.math.ucdavis.edu/~latte/software.php) to be installed. You can find the latest releases on their [GitHub releases page](https://github.com/latte-int/latte/releases). You'll probably want the bundle: latte-integrale. **Summary** 1. `wget "https://github.com/latte-int/latte/releases/download/version_1_7_5/latte-integrale-1.7.5.tar.gz"` 2. `tar -xvzf latte-integrale-1.7.5.tar.gz` 3. `cd latte-integrale-1.7.5` 4. `./configure` 5. `make` ## Usage ### Calling pywmi **Setup density and query** import pysmt.shortcuts as smt # Create a "domain" with boolean variables a and b and real variables x, y (both between 0 and 1) domain = Domain.make(["a", "b"], ["x", "y"], [(0, 1), (0, 1)]) a, b = domain.get_bool_symbols() # Get PySMT symbols for the boolean variables x, y = domain.get_real_symbols() # Get PySMT variables for the continuous variables # Create support support = (a | b) & (~a | ~b) & (x <= y) & domain.get_bounds() # Create weight function (PySMT requires constants to be wrapped, e.g., smt.Real(0.2)) weight_function = smt.Ite(a, smt.Real(0.2), smt.Real(0.8)) * (smt.Ite(x <= 0.5, smt.Real(0.2), 0.2 + y) + smt.Real(0.1)) # Create query query = x <= y / 2 **Use engine to perform inference** # Create rejection-sampling based engine (no setup required) rejection_engine = RejectionEngine(domain, support, weight_function, sample_count=100000) print("Volume (Rejection): ", rejection_engine.compute_volume()) # Compute the weighted model integral print("Query probability (Rejection):", rejection_engine.compute_probability(query)) # Compute query probability **Use XADD engine (make sure you have installed the prerequisites)** # Create XADD engine (mode resolve refers to the integration algorithm described in # Kolb et al. Efficient symbolic integration for probabilistic inference. IJCAI 2018) # !! Requires XADD solver to be setup (see above) !! xadd_engine = XaddEngine(domain, support, weight_function, mode="resolve") print("Volume (XADD): ", xadd_engine.compute_volume()) # Compute the weighted model integral print("Query probability (XADD): ", xadd_engine.compute_probability(query)) # Compute query probability **Generating uniform samples and their labels** from pywmi.sample import uniform # n: Required number of samples # domain, support: Domain and support defined as above samples = uniform(domain, n) labels = evaluate(samples, support, samples) **Generating weighted positive samples** from pywmi.sample import positive # n: Required number of samples # domain, support, weight: Defining the density as above # Optional: # sample_pool_size: The number of uniformly sampled positive samples to weight and select the samples from # sample_count: The number of samples to draw initially, from which to build the positive pool # max_samples: The maximum number of uniformly sampled samples (positive or negative) to generate before failing # => If max_samples is exceeded a SamplingError will be raised samples, positive_ratio = positive(n, domain, support, weight) **Handle densities and write to files** # Wrap support and weight function (and optionally queries) in a density object density = Density(domain, support, weight_function, [query]) # Density object can be saved to and loaded from files filename = "my_density.json" density.to_file(filename) # Save to file density = Density.from_file(filename) # Load from file **Work from command line** # Compare engines from command line python -m pywmi my_density.json compare rej:n100000 xadd:mresolve # Compute the weighted model integral python -m pywmi my_density.json compare rej:n100000 xadd:mresolve -q 0 # Compute query probability (query at index 0) # Compute volumes and probabilities from command line # You can provide multiple engines and the result of the first engine not to fail will be returned python -m pywmi my_density.json volume rej:n100000 # Compute weighted model integral python -m pywmi my_density.json prob rej:n100000 # Compute all query probabilities # Plot 2-D support python -m pywmi my_density.json plot -o my_density.png Find the complete running example in [pywmi/tests/running_example.py](pywmi/tests/running_example.py) %package -n python3-pywmi Summary: Essential tools and interfaces for WMI solving. Provides: python-pywmi BuildRequires: python3-devel BuildRequires: python3-setuptools BuildRequires: python3-pip %description -n python3-pywmi # pywmi [![Build Status](https://travis-ci.org/weighted-model-integration/pywmi.svg?branch=master)](https://travis-ci.org/weighted-model-integration/pywmi) ## Installation pip install pywmi pywmi offers various services and engines that require additional installation steps. ### SMT solvers pywmi relies upon pysmt to interface with SMT solvers. If you want to benefit from functionality relying on SMT solvers please install an SMT solver through the pysmt-install tool that comes as part of your pywmi installation. pysmt-install --msat # example to install mathsat, more solvers are available For older versions of PySMT (older than version 0.8), you have to make sure that when you use pywmi, the SMT solvers are on your path. The pysmt-install tool can show you the necessary commands. pysmt-install --env ### XADD engine The XADD engine performs WMI using XADDs as described in [Kolb et al., 2018](https://www.ijcai.org/proceedings/2018/698). To use this engine you need [Java](https://www.oracle.com/technetwork/java/javase/downloads/index.html), [Gurobi](https://www.gurobi.com) and the xadd library JAR file. The pywmi-install tool that comes with your pywmi installation can automatically download and install the JAR file, however, you need to install Java and Gurobi manually. Once you did that, just call: pywmi-install xadd pywmi-install xadd --force # To download a new version ### Predicate abstraction engine The predicate abstraction engine (short PA engine) uses MathSAT and Latte to solve WMI using predicate abstraction, as described in [Morettin et al., 2017](https://www.ijcai.org/proceedings/2017/0100.pdf). In order to use the PA engine, you need to install the MathSAT SMT solver (see instructions above), Latte (see instructions below) and the [wmipa library](https://github.com/unitn-sml/wmi-pa). You can use the `pysmt-install` utility to download the library. pywmi-install pa pywmi-install pa --force # To download a new version **Manual installation** You can also download or clone the library manually and add it to your `PYTHONPATH` 1. Download / clone the [wmipa library](https://github.com/unitn-sml/wmi-pa) 2. Add the directory containing the library to your `PYTHONPATH` ### Native XSDD engine The native XSDD engine (and the PiecewiseXSDD class for representing piecewise functions) are implemented using the [PySDD](https://github.com/wannesm/PySDD) library. The PySDD package can be installed as follows: pip install git+https://github.com/wannesm/PySDD.git#egg=PySDD ### External XSDD engine WMI using XSDD inference is also supported by pywmi. To use the XSDD engine you need to install [HAL-ProbLog](https://bitbucket.org/pedrozudo/hal_problog) by following the instructions provided in the README file. **Summary** 1. Install the [dmd compiler v2.078.3](http://downloads.dlang.org/releases/2.x/2.078.3/) 2. `git clone https://github.com/ariovistus/pyd.git` 3. `cd pyd` 4. `python setup.py install` 5. `cd ../` 6. `git clone --recursive https://github.com/ML-KULeuven/psipy.git` 7. `cd psypi` 8. `python psipy/build_psi.py` 9. `python setup.py install` 10. Add the psi library to your path (command printed during the previous step) 11. `cd ../` 12. `git clone https://bitbucket.org/pedrozudo/hal_problog.git` 13. `cd hal_problog` 14. `python setup.py install` Take care that your code does not run in the same directory as the one you cloned the libraries, as they will pollute your namespace. ### Latte The Latte integration backend as well as the predicate abstraction solver require [Latte](https://www.math.ucdavis.edu/~latte/software.php) to be installed. You can find the latest releases on their [GitHub releases page](https://github.com/latte-int/latte/releases). You'll probably want the bundle: latte-integrale. **Summary** 1. `wget "https://github.com/latte-int/latte/releases/download/version_1_7_5/latte-integrale-1.7.5.tar.gz"` 2. `tar -xvzf latte-integrale-1.7.5.tar.gz` 3. `cd latte-integrale-1.7.5` 4. `./configure` 5. `make` ## Usage ### Calling pywmi **Setup density and query** import pysmt.shortcuts as smt # Create a "domain" with boolean variables a and b and real variables x, y (both between 0 and 1) domain = Domain.make(["a", "b"], ["x", "y"], [(0, 1), (0, 1)]) a, b = domain.get_bool_symbols() # Get PySMT symbols for the boolean variables x, y = domain.get_real_symbols() # Get PySMT variables for the continuous variables # Create support support = (a | b) & (~a | ~b) & (x <= y) & domain.get_bounds() # Create weight function (PySMT requires constants to be wrapped, e.g., smt.Real(0.2)) weight_function = smt.Ite(a, smt.Real(0.2), smt.Real(0.8)) * (smt.Ite(x <= 0.5, smt.Real(0.2), 0.2 + y) + smt.Real(0.1)) # Create query query = x <= y / 2 **Use engine to perform inference** # Create rejection-sampling based engine (no setup required) rejection_engine = RejectionEngine(domain, support, weight_function, sample_count=100000) print("Volume (Rejection): ", rejection_engine.compute_volume()) # Compute the weighted model integral print("Query probability (Rejection):", rejection_engine.compute_probability(query)) # Compute query probability **Use XADD engine (make sure you have installed the prerequisites)** # Create XADD engine (mode resolve refers to the integration algorithm described in # Kolb et al. Efficient symbolic integration for probabilistic inference. IJCAI 2018) # !! Requires XADD solver to be setup (see above) !! xadd_engine = XaddEngine(domain, support, weight_function, mode="resolve") print("Volume (XADD): ", xadd_engine.compute_volume()) # Compute the weighted model integral print("Query probability (XADD): ", xadd_engine.compute_probability(query)) # Compute query probability **Generating uniform samples and their labels** from pywmi.sample import uniform # n: Required number of samples # domain, support: Domain and support defined as above samples = uniform(domain, n) labels = evaluate(samples, support, samples) **Generating weighted positive samples** from pywmi.sample import positive # n: Required number of samples # domain, support, weight: Defining the density as above # Optional: # sample_pool_size: The number of uniformly sampled positive samples to weight and select the samples from # sample_count: The number of samples to draw initially, from which to build the positive pool # max_samples: The maximum number of uniformly sampled samples (positive or negative) to generate before failing # => If max_samples is exceeded a SamplingError will be raised samples, positive_ratio = positive(n, domain, support, weight) **Handle densities and write to files** # Wrap support and weight function (and optionally queries) in a density object density = Density(domain, support, weight_function, [query]) # Density object can be saved to and loaded from files filename = "my_density.json" density.to_file(filename) # Save to file density = Density.from_file(filename) # Load from file **Work from command line** # Compare engines from command line python -m pywmi my_density.json compare rej:n100000 xadd:mresolve # Compute the weighted model integral python -m pywmi my_density.json compare rej:n100000 xadd:mresolve -q 0 # Compute query probability (query at index 0) # Compute volumes and probabilities from command line # You can provide multiple engines and the result of the first engine not to fail will be returned python -m pywmi my_density.json volume rej:n100000 # Compute weighted model integral python -m pywmi my_density.json prob rej:n100000 # Compute all query probabilities # Plot 2-D support python -m pywmi my_density.json plot -o my_density.png Find the complete running example in [pywmi/tests/running_example.py](pywmi/tests/running_example.py) %package help Summary: Development documents and examples for pywmi Provides: python3-pywmi-doc %description help # pywmi [![Build Status](https://travis-ci.org/weighted-model-integration/pywmi.svg?branch=master)](https://travis-ci.org/weighted-model-integration/pywmi) ## Installation pip install pywmi pywmi offers various services and engines that require additional installation steps. ### SMT solvers pywmi relies upon pysmt to interface with SMT solvers. If you want to benefit from functionality relying on SMT solvers please install an SMT solver through the pysmt-install tool that comes as part of your pywmi installation. pysmt-install --msat # example to install mathsat, more solvers are available For older versions of PySMT (older than version 0.8), you have to make sure that when you use pywmi, the SMT solvers are on your path. The pysmt-install tool can show you the necessary commands. pysmt-install --env ### XADD engine The XADD engine performs WMI using XADDs as described in [Kolb et al., 2018](https://www.ijcai.org/proceedings/2018/698). To use this engine you need [Java](https://www.oracle.com/technetwork/java/javase/downloads/index.html), [Gurobi](https://www.gurobi.com) and the xadd library JAR file. The pywmi-install tool that comes with your pywmi installation can automatically download and install the JAR file, however, you need to install Java and Gurobi manually. Once you did that, just call: pywmi-install xadd pywmi-install xadd --force # To download a new version ### Predicate abstraction engine The predicate abstraction engine (short PA engine) uses MathSAT and Latte to solve WMI using predicate abstraction, as described in [Morettin et al., 2017](https://www.ijcai.org/proceedings/2017/0100.pdf). In order to use the PA engine, you need to install the MathSAT SMT solver (see instructions above), Latte (see instructions below) and the [wmipa library](https://github.com/unitn-sml/wmi-pa). You can use the `pysmt-install` utility to download the library. pywmi-install pa pywmi-install pa --force # To download a new version **Manual installation** You can also download or clone the library manually and add it to your `PYTHONPATH` 1. Download / clone the [wmipa library](https://github.com/unitn-sml/wmi-pa) 2. Add the directory containing the library to your `PYTHONPATH` ### Native XSDD engine The native XSDD engine (and the PiecewiseXSDD class for representing piecewise functions) are implemented using the [PySDD](https://github.com/wannesm/PySDD) library. The PySDD package can be installed as follows: pip install git+https://github.com/wannesm/PySDD.git#egg=PySDD ### External XSDD engine WMI using XSDD inference is also supported by pywmi. To use the XSDD engine you need to install [HAL-ProbLog](https://bitbucket.org/pedrozudo/hal_problog) by following the instructions provided in the README file. **Summary** 1. Install the [dmd compiler v2.078.3](http://downloads.dlang.org/releases/2.x/2.078.3/) 2. `git clone https://github.com/ariovistus/pyd.git` 3. `cd pyd` 4. `python setup.py install` 5. `cd ../` 6. `git clone --recursive https://github.com/ML-KULeuven/psipy.git` 7. `cd psypi` 8. `python psipy/build_psi.py` 9. `python setup.py install` 10. Add the psi library to your path (command printed during the previous step) 11. `cd ../` 12. `git clone https://bitbucket.org/pedrozudo/hal_problog.git` 13. `cd hal_problog` 14. `python setup.py install` Take care that your code does not run in the same directory as the one you cloned the libraries, as they will pollute your namespace. ### Latte The Latte integration backend as well as the predicate abstraction solver require [Latte](https://www.math.ucdavis.edu/~latte/software.php) to be installed. You can find the latest releases on their [GitHub releases page](https://github.com/latte-int/latte/releases). You'll probably want the bundle: latte-integrale. **Summary** 1. `wget "https://github.com/latte-int/latte/releases/download/version_1_7_5/latte-integrale-1.7.5.tar.gz"` 2. `tar -xvzf latte-integrale-1.7.5.tar.gz` 3. `cd latte-integrale-1.7.5` 4. `./configure` 5. `make` ## Usage ### Calling pywmi **Setup density and query** import pysmt.shortcuts as smt # Create a "domain" with boolean variables a and b and real variables x, y (both between 0 and 1) domain = Domain.make(["a", "b"], ["x", "y"], [(0, 1), (0, 1)]) a, b = domain.get_bool_symbols() # Get PySMT symbols for the boolean variables x, y = domain.get_real_symbols() # Get PySMT variables for the continuous variables # Create support support = (a | b) & (~a | ~b) & (x <= y) & domain.get_bounds() # Create weight function (PySMT requires constants to be wrapped, e.g., smt.Real(0.2)) weight_function = smt.Ite(a, smt.Real(0.2), smt.Real(0.8)) * (smt.Ite(x <= 0.5, smt.Real(0.2), 0.2 + y) + smt.Real(0.1)) # Create query query = x <= y / 2 **Use engine to perform inference** # Create rejection-sampling based engine (no setup required) rejection_engine = RejectionEngine(domain, support, weight_function, sample_count=100000) print("Volume (Rejection): ", rejection_engine.compute_volume()) # Compute the weighted model integral print("Query probability (Rejection):", rejection_engine.compute_probability(query)) # Compute query probability **Use XADD engine (make sure you have installed the prerequisites)** # Create XADD engine (mode resolve refers to the integration algorithm described in # Kolb et al. Efficient symbolic integration for probabilistic inference. IJCAI 2018) # !! Requires XADD solver to be setup (see above) !! xadd_engine = XaddEngine(domain, support, weight_function, mode="resolve") print("Volume (XADD): ", xadd_engine.compute_volume()) # Compute the weighted model integral print("Query probability (XADD): ", xadd_engine.compute_probability(query)) # Compute query probability **Generating uniform samples and their labels** from pywmi.sample import uniform # n: Required number of samples # domain, support: Domain and support defined as above samples = uniform(domain, n) labels = evaluate(samples, support, samples) **Generating weighted positive samples** from pywmi.sample import positive # n: Required number of samples # domain, support, weight: Defining the density as above # Optional: # sample_pool_size: The number of uniformly sampled positive samples to weight and select the samples from # sample_count: The number of samples to draw initially, from which to build the positive pool # max_samples: The maximum number of uniformly sampled samples (positive or negative) to generate before failing # => If max_samples is exceeded a SamplingError will be raised samples, positive_ratio = positive(n, domain, support, weight) **Handle densities and write to files** # Wrap support and weight function (and optionally queries) in a density object density = Density(domain, support, weight_function, [query]) # Density object can be saved to and loaded from files filename = "my_density.json" density.to_file(filename) # Save to file density = Density.from_file(filename) # Load from file **Work from command line** # Compare engines from command line python -m pywmi my_density.json compare rej:n100000 xadd:mresolve # Compute the weighted model integral python -m pywmi my_density.json compare rej:n100000 xadd:mresolve -q 0 # Compute query probability (query at index 0) # Compute volumes and probabilities from command line # You can provide multiple engines and the result of the first engine not to fail will be returned python -m pywmi my_density.json volume rej:n100000 # Compute weighted model integral python -m pywmi my_density.json prob rej:n100000 # Compute all query probabilities # Plot 2-D support python -m pywmi my_density.json plot -o my_density.png Find the complete running example in [pywmi/tests/running_example.py](pywmi/tests/running_example.py) %prep %autosetup -n pywmi-0.7.15 %build %py3_build %install %py3_install install -d -m755 %{buildroot}/%{_pkgdocdir} if [ -d doc ]; then cp -arf doc %{buildroot}/%{_pkgdocdir}; fi if [ -d docs ]; then cp -arf docs %{buildroot}/%{_pkgdocdir}; fi if [ -d example ]; then cp -arf example %{buildroot}/%{_pkgdocdir}; fi if [ -d examples ]; then cp -arf examples %{buildroot}/%{_pkgdocdir}; fi pushd %{buildroot} if [ -d usr/lib ]; then find usr/lib -type f -printf "/%h/%f\n" >> filelist.lst fi if [ -d usr/lib64 ]; then find usr/lib64 -type f -printf "/%h/%f\n" >> filelist.lst fi if [ -d usr/bin ]; then find usr/bin -type f -printf "/%h/%f\n" >> filelist.lst fi if [ -d usr/sbin ]; then find usr/sbin -type f -printf "/%h/%f\n" >> filelist.lst fi touch doclist.lst if [ -d usr/share/man ]; then find usr/share/man -type f -printf "/%h/%f.gz\n" >> doclist.lst fi popd mv %{buildroot}/filelist.lst . mv %{buildroot}/doclist.lst . %files -n python3-pywmi -f filelist.lst %dir %{python3_sitelib}/* %files help -f doclist.lst %{_docdir}/* %changelog * Wed May 31 2023 Python_Bot - 0.7.15-1 - Package Spec generated