search

cl-model-languages / cl-sat.glucose

CL-SAT instance to Glucose state-of-the-art SAT solver. This downloads the later 2014 version (2nd in the 2014 SAT competition).
3 stars 0 forks source link

installation broken in MacOS #1

Closed arademaker closed 5 years ago

arademaker commented 8 years ago

The automation of the installation of the SAT solver is not working and not necessary. I would remove it and make clear to the users that the systems must be in the PATH. Also, I would combine all APIs in the single system cl-sat.

guicho271828 commented 8 years ago
  1. Regarding the build failure of the solver on Mac, I suppose the Mac specific things can be easily fixed by #ifdef in makefile, I am ready to merge such a pull request. I need an error log, which is helpful if I do the fix by myself.
  2. Regarding the API, Id like to know a bit more detail, which API are you referring to? AFAIK subsystem as a plug-in has been considered successful in libraries like CL-DBI (SQL interface) and clack (web server). One-big-system approach does not work.
guicho271828 commented 5 years ago

Update on this: If you want the latest SAT solver from competitions, use the :competition option in cl-sat.

quicklisp commented 5 years ago

What changed? I get this now: http://report.quicklisp.org/2019-08-06/failure-report/cl-sat.glucose.html#cl-sat.glucose

guicho271828 commented 5 years ago

The glucose server started using https.

guicho271828 commented 5 years ago

this is now fixed.