congress.z3.z3theory module

A theory that contains rules that must be treated by Z3.

class congress.z3.z3theory.Z3Context

Bases: object

An instance of Z3 defined first by its execution context

compile_all(type_env)

Compile all Z3 theories

compile_atoms(type_env, theory, head, body)

Compile a list of atoms belonging to a single variable scope

As it is used mainly for rules, the head is distinguished.

compile_facts(theory)

Compiles the facts of a theory in Z3 context

compile_query(theory, literal)

compiles a query litteral

Parameters

• theory – theory used as the context of the query

• litteral – the query

Returns

an existentially quantified litteral in Z3 format.

compile_rule(type_env, theory, rule)

compiles a single rule

Parameters

• theory – the theory containing the rule

• rule – the rule to compile.

compile_theory(type_env, theory)

Compiles all the rules of a theory

Parameters

theory – theory to compile. Will be marked clean after.

declare_external_tables()

Declares tables from other theories used in Z3 context

declare_table(theory, tablename)

Declares a new table in Z3 context

declare_tables()

Declares all tables defined in Z3 context

drop(theory)

Unregister a Z3 theory from the context

eval(theory, query)

Solves a query and gives back a raw result

Result is in Z3 ast format with a translator

static get_context()

Gives back the unique instance of this class.

Users should not use the class constructor but this method.

inject(theoryname, tablename)

Inject the values of an external table in the Z3 Context.

Loops over the literal retrieved from a standard query.

register(theory)

Registers a Z3 theory in the context

select(theory, query, find_all)

Query a theory

synchronize_external()

Synchronize all external tables

typecheck()

Typechecker for rules defined

class congress.z3.z3theory.Z3Theory(name=None, abbr=None, schema=None, theories=None, desc=None, owner=None)

Bases: congress.datalog.nonrecursive.RuleHandlingMixin, congress.datalog.base.Theory

Theory for Z3 engine

Z3Theory is a datalog theory interpreted by the Z3 engine instead of the usual congress internal engine.

arity(tablename, modal=None)

Arity of a table

drop()

To call when the theory is forgotten

select(query, find_all=True)

Performs a query

congress.z3.z3theory.congress_constant(val)

Creates an object constant from a value using its type

congress.z3.z3theory.cycle_not_contained_in_z3(theories, cycles)

Check that there is a true cycle not through Z3 theory

A cycle is irreducible if it contains at least one element which is not a Z3Theory for which recursion is allowed. Cycles are represented by lists of qualified table names.

congress.z3.z3theory.retrieve(theory, tablename)

Retrieves all the values of an external table.

Performs a select on the theory with a query computed from the schema of the table.