This document presents the technical architecture of IDP-Z3.
Essentially, the IDP-Z3 components translate the requested inferences on the knowledge base into satisfiability problems that Z3 can solve.
The repository for the web clients is in a separate GitLab repository.
The clients are written in Typescript, using the Angular framework (version 7.1), and the primeNG library of widgets. It uses the Monaco editor. The interactions with the server are controlled by idp.service.ts. The AppSettings file contains important settings, such as the address of the IDP-Z3 sample theories.
The web clients are sent to the browser by the IDP-Z3 server as static files.
The static files are generated by the
/IDP-Z3/deploy.py script as part of the deployment, and saved in the
See the Appendix of Development and deployment guide on the wiki for a discussion on how to set-up your environment to develop web clients.
/docs/zettlr/REST.md file describes the format of the data exchanged between the web client and the server. The exchange of data while using web clients can be visualised in the developer mode of most browsers (Chrome, Mozilla, …).
The web clients could be packaged into an executable using nativefier.
Read The Docs, Homepage¶
The online documentation and Homepage are written in ReStructuredText, generated using sphinx and hosted on readthedocs.org and GitLab Pages respectively. The contents is in the
/homepage folders of IDP-Z3.
The code for the IDP-Z3 server is in the
The IDP-Z3 server is written in python 3.8, using the Flask framework. Pages are served by
/idp_server/rest.py. Static files are served from the
/idp_server/static directory, including the compiled version of the client software.
At start-up, and every time the idp code is changed on the client, the idp code is sent to the
/meta URL by the client. The server responds with the list of symbols to be displayed. A subsequent call (
/eval) returns the questions to be displayed. After that, when the user clicks on a GUI element, information is sent to the
/eval URL, and the server responds as necessary.
The information given by the user is combined with the idp code (in State.py), and, using adequate inferences, the questions are put in these categories with their associated value (if any):
given: given by the user
universal: always true (or false), per idp code
consequences: consequences of user’s input according to theory
irrelevant: made irrelevant by user’s input
The IDP-Z3 server implements custom inferences such as the computation of relevance (Inferences.py), and the handling of environmental vs. decision variables.
The IDP-Z3 server exposes multiple API endpoints, which are used to communicate information between the interface and server.
POST: Runs an IDP program containing a main block. The program is be executed by the IDP-Z3 directly, and the output is returned. This endpoint is e.g. used to execute the code in the IDP webIDE.
code: IDP code, containing a main block.
A string, containing the output of the IDP-Z3 engine after executing the program.
POST: generate the metaJSON for an IDP program. In the IC, this metaJSON is among others used to correctly lay out the different symbol tiles and to generate extra expanded symbols.
code: IDP code, with or without main block.
title: the title that the IC should have.
symbols: contains information on each symbol used in the IDP program. This information includes symbol name, type, view, …
optionalPropagation: a bool representing if a propagation toggle should be shown in the interface.
manualPropagation: a bool representing if propagation should be manual via a button.
optionalRelevance: a bool representing if a relevance toggle should be shown in the interface.
manualRelevance: a bool representing if relevance computation should be manual via a button.
propagated: contains the information on all the (expanded) symbols.
POST: execute one of IDP-Z3’s inference methods.
method: string containing the method to execute. Supported methods are: propagate, get_range, modelexpand, explain, minimize, and abstract.
code: the IDP code.
active: the active assignments, already input in the interface.
previous_active: the same as the above, sans the last added assignment.
symbol: the name of a symbol, only used for minimize or explain.
value: a value, only used for explain.
field: the applied symbol for which a range must be determined, only for get_range.
minimize: true for minimization, false for maximization.
Global: the global information of the current state of the IC.
A field for every symbol that appears in the IDP program, containing all its information.
Translating knowledge inferences into satisfiability problems that Z3 can solve involves these steps:
parsing the idp code and the info entered by the user,
converting it to the Z3 format,
calling the appropriate method,
formatting the response.
The conversion to the Z3 format is performed by the following passes over the AST generated by the parser:
annotate the nodes by resolving names, and computing some derived information (e.g. type) (
expand quantifiers in the theory, as far as possible. (
when a structure is given, use the interpretation (
a) expand quantifiers based on the structure (grounding); perform type inference as necessary;
b) simplify the theory using the data in the structure and the laws of logic;
c) instantiate the definitions for every calls of the defined symbols (recursively)
convert to Z3, adding the type constraints not enforced by Z3 (
The graph of calls is outlined in
The code is organised by steps, not by classes: for example, all methods to annotate an expression by another are grouped in Annotate.py. We use monkey-patching to attach methods to the classes declared in another module.
Substitute() modifies the AST “in place”. Because the results of step 1-2 are cached, steps 4-7 are done after copying the AST (custom
You may also want to refer to the Z3py reference.
Appendix: Dependencies and Licences¶
The IDP-Z3 tools are published under the GNU LGPL v3 license.
The server software uses the following components (see requirements.txt):
Z3-solver: MIT license
Flask: BSD License (BSD-3-Clause)
flask_restful : BSD license
flask_cors : MIT license
pycallgraph2 : GNU GPLv2
gunicorn : MIT license
textx: MIT license
The client-side software uses the following components: