pmGenerator 1.2 (patch 1)

pmGenerator-1.2.1-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.9.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Microsoft MPI 10.1.1-10, library bindings from MSYS2 package mingw-w64-x86_64-msmpi
  • msmpi.dll (version 10.1.12498.18) from Microsoft software installer Microsoft MPI v10.1.2
• 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 -Wconversion -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 -lmsmpi.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
• Exemplary linker options -pthread -ltbb

Exemplary build script:

#!/bin/zsh
cmp='-O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread'
inc='-I/home/oneTBB/include/'
lnk='-pthread -ltbb'
lib='-L/home/oneTBB/intel_19.0_cxx11_64_relwithdebinfo/'
mkdir -p {helper,cryptography,grammar,metamath,logic}
set -x
export I_MPI_CXX=icpx
mpicxx $inc $cmp -o helper/FctHelper.o ../helper/FctHelper.cpp
mpicxx $inc $cmp -o helper/IPrintable.o ../helper/IPrintable.cpp
mpicxx $inc $cmp -o helper/ProgressData.o ../helper/ProgressData.cpp
mpicxx $inc $cmp -o helper/Resources.o ../helper/Resources.cpp
mpicxx $inc $cmp -o cryptography/sha2.o ../cryptography/sha2.cpp
mpicxx $inc $cmp -o grammar/CfgGrammar.o ../grammar/CfgGrammar.cpp
mpicxx $inc $cmp -o metamath/DRuleParser.o ../metamath/DRuleParser.cpp
mpicxx $inc $cmp -o metamath/DRuleReducer.o ../metamath/DRuleReducer.cpp
mpicxx $inc $cmp -o logic/DlCore.o ../logic/DlCore.cpp
mpicxx $inc $cmp -o logic/DlFormula.o ../logic/DlFormula.cpp
mpicxx $inc $cmp -o logic/DlProofEnumerator.o ../logic/DlProofEnumerator.cpp
mpicxx $inc $cmp -o logic/DlStructure.o ../logic/DlStructure.cpp
mpicxx $inc $cmp -o main.o ../main.cpp
mpicxx $lib $lnk -o pmGenerator cryptography/sha2.o grammar/CfgGrammar.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o

Verified to compile with GCC, Clang/LLVM, and MSVC.

pmGenerator 1.2

pmGenerator-1.2.0-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.9.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Microsoft MPI 10.1.1-10, library bindings from MSYS2 package mingw-w64-x86_64-msmpi
  • msmpi.dll (version 10.1.12498.18) from Microsoft software installer Microsoft MPI v10.1.2
• 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 -Wconversion -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 -lmsmpi.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 script:

#!/bin/zsh
cmp='-O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread'
inc='-I/home/oneTBB/include/'
lnk='-pthread -ltbb'
lib='-L/home/oneTBB/intel_19.0_cxx11_64_relwithdebinfo/'
mkdir -p {helper,cryptography,grammar,metamath,logic}
set -x
export I_MPI_CXX=icpx
mpicxx $inc $cmp -o helper/FctHelper.o ../helper/FctHelper.cpp
mpicxx $inc $cmp -o helper/IPrintable.o ../helper/IPrintable.cpp
mpicxx $inc $cmp -o helper/ProgressData.o ../helper/ProgressData.cpp
mpicxx $inc $cmp -o helper/Resources.o ../helper/Resources.cpp
mpicxx $inc $cmp -o cryptography/sha2.o ../cryptography/sha2.cpp
mpicxx $inc $cmp -o grammar/CfgGrammar.o ../grammar/CfgGrammar.cpp
mpicxx $inc $cmp -o metamath/DRuleParser.o ../metamath/DRuleParser.cpp
mpicxx $inc $cmp -o metamath/DRuleReducer.o ../metamath/DRuleReducer.cpp
mpicxx $inc $cmp -o logic/DlCore.o ../logic/DlCore.cpp
mpicxx $inc $cmp -o logic/DlFormula.o ../logic/DlFormula.cpp
mpicxx $inc $cmp -o logic/DlProofEnumerator.o ../logic/DlProofEnumerator.cpp
mpicxx $inc $cmp -o logic/DlStructure.o ../logic/DlStructure.cpp
mpicxx $inc $cmp -o main.o ../main.cpp
mpicxx $lib $lnk -o pmGenerator cryptography/sha2.o grammar/CfgGrammar.o helper/FctHelper.o helper/IPrintable.o helper/ProgressData.o helper/Resources.o main.o metamath/DRuleParser.o metamath/DRuleReducer.o logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o

