feat(minisat): recompile minisat with ALLOW_MEMORY_GROWTH=1

[cunneen]

Recompile minisat to address meteor/meteor#12902 (MINISAT-out: Cannot enlarge memory arrays), which despite being closed is still being reported .

[CLAassistant]

All committers have signed the CLA.

[nachocodoner]

Hey @cunneen,

I'm trying to understand the code and compile the new minisat file myself. I followed the README.md guide, but I ran into some issues along the way. It seems like you added code that requires additional dependencies, such as running npm install in ./meteor/test. I used Node 16.20.2 since lockfileVersion 2 matches npm 8.x for that version. I am using my Mac M1 machine for the compilation.

I encountered another error I haven't been able to fix yet. The output of minisat doesn't seem to be properly formatted. Any idea how to resolve this?

It would be great if we could also update the README.md to include the new instructions for compiling minisat.

[cunneen]

Hi @nachocodoner ,

Sorry about this; it looks like emscripten version 4 has been released since I started on this, and I'm guessing that's the cause of your issue. I'm on emscripten 3.1.74. I'll update the README accordingly.

The rest of my setup is very similar to what you describe:

$ echo -e "===macOS===\n$(sw_vers) \n\n===node===\n$(node --version) \n\n===npm===\n$(npm --version) \n\n===emscripten===\n$(emcc --version) \n\n===uname===\n$(uname -a)"
===macOS===
ProductName:		macOS
ProductVersion:		14.5
BuildVersion:		23F79 

===node===
v16.20.2 

===npm===
8.19.4 

===emscripten===
emcc (Emscripten gcc/clang-like replacement + linker emulating GNU ld) 3.1.74-git
Copyright (C) 2014 the Emscripten authors (see AUTHORS.txt)
This is free and open source software under the MIT license.
There is NO warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 

===uname===
Darwin Mikes-MacBook-Air-M1.local 23.5.0 Darwin Kernel Version 23.5.0: Wed May  1 20:16:51 PDT 2024; root:xnu-10063.121.3~5/RELEASE_ARM64_T8103 arm64

$ git clone https://github.com/cunneen/minisat --branch=emscripten
Cloning into 'minisat'...
remote: Enumerating objects: 1945, done.
remote: Counting objects: 100% (45/45), done.
remote: Compressing objects: 100% (43/43), done.
remote: Total 1945 (delta 12), reused 2 (delta 2), pack-reused 1900 (from 3)
Receiving objects: 100% (1945/1945), 635.98 KiB | 1.51 MiB/s, done.
Resolving deltas: 100% (1190/1190), done.

$ cd minisat
$ cd meteor/test
$ npm install

added 4 packages, and audited 5 packages in 2s

found 0 vulnerabilities
$ cd ../..
$ ./meteor/make-emscripten.sh 
Building
make: make -s -C /Users/mikecunneen/Development/minisat/meteor/.. lr
Compiling: build/release/minisat/core/Solver.o
Compiling: build/release/minisat/simp/SimpSolver.o
Compiling: build/release/minisat/utils/Options.o
Compiling: build/release/minisat/utils/System.o
Linking Static Library: build/release/lib/libminisat.a
make: make -s ENABLE_INSTRUMENTATION=false minisat-meteor.js -C /Users/mikecunneen/Development/minisat/meteor/.. --file=Makefile.meteor
make[1]: *** No rule to make target `build/release/minisat/simp/Main.d'.  Stop.
make[1]: *** No rule to make target `build/release/minisat/core/Main.d'.  Stop.
make[1]: *** No rule to make target `build/release/meteor/logic-solver.d'.  Stop.
make[1]: *** No rule to make target `config.mk'.  Stop.
Compiling: build/release/meteor/logic-solver.o
====== Linking Binary: build/release/bin/minisat-meteor.js
====== Prerequisites: build/release/lib/libminisat.a build/release/meteor/logic-solver.o
Instrumentation NOT enabled; set env var ENABLE_INSTRUMENTATION=true to enable instrumentation and disable minification
Testing
running logic tests
tinytest - logic-solver - require : OK
tinytest - logic-solver - _clauseStrings : OK
tinytest - logic-solver - illegal NameTerms : OK
tinytest - logic-solver - toNameTerm, toNumTerm : OK
tinytest - logic-solver - bad NumTerms : OK
tinytest - logic-solver - true and false : OK
tinytest - logic-solver - Logic.or : OK
tinytest - logic-solver - Formula sharing : OK
tinytest - logic-solver - nested Logic.or : OK
tinytest - logic-solver - Logic.not term : OK
tinytest - logic-solver - Logic.not formula : OK
tinytest - logic-solver - Require/forbid after formula gen : OK
tinytest - logic-solver - Logic.and : OK
tinytest - logic-solver - Logic.xor : OK
tinytest - logic-solver - require/forbid generation : OK
tinytest - logic-solver - Logic.atMostOne : OK
tinytest - logic-solver - Logic.implies, Logic.equiv : OK
tinytest - logic-solver - Logic.exactlyOne : OK
tinytest - logic-solver - Logic.constantBits : OK
tinytest - logic-solver - Logic.equalBits : OK
tinytest - logic-solver - Logic.lessThan[OrEqual] : OK
tinytest - logic-solver - half/full sum/carry : OK
tinytest - logic-solver - sum of terms : OK
tinytest - logic-solver - MiniSat : OK
tinytest - logic-solver - MiniSat solveAssuming : OK
tinytest - logic-solver - simple solve : OK
tinytest - logic-solver - getVarNum : OK
tinytest - logic-solver - assumptions : OK
tinytest - logic-solver - eight queens : OK
tinytest - logic-solver - Sudoku : OK
tinytest - logic-solver - goes to eleven : OK
tinytest - logic-solver - evaluate : OK
tinytest - logic-solver - toy packages : OK
tinytest - logic-solver - minimize : OK
tinytest - logic-solver - maximize : OK
tinytest - logic-solver - weightedSum : OK
tinytest - logic-solver - type-checking : OK
passed/expected/failed/total 37 / 0 / 0 / 37
ALL TESTS PASSED

[nachocodoner]

Thank you for your contribution and your detailed explanation on the recompile process