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

Updated fast boolean

Browse source
This commit is contained in:
Shromona MacBook 2016-12-02 14:27:04 -08:00
parent 92ff8c1526
commit fb80b0c3ce
1 changed files with 0 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

9
stl/fastboolean_eval.py
View file

@ -24,7 +24,6 @@ def _(stl):
val = pointwise_sat(arg)(x, t) | val val = pointwise_sat(arg)(x, t) | val
return val return val
return sat_comp return sat_comp
#return lambda x, t: any(pointwise_sat(arg)(x, t) for arg in stl.args)
@pointwise_sat.register(stl.And) @pointwise_sat.register(stl.And)
@ -35,7 +34,6 @@ def _(stl):
val = pointwise_sat(arg)(x, t) & val val = pointwise_sat(arg)(x, t) & val
return val return val
return sat_comp return sat_comp
#return lambda x, t: all(pointwise_sat(arg)(x, t) for arg in stl.args)
@pointwise_sat.register(stl.F) @pointwise_sat.register(stl.F)
@ -48,8 +46,6 @@ def _(stl):
val = (val << 1) | (pointwise_sat(stl.arg)(x, tau_t) > 0) val = (val << 1) | (pointwise_sat(stl.arg)(x, tau_t) > 0)
return val return val
return sat_comp return sat_comp
#return lambda x, t, val: [pointwise_sat(stl.arg)(x, [min(deltat + t2, x.index[-1])
# for t2 in x[lo:hi].index], 0) for deltat in t]
@pointwise_sat.register(stl.G) @pointwise_sat.register(stl.G)
@ -62,8 +58,6 @@ def _(stl):
val = (val << 1) | (gp.popcount(pointwise_sat(stl.arg)(x, tau_t)) == len(tau_t)) val = (val << 1) | (gp.popcount(pointwise_sat(stl.arg)(x, tau_t)) == len(tau_t))
return val return val
return sat_comp return sat_comp
#return lambda x, t: all((pointwise_sat(stl.arg)(x, min(t + t2, x.index[-1]))
# for t2 in x[lo:hi].index))
@pointwise_sat.register(stl.Neg) @pointwise_sat.register(stl.Neg)
@ -72,7 +66,6 @@ def _(stl):
val = pointwise_sat(arg)(x, t) ^ (2**(len(t))-1) val = pointwise_sat(arg)(x, t) ^ (2**(len(t))-1)
return val return val
return sat_comp return sat_comp
#return lambda x, t: pointwise_sat(arg)(x, t, val)
op_lookup = { op_lookup = {
@ -92,7 +85,6 @@ def _(stl):
val = (val << 1) | (1 if x[stl.id][tau] else 0) val = (val << 1) | (1 if x[stl.id][tau] else 0)
return val return val
return sat_comp return sat_comp
#return lambda x, t, val: [(val << 1) | (x[stl.id][deltat] == True) for deltat in t]
@pointwise_sat.register(stl.LinEq) @pointwise_sat.register(stl.LinEq)
@ -104,7 +96,6 @@ def _(stl):
val = (val << 1) | (op(eval_terms(stl, x, tau), stl.const) == True) val = (val << 1) | (op(eval_terms(stl, x, tau), stl.const) == True)
return val return val
return sat_comp return sat_comp
#return lambda x, t, val: [(val << 1) |(op(eval_terms(stl, x, deltat), stl.const) == True) for deltat in t]
def eval_terms(lineq, x, t): def eval_terms(lineq, x, t):