Sat4j
  1. Sat4j
  2. SAT-35

LexicoHelper constructors are incorrect when explain option is set to true

    Details

    • Type: Bug Bug
    • Status: Resolved
    • Priority: Major Major
    • Resolution: Fixed
    • Affects Version/s: 2.3.0
    • Fix Version/s: 2.3.1
    • Component/s: pseudo
    • Security Level: Public (Everybody can see)
    • Labels:
      None

      Description

      The LexicoHelper class keeps track of the PBSolverDecorator used in the LexicoDecorator object.
      The object gathered when setting the xplain flag to true is not a PBSolverDecorator but an XplainPB.
      As such, an exception is launched when the explanation is enabled.

      See here a trace of the error shown in p2cudf:
      org.sat4j.pb.tools.XplainPB cannot be cast to org.sat4j.pb.PBSolverDecorator
      Exception in thread "Thread-0" java.lang.NullPointerException
      at org.eclipse.equinox.p2.cudf.solver.Projector.stopSolver(Projector.java:490)
      at org.eclipse.equinox.p2.cudf.solver.SimplePlanner.stopSolver(SimplePlanner.java:61)
      at org.eclipse.equinox.p2.cudf.Main$1.run(Main.java:55)

        Activity

        Hide
        Daniel Le Berre added a comment -

        Fixed in r989.

        Show
        Daniel Le Berre added a comment - Fixed in r989.

          People

          • Assignee:
            Daniel Le Berre
            Reporter:
            Daniel Le Berre
          • Votes:
            0 Vote for this issue
            Watchers:
            0 Start watching this issue

            Dates

            • Created:
              Updated:
              Resolved:

              Development