From 79bf4f4d20d944660d3ecc9bb00e0e18e8c989ae Mon Sep 17 00:00:00 2001
From: Marcell Vazquez-Chanlatte <mvc@linux.com>
Date: Fri, 7 Oct 2016 02:01:00 -0700
Subject: [PATCH] start work on binary search for param synth + add
 indeterminate names

---
 parser.py     |  4 ++--
 robustness.py | 27 +++++++++++++++++++++++++++
 2 files changed, 29 insertions(+), 2 deletions(-)

diff --git a/parser.py b/parser.py
index c45f9dc..f04500f 100644
--- a/parser.py
+++ b/parser.py
@@ -49,8 +49,8 @@ prime = "'"
 
 pm = "+" / "-"
 dt = "dt"
-unbound = "?"
-id = ~r"[a-zA-z\d]*"
+unbound = "?" id
+id = ~r"[a-zA-z\d]+"
 const = ~r"[\+\-]?\d*(\.\d+)?"
 op = ">=" / "<=" / "<" / ">" / "="
 _ = ~r"\s"+
diff --git a/robustness.py b/robustness.py
index 994303f..aaf5bbe 100644
--- a/robustness.py
+++ b/robustness.py
@@ -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
+