Beta review

[GoogleCodeExporter]

I tested the beta tests ^^. After finding some bugs on my side, I get the 
impression that they are correct. I have some remarks on CnfContentBewiedTest:

* ListeningBewiedClause should not build clauses containing null literals, see
https://forum.st.cs.uni-saarland.de/boards/viewthread?thread=1527
Better use some dummy name instead (tested it with MyDummy)

* The Messages of assertPureIsAny print the object name of the cnf and literal, 
instead of a human-readable string representation. The same goes for the 
methods above.

* I would suggest to put a dynamically typed toStr method in TestUtilFelix, 
that would call cnfToString, literalToString... depending on the type of the 
argument. Like this:

public static String toStr(Object o) {
    if (o instanceof Literal) return literalToString((Literal)o);
    if (o instanceof Clause)  return  clauseToString((Clause)o);
    if (o instanceof Cnf)     return     cnfToString((Cnf)o);
    throw new IllegalArgumentException("toStr: bad object type");
}

Besides, after seeing how Ben passes around closures, I get the impression that 
using scala or jython could make the tests much better readable (and easier to 
write, too). When I have time, I'll check out if that's possible. 

Original issue reported on code.google.com by Wob...@gmx.de on 3 Jul 2012 at 3:44

[GoogleCodeExporter]

* ListeningBewiedClause: I'll probably just call super with 
createPositiveLiteral(createVariable(VariableNameGenerator.getVariableName())). 
Thanks for the heads up!

* Already reported by Felix.
There are multiple other issues with this test, like other bad comments, 
missing documentation, bad readability, and even tests that are "over shooting" 
the specification.
I'll need a bit time to do all this. But please report any further issues you 
can find, I'll upload a new version soon.

* toStr: Can be done via method overloading, like:

public static String toString(Cnf cnf) {
    return cnfToString(cnf);
}
public static String toString(Clause c) {
    return clauseToString(cnf);
} // Etc.

But what would be the direct benefit of this?

* Scala and jython:

I. Hate. Java.

And even though I'd like to stick with it, since this is a project in Java, and 
it would be nice to distribute the SOURCE that can be hand-edited by users, and 
compiled by anyone.

On the other hand: Lisp Macros would come in handy here.

Original comment by Nichmen...@gmail.com on 3 Jul 2012 at 4:33

• Changed state: Accepted

[GoogleCodeExporter]

I agree to Ben here: This is a Java project, and our update tool distributes 
Java source code. Any other language is OK to generate test files, but the 
tests itself must be in pure Java 6.

Original comment by felix@familie-freiberger.net on 4 Jul 2012 at 2:01

[GoogleCodeExporter]

Updated CnfContentBewiedTest.

Are there still any loopholes?

Original comment by Nichmen...@gmail.com on 4 Jul 2012 at 9:40

• Changed state: Started

[GoogleCodeExporter]

Closing as this ticket is no longer relevant.

Original comment by Nichmen...@gmail.com on 9 Jul 2012 at 8:46

• Changed state: Fixed