bringing cryptominisat into the main branch

1 files changed, 37 insertions, 0 deletions

diff --git a/src/prop/cryptominisat/HOWTO_VisualCpp b/src/prop/cryptominisat/HOWTO_VisualCpp
new file mode 100644
index 000000000..dfa8956d2
--- /dev/null
+++ b/src/prop/cryptominisat/HOWTO_VisualCpp
@@ -0,0 +1,37 @@
+If compiling with Visual C, the CHUNK_LIMIT poses problems.
+Problem is, that VC2008 seems to have a too small default stack, which is not
+big enough. With default command line parameters it will crash.
+The workaround is to give the command line parameter /F. With this you can
+increase the stack to a certain size. Setting it to 2 MB is good enough
+
+ZLIB might also pose problems. If you cannot correctly compile it under
+windows, I suggest you add the -DDISABLE_ZLIB to your compilation flags.
+
+The compilation instruction should finally be:
+
+64-bit version:
+
+cl /openmp /favor:INTEL64 /O2
+/Fecryptominisat64.exe -DVERSION="__DATE__" -DDISABLE_ZLIB /F2097152 /TP
+/EHsc -I. -I../mtl/ -I../MTRand/ Main.cpp Solver.cpp ClauseCleaner.cpp
+PackedRow.cpp RestartTypeChooser.cpp VarReplacer.cpp XorFinder.cpp
+XorSubsumer.cpp Subsumer.cpp PartFinder.cpp PartHandler.cpp
+FailedLitSearcher.cpp ClauseAllocator.cpp UselessBinRemover.cpp
+StateSaver.cpp ClauseVivifier.cpp SolverMisc.cpp SolverDebug.cpp
+CompleteDetachReattacher.cpp DimacsParser.cpp SCCFinder.cpp SolverConf.cpp
+OnlyNonLearntBins.cpp DataSync.cpp MatrixFinder.cpp Gaussian.cpp BothCache.cpp
+
+32-bit version:
+
+cl /O2 /Fecryptominisat32.exe -DVERSION="__DATE__" -DDISABLE_ZLIB /F2097152
+/TP /EHsc -I. -I../mtl/ -I../MTRand/ Main.cpp Solver.cpp ClauseCleaner.cpp
+PackedRow.cpp RestartTypeChooser.cpp VarReplacer.cpp XorFinder.cpp
+XorSubsumer.cpp Subsumer.cpp PartFinder.cpp PartHandler.cpp
+FailedLitSearcher.cpp ClauseAllocator.cpp UselessBinRemover.cpp
+StateSaver.cpp ClauseVivifier.cpp SolverMisc.cpp SolverDebug.cpp
+CompleteDetachReattacher.cpp DimacsParser.cpp SCCFinder.cpp SolverConf.cpp
+OnlyNonLearntBins.cpp DataSync.cpp MatrixFinder.cpp Gaussian.cpp BothCache.cpp
+
+executed from the 'Solver' subdirectory
+
+--- Build instructions by Martin Maurer