The datalog_theory module

Transform an AST describing a theory in a Z3 context

class octant.datalog_theory.Z3Theory(rules)

A theory of Z3 rules.

build_relations()

Builds the compiled relations

build_rules()

Compiles rules to Z3

build_theory()

Builds the Z3 theory

compile_atom(variables, atom, env)

Compiles an atom to Z3

compile_expr(variables, expr, env)

Compile an expression to Z3

query(str_query)

Query a relation on the compiled theory

retrieve_data()

Retrieve the network configuration data over the REST api

octant.datalog_theory.main()

Octant entry point

octant.datalog_theory.print_result(query, variables, answers, time_used, show_pretty)

Pretty-print the result of a query