pmGenerator 1.0 final

pmGenerator-1.0.2-win.7z contains Windows binaries only.

• Compiled by GCC 11.3.0, binaries from winlibs-x86_64-posix-seh-gcc-11.3.0-llvm-14.0.3-mingw-w64msvcrt-10.0.0-r3
• Used oneTBB 2021.8.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Boost 1.81.0 (header-only)
• Used compiler options -O3 -fno-align-functions -fno-align-jumps -fno-align-loops -fno-align-labels -pedantic -Wall -c -m64 -fmessage-length=0 -std=c++20 -D_FILE_OFFSET_BITS=64
• Used linker options -s -Wl,--subsystem,console -fuse-ld=lld -lpthread -ltbb12.dll

Known issues:

• The Windows Command Prompt (CMD) does not support UTF-8 encoded output, e.g. ≈ is printed as Ôëê. [won't fix]
  • You can work around this by redirecting all output into a file like pmGenerator [args] > out.txt 2>&1,
    or by using a different console, e.g. Cygwin64 Terminal that comes with Cygwin (requires ./pmGenerator).

Linux

• Exemplary compiler options -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread
  • Old compiler (on c++11 branch) -O3 -Wall -c -fmessage-length=0 -std=c++11 -pthread
• Exemplary linker options -pthread -ltbb
  • Old Boost version (e.g. 1.53.0 ; on c++11 branch) additionally requires -lboost_system -lboost_filesystem

Exemplary build instructions:

g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o helper/FctHelper.o ../helper/FctHelper.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o helper/IPrintable.o ../helper/IPrintable.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o helper/ProgressData.o ../helper/ProgressData.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o helper/Resources.o ../helper/Resources.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o grammar/CfgGrammar.o ../grammar/CfgGrammar.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o metamath/DRuleParser.o ../metamath/DRuleParser.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o metamath/DRuleReducer.o ../metamath/DRuleReducer.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o nortmann/DlCore.o ../nortmann/DlCore.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o nortmann/DlFormula.o ../nortmann/DlFormula.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o nortmann/DlProofEnumerator.o ../nortmann/DlProofEnumerator.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o nortmann/DlStructure.o ../nortmann/DlStructure.cpp
g++ -I/home/oneTBB/include/ -O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread -o main.o ../main.cpp
g++ -L/home/oneTBB/intel_19.0_cxx11_64_relwithdebinfo/ -pthread -ltbb -o pmGenerator grammar/CfgGrammar.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o nortmann/DlCore.o nortmann/DlFormula.o nortmann/DlProofEnumerator.o nortmann/DlStructure.o

Verified to compile also with Clang/LLVM.