Architecture

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.

Web clients

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 /IDP-Z3/idp_server/static folder.

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.

The /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 /docs and /homepage folders of IDP-Z3.

We use the following sphinx extensions: Mermaid (diagrams), and Markdown.

IDP-Z3 server

The code for the IDP-Z3 server is in the /idp_server folder.

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

  • unknown

The IDP-Z3 server implements custom inferences such as the computation of relevance (Inferences.py), and the handling of environmental vs. decision variables.

IDP-Z3 solver

The code for the IDP-Z3 solver and IDP-Z3-CLI is in the /idp_solver folder. The IDP-Z3 solver exposes an API implemented by Run.py and Problem.py.

Translating knowledge inferences into satisfiability problems that Z3 can solve involves these steps:

  1. parsing the idp code and the info entered by the user,

  2. converting it to the Z3 format,

  3. calling the appropriate method,

  4. formatting the response.

The IDP-Z3 code is parsed into an abstract syntax tree (AST) using the textx package, according to this grammar.  There is one python class per type of AST nodes (see Parse.py and Expression.py)

The conversion to the Z3 format is performed by the following passes over the AST generated by the parser:

  1. annotate the nodes by resolving names, and computing some derived information (e.g. type) (annotate())

  2. expand quantifiers in the theory, as far as possible. (interpret())

  3. when a structure is given, use the interpretation (interpret() ), i.e.:

    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)

  4. convert to Z3, adding the type constraints not enforced by Z3 (.translate())

The graph of calls is outlined in /docs/zettlr/Call graph.md.

The code is organised by steps, not by classes: for example, all methods to substitute an expression by another are grouped in Substitute.py. We use monkey-patching to attach methods to the classes declared in another module.

Important classes of the IDP-Z3 solver are: Expression, Assignment, Problem.

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 copy()).

Z3

See this tutorial for an introduction to Z3 (or this guide).

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

The client-side software uses the following components: