Conflicts throw unexpected AttributeError

[olofk]

Not totally sure I have set things up correctly, but the following situation me an internal AttributeError instead of raising SatisfiabilityError.

from okonomiyaki.versions import EnpkgVersion
from simplesat.constraints import PrettyPackageStringParser, Requirement
from simplesat.dependency_solver import DependencySolver
from simplesat.errors import SatisfiabilityError
from simplesat.pool import Pool
from simplesat.repository import Repository
from simplesat.request import Request

request     = Request()
requirement = Requirement._from_string('c')
request.install(requirement)

parser = PrettyPackageStringParser(EnpkgVersion.from_string)
pp = parser.parse_to_package
pa = pp('a 0')
pb = pp('b 0; conflicts (a)')
pc = pp('c 0; depends (a, b)')

packages = [pa, pb, pc]

remote_repo = Repository(packages)
inst_repo = Repository([])
pool = Pool([remote_repo, inst_repo])

solver = DependencySolver(pool, remote_repo, inst_repo)

Stack trace

Traceback (most recent call last):
  File "con.py", line 31, in <module>
    s = requirements_are_satisfiable(packages, [requirement])
  File "/home/olof/code/sat-solver/simplesat/dependency_solver.py", line 139, in requirements_are_satisfiable
    DependencySolver(pool, repositories, []).solve(request)
  File "/home/olof/code/sat-solver/simplesat/dependency_solver.py", line 237, in solve
solution = sat_solver.search()
  File "/home/olof/code/sat-solver/simplesat/sat/minisat.py", line 446, in search
    raise SatisfiabilityError(conflict)
  File "/home/olof/code/sat-solver/simplesat/errors.py", line 41, in __init__
    super(SatisfiabilityError, self).__init__(self.reason)
  File "/home/olof/code/sat-solver/simplesat/errors.py", line 45, in reason
    return self.unsat.to_string()
  File "/home/olof/code/sat-solver/simplesat/sat/minisat.py", line 241, in to_string
    for clauses in self._conflict_paths)
  File "/home/olof/code/sat-solver/simplesat/sat/minisat.py", line 241, in <genexpr>
    for clauses in self._conflict_paths)
  File "/home/olof/code/sat-solver/simplesat/sat/minisat.py", line 249, in string_from_clauses
    flat_clauses = self.clause_trail(clause) or (clause,)
  File "/home/olof/code/sat-solver/simplesat/sat/minisat.py", line 227, in clause_trail
    if clause.learned:
AttributeError: 'int' object has no attribute 'learned'

[johntyree]

I see it.

c is impossible to install because its dependencies conflict. The solver correctly fails to find a solution, but the code that tries to determine why it failed has a type error in it.

In this particular case, it only finds one conflicting requirement but it's expecting two or more (because it's searching for paths). It has a check for this, but it just returns end_clauses (a tuple of Clause) which is not the same type as the normal return value paths (a tuple of tuple of Clause).

Fix for the unexpected exception is simple, but it won't give you a nice error message without more effort. It seems that we are currently assuming that packages have consistent metadata.

diff --git a/simplesat/sat/minisat.py b/simplesat/sat/minisat.py
index ee442e6..2d0f8b6 100644
--- a/simplesat/sat/minisat.py
+++ b/simplesat/sat/minisat.py
@@ -114,7 +114,7 @@ class UNSAT(object):
         # If there aren't two end points then none of this makes any sense.
         # Just return what we have.
         if len(end_clauses) < 2:
-            return end_clauses
+            return (end_clauses,)

         ends = OrderedDict.fromkeys(end_clauses)
         ends = tuple(ends.keys())

[johntyree]

@olofk oh! You're new! Thanks for opening this issue! :+1:

[olofk]

Thanks for the quick response and fix. Yes, I'm new, and I plan to use sat-solver to solve package dependencies for FPGA/ASIC IP cores in my FuseSoC project. Expect to hit more corner cases as I go on. Will report what I find :)

Right now I'm still digging through the sat-solver codebase to understand more about how to use it for its intended purposes

[johntyree]

Sounds good!

[cournape]

@olofk the latest 0.2.1 release should fix the AttributeError (but not the lack of good error message)