blob: dfa8956d227eecfb50b7e844f5b6d8d4b84861aa (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
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
|
