Mergesat #354
Mergesat #354
Conversation
conp-solutions
force-pushed
the
mergesat
branch
4 times, most recently
from
c3ffb1d
to
f2eb939
Compare
|
The Travis checks fail with an error that is hard to understand given the current output. Interestingly, it does not seem to fail for Riss, alghouth Riss uses almost the same cmake and make invocation. Digging through this might take a while. |
These files are required to combine STP with MergeSat. Essentially, they provide the very same functionality as the MiniSat glue files. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
The new solving backend has to be selectable. Hence, introduce the relevant variables and constants that are also used for the already present SAT backends. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
As MergeSat has the very same SAT interface as MiniSat, and also relies on the same include structure, we can use MergeSat whereever we can use MiniSat. Hence, in case MergeSat is used, do not search for MiniSat at all. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
Instead of always relying on the namespace for the Minisat solver being Minisat, allow to define the namespace at compile time. This allows to replace Minisat more easily with other solvers, e.g. Glucose, that come with a different namespace, but otherwise use the same symbols. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
To make sure we do not break the new SAT backend, add it to the travis build configurations, and build with a known good version of MergeSat. To make sure we do not clash with MiniSat, compile MergeSat with the namespace MergeSat. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
MergeSat has recieved plenty updates. Pick a more recent version for starexec. Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
|
@conp-solutions sorry if this is a silly question, but why are the Riss and MergeSat back-ends only compiled statically? We recently disabled static builds through Travis (as they didn't work). I'd love to get your stuff moving along, but I'd like to not build it statically if possible. I have nothing against the static builds, there's just work to do in getting them reinstated, so I don't want to block your PRs because of that. |
|
There is no clear reason. I quickly managed to produce a static build, hence, i just used that. It might be possible to just drop the static keyword, I simply did not test that route, as static binaries have been the easier approach for the SMT competition. Best, |
|
@conp-solutions do you think we can split off 8e4ff44 into a separate PR? I don't think you need this for this branch (as it seems this branch only has Genuinely, I get the intent, but it makes it hard to see what's Mergesat related vs. that change. If it works like I believe it does, then it would be good to have a CMake option to set which solver to use for |
This series adds MergeSat as another SAT backend. During working on it, I noticed that instead of just adding MergeSat, I could have actually implemented a compile-time replacement strategy for MiniSat.
As I currently only wanted to integrate MergeSat, I'll leave the other task open for now.
This series has not been tested extensively.
This is related to #349