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.