Unsat for correct cases

[GoogleCodeExporter]

Unsat for correct cases

[GoogleCodeExporter]

another example 

Original comment by [email protected] on 21 Feb 2010 at 4:42

Attachments:

• bad3.hmp

[GoogleCodeExporter]

badcase1 reduced:
var string:6;
cfg q1 := "Ap";
cfg q2 := "Mo";
cfg q3 := "Sa";
cfg qx :=  q1 q2 q3;
assert string in qx;
Still gives UNSAT

Original comment by [email protected] on 26 Feb 2010 at 6:59

[GoogleCodeExporter]

As discovered by Devdatta, the problem is in PigeonHoleDistributor, line: if
(is.contains(i)) continue firstHoleAllocation;

So, for bound 6, lowers [1,1,1] uppers[4,4,4], it will first generate 
permutations
[1,4,1], [1,1,4], [1,2,3], [1,3,2] and then skip [2,2,2] because it thinks that 
2 is
already taken care of.

The fix would be to simply remove the broken 'optimization' - the perf impact 
on the
tests is so severe that tests stop working. This bugs must to be fixed with or 
after
issue#3.

Original comment by [email protected] on 26 Feb 2010 at 7:58

[GoogleCodeExporter]

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

Original comment by [email protected] on 26 Feb 2010 at 8:12