#418: Add SAT Solvers
--------------------------------------------------------------+-------------
Reporter: malb | Owner:
was
Type: enhancement | Status:
needs_work
Priority: minor | Milestone:
sage-5.1
Component: packages | Resolution:
Keywords: SAT | Work issues:
Report Upstream: Fixed upstream, in a later stable release. | Reviewers:
Authors: Martin Albrecht | Merged in:
Dependencies: | Stopgaps:
--------------------------------------------------------------+-------------
Changes (by AlexanderDreyer):
* status: needs_review => needs_work
Comment:
It seems that interfaces had changes, so the spkg doesn't fit with the
sage library patches.
It seems that your installation picked up the headers from the old
install. Maybe its enough to delete `SAGE_INC+"/cryptominisat/`?
I fixed a few trivial things below, but there's more to be done:
{{{ #!diff
diff -r ef5eaff5d6cd module_list.py
--- a/module_list.py Fri Jun 29 17:04:34 2012 +0100
+++ b/module_list.py Sun Jul 01 23:40:53 2012 +0200
@@ -1891,12 +1891,12 @@
ext_modules.extend([
Extension("sage.sat.solvers.cryptominisat.cryptominisat",
["sage/sat/solvers/cryptominisat/cryptominisat.pyx"],
- include_dirs = [SAGE_INC,
SAGE_INC+"/cryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],
+ include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"],
language = "c++",
libraries = ['cryptominisat', 'z']),
Extension("sage.sat.solvers.cryptominisat.solverconf",
["sage/sat/solvers/cryptominisat/solverconf.pyx",
"sage/sat/solvers/cryptominisat/solverconf_helper.cpp"],
- include_dirs = [SAGE_INC,
SAGE_INC+"/cryptominisat/mtl", SAGE_INC+"/cryptominisat/Solver"],
+ include_dirs = [SAGE_INC, SAGE_INC+"/cmsat/"],
language = "c++",
libraries = ['cryptominisat', 'z'])
])
diff -r ef5eaff5d6cd sage/sat/solvers/cryptominisat/solverconf_helper.h
--- a/sage/sat/solvers/cryptominisat/solverconf_helper.h Fri Jun 29
17:04:34 2012 +0100
+++ b/sage/sat/solvers/cryptominisat/solverconf_helper.h Sun Jul 01
23:40:53 2012 +0200
@@ -14,7 +14,7 @@
* http://www.gnu.org/licenses/
****************************************************************************/
-#include <cryptominisat/Solver/SolverConf.h>
+#include <SolverConf.h>
enum sc_type {
t_int = 1<<0,
}}}
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/418#comment:25>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