Verified to compile with GCC, Clang/LLVM, and MSVC.

pmGenerator 1.1 final

This version does not yet support custom axioms or necessitation!

pmGenerator-1.1.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.9.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Microsoft MPI 10.1.1-10, library bindings from MSYS2 package mingw-w64-x86_64-msmpi
  • msmpi.dll (version 10.1.12498.18) from Microsoft software installer Microsoft MPI v10.1.2
• 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 -lmsmpi.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 script:

#!/bin/zsh
cmp='-O3 -ffast-math -mtune=native -Wall -c -m64 -fmessage-length=0 -std=c++20 -pthread'
inc='-I/home/oneTBB/include/'
lnk='-pthread -ltbb'
lib='-L/home/oneTBB/intel_19.0_cxx11_64_relwithdebinfo/'
mkdir -p {helper,grammar,metamath,logic}
set -x
export I_MPI_CXX=icpx
mpicxx $inc $cmp -o helper/FctHelper.o ../helper/FctHelper.cpp
mpicxx $inc $cmp -o helper/IPrintable.o ../helper/IPrintable.cpp
mpicxx $inc $cmp -o helper/ProgressData.o ../helper/ProgressData.cpp
mpicxx $inc $cmp -o helper/Resources.o ../helper/Resources.cpp
mpicxx $inc $cmp -o grammar/CfgGrammar.o ../grammar/CfgGrammar.cpp
mpicxx $inc $cmp -o metamath/DRuleParser.o ../metamath/DRuleParser.cpp
mpicxx $inc $cmp -o metamath/DRuleReducer.o ../metamath/DRuleReducer.cpp
mpicxx $inc $cmp -o logic/DlCore.o ../logic/DlCore.cpp
mpicxx $inc $cmp -o logic/DlFormula.o ../logic/DlFormula.cpp
mpicxx $inc $cmp -o logic/DlProofEnumerator.o ../logic/DlProofEnumerator.cpp
mpicxx $inc $cmp -o logic/DlStructure.o ../logic/DlStructure.cpp
mpicxx $inc $cmp -o main.o ../main.cpp
mpicxx $lib $lnk -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 logic/DlCore.o logic/DlFormula.o logic/DlProofEnumerator.o logic/DlStructure.o

Verified to compile with GCC, Clang/LLVM, and MSVC.

pmGenerator 1.1 (patch 1)

pmGenerator-1.1.1-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.9.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Microsoft MPI 10.1.1-10, library bindings from MSYS2 package mingw-w64-x86_64-msmpi
  • msmpi.dll (version 10.1.12498.18) from Microsoft software installer Microsoft MPI v10.1.2
• 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 -lmsmpi.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

Verified to compile with GCC, Clang/LLVM, and MSVC.

pmGenerator 1.1

pmGenerator-1.1.0-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.9.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Microsoft MPI 10.1.1-10, library bindings from MSYS2 package mingw-w64-x86_64-msmpi
  • msmpi.dll (version 10.1.12498.18) from Microsoft software installer Microsoft MPI v10.1.2
• 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 -lmsmpi.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

Verified to compile with GCC and Clang/LLVM.

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.

pmGenerator 1.0 (patch 1)

pmGenerator-1.0.1-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).
• Wrong progress durations are displayed for large maximum numbers (e.g. the amount of D-proof candidates for dProofs35), due to overflows. [fixed since 1.0.2]
• Contents of concurrently loaded D-proof collections may be skipped due to vector reallocation. [fixed since 1.0.2]

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

Verified to compile also with Clang/LLVM.

pmGenerator 1.0

pmGenerator-1.0-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.6.0-1, libtbb12.dll from MSYS2 package mingw-w64-x86_64-tbb
• Used Boost 1.80.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,windows -mwindows -fuse-ld=lld -lpthread -ltbb12.dll

Known issues:

• The output is not shown on a Windows Command Prompt (CMD). [fixed since 1.0.1]
  • 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).
• Wrong progress durations are displayed for large maximum numbers (e.g. the amount of D-proof candidates for dProofs35), due to overflows. [fixed since 1.0.2]
• Contents of concurrently loaded D-proof collections may be skipped due to vector reallocation. [fixed since 1.0.2]

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

Verified to compile also with Clang/LLVM.