test for corner cases

[GoogleCodeExporter]

Hi, I have written a haskell script to automatically generate lots tests for 
isSatisfiable() for corner cases. That is, all that consist of two binary 
operants. All possible relations between varaibles, as well as all combinations 
with negations have been established. There are 152 726 test cases in total.

I first had the idea of outputting all of them into a .java file, but java 
cannot handle that. For 500 test cases, it works, though. I'll include the 
script and the output of 500 test cases with this message.

If someone feels like including the test here, feel free to contact me.

For know, I suppose writing everything in some data file and reading it from a 
testcase is the best idea. I can generate any format you'd like with haskell, 
but I can't write a testcase in java to read stuff in.

Btw, why are we posting in English?

Original issue reported on code.google.com by Wob...@gmx.de on 24 Jun 2012 at 7:53

Attachments:

• genSatTestsFabian.hs
• SatCornerCasesTestFabian.java

[GoogleCodeExporter]

Hi, can you generate two files for me:
one with all satisfiable formulas, one with all unsatisfiable formulas?
Just one line per formula, nothing else.

I can write the test to check them all.

English: Because every programmer is used to that :)

Original comment by felix@familie-freiberger.net on 24 Jun 2012 at 7:57

• Changed state: Accepted

[GoogleCodeExporter]

Done. Haskell is greak!

Original comment by Wob...@gmx.de on 24 Jun 2012 at 8:14

Attachments:

• sat.txt
• unsat.txt

[GoogleCodeExporter]

Whoops, that are big test-files. I'll see what I can do. Can I mention your 
name in the test?

Original comment by felix@familie-freiberger.net on 24 Jun 2012 at 8:16

[GoogleCodeExporter]

Thanks for taking care of the boring stuff! And for the test suite in general!

Btw feel free to mention me in the test case :-) (Fabian Wobito)

Original comment by Wob...@gmx.de on 24 Jun 2012 at 8:16

[GoogleCodeExporter]

OK, the test is ready. Can you check it is working for you?
Just open SatSolverTestUpdateTool and set "OWN_CHANNEL = 1". Then, you will get 
beta-versions of tests, including this one.
For me, the test is not yet working, but that is definitely because my 
implementation is wrong.

Original comment by felix@familie-freiberger.net on 24 Jun 2012 at 8:50

[GoogleCodeExporter]

Yess, finally,

I can verify that the data is most definitely correct. It runs. Also, thanks 
for showing me a slight bug in my implementation.

TestIntegrationSat1 takes 87 seconds over here.
I think I should rewrite the testing -- buffering the tests in a linkedlist is 
not a good idea. It should run faster then.
Also, a little notification would be nice. Maybe I'll make a notification when 
test #8304, #16608, #33216 and #66432 are complete.

I'll push it tomorrow onto the main channel.

Original comment by Nichmen...@gmail.com on 24 Jun 2012 at 10:58

• Changed state: Started

[GoogleCodeExporter]

The test is now live, although it can still be improved, as Ben suggested.

Original comment by felix@familie-freiberger.net on 25 Jun 2012 at 5:27

• Changed state: Added

[GoogleCodeExporter]

The test is working for me. All tests together take 38s (and my machine is 
really slow!). Probably, you've stuffed your code with tons of checks and 
asserts, but in this lecture that's the way to go, I guess.

I can assure you that changing how the test are buffered will not make the 
tests significantly faster, so don't waste your time with it (unless you really 
want, of course). Either way, some progress notification would be comfortable.

Original comment by Wob...@gmx.de on 25 Jun 2012 at 6:43

[GoogleCodeExporter]

If I didn't hit the wrong buttons, the test is already live as 
"IntegrationFelixTest.java". Your example files should have been deployed 
automatically to examples|Fabian|. Please, let me know if the auto-deployment 
is not working for you.

Original comment by felix@familie-freiberger.net on 25 Jun 2012 at 6:52