IDP-Z3 is a collection of software components implementing the Knowledge Base paradigm using the IDP language and a Z3 SMT solver.
In the Knowledge Base paradigm, the knowledge about a particular problem domain is encoded using a declarative language, and later used to solve particular problems by applying the appropriate type of reasoning, or “inference”. The inferences include:
model checking: does a particular solution satisfy the laws in the knowledge base ?
model search: extend a partial solution into a full solution
model propagation: find the facts that are common to all solutions that extend a partial one
The IDP-Z3 components together enable the creation of these solutions:
the Interactive Consultant, which allow a knowledge expert to enter knowledge about a particular problem domain, and an end user to interactively find solutions for particular problem instances;
a program with a command line interface to compute inferences on a knowledge base;
a web-based Interactive Development Environment (IDE) to create Knowledge bases.
You may want to verify that you are seeing the documentation relevant for the version of IDP-Z3 you are using. On readthedocs, you can see the version under the title (top left corner), and you can change it using the listbox at the bottom left corner.
Installation using poetry¶
Poetry is a package manager for python.
Install python3 on your machine
after that, logout and login if requested, to update
Use git to clone https://gitlab.com/krr/IDP-Z3 to a directory on your machine
Open a terminal in that directory
If you have several versions of python3, and want to run on a particular one, e.g., 3.9:
poetry env use 3.9
python3.9in the commands below
To launch the Interactive Consultant web server:
open a terminal in that directory and run
poetry run python3 main.py
After that, you can open
Installation using pip¶
IDP-Z3 can be installed using the python package ecosystem.
use git to clone https://gitlab.com/krr/IDP-Z3 to a directory on your machine
(For Linux and MacOS) open a terminal in that directory and run the following commands.
python3 -m venv . source bin/activate python3 -m pip install -r requirements.txt
(For Windows) open a terminal in that directory and run the following commands.
python3 -m venv . .\Scripts\activate python3 -m pip install -r requirements.txt
To launch the web server on Linux/MacOS, run
source bin/activate python3 main.py
On Windows, the commands are:
.\Scripts\activate python3 main.py
After that, you can open
Installation of idp_solver module¶
The idp_solver module is available for installation through the official Python package repository.
This comes with a command line program,
idp_solver that functions as described in Command Line Interface.
To install the module via poetry, the following commands can be used to add the module, and then install it.
poetry add idp_solver poetry install
Installing the module via pip can be done as such:
pip3 install idp_solver