start work on binary search for param synth + add indeterminate names

This commit is contained in:
Marcell Vazquez-Chanlatte 2016-10-07 02:01:00 -07:00
parent 8e728abfa8
commit 79bf4f4d20
2 changed files with 29 additions and 2 deletions

View file

@ -62,3 +62,30 @@ def eval_terms(lineq, x, t):
def eval_term(x, t):
return lambda term: term.coeff*x[term.id.name][t]
def binsearch(stleval, *, tol=1e-3, lo, hi):
"""Only run search if tightest robustness was positive."""
# Only check low since hi taken care of by precondition.
r = stleval(lo)
if r > 0 or abs(r) < tol:
return r, lo
while abs(r) < tol:
mid = lo + (hi - lo) / 2
r = stleval(mid)
if r < 0:
lo, hi = mid, hi
else:
lo, hi = lo, mid
return r, mid
def lex_param_project(stl, x, *, order, polarity, ranges, tol=1e-3):
val = {var: (ranges[0] if polarity[var] else ranges[1]) for var in order}
# TODO: evaluate top paramater
for var in order:
r, param = binsearch() #TODO
# TODO: update val
return val