search

warthog-logic / warthog

A Logic Framework in Scala
16 stars 5 forks source link

getModel of Picosat class throws UnsupportedOperationException when using formulas containing no variables #2

Closed ghost closed 12 years ago

ghost commented 12 years ago

The code of the getModel method of the Picosat class uses the reduceLeft method which does not support a empty list. The list created in the getModel method contains the assigned variables of the Picosat-Solver. If the formula, previously added to the Picosat-Solver, however does not contain a variable, the reduceLeft method will throw an error.

This holds for all formulas which are satisfiable (formulas which are unsatisfiable will be treated correctly), and also for the empty formula.

Below are some examples:

// Verum formula:

scala> val ps = new Picosat ps: org.warthog.pl.decisionprocedures.satsolver.impl.picosat.Picosat = org.warth og.pl.decisionprocedures.satsolver.impl.picosat.Picosat@d434f0

scala> ps.init scala> ps.add("$true".pl) scala> ps.sat(Infinity) res3: Int = 1 scala> ps.getModel java.lang.UnsupportedOperationException: empty.reduceLeft [...]

// Falsum formula:

scala> ps.reset scala> ps.init scala> ps.add("$false".pl) scala> ps.sat(Infinity) res9: Int = -1 scala> ps.getModel res10: org.warthog.generic.formulas.Formula[org.warthog.pl.formulas.PL] = ?

// '?' should be a falsum, the the windows console can not display the character

// Empty formula:

scala> ps.reset scala> ps.init scala> ps.sat(Infinity) res13: Int = 1 scala> ps.getModel java.lang.UnsupportedOperationException: empty.reduceLeft

kuebler commented 12 years ago

fixed