The datalog_compiler module

Transform an AST describing a theory in a Z3 context

class octant.datalog_compiler.Z3Compiler(rules, constants, datasource)

Prepare octant Datalog for compilation to Z3 (extensible tables).

compile(z3compiler)

Compile preprocess high level Datalog.

It removes constants, make variables unique and extract columns used in extensible tables. It also controls the type-checker.

find_base_relations()

Extracts base relations of the theory

flatten(atom, fields)

Replace named arguments with positional args.

Knowing the columns in use for extensible tables, column names are replaced by positions as regular tables.

substitute_constants()

Substitute constants phase

substitutes_constants_in_array(args)

Substitute constants in arguments arrays

exception octant.datalog_compiler.Z3NotWellFormed(*args, **kwargs)

Raised for a theory that do not respect well-formedness rules