teaching/mtl-aas
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor fastboolean_eval

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2017-04-20 21:30:23 -07:00
parent 07bf9f50e4
commit efcfbf7f0d
1 changed files with 10 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

25
stl/fastboolean_eval.py
View file

@ -1,4 +1,4 @@
from functools import singledispatch from functools import singledispatch, reduce
from operator import and_, or_ from operator import and_, or_
from bitarray import bitarray from bitarray import bitarray
@ -15,14 +15,9 @@ def pointwise_satf(stl):
raise NotImplementedError raise NotImplementedError
def bool_op(stl, conjunction=False): def bool_op(stl, conjunction=False):
f = and_ if conjunction else or_ binop = and_ if conjunction else or_
def sat_comp(x,t): fs = [pointwise_satf(arg) for arg in stl.args]
sat = bitarray(len(t)) return lambda x, t: reduce(binop, (f(x, t) for f in fs))
sat.setall(True) if conjunction else sat.setall(False)
for arg in stl.args:
sat = f(pointwise_satf(arg)(x, t), sat)
return sat
return sat_comp
@pointwise_satf.register(stl.Or) @pointwise_satf.register(stl.Or)
@ -35,15 +30,15 @@ def _(stl):
return bool_op(stl, conjunction=True) return bool_op(stl, conjunction=True)
def get_times(x, lo, hi, tau):
return [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index]
def temporal_op(stl, lo, hi, conjunction=False): def temporal_op(stl, lo, hi, conjunction=False):
f = bitarray.all if conjunction else bitarray.any fold = bitarray.all if conjunction else bitarray.any
f = pointwise_satf(stl.arg)
def sat_comp(x,t): def sat_comp(x,t):
sat = bitarray() return bitarray([fold(f(x, get_times(x, lo, hi, tau))) for tau in t])
for tau in t:
tau_t = [min(tau + t2, x.index[-1]) for t2 in x[lo:hi].index]
sat.append(f(pointwise_satf(stl.arg)(x, tau_t)))
return sat
return sat_comp return sat_comp