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:
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 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:
annotate the nodes by resolving names, and computing some derived information (e.g. type) (
annotate()
)expand quantifiers in the theory, as far as possible. (
interpret()
)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)
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):
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:
ngx-monaco-editor: MIT license
packery: GPL-3.0
primeicons: MIT
isotope-layout: GNU GPL-3.0
isotope-packery: MIT
core-js: MIT
dev: None
git-describe: MIT
rxjs: Apache 2.0
tslib: Apache 2.0
zone.js: MIT