CNFFactorisation throws null pointer exception.
d-bischoff opened this issue · 2 comments
Try to run this code:
PropositionalParser parser = new PropositionalParser(f);
Formula f1 = parser.parse("((((var4711&var0815&Multiversum&var494|var4711&var0815&var007|var0815&var007&var494)&~(var4712&Multiversum)&~(var4712&var007&var494)&~Variablenname&~Zorro)&Hura)|(((var4711&var0815&Multiversum&var494|var4711&var0815&var007|var0815&var007&var494)&~(var4712&Multiversum)&~(var4712&var007)&~Variablenname&~Zorro)&Feuerwerk)|((Multiversum&Pistole&~Variablenname&~Zorro)&Hura)|((Multiversum&Pistole&~Variablenname&~Zorro)&Feuerwerk)|((Ix&Wonderwoman&~Variablenname&~Zorro)&Feuerwerk))");
Formula f2 = parser.parse("(Hura&Multiversum&Pistole|Feuerwerk&(Ix&Wonderwoman|Multiversum&Pistole)|var0815&(Hura&var4711&var007&~var494&Multiversum|(Hura|Feuerwerk)&(var494&(var4711&Multiversum|var007)|var4711&var007)&~var4712))&~Variablenname&~Zorro");
Formula equiv = f.equivalence(f1,f2);
System.out.println("Equivalent? "+equiv.holds(new TautologyPredicate(f)));
it produces a NullPointerException.
Exception in thread "main" java.lang.NullPointerException at org.logicng.formulas.FormulaFactory.condenseOperandsAnd(FormulaFactory.java:885) at org.logicng.formulas.FormulaFactory.constructAnd(FormulaFactory.java:423) at org.logicng.formulas.FormulaFactory.and(FormulaFactory.java:392) at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:109) at org.logicng.transformations.cnf.CNFFactorization.apply(CNFFactorization.java:83) at org.logicng.formulas.Formula.transform(Formula.java:222) at org.logicng.transformations.cnf.CNFEncoder.singleAdvancedEncoding(CNFEncoder.java:130) at org.logicng.transformations.cnf.CNFEncoder.advancedEncoding(CNFEncoder.java:126) at org.logicng.transformations.cnf.CNFEncoder.encode(CNFEncoder.java:107) at org.logicng.formulas.Formula.cnf(Formula.java:213) at org.logicng.solvers.MiniSat.add(MiniSat.java:204) at org.logicng.predicates.satisfiability.SATPredicate.test(SATPredicate.java:82) at org.logicng.formulas.Formula.holds(Formula.java:242) at org.logicng.predicates.satisfiability.TautologyPredicate.test(TautologyPredicate.java:77) at org.logicng.formulas.Formula.holds(Formula.java:242)
We were able to fix this instance of the bug by changing line 100ff of class CNFFactorization from
case AND:
nops = new LinkedHashSet<>();
for (final Formula op : formula) {
if (!this.proceed) {
return null;
}
nops.add(this.apply(op, cache);
}
cached = formula.factory().and(nops);
break;
to
case AND:
nops = new LinkedHashSet<>();
for (final Formula op : formula) {
final Formula apply = this.apply(op, cache);
if (!this.proceed) {
return null;
}
nops.add(apply);
}
cached = formula.factory().and(nops);
break;
We believe this is not the whole fix needed for this type of bug. It solves this instance, but CNFFactorization looks like it has multiple places where the proceed check is done too early or should at least be done again.
This really seems to be a bug in the CNFFactorization when a handler is used. I commited a fix with the respective tests in branch fix_cnffactorization.
The problem occurred when apply or distribute are called within a loop and the handler cancels during the last iteration. Then null was added to the list of operands and the proceed-Flag was not checked again. This caused the NullPointerException when conjoining them with f.and().
Fixed with Version 1.0.3.