add missing new_value_eh when repaired up

Signed-off-by: Nikolaj Bjorner <[email protected]>

Author: NikolajBjorner

src/ast/sls/sls_seq_plugin.cpp

@@ -15,7 +15,7 @@ Module Name:
 
 Notes:
 
-- regex
+Regex
   Assume regexes are ground and for zstring.
   to repair: 
      x in R
@@ -28,11 +28,29 @@ Module Name:
        - sample extension of x that is not in R
        - sample prefix of x in R, with extension not in R
 
-- sequences
-
-- use length constraints as tabu for updates.
-
-- alternate to lookahead strategy:
+     next_tokens(R) = { a | exists s: as in R }
+     delta(a, R) = derivative of R with respect to a.
+     delta(s, R) = delta(s[n-1], delta(s[0..n-2], R))
+     nullable(R) = epsilon in R
+     empty(R) = R is empty
+
+     samples(x, R): 
+        yield choose(R)
+        for i in 0..|x|-1 & delta(x[0..i], R) != empty:
+           yield x[0..i]choose(delta(x[0..i], R))
+         
+     choose(R):
+       if nullable(R):
+          return epsilon
+       T = next_tokens(R)
+       a = choose(T)  use a bias on characters that make progress (skip *).
+       return choose(delta(a, R))
+
+Sequences
+
+Use length constraints as tabu for updates.
+
+Alternate to lookahead strategy:
   Lookahead repair based of changing leaves:
   With each predicate, track the leaves of non-value arguments.
   Suppose x is a leaf string used in a violated predicate.
@@ -51,6 +69,9 @@ Module Name:
     - label each eval subterm by a timestamp that gets set.
     - strval0 evaluates to strval1 if timestamp matches global timestamp.
     
+Revert bias on long strings:
+- give preference to reset leaves that are assigned to long strings
+- bake in bias for shorter strings into equation solving?
 --*/
 
 #include "ast/sls/sls_seq_plugin.h"