congress.z3.z3types module¶

Type translators between Congress and Z3.

class congress.z3.z3types.BoolType¶

Bases: congress.z3.z3types.Z3Type

Transcode boolean in Z3

to_os(val)¶

Transforms a value from Z3 back to python

to_z3(val, strict=False)¶

Transforms a value from OpenStack in a Z3 value

class congress.z3.z3types.DummyType(name, type_instance)¶

Bases: congress.z3.z3types.Z3Type

Dummy type when Z3 not available

to_os(val)¶

Transforms a value from Z3 back to python

to_z3(val, strict=False)¶

Transforms a value from OpenStack in a Z3 value

class congress.z3.z3types.FiniteType(name, domain)¶

Bases: congress.z3.z3types.StringType

Z3 Coding for data_types with a finite number of elements

This is the counterpart to data_types.CongressTypeFiniteDomain.

to_z3(val, strict=False)¶

Transforms a value from OpenStack in a Z3 value

class congress.z3.z3types.IntType(name, size=32)¶

Bases: congress.z3.z3types.Z3Type

Transcode numbers in Z3

to_os(val)¶

Transforms a value from Z3 back to python

to_z3(val, strict=False)¶

Transforms a value from OpenStack in a Z3 value

class congress.z3.z3types.StringType(name, size=16)¶

Bases: congress.z3.z3types.Z3Type

Transcode strings in Z3

reset()¶

Reset internal state of type transformer

to_os(val)¶

Transforms a value from Z3 back to python

to_z3(val, strict=False)¶

Transforms a value from OpenStack in a Z3 value

class congress.z3.z3types.TypeRegistry¶

Bases: object

A registry of Z3 types and their translators

get_translator(name)¶

Return the translator for a given type name

get_type(name)¶

Return a Z3 type given a type name

init()¶

Initialize the registry

register(typ)¶

Registers a new Z3 type

reset()¶

Reset the internal tables of all types

class congress.z3.z3types.Z3Type(name, type_instance)¶

Bases: object

Translate Openstack values to Z3

reset()¶

Reset internal state of type transformer

to_os(val)¶

Transforms a value from Z3 back to python

to_z3(val, strict=False)¶

Transforms a value from OpenStack in a Z3 value

type()¶

Gives back the Z3 type

congress.z3.z3types.z3_to_array(expr)¶

Compiles back a Z3 result to a matrix of values