congress.z3.typechecker module

A static Datalog typechecker.

It is mandatory for Z3, but should be usable by the standard engine. Everything should be typable as we can always assign CongressStr as a catch-all type.

The typechecker works as follows:

  • Types are stored in theories schema.

  • First we reset all types to bottom in theories that we want to type-check. The type-checker must not change the types in other theories. The bottom type is None with nullability set to False. It must be set explicitly because otherwise the default type is scalar, True which corresponds to the top type in the type hierarchy.

  • We prepare a type environment for each rule (identified by rule.id).that contains the type of the variables (again a cell initialized to the bottom type)

  • First we type facts. Then we type rules iteratively. A work phase types all the rules in the theories. Typing a rule means propagating constraints in atoms. head and body atoms are treated with the same algorithm.

  • We request types to be the same when we solve a constraint or to be in direct subtype relation. In that case we take the most precise type. The reason for this is that we do not precisely constrain constants in programs. Their type will be forced by the constraints from external tables. Verification will occur when we translate the value to Z3.

  • Types from external tables cannot be constrained. If the type of an external table should be changed, typing fails.

  • built-ins support will be added in the future. It is the only tricky point as we usually need polymorphism for equalities, tests, some numeric operations that can operate on various size of integers.

  • convergence: there is a finite number of type cells (one per column for tables and one per variable for rules). We iterate only if the type of at least one type cell has been made more precise. There are only finite ascending chains of types if the type hierarchy is well founded (and it is ultimately based on python inheritance hierarchy which is well-founded).

class congress.z3.typechecker.Typechecker(theories, world)

Bases: object

Typechecks a set of theories

constrain_type(cell, typ)

Constrains the type set in a type cell

reset_type_environment()

Reset the type environment for all variables in rules

reset_types()

Set all types in theory to typechecks to bottom

set_nullable(cell)

Force type to be nullable

type_all()

Iterative typechecker

type_cells(cell1, cell2, strict)

Propagates type constraints between two type cells

Updates work if a change has been made.

Parameters

  • cell1 – type cell to constrain

  • cell2 – type cell to constrain

  • strict – boolean, true if cell2 is from an external table and cannot be changed.

Returns

None if ok, the text of an error otherwise.

type_constant(value, column)

Types a constant and set the constraint

type_facts(theory)

Types the facts taking the best plausible type from arguments

type_rule(theory, rule)

One type iteration over a single rule

congress.z3.typechecker.min_type(name1, name2, strict)

Given two type names, gives back the most precise one or None.

If one of the type is more precise than the other, give it back otherwise gives back None. strict implies that the second type cannot be constrained. Usually because it is defined in an external table.