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

keep in lining fast boolean eval bitarray calls

Browse source
This commit is contained in:
Marcell Vazquez-Chanlatte 2017-04-20 21:40:31 -07:00
parent efcfbf7f0d
commit 5eb3674d95
1 changed files with 4 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

16
stl/fastboolean_eval.py
View file

@ -38,7 +38,7 @@ def temporal_op(stl, lo, hi, conjunction=False):
fold = bitarray.all if conjunction else bitarray.any fold = bitarray.all if conjunction else bitarray.any
f = pointwise_satf(stl.arg) f = pointwise_satf(stl.arg)
def sat_comp(x,t): def sat_comp(x,t):
return bitarray([fold(f(x, get_times(x, lo, hi, tau))) for tau in t]) return bitarray(fold(f(x, get_times(x, lo, hi, tau))) for tau in t)
return sat_comp return sat_comp
@ -61,18 +61,10 @@ def _(stl):
@pointwise_satf.register(stl.AtomicPred) @pointwise_satf.register(stl.AtomicPred)
def _(stl): def _(stl):
def sat_comp(x, t): return lambda x, t: bitarray(x[str(stl.id)][tau] for tau in t)
sat = bitarray()
[sat.append(x[str(stl.id)][tau]) for tau in t]
return sat
return sat_comp
@pointwise_satf.register(stl.LinEq) @pointwise_satf.register(stl.LinEq)
def _(stl): def _(stl):
op = op_lookup[stl.op] op = lambda a: op_lookup[stl.op](a, stl.const)
def sat_comp(x, t): return lambda x, t: bitarray(op(eval_terms(stl, x, tau)) for tau in t)
sat = bitarray()
[sat.append(op(eval_terms(stl, x, tau), stl.const)) for tau in t]
return sat
return sat_comp