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

abstract to_os(val)

Transforms a value from Z3 back to python

abstract 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