Hampi bug investigation

[Tim Hinrichs]

Hi all,

I asked a colleague to investigate one of the Hampi bugs that were
giving us trouble--the one that results in incorrect
unsatisfiability. It's issue 1 on google-code.

http://code.google.com/p/hampi/issues/detail?id=1

Here's his analysis. We're hoping it's enough of a lead that someone
more familiar with the code might be able to implement a fix easily.

As far as I can tell the unsatisfiability bug happens in
HContraintPreparer.java and GrammarStringBounder.java.
HContraintPreparer has a function called prepareSizeFixRegexp() which
creates a GrammarStringBounder and calls getBoundedRegexp() on it.
getBoundedRegexp() then goes on to call internalGetBoundedRegexp().
internalGetBoundedRegexp() then fails to compute the bounds properly
for some reason I'm not sure about and returns null, which propagates
all the way back to prepareSizeFixRegexp(), which in turn after seeing
null throws an unsatisfiability exception.

Tim

[Devdatta]

Hi

I got some time today to investigate this. Like Tim, I had also
noticed this problem in the past.

summary for the people only interested in the fix :
The bug is src/hampi/utils/PigeonHoleDistributor.java. Comment out
line number 148 "continue firstHoleAllocation;" and the examples given
at Issue 1 work just fine.
------

The bug is in the permutations Hampi generates for a given max length.
At line 148 src/hampi/utils/PigeonHoleDistributor.java , there is an
optimization that skips a possibility if a permutation with that
element already exists.This is wrong. The problem is as below :

consider permutations for 13.
It tries permutations with first hole having 1 pigeon, finds (1,1,11)
(1,2,10) (1,3,9) (1,4,10) (1,5,7) (1,6,6)
After this, it skips all permutations with first hole having 2,3,4,..
permutations. But there are permutations with 2 in them that do not
have 1.(5,6,2) It misses these permutations and Hampi fails with an
unsat.

-----------

Adam : I don't know how to run perf-tests, so I haven't committed this
change. If you figure out a better way to fix this , or you think this
is the only fix , push it in.

Cheers
Devdatta

It figures out 5,7,1 and thus skips all other attempts at permutations
with first hole having 5 pigeons. Thus it misses out on

[Adam Kiezun]

Devdatta, Tim,
Thanks for looking into this. Can you run the tests: make verify to
check if the fix works? If yes, feel free to check it in. Correctness
trumps speed here.
./adam

[Devdatta]

Hi

make verify fails as some test runs out of memory, which is
unsurprising as it now has a lot more cases to deal with. But all the
regex-Hampi tests succeed. My Java foo isn't good enough to figure out
which test exactly failed. :(

I think this is a problem with the pigeonHole distributor :
for e.g, if we have
q1 := q2 q3 q5;
q1 has a bound of 13
q2 := "Apple"

it tries all possibilities for q2 in the distributor (although it
should realise that q2 can only be 6). This is related to issue#3 in
the issues list.

-devdatta

[Adam Kiezun]

Thanks Devdatta,
Your diagnosis is correct. I annotated issue#1 with my comments:
http://code.google.com/p/hampi/issues/detail?id=1

I'll try to find some time to fix both.
./adam

[Adam Kiezun]

The workaround for now is to inline the constant string, eg for
badcase1 in issue1:
cfg q3 := [\032 - \126];
cfg q4 := (q3)*;
cfg q6 := [\032 - \126];
cfg q7 := (q6)*;
cfg q1 := "Apple" q4 "Mobile" q7 "Safari";
cfg flax0 := q1;

./adam