search

sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
106 stars 29 forks source link

monosat.aiger? #10

Closed copumpkin closed 6 years ago

copumpkin commented 6 years ago

Hi! This project is awesome. Thanks for the great work!

I'm packaging monosat in nixpkgs, should handle some of the more annoying issues with pypi and other packaging not handling the native dependencies.

While packaging the python module, I noticed that one of its tests seems to refer to a .aiger module that I can't find anywhere in the source. Did something get removed or refactored?

======================================================================
ERROR: cnf (unittest.loader._FailedTest)
----------------------------------------------------------------------
ImportError: Failed to import test module: cnf
Traceback (most recent call last):
  File "/nix/store/89ammdpygm0cx2y4184x4kfvsncc0dsr-python3-3.6.5/lib/python3.6/unittest/loader.py", line 153, in loadTestsFromName
    module = __import__(module_name)
  File "/private/tmp/nix-build-python3.6-monosat-1nx3wh3.drv-0/source/src/monosat/api/python/monosat/cnf.py", line 24, in <module>
    from monosat.aiger import *
ModuleNotFoundError: No module named 'monosat.aiger'

You can find it here.

Edit: the monosat.graphcircuit module referenced right below it also seems to be an orphan. Is that cnf module still used?

copumpkin commented 6 years ago

Hmm, now I'm just confused why unittest is trying to load cnf at all. It seems to be unreferenced anywhere and it doesn't start with test*. Anyway, for now I'll just manually exclude it.

sambayless commented 6 years ago

The aiger and cnf modules are obsolete and should be removed entirely. The unit tests should definitely not be referring to them.

I'll fix this shortly, but in the meantime your workaround sounds good to me.

Also - thank you for doing this!

On Sun, Jul 8, 2018, 8:45 AM Daniel Peebles notifications@github.com wrote:

Hmm, now I'm just confused why unittest is trying to load cnf at all. It seems to be unreferenced anywhere and it doesn't start with test*. Anyway, for now I'll just manually exclude it.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/sambayless/monosat/issues/10#issuecomment-403296479, or mute the thread https://github.com/notifications/unsubscribe-auth/AALiCk7Fw-fH5CGIxDTpE4K2wk6xG7wwks5uEij8gaJpZM4VGw2q .

copumpkin commented 6 years ago

Thanks! Indeed as soon as I removed cnf.py from the source tree, unittest stopped wanting to import it. Not sure why my machinery moans about it and your tests on Travis don't, but 🤷‍♂️

copumpkin commented 6 years ago

Not strictly related to this ticket, but if you're curious what the package looks like, here it is:

https://github.com/NixOS/nixpkgs/commit/631dd7a4e974547b9ff483401e5256fa5aa3797e