from operator import eq


def stl_model_to_cnf(model, aps):
    """ Converts a z3 model for a STL formula into a conjunctive normal form."""
    terms = list()
    for x in aps:
        value = model[x]
        if value is None: continue
        terms += [eq(x, value)]
    return terms