Sat4j
  1. Sat4j
  2. SAT-34

Make sure that all solvers return a unit clause in addClause

    Details

    • Type: Improvement Improvement
    • Status: Resolved
    • Priority: Major Major
    • Resolution: Fixed
    • Affects Version/s: 2.2.2, 2.2.3, 2.3.0
    • Fix Version/s: 2.3.1
    • Component/s: core
    • Security Level: Public (Everybody can see)
    • Labels:
      None

      Description

      In many cases, to allow the end user to easily remove unit clauses or constraints that propagate literals, we retour UnitClause or UnitClauses objects in the addXxxx() methods.

      However, especially in the simple SAT case, that behavior is not enforced for all DataStructureFactory.

      We thus need to make sure that all DSF do return a UnitClause object instead of null when a unit clause is detected.

        Activity

        Hide
        Daniel Le Berre added a comment -

        Should be fixed in r987. See tests BugSAT34 in both core and pb projects.

        Show
        Daniel Le Berre added a comment - Should be fixed in r987. See tests BugSAT34 in both core and pb projects.

          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