Notes

Passing query results to Python script

Convert to Python source code

Use ${query_val$} in an interpolated string (enclosed in '''). Simple types (numeric, boolean, string) are converted to their string representation. Lists and tuples are represented as Python lists and tuples. Java objects from the instance model are converted to an integer ID.

If queries are extended to include Java objects that are not part of the instance model, the approach for generating IDs needs to be changed. Currently, we generate an ID for each object in the instance model and use a lookup table to get the ID corresponding to an object.

Pass Java object to Python

Use ${:query_val$} in an interpolated string (enclosed in '''). This makes all Java methods available in Python. However, each access to the data requires a call to Java, which is inefficient. Fields a Java object can be accessed via py4j.java_gateway.get_field(java_object, field_name).

Convert an ID to the corresponding Java object

The Python script has access to a global variable to_java that contains a reference to the Java mapper object. Use to_java.getInstanceObject(id) in python to get the Java object for the given id.

See more py4j documentation at https://www.py4j.org/contents.html

Declarations for Z3

Z3 variables are declared in Python code, ideally in a domain. SMT expressions can also be declared there.

domain schedulability {
    queries
        val count = ...;
    declarations 
        '''
        Periods = IntVector('period', ${count$})
        Deadlines = IntVector('deadline', ${count$}) 
        Responses = IntVector('response', ${count$})
        responses_leq_deadlines = [Deadlines[i] <= Periods[i] for i in range(len(Deadlines))]
        '''
}

SMT expressions can be the return value of a Python function:

def gen_smt(count):
    return [Deadlines[i] <= Periods[i] for i in range(count)]