@@ -0,0 +1,1021 @@
+import operator as op%0Afrom functools import singledispatch%0A%0Afrom pysmt.shortcuts import Symbol, Equals%0Afrom pysmt.typing import REAL%0A%0Aimport stl%0A%0Afrom blustl import game%0A%0Adef sl_to_smt(phi:%22SL%22):%0A    store = %7B(s, t): Symbol(f%22%7Bs%7D%5B%7Bt%7D%5D%22, REAL) for s, t in game.vars_in_phi(phi)%7D%0A    return encode(phi, store)%0A    %0AGET_OP = %7B%0A    %22=%22: op.eq,%0A    %22%3E=%22: op.ge,%0A    %22%3C=%22: op.le,%0A    %22%3E%22: op.gt,%0A    %22%3C%22: op.lt,%0A%7D%0A%0A%0A@singledispatch%0Adef encode(psi, s):%0A    raise NotImplementedError(psi)%0A%0A@encode.register(stl.LinEq)%0Adef _(psi, s:dict):%0A    if psi.op == %22=%22:%0A        # There's a bug here...need to fix%0A        raise NotImplementedError%0A    x = sum(float(term.coeff)*(s%5B(term.id, term.time)%5D+0) for term in psi.terms)%0A    return GET_OP%5Bpsi.op%5D(x, psi.const)%0A%0A%0A@encode.register(stl.And)%0Adef _(psi, s:dict):%0A    return stl.andf(*(encode(x, s) for x in psi.args))%0A%0A@encode.register(stl.Or)%0Adef _(psi, s:dict):%0A    return stl.andf(*(encode(x, s) for x in psi.args))%0A%0A@encode.register(stl.Neg)%0Adef _(psi, s:dict):%0A    return ~psi.arg%0A

add sketch of SMT encoding