[hampi-devel] subsequence and string length

[Adam Kiezun]

Hi all,
We're working on an implementation of sub-string extraction, and an
idea emerged that perhaps we should support string-length expressions.
This seems to become important when substrings are used together with
bounded-length variables.

For example
var v : 1..100;

What is being implemented now is fixed-size substrings:
var sub := v[3:5]; //offset 3 length 5
This fixed-size substrings become too limited because, when v is
shorter than 9, the very declaration of sub does not make sense.

So, how do you say that you're interested in suffices of v starting at
offset 3? It's easy with length:
val suff := v[3:length(v)-3]

An alternative for suffixes would be to use notation such as:
val suff1 := v[3:] // start at offset 4, go all the way
but there seems no easy way to extend this notation to prefixes or substrings.

However, if we have length(v), then we'd probably want things like
length(suff), arithmetic (2*(length(v)+3)), and probably arithmetic
constraints eg "assert length(v) / length(sub) = 3"

What is you opinion of whether it is important to support length?
./adam

[Tim Hinrichs]

Hi Adam,

A couple of months ago, I asked Vijay for several extensions to Hampi: (1) multiple variables, (2) fixed-range (as opposed to fixed-size) variables and (3) string-length expressions with arithmetic.  I ended up hacking together a wrapper around Hampi to deal with all 3, which sufficed for the application we were working on only because the constraints we encountered were so simple.  For even relatively interesting constraints, my wrapper's not going to cut it.  In short, we would be excited if Hampi supported what you're suggesting. 

I'm guessing you've seen Kaluza.  I can't quite tell if their constraint language subsumes your extended language.  They handle string-length expressions and arithmetic.  They don't handle substrings explicitly but have concatenation (of variables), which might do the trick.  Currently we're planning to investigate replacing my wrapper around Hampi with Kaluza; if Hampi is extended I imagine we'd try both and see which works better.

http://webblaze.cs.berkeley.edu/2010/kaluza/

Tim

[Adam Kiezun]

Hi Tim,
(2), fixed-range variables are supported now (there are some remaining
issues but you can try using them).

./adam

[Vijay Ganesh]

On Fri, May 21, 2010 at 11:16 AM, Tim Hinrichs <t...@uchicago.edu> wrote:

> Hi Adam,
>
> A couple of months ago, I asked Vijay for several extensions to Hampi: (1)
> multiple variables, (2) fixed-range (as opposed to fixed-size) variables and
> (3) string-length expressions with arithmetic.  I ended up hacking together
> a wrapper around Hampi to deal with all 3, which sufficed for the
> application we were working on only because the constraints we encountered
> were so simple.  For even relatively interesting constraints, my wrapper's
> not going to cut it.  In short, we would be excited if Hampi supported what
> you're suggesting.
>
> I'm guessing you've seen Kaluza.  I can't quite tell if their constraint
> language subsumes your extended language.  They handle string-length
> expressions and arithmetic.  They don't handle substrings explicitly but
> have concatenation (of variables), which might do the trick.  Currently
> we're planning to investigate replacing my wrapper around Hampi with Kaluza;
> if Hampi is extended I imagine we'd try both and see which works better.
>
> http://webblaze.cs.berkeley.edu/2010/kaluza/

We are definitely aware of Kaluza, since we consulted for Prateek (the
main author of Kaluza) with regard to STP/Hampi support, and
early-stage design discussions.

-Vijay.