# Introduction¶

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 source code of IDP-Z3 is publicly available under the GNU LGPL v3 license.

Warning

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

• Install poetry

• after that, logout and login if requested, to update \$PATH

• 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:

• run poetry env use 3.9

• replace python3 by python3.9 in the commands below

• Run poetry install

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.

• install python 3, with pip3, making sure that python3 is in the PATH.

• 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