The datalog_source module

Generic interface for datasources used by theory

class octant.datalog_source.Datasource(types)

Represents the source of facts used by the Datalog interpreter

Parameters:types – Basic types used by the source.
get_table_types(table, fields)

Return the types of the fields for a given table

Parameters:
  • table – the table name
  • fields – a list of field names
Returns:

a list of the type names of the fiels
is_extensible(atom)

Check if the atom uses a table registered in the datasource

Parameters:atom – the atom
Returns:a boolean
register(session, accessors)

Registers a new source.

A source is described by a way to create a sessions and accessors to populate each table. The complete type using Haskell-like existential type (generics with limited scope) would be:

(session: Callable[[], S],
 accessor: Dict[
   str,
   Forall[R,
     Tuple[
       Callable[[S], R],
       Dict[str, Tuple[str, Callable[[R], int | str]]]]]]
) -> None
Parameters:
  • session – a callback () -> S where S is the type of a session.
  • accessors – a map where keys are table (predicate) names and values are pairs of a row accessor of type (S) -> R where R is the type of the internal datasource row representation and a map that associates to each field name of the row a pair of the name of an octant type t and a field accessor of type (R) -> T where T is the source representation of t.
retrieve_table(table_name, fields, mk_relation, extract=None)

Get the facts on the cloud or in the csv cache.

Parameters:
  • table_name – the name of the table to retrieve
  • fields – the list of field names of the table used
  • mk_relation – a callback called on each row an taking a row value as a list of Z3 objects associated to each field and creating a fact in the Z3 context for the row.
  • extract – an optional list of integer indexes defining the args to give back as a result (used by unfolding)
Returns:

None or a list of tuples for the columns requested in extract.
use_cache()

check if it uses the cache

class octant.datalog_source.TableAccessor(session, access, fields)
access

Alias for field number 1

fields

Alias for field number 2

session

Alias for field number 0