ikpx 2.2

For scripts to aid with computation or simulation in cellular automata.
Post Reply
GUYTU6J
Posts: 2200
Joined: August 5th, 2016, 10:27 am
Location: 拆哪！I repeat, CHINA! (a.k.a. 种花家)
Contact:
Contact GUYTU6J

Re: ikpx 2.2

Post by GUYTU6J »

yujh wrote: October 29th, 2021, 3:27 pm
GUYTU6J wrote: October 29th, 2021, 8:45 am
yujh wrote: October 29th, 2021, 8:38 am ...but if you are on windows remember to use WSL1 not 2
Why? I don't see any ikpx2 documentation that says so.
That’s window’s own problem, because at least in Qi does 10 you can’t use WSL2
What is Qi? How exactly does it show the error/warning message(s) when attempting to install WSL2? Or is it simply not using a Win10 that satisfies the following requirement?

Code: Select all

For x64 systems: Version 1903 or higher, with Build 18362 or higher.
For ARM64 systems: Version 2004 or higher, with Build 19041 or higher.
If there is another reason, please find an external link (like in stackoverflow, github issue, etc) describing it, or we cannot really take your suggestion of using the older WSL1 instead of WSL2.

Meanwhile, here is my attempt to run ikpx2 in WSL2. There is no problem with git clone:

Code: Select all

Cloning into 'ikpx2'...
remote: Enumerating objects: 647, done.
remote: Counting objects: 100% (50/50), done.
remote: Compressing objects: 100% (25/25), done.
remote: Total 647 (delta 30), reused 45 (delta 25), pack-reused 597
Receiving objects: 100% (647/647), 185.09 KiB | 304.00 KiB/s, done.
Resolving deltas: 100% (445/445), done.
And apart from a few warnings at the bottom, recompile.sh does its job as well:

Code: Select all

Updating submodules...
Submodule 'apgmera' (https://gitlab.com/apgoucher/apgmera.git) registered for path 'apgmera'
Submodule 'cadical' (https://github.com/arminbiere/cadical.git) registered for path 'cadical'
Submodule 'kissat' (https://github.com/arminbiere/kissat.git) registered for path 'kissat'
Cloning into '/home/azulena/ikpx2/apgmera'...
Cloning into '/home/azulena/ikpx2/cadical'...
Cloning into '/home/azulena/ikpx2/kissat'...
fatal: unable to access 'https://github.com/arminbiere/kissat.git/': GnuTLS recv error (-110): The TLS connection was non-properly terminated.
fatal: clone of 'https://github.com/arminbiere/kissat.git' into submodule path '/home/azulena/ikpx2/kissat' failed
Failed to clone 'kissat'. Retry scheduled
Cloning into '/home/azulena/ikpx2/kissat'...
Submodule path 'apgmera': checked out '912dceae9d7ccad328e6cd113afef7923aff8070'
Submodule 'lifelib' (https://gitlab.com/apgoucher/lifelib.git) registered for path 'apgmera/lifelib'
Cloning into '/home/azulena/ikpx2/apgmera/lifelib'...
Submodule path 'apgmera/lifelib': checked out 'ffa7ad8358e65194eca0f43164a63af127f1e524'
Submodule path 'cadical': checked out '88623ef0866370448c34f6e320c148fc18e6f4cc'
Submodule path 'kissat': checked out '8cf49a4351933e5ee73a5d7132d1c23e0528c13c'
Submodule path 'kissat': checked out '8cf49a4351933e5ee73a5d7132d1c23e0528c13c'
Building kissat solver...
configure: new build directory 'build'
configure: assuming GCC version 9.3.0 uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/allocate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/analyze.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ands.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/arena.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/assign.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/autarky.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/averages.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backbone.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backtrack.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backward.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/bits.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -I../build -c ../src/build.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/bump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/cache.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/check.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/clause.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/clueue.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/collect.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/colors.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/compact.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/config.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/decide.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/deduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/definition.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dominate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/eliminate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/equivalences.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/error.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/extend.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/failed.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/file.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/flags.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/format.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/forward.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/gates.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/heap.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ifthenelse.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/import.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/internal.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kitten.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/learn.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/limits.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/logging.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/minimize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/mode.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/nonces.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/options.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/phases.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/print.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/probe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/profile.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/promote.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proof.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propdense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/prophyper.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proprobe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propsearch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/queue.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reap.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reluctant.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/rephase.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/report.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resolve.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resources.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/restart.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/search.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/shrink.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/smooth.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sort.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/stack.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/statistics.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/strengthen.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/substitute.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sweep.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/terminate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ternary.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/trail.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/transitive.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/utilities.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vector.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vivify.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/walk.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/watch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/weaken.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/xors.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o autarky.o averages.o backbone.o backtrack.o backward.o bits.o build.o bump.o cache.o check.o clause.o clueue.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dominate.o dump.o eliminate.o equivalences.o error.o extend.o failed.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kitten.o learn.o limits.o logging.o minimize.o mode.o nonces.o options.o phases.o print.o probe.o profile.o promote.o proof.o propdense.o prophyper.o proprobe.o propsearch.o queue.o reap.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o ternary.o trail.o transitive.o utilities.o vector.o vivify.o walk.o watch.o weaken.o xors.o
Building cadical solver...
configure: making default 'build' directory
configure: building in default '/home/azulena/ikpx2/cadical/build'
configure: root directory '/home/azulena/ikpx2/cadical'
configure: compiler supports all required C99/C++11 extensions
configure: unlocked IO with '{putc,getc}_unlocked' seems to work
configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3'
configure: generated 'build/makefile' from '../makefile.in'
configure: generated '../makefile' as proxy to ...
configure: ... '/home/azulena/ikpx2/cadical/build/makefile'
configure: now run 'make' to compile CaDiCaL
configure: optionally run 'make test'
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/analyze.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/arena.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/assume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/averages.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/backtrack.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/backward.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/bins.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/block.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/ccadical.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/checker.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/clause.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/collect.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/compact.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/condition.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/config.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/contract.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/cover.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/decide.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/decompose.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/deduplicate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/elim.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/ema.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/extend.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/external.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/file.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/flags.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/format.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/gates.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/instantiate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/internal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/ipasir.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/limit.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/logging.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/lookahead.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/lucky.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/message.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/minimize.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/occs.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/options.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/parse.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/phases.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/probe.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/profile.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/proof.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/propagate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/queue.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/random.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/reap.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/reduce.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/rephase.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/report.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/resources.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/restart.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/restore.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/score.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/shrink.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/signal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/solution.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/solver.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/stats.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/subsume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/terminal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/ternary.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/tracer.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/transred.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/util.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/var.cpp
../scripts/make-build-header.sh > build.hpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/version.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/vivify.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/walk.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -I../build -c ../src/watch.cpp
ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
Configuring lifelib...
Using /usr/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
In file included from src/main.cpp:3:
src/core.hpp: In member function ‘void semisearch::load_file(std::string, uint32_t)’:
src/core.hpp:282:14: warning: ignoring return value of ‘size_t fread(void*, size_t, size_t, FILE*)’, declared with attribute warn_unused_result [-Wunused-result]
  282 |         fread(&bigheader, 8, 1, fptr);
      |         ~~~~~^~~~~~~~~~~~~~~~~~~~~~~~
In file included from src/core.hpp:3,
                 from src/main.cpp:3:
src/ikpxtree.hpp: In member function ‘void ikpxtree::read_from_file(FILE*)’:
src/ikpxtree.hpp:46:14: warning: ignoring return value of ‘size_t fread(void*, size_t, size_t, FILE*)’, declared with attribute warn_unused_result [-Wunused-result]
   46 |         fread(header, 8, 2, fptr);
      |         ~~~~~^~~~~~~~~~~~~~~~~~~~
src/ikpxtree.hpp:52:18: warning: ignoring return value of ‘size_t fread(void*, size_t, size_t, FILE*)’, declared with attribute warn_unused_result [-Wunused-result]
   52 |             fread(&ps, 16, 1, fptr);
      |             ~~~~~^~~~~~~~~~~~~~~~~~
src/ikpxtree.hpp:53:18: warning: ignoring return value of ‘size_t fread(void*, size_t, size_t, FILE*)’, declared with attribute warn_unused_result [-Wunused-result]
   53 |             fread(u.data(), 8, N, fptr);
      |             ~~~~~^~~~~~~~~~~~~~~~~~~~~~

 **** build process completed successfully ****
And finally, I can submit hauls to b3s23/ikpx2 such as this one.
Top
User avatar
yujh
Posts: 3153
Joined: February 27th, 2020, 11:23 pm
Location: I'm not sure where I am, so please tell me if you know
Contact:
Contact yujh

Re: ikpx 2.2

Post by yujh »

GUYTU6J wrote: October 29th, 2021, 10:44 pm..
Sorry, that one’s a typo
And, for most windows users I know, they just simply can’t use WSL2, but I don’t really know why, I’ve tried this on three windows computers and one is just three month old and I system still can’t WSL2. Quite a few other people have this problem too.
Rule modifier

B34kz5e7c8/S23-a4ityz5k
b2n3-q5y6cn7s23-k4c8
B3-kq6cn8/S2-i3-a4ciyz8
B3-kq4z5e7c8/S2-ci3-a4ciq5ek6eik7

Bored of Conway's Game of Life? Try Pedestrian Life -- not pedestrian at all!
Top
User avatar
pzq_alex
Posts: 801
Joined: May 1st, 2021, 9:00 pm
Location: tell me if you know

Re: ikpx 2.2

Post by pzq_alex »

yujh wrote: October 30th, 2021, 8:31 am Sorry, that one’s a typo
And, for most windows users I know, they just simply can’t use WSL2, but I don’t really know why, I’ve tried this on three windows computers and one is just three month old and I system still can’t WSL2. Quite a few other people have this problem too.
Maybe try upgrading to Windows 11? WSL2 is running perfectly well on my Win11 laptop.

Edit: My 200th post.
Last edited by pzq_alex on February 27th, 2022, 12:50 am, edited 1 time in total.
\sum_{n=1}^\infty H_n/n^2 = \zeta(3)

How much of current CA technology can I redevelop "on a desert island"?
Top
User avatar
yujh
Posts: 3153
Joined: February 27th, 2020, 11:23 pm
Location: I'm not sure where I am, so please tell me if you know
Contact:
Contact yujh

Re: ikpx 2.2

Post by yujh »

pzq_alex wrote: February 25th, 2022, 5:54 am
yujh wrote: October 30th, 2021, 8:31 am Sorry, that one’s a typo
And, for most windows users I know, they just simply can’t use WSL2, but I don’t really know why, I’ve tried this on three windows computers and one is just three month old and I system still can’t WSL2. Quite a few other people have this problem too.
Maybe try upgrading to Windows 11? WSL2 is running perfectly well on my Win11 laptop.
I don’t really like the design of windows 11 lol
Rule modifier

B34kz5e7c8/S23-a4ityz5k
b2n3-q5y6cn7s23-k4c8
B3-kq6cn8/S2-i3-a4ciyz8
B3-kq4z5e7c8/S2-ci3-a4ciq5ek6eik7

Bored of Conway's Game of Life? Try Pedestrian Life -- not pedestrian at all!
Top
GUYTU6J
Posts: 2200
Joined: August 5th, 2016, 10:27 am
Location: 拆哪！I repeat, CHINA! (a.k.a. 种花家)
Contact:
Contact GUYTU6J

Re: ikpx 2.2

Post by GUYTU6J »

For some rules that already has a large average object/soup ratio in random soup-searching, like b2kn3-ekqr4i5eq6n8s23-aeny4cikqr5ek6ace7c, using ikpx2 on it to find low-period ships may result in a haul that exceeds 1500KiB even at the minimum haul size of 10000 soups (try c/2o on it). How should the spaceships be uploaded, then?

EDIT: and meanwhile, can the object separation be improved further for cases like c/2o in Glimmering Garden?
Top
User avatar
pzq_alex
Posts: 801
Joined: May 1st, 2021, 9:00 pm
Location: tell me if you know

Re: ikpx 2.2

Post by pzq_alex »

GUYTU6J wrote: March 1st, 2022, 9:13 am For some rules that already has a large average object/soup ratio in random soup-searching, like b2kn3-ekqr4i5eq6n8s23-aeny4cikqr5ek6ace7c, using ikpx2 on it to find low-period ships may result in a haul that exceeds 1500KiB even at the minimum haul size of 10000 soups (try c/2o on it). How should the spaceships be uploaded, then?

EDIT: and meanwhile, can the object separation be improved further for cases like c/2o in Glimmering Garden?
… I sort of remember that the limit of 10000 was lifted for ikpx2_stdin?

edit: here
\sum_{n=1}^\infty H_n/n^2 = \zeta(3)

How much of current CA technology can I redevelop "on a desert island"?
Top
User avatar
yujh
Posts: 3153
Joined: February 27th, 2020, 11:23 pm
Location: I'm not sure where I am, so please tell me if you know
Contact:
Contact yujh

Re: ikpx 2.2

Post by yujh »

You can glitch apgluxe to upload one soup per haul. It’s client side only I believe(or you’ll have to be a custom symmetry)
The current limit for normal hauls is 5000 and for ikpx2 it’s less than four digits. If you have an excessive amount of objects in a single soup over some limit, it can also be uploaded.
Top
User avatar
May13
Posts: 1082
Joined: March 11th, 2021, 8:33 am

Re: ikpx 2.2

Post by May13 »

How to run ikpx2 to extend this partial (in hexagonal rule)?
c5dhex.rle

Code: Select all

#CXRLE Pos=-30,-10
x = 44, y = 70, rule = B2/S245H
5bo$5b2o$3bobobobo$bo4b2o4bo$o3b3ob3o3bo$2bo2b6o2bo$bo13bo$3b2o3b2o3b
2o$2bob5ob5obo$7b6o$6bo3bo3bo$6bo2bo2bo2bo2$7bo2b4o2bo$9bo2bo2bo$7b2ob
ob2obob2o$10bob3obo$10bobo2bobo$8bob2o5b2obo$9bo2bo4bo2bo$9bo3bo3bo3bo
$11b2ob4ob2o$14bobobo2$12b4obob4o$11b2o2bo4bo2b2o$12b2o9b2o$14bo3b2o3b
o$15b2obobob2o$14bo4b2o4bo$15b2o3bo3b2o$14bo3bo4bo3bo$17b2o2bo2b2o$18b
o2b2o2bo$14bob2o2bobobo2b2obo$20bo4bo$19bo2bobo2bo$19bobo4bobo$22b5o$
21bo6bo$24bobo$23bo4bo$23bob3obo2$26b3o$27b2o$26b2ob2o$26b2o2b2o$27b5o
$27bo4bo$25b2o2b3o2b2o$27b2o4b2o$26bobobobobobo$31b2o$32bo$32b2o$31bob
obo$32b4o$30bobo3bobo$30b2obo2bob2o$31b9o$29bo3b2o2b2o3bo$30bo2bo2bo2b
o2bo$30b3o8b3o$35bo3bo$32bo10bo$33b2obo3bob2o$37bo2bo$35b2ob3ob2o$39b
2o!
Here's what ikpx2 returns:

Code: Select all

$ ./ikpx2 c5dhex.rle -v "2,1c5" -m 10

           :'',
          ,: '' '' ,,
         :     : ,, ' ,
        :    ,:   : : :
         : , : , ', ,
              ,,' ' ':  ,,
                  ,  :'''',
                 ,: :,'' ,,
                    :, :',
                  ,, :  '' :
                   '''','': ,
                          ',:
                   '''     '  :
                   ,    :'  , '
                   ''', ',:,
          *---*   *---*  '*---------*   *---*   *---*
         /   /|  /   /'   |\         \   \   \ /   /
        /   / * /   *---*:* \   v2.2  \   \   v   /
       /   / / /         \ \ \         *   *     *
      /   / / /       *---* \ \   *---*   /       \
     /   / / /   / \   \  ,,,\ \   \,    /   / \   \
    *---* / *---* | *---* : ,:\ *---*   *---* | *---*
    |   |/  |   |/ \|   | '   :\|   |'' |   |/ \|   |
    *---*   *---*   *---*  '''  *---*   *---*   *---*
                           ,''',
                            ' ::,
                         ::' , ,:'
                           '',  '
                         ,''''':'',
                          , ,:  :,:
                                ''' ,,
                              ':  , :
                            ':,  ': :'
                             ':',,' :
                              ' ' :   ,
                               ::,, '
                                  :::
                                ,,,''
                                ',,

Instruction set AVX1 detected
ikpx2 has been compiled for the rule b2s245h  (92 prime implicants).

Checking SAT solver...
...check complete!

sizeof(workitem) = 32
sizeof(iterator) = 8
# Valid velocity: (2,1)c/5
# Jacobian: [(-1, 2), (2, 1), (0, 1)]
# lookahead = 18; jumpahead = 2
total rows: [0, 184]; valid rows: [182, 184].
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 4 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 5 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 6 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 7 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 8 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 9 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 10 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 11 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 12 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 13 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 14 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 15 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 16 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 17 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 18 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 19 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 20 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 21 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 22 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 23 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 24 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 25 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 26 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 27 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 28 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 29 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 30 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 31 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 32 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 33 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 34 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 35 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 36 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 37 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 38 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 39 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 40 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 41 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 42 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 43 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 44 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 45 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 46 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 47 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 48 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 49 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 50 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 51 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 52 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 53 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 54 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 55 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 56 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 57 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 58 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 59 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
# Adaptive widening to width 60 (treesize = 2)
# Profile: depth0 = 1 1 = depth1
# solvers invoked: trivial=0, cadical=0, kissat=0
Both 2,1c5 and c5d fails.
Spaceship databases:
new-gliders.db (30683 gliders, square grid)
hex-gliders.db (668 gliders, hexagonal grid)
My scripts: new-glider.py v0.2, nbsearch2a.py, collector.py v0.3

-Dmitry Maitak
Top
User avatar
pzq_alex
Posts: 801
Joined: May 1st, 2021, 9:00 pm
Location: tell me if you know

Re: ikpx 2.2

Post by pzq_alex »

calcyman wrote: October 17th, 2020, 11:35 am
wwei23 wrote: October 17th, 2020, 8:26 am
calcyman wrote: October 17th, 2020, 5:59 am(Adding symmetry to odd-period diagonal searches would be extremely difficult.)
Out of curiosity, why so?
Also, could ikpx2 be adapted to oscillator searches as a "0c spaceship"?
I'll answer these questions in the reverse order.

Let's start by considering how to represent the problem of 'a pattern that moves by (a,b) every p generations'. We can think of this as being an infinite three-dimensional pattern of live and dead cells (in Z^3) satisfying the following:
  • (x, y, t) is a function of [(x+u, y+v, t-1) for u in [-1, 0, 1] for v in [-1, 0, 1]] according to the cellular automaton;
  • (x, y, t) is always equal to (x+a, y+b, t+p);
Now, there's a lot of redundancy here as a result of the second of these rules. So the space in which these patterns live isn't Z^3, but rather the quotient space Z^3 / <(a, b, p)>. It can be shown that this space is isomorphic to the product of Z^2 and a cyclic group of order gcd(a, b, p).

The 'torsion-free' case where gcd(a, b, p) = 1 is conceptually much simpler, because it means that the patterns just live on an ordinary grid isomorphic to Z^2; ikpx2 was written using this assumption for the sake of simplicity, and as such can't find oscillators.

As for the lattice, it's not canonically isomorphic to Z^2; you need to choose a somewhat arbitrary pair of basis vectors. These influence the possible shapes that partials can form. The first basis vector is chosen in the direction of the spaceship; the second basis vector is chosen to be reduced with respect to this first vector.

For even-period diagonal velocities, it's possible for the second basis vector to be perpendicular to the first. That way, even/odd reflections about a vertical axis (in the 'logical' quotient lattice) correspond to glide-reflections and diagonal reflections (in the 'physical' pattern). For odd-period diagonal velocities, the second vector doesn't end up being completely perpendicular, and you don't get this nice property.
I need some help to make sense of this. Specifically, what basis vectors would ikpx2 choose for a (2,1)c/6 search? What about (1, 0)c/3?

Edit: Looking at src/lattice.hpp, the following function seems to be responsible for choosing the basis vectors:

Code: Select all

std::vector<int> get_transformation(int vd, int hd, int p) {

    int vdp = apg::euclid_gcd(vd, p);

    if (apg::euclid_gcd(vdp, hd) != 1) {
        ERREXIT("vertical displacement, horizontal displacement, and period must be coprime");
    }

    if ((p <= 0) || (vd <= 0)) {
        ERREXIT("vertical displacement and period must be positive");
    }

    if (hd < 0) {
        ERREXIT("horizontal displacement must be nonnegative");
    }

    if (hd > vd) {
        ERREXIT("horizontal displacement cannot exceed vertical displacement");
    }

    // Find the first lattice basis vector:

    int vdhd = apg::euclid_gcd(vd, hd);
    int du_dx =  vd / vdhd;
    int du_dy = -hd / vdhd;

    // Find a second lattice basis vector:

    int dv_dx = 0;
    int dv_dy = 0;
    int dv_dt = 0;

    for (;; dv_dx = signedinc(dv_dx)) {

        if ((dv_dx * hd) % vdp) { continue; }

        dv_dy = 0;
        while  ((dv_dy * vd + dv_dx * hd) <= 0) { dv_dy += 1; }
        while  ((dv_dy * vd + dv_dx * hd)  % p) { dv_dy += 1; }
        dv_dt = (dv_dy * vd + dv_dx * hd) / p;

        int det = du_dy * dv_dx - dv_dy * du_dx;
        if (det < 0) { det = -det; }

        if (apg::euclid_gcd(det, dv_dt) != 1) { continue; }

        break;
    }

    // Reduce the second lattice basis vector against the first.
    // We use L1 distance as a primary objective and L2 distance
    // as a tie-breaker, which yields a total order on Z^2 / D8_1:
    // (0, 0) < (1, 0) < (1, 1) < (2, 0) < (2, 1) < (3, 0) <
    // (2, 2) < (3, 1) < (4, 0) < (3, 2) < (4, 1) < (5, 0) < ...

    while (sqdist(dv_dy, dv_dx) > sqdist(dv_dy + du_dy, dv_dx + du_dx)) {
        dv_dy += du_dy; dv_dx += du_dx;
    }

    while (sqdist(dv_dy, dv_dx) > sqdist(dv_dy - du_dy, dv_dx - du_dx)) {
        dv_dy -= du_dy; dv_dx -= du_dx;
    }

    while (l1dist(dv_dy, dv_dx) > l1dist(dv_dy + du_dy, dv_dx + du_dx)) {
        dv_dy += du_dy; dv_dx += du_dx;
    }

    while (l1dist(dv_dy, dv_dx) > l1dist(dv_dy - du_dy, dv_dx - du_dx)) {
        dv_dy -= du_dy; dv_dx -= du_dx;
    }

    return {du_dy, dv_dy,
            du_dx, dv_dx,
                0, dv_dt};

}
The following code produces the output -1 3 2 0 0 1:

Code: Select all

#include <stdio.h>
#include "src/lattice.hpp"

int main()
{
    auto v = get_transformation(2, 1, 6);
    for (auto&& i : v)
        printf("%d ", i);
}
Thus the basis vectors are <-1, 2, 0> and <3, 0, 1>. However, I am purplexed to see that the determinant of <2, 1, 6> together with these vectors is not 1. Did I do something wrong here?
\sum_{n=1}^\infty H_n/n^2 = \zeta(3)

How much of current CA technology can I redevelop "on a desert island"?
Top
User avatar
ClippyCosmologist
Posts: 22
Joined: May 7th, 2022, 5:24 pm

Re: ikpx 2.2

Post by ClippyCosmologist »

It would be convenient if there was an option to upload hauls every n hours rather than every n soups. The number of soups per hour seems to vary significantly over the course of a search.
"Human beings, five hundred years after the Scientific Revolution, are only just starting to match their wits against the billion-year heritage of biology." -- E. Yudkowsky
Top
User avatar
LaundryPizza03
Posts: 2623
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: ikpx 2.2

Post by LaundryPizza03 »

After updating ikpx 2.2 on my new system, I can no longer compile this program properly. The command "linker" failed; the first round of output was also unusually verbose.

Code: Select all

> ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
Submodule path 'apgmera': checked out 'd3a5dac8387c5b6a84f05357db99a36a7fb6bcff'
Submodule path 'apgmera/lifelib': checked out 'e32644d83c68a347e0314f85844adc642db989fc'
Submodule path 'cadical': checked out 'ca9bff05c11bde5eae4912f9932871d1527e61d8'
Submodule path 'kissat': checked out '97917ddf2b12adc6f63c7b2a5a403a1ee7d81836'
Building kissat solver...
configure: reusing existing build directory 'build'
configure: assuming GCC version (clang-1316.0.21.2.5) uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: linking src/makefile
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/allocate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/analyze.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ands.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/arena.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/assign.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/averages.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backbone.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -I../build -c ../src/build.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/bump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/check.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/clause.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/collect.c
../src/collect.c:326:10: warning: variable 'redundant_bytes' set but not used [-Wunused-but-set-variable]
  size_t redundant_bytes = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/colors.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/compact.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/config.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/decide.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/deduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/definition.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/eliminate.c
../src/eliminate.c:351:12: warning: variable 'eliminated' set but not used [-Wunused-but-set-variable]
  unsigned eliminated = 0;
           ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/equivalences.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/error.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/extend.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/file.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/flags.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/format.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/forward.c
../src/forward.c:78:10: warning: variable 'removed' set but not used [-Wunused-but-set-variable]
  size_t removed = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/gates.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/heap.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ifthenelse.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/import.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/internal.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kimits.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kitten.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/learn.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/logging.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/minimize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/mode.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/options.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/phases.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/print.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/probe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/profile.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/promote.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proof.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propbeyond.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propdense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proprobe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propsearch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/queue.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reluctant.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/rephase.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/report.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resolve.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resources.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/restart.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/search.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/shrink.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/smooth.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sort.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/stack.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/statistics.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/strengthen.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/substitute.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sweep.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/terminate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/trail.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/utilities.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vector.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vivify.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/walk.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/warmup.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/watch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
Building cadical solver...
configure: reusing default 'build' directory
configure: building in default '/Users/gb/ikpx2/cadical/build'
configure: root directory '/Users/gb/ikpx2/cadical'
configure: source directory '/Users/gb/ikpx2/cadical/src'
configure: using '-std=c++11' for all required C99/C++11 extensions
configure: unlocked IO with '{putc,getc}_unlocked' seems to work
configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11'
configure: generated 'build/makefile' from '../makefile.in'
configure: generated '../makefile' as proxy to ...
configure: ... '/Users/gb/ikpx2/cadical/build/makefile'
configure: linking '/Users/gb/ikpx2/cadical/makefile'
configure: now run 'make' to compile CaDiCaL
configure: optionally run 'make test'
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/analyze.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/arena.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/assume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/averages.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backtrack.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backward.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/bins.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/block.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ccadical.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/checker.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/clause.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/collect.cpp
../src/collect.cpp:232:11: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  int64_t collected_bytes = 0, collected_clauses = 0;
          ^
../src/collect.cpp:273:33: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  size_t collected_clauses = 0, collected_bytes = 0;
                                ^
2 warnings generated.
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/compact.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/condition.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/config.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/constrain.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/contract.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/cover.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decide.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decompose.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/deduplicate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/elim.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ema.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/extend.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/external.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/file.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/flags.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/format.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/gates.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/instantiate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/internal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ipasir.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/limit.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/logging.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lookahead.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lucky.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/message.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/minimize.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/occs.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/options.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/parse.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/phases.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/probe.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/profile.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/proof.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/propagate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/queue.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/random.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reap.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reduce.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/rephase.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/report.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/resources.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restart.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restore.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/score.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/shrink.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/signal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solution.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solver.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/stats.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/subsume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/terminal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ternary.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/tracer.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/transred.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/util.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/var.cpp
../scripts/make-build-header.sh > build.hpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/version.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/vivify.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/walk.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/watch.cpp
ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o constrain.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(contract.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(logging.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(profile.o) has no symbols
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

> ikpx2 % ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
libkissat.a already detected
libcadical.a already detected
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia
Top
User avatar
pzq_alex
Posts: 801
Joined: May 1st, 2021, 9:00 pm
Location: tell me if you know

Re: ikpx 2.2

Post by pzq_alex »

LaundryPizza03 wrote: August 21st, 2022, 10:39 pm After updating ikpx 2.2 on my new system, I can no longer compile this program properly. The command "linker" failed; the first round of output was also unusually verbose.

Code: Select all

> ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
Submodule path 'apgmera': checked out 'd3a5dac8387c5b6a84f05357db99a36a7fb6bcff'
Submodule path 'apgmera/lifelib': checked out 'e32644d83c68a347e0314f85844adc642db989fc'
Submodule path 'cadical': checked out 'ca9bff05c11bde5eae4912f9932871d1527e61d8'
Submodule path 'kissat': checked out '97917ddf2b12adc6f63c7b2a5a403a1ee7d81836'
Building kissat solver...
configure: reusing existing build directory 'build'
configure: assuming GCC version (clang-1316.0.21.2.5) uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: linking src/makefile
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/allocate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/analyze.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ands.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/arena.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/assign.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/averages.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backbone.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -I../build -c ../src/build.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/bump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/check.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/clause.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/collect.c
../src/collect.c:326:10: warning: variable 'redundant_bytes' set but not used [-Wunused-but-set-variable]
  size_t redundant_bytes = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/colors.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/compact.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/config.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/decide.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/deduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/definition.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/eliminate.c
../src/eliminate.c:351:12: warning: variable 'eliminated' set but not used [-Wunused-but-set-variable]
  unsigned eliminated = 0;
           ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/equivalences.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/error.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/extend.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/file.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/flags.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/format.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/forward.c
../src/forward.c:78:10: warning: variable 'removed' set but not used [-Wunused-but-set-variable]
  size_t removed = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/gates.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/heap.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ifthenelse.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/import.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/internal.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kimits.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kitten.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/learn.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/logging.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/minimize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/mode.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/options.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/phases.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/print.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/probe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/profile.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/promote.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proof.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propbeyond.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propdense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proprobe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propsearch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/queue.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reluctant.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/rephase.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/report.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resolve.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resources.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/restart.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/search.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/shrink.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/smooth.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sort.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/stack.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/statistics.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/strengthen.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/substitute.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sweep.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/terminate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/trail.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/utilities.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vector.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vivify.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/walk.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/warmup.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/watch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
Building cadical solver...
configure: reusing default 'build' directory
configure: building in default '/Users/gb/ikpx2/cadical/build'
configure: root directory '/Users/gb/ikpx2/cadical'
configure: source directory '/Users/gb/ikpx2/cadical/src'
configure: using '-std=c++11' for all required C99/C++11 extensions
configure: unlocked IO with '{putc,getc}_unlocked' seems to work
configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11'
configure: generated 'build/makefile' from '../makefile.in'
configure: generated '../makefile' as proxy to ...
configure: ... '/Users/gb/ikpx2/cadical/build/makefile'
configure: linking '/Users/gb/ikpx2/cadical/makefile'
configure: now run 'make' to compile CaDiCaL
configure: optionally run 'make test'
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/analyze.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/arena.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/assume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/averages.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backtrack.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backward.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/bins.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/block.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ccadical.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/checker.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/clause.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/collect.cpp
../src/collect.cpp:232:11: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  int64_t collected_bytes = 0, collected_clauses = 0;
          ^
../src/collect.cpp:273:33: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  size_t collected_clauses = 0, collected_bytes = 0;
                                ^
2 warnings generated.
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/compact.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/condition.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/config.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/constrain.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/contract.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/cover.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decide.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decompose.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/deduplicate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/elim.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ema.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/extend.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/external.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/file.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/flags.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/format.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/gates.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/instantiate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/internal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ipasir.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/limit.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/logging.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lookahead.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lucky.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/message.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/minimize.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/occs.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/options.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/parse.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/phases.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/probe.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/profile.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/proof.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/propagate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/queue.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/random.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reap.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reduce.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/rephase.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/report.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/resources.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restart.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restore.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/score.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/shrink.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/signal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solution.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solver.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/stats.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/subsume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/terminal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ternary.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/tracer.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/transred.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/util.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/var.cpp
../scripts/make-build-header.sh > build.hpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/version.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/vivify.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/walk.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/watch.cpp
ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o constrain.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(contract.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(logging.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(profile.o) has no symbols
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

> ikpx2 % ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
libkissat.a already detected
libcadical.a already detected
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Is your system based on x86_64? It seems that you’re using Mac. I’ve had no problems compiling ikpx2 on my Mac.
\sum_{n=1}^\infty H_n/n^2 = \zeta(3)

How much of current CA technology can I redevelop "on a desert island"?
Top
User avatar
LaundryPizza03
Posts: 2623
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: ikpx 2.2

Post by LaundryPizza03 »

pzq_alex wrote: August 22nd, 2022, 2:53 am
LaundryPizza03 wrote: August 21st, 2022, 10:39 pm After updating ikpx 2.2 on my new system, I can no longer compile this program properly. The command "linker" failed; the first round of output was also unusually verbose.

Code: Select all

> ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
Submodule path 'apgmera': checked out 'd3a5dac8387c5b6a84f05357db99a36a7fb6bcff'
Submodule path 'apgmera/lifelib': checked out 'e32644d83c68a347e0314f85844adc642db989fc'
Submodule path 'cadical': checked out 'ca9bff05c11bde5eae4912f9932871d1527e61d8'
Submodule path 'kissat': checked out '97917ddf2b12adc6f63c7b2a5a403a1ee7d81836'
Building kissat solver...
configure: reusing existing build directory 'build'
configure: assuming GCC version (clang-1316.0.21.2.5) uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: linking src/makefile
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/allocate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/analyze.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ands.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/arena.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/assign.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/averages.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backbone.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -I../build -c ../src/build.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/bump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/check.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/clause.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/collect.c
../src/collect.c:326:10: warning: variable 'redundant_bytes' set but not used [-Wunused-but-set-variable]
  size_t redundant_bytes = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/colors.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/compact.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/config.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/decide.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/deduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/definition.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/eliminate.c
../src/eliminate.c:351:12: warning: variable 'eliminated' set but not used [-Wunused-but-set-variable]
  unsigned eliminated = 0;
           ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/equivalences.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/error.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/extend.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/file.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/flags.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/format.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/forward.c
../src/forward.c:78:10: warning: variable 'removed' set but not used [-Wunused-but-set-variable]
  size_t removed = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/gates.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/heap.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ifthenelse.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/import.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/internal.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kimits.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kitten.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/learn.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/logging.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/minimize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/mode.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/options.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/phases.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/print.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/probe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/profile.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/promote.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proof.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propbeyond.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propdense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proprobe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propsearch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/queue.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reluctant.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/rephase.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/report.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resolve.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resources.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/restart.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/search.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/shrink.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/smooth.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sort.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/stack.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/statistics.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/strengthen.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/substitute.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sweep.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/terminate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/trail.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/utilities.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vector.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vivify.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/walk.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/warmup.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/watch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
Building cadical solver...
configure: reusing default 'build' directory
configure: building in default '/Users/gb/ikpx2/cadical/build'
configure: root directory '/Users/gb/ikpx2/cadical'
configure: source directory '/Users/gb/ikpx2/cadical/src'
configure: using '-std=c++11' for all required C99/C++11 extensions
configure: unlocked IO with '{putc,getc}_unlocked' seems to work
configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11'
configure: generated 'build/makefile' from '../makefile.in'
configure: generated '../makefile' as proxy to ...
configure: ... '/Users/gb/ikpx2/cadical/build/makefile'
configure: linking '/Users/gb/ikpx2/cadical/makefile'
configure: now run 'make' to compile CaDiCaL
configure: optionally run 'make test'
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/analyze.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/arena.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/assume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/averages.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backtrack.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backward.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/bins.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/block.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ccadical.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/checker.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/clause.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/collect.cpp
../src/collect.cpp:232:11: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  int64_t collected_bytes = 0, collected_clauses = 0;
          ^
../src/collect.cpp:273:33: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  size_t collected_clauses = 0, collected_bytes = 0;
                                ^
2 warnings generated.
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/compact.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/condition.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/config.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/constrain.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/contract.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/cover.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decide.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decompose.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/deduplicate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/elim.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ema.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/extend.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/external.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/file.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/flags.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/format.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/gates.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/instantiate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/internal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ipasir.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/limit.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/logging.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lookahead.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lucky.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/message.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/minimize.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/occs.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/options.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/parse.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/phases.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/probe.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/profile.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/proof.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/propagate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/queue.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/random.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reap.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reduce.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/rephase.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/report.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/resources.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restart.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restore.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/score.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/shrink.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/signal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solution.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solver.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/stats.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/subsume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/terminal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ternary.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/tracer.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/transred.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/util.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/var.cpp
../scripts/make-build-header.sh > build.hpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/version.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/vivify.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/walk.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/watch.cpp
ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o constrain.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(contract.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(logging.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(profile.o) has no symbols
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

> ikpx2 % ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
libkissat.a already detected
libcadical.a already detected
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Is your system based on x86_64? It seems that you’re using Mac. I’ve had no problems compiling ikpx2 on my Mac.
macOS 12.5.1.

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia
Top
User avatar
dexter1
Posts: 95
Joined: February 26th, 2020, 8:46 am

Re: ikpx 2.2

Post by dexter1 »

LaundryPizza03 wrote: August 21st, 2022, 10:39 pm After updating ikpx 2.2 on my new system, I can no longer compile this program properly. The command "linker" failed; the first round of output was also unusually verbose.
Try removing the solver/lib*.a files. When present, the script will not attempt to recompile these static libraries, resulting in symbol mismatches.
Frank Everdij
Top
User avatar
LaundryPizza03
Posts: 2623
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: ikpx 2.2

Post by LaundryPizza03 »

dexter1 wrote: August 22nd, 2022, 7:06 am
LaundryPizza03 wrote: August 21st, 2022, 10:39 pm After updating ikpx 2.2 on my new system, I can no longer compile this program properly. The command "linker" failed; the first round of output was also unusually verbose.
Try removing the solver/lib*.a files. When present, the script will not attempt to recompile these static libraries, resulting in symbol mismatches.
Didn't work. Should I set specific parameters for clang before the first recompile?

Code: Select all

> ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
Building kissat solver...
configure: reusing existing build directory 'build'
configure: assuming GCC version (clang-1316.0.21.2.5) uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: removing src/makefile
configure: linking src/makefile
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/allocate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/analyze.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ands.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/arena.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/assign.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/averages.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backbone.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -I../build -c ../src/build.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/bump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/check.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/clause.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/collect.c
../src/collect.c:326:10: warning: variable 'redundant_bytes' set but not used [-Wunused-but-set-variable]
  size_t redundant_bytes = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/colors.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/compact.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/config.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/decide.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/deduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/definition.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/dump.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/eliminate.c
../src/eliminate.c:351:12: warning: variable 'eliminated' set but not used [-Wunused-but-set-variable]
  unsigned eliminated = 0;
           ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/equivalences.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/error.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/extend.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/file.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/flags.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/format.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/forward.c
../src/forward.c:78:10: warning: variable 'removed' set but not used [-Wunused-but-set-variable]
  size_t removed = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/gates.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/heap.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/ifthenelse.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/import.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/internal.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kimits.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/kitten.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/learn.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/logging.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/minimize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/mode.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/options.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/phases.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/print.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/probe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/profile.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/promote.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proof.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propbeyond.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propdense.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/proprobe.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/propsearch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/queue.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reduce.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/reluctant.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/rephase.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/report.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resize.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resolve.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/resources.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/restart.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/search.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/shrink.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/smooth.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sort.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/stack.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/statistics.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/strengthen.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/substitute.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/sweep.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/terminate.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/trail.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/utilities.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vector.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/vivify.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/walk.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/warmup.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/watch.c
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
Building cadical solver...
configure: reusing default 'build' directory
configure: building in default '/Users/gb/ikpx2/cadical/build'
configure: root directory '/Users/gb/ikpx2/cadical'
configure: source directory '/Users/gb/ikpx2/cadical/src'
configure: using '-std=c++11' for all required C99/C++11 extensions
configure: unlocked IO with '{putc,getc}_unlocked' seems to work
configure: compiling with 'g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11'
configure: generated 'build/makefile' from '../makefile.in'
configure: generated '../makefile' as proxy to ...
configure: ... '/Users/gb/ikpx2/cadical/build/makefile'
configure: removing '/Users/gb/ikpx2/cadical/src/makefile'
configure: linking '/Users/gb/ikpx2/cadical/makefile'
configure: now run 'make' to compile CaDiCaL
configure: optionally run 'make test'
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/analyze.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/arena.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/assume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/averages.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backtrack.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/backward.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/bins.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/block.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ccadical.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/checker.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/clause.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/collect.cpp
../src/collect.cpp:232:11: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  int64_t collected_bytes = 0, collected_clauses = 0;
          ^
../src/collect.cpp:273:33: warning: variable 'collected_bytes' set but not used [-Wunused-but-set-variable]
  size_t collected_clauses = 0, collected_bytes = 0;
                                ^
2 warnings generated.
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/compact.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/condition.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/config.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/constrain.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/contract.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/cover.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decide.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/decompose.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/deduplicate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/elim.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ema.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/extend.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/external.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/file.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/flags.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/format.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/gates.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/instantiate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/internal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ipasir.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/limit.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/logging.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lookahead.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/lucky.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/message.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/minimize.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/occs.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/options.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/parse.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/phases.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/probe.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/profile.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/proof.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/propagate.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/queue.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/random.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reap.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/reduce.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/rephase.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/report.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/resources.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restart.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/restore.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/score.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/shrink.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/signal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solution.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/solver.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/stats.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/subsume.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/terminal.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/ternary.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/tracer.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/transred.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/util.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/var.cpp
../scripts/make-build-header.sh > build.hpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/version.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/vivify.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/walk.cpp
g++ -Wall -Wextra -O3 -DNDEBUG -DQUIET -DNCONTRACTS -DNTRACING -ggdb3 -std=c++11 -I../build -c ../src/watch.cpp
ar rc libcadical.a analyze.o arena.o assume.o averages.o backtrack.o backward.o bins.o block.o ccadical.o checker.o clause.o collect.o compact.o condition.o config.o constrain.o contract.o cover.o decide.o decompose.o deduplicate.o elim.o ema.o extend.o external.o file.o flags.o format.o gates.o instantiate.o internal.o ipasir.o limit.o logging.o lookahead.o lucky.o message.o minimize.o occs.o options.o parse.o phases.o probe.o profile.o proof.o propagate.o queue.o random.o reap.o reduce.o rephase.o report.o resources.o restart.o restore.o score.o shrink.o signal.o solution.o solver.o stats.o subsume.o terminal.o ternary.o tracer.o transred.o util.o var.o version.o vivify.o walk.o watch.o
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(contract.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(logging.o) has no symbols
/Library/Developer/CommandLineTools/usr/bin/ranlib: file: libcadical.a(profile.o) has no symbols
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

> ./recompile.sh --rule b2-a4inrtwyz5-jky6-cn78s1c3kq4-jq5-er67
Updating submodules...
libkissat.a already detected
libcadical.a already detected
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia
Top
hotdogPi
Moderator
Posts: 2262
Joined: August 12th, 2020, 8:22 pm

Re: ikpx 2.2

Post by hotdogPi »

pzq_alex wrote: August 22nd, 2022, 2:53 am
LaundryPizza03 wrote: August 21st, 2022, 10:39 pm code
[/code]
Is your system based on x86_64? It seems that you’re using Mac. I’ve had no problems compiling ikpx2 on my Mac.
Congratulations for post #150000
User:HotdogPi/My discoveries

Periods discovered:

All evens ≤128 except 52,58,78,82,92,94,98,104,118,122

5-15,㉕-㉛,㉟㊺,51,63,65,73,75
1㊳㊵㊹㊼㊽,54,56,72,74,80,90,92
217,240,300,486,576

Guns: 20,21,32,54,55,57,114,117,124,126
SKOPs: 32,74,76,102,196
Top
User avatar
dexter1
Posts: 95
Joined: February 26th, 2020, 8:46 am

Re: ikpx 2.2

Post by dexter1 »

LaundryPizza03 wrote: August 22nd, 2022, 5:42 pm Didn't work. Should I set specific parameters for clang before the first recompile?
I haven't got any development experience on Macs, but thinking out loud, possible causes for this symbol mismatch could be:
- Multiple toolsets installed (compiler and linker from different toolsets)
- Old toolset version (maybe Xcode needs an upgrade?)
- The kissat library is C code, whereas the rest is C++. Name mangling for C objects could be an issue. Try specifying export CC=g++ or export CC=clang or export GCC=clang
- Try specifying a different linker, like export LD=clang or export LD=g++

You could also test kissat by building a standalone kissat binary: Go to the "ikpx2/kissat" directory and issue

Code: Select all

make kissat
If successful, the kissat binary should then be in "ikpx2/kissat/build".
Frank Everdij
Top
User avatar
LaundryPizza03
Posts: 2623
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: ikpx 2.2

Post by LaundryPizza03 »

dexter1 wrote: August 25th, 2022, 4:27 am
LaundryPizza03 wrote: August 22nd, 2022, 5:42 pm Didn't work. Should I set specific parameters for clang before the first recompile?
I haven't got any development experience on Macs, but thinking out loud, possible causes for this symbol mismatch could be:
- Multiple toolsets installed (compiler and linker from different toolsets)
- Old toolset version (maybe Xcode needs an upgrade?)
- The kissat library is C code, whereas the rest is C++. Name mangling for C objects could be an issue. Try specifying export CC=g++ or export CC=clang or export GCC=clang
- Try specifying a different linker, like export LD=clang or export LD=g++

You could also test kissat by building a standalone kissat binary: Go to the "ikpx2/kissat" directory and issue

Code: Select all

make kissat
If successful, the kissat binary should then be in "ikpx2/kissat/build".
Make failed on kissat, no matter which export configs I used.

Code: Select all

> make kissat     
/Library/Developer/CommandLineTools/usr/bin/make -C "/Users/gb/ikpx2/kissat/build" kissat
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -ggdb3 -DCOMPACT -DNDEBUG -DNOPTIONS -DQUIET -DSAT -I../build -c ../src/build.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
gcc -o kissat main.o application.o handle.o parse.o witness.o libkissat.a -lm
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[1]: *** [kissat] Error 1
make: *** [kissat] Error 2

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia
Top
User avatar
LaundryPizza03
Posts: 2623
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: ikpx 2.2

Post by LaundryPizza03 »

I still need help fixing the recompile.sh script. The issue is probably in kissat.

Code: Select all

./recompile.sh --rule b38s23
Updating submodules...
libkissat.a already detected
libcadical.a already detected
Configuring lifelib...
Using /Library/Frameworks/Python.framework/Versions/3.9/bin/python3 to configure lifelib...
Valid symmetry: ikpx2_stdin
Success!
Gathering latest library versions...
Compiling ikpx2...
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
EDIT: The following error occurred while attempting to compile kissat according to the directions in its github repository:

Code: Select all

> ./configure && make test
configure: default configuration (see '-h')
configure: reusing existing build directory 'build'
configure: assuming GCC version (clang-1316.0.21.2.5) uses C99 by default
configure: compiler 'gcc  -W -Wall -O3 -DNDEBUG'
configure: linker 'gcc' (no additional options)
configure: using default 'ar' (no cross compilation)
configure: no 'tissat' binary generated (without '--test')
configure: no 'libkissat.so' shared library generated (without '-shared')
configure: no 'kitten' binary generated (without '--kitten')
configure: removing src/makefile
configure: linking src/makefile
/Library/Developer/CommandLineTools/usr/bin/make -C "/Users/gb/ikpx2/kissat/build" test
gcc -W -Wall -O3 -DNDEBUG -c ../src/allocate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/analyze.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/ands.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/arena.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/assign.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/averages.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/backbone.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/backtrack.c
../scripts/generate-build-header.sh > build.h
gcc -W -Wall -O3 -DNDEBUG -I../build -c ../src/build.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/bump.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/check.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/clause.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/collect.c
../src/collect.c:326:10: warning: variable 'redundant_bytes' set but not used [-Wunused-but-set-variable]
  size_t redundant_bytes = 0;
         ^
1 warning generated.
gcc -W -Wall -O3 -DNDEBUG -c ../src/colors.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/compact.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/config.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/decide.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/deduce.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/definition.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/dense.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/dump.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/eliminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/equivalences.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/error.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/extend.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/file.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/flags.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/format.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/forward.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/gates.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/heap.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/ifthenelse.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/import.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/internal.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/kimits.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/kitten.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/learn.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/logging.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/minimize.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/mode.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/options.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/phases.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/print.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/probe.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/profile.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/promote.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/proof.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propbeyond.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propdense.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/proprobe.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/propsearch.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/queue.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/reduce.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/reluctant.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/rephase.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/report.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resize.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resolve.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/resources.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/restart.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/search.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/shrink.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/smooth.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/sort.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/stack.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/statistics.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/strengthen.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/substitute.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/sweep.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/terminate.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/trail.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/utilities.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/vector.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/vivify.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/walk.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/warmup.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/watch.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/weaken.c
ar rc libkissat.a allocate.o analyze.o ands.o arena.o assign.o averages.o backbone.o backtrack.o build.o bump.o check.o clause.o collect.o colors.o compact.o config.o decide.o deduce.o definition.o dense.o dump.o eliminate.o equivalences.o error.o extend.o file.o flags.o format.o forward.o gates.o heap.o ifthenelse.o import.o internal.o kimits.o kitten.o learn.o logging.o minimize.o mode.o options.o phases.o print.o probe.o profile.o promote.o proof.o propbeyond.o propdense.o proprobe.o propsearch.o queue.o reduce.o reluctant.o rephase.o report.o resize.o resolve.o resources.o restart.o search.o shrink.o smooth.o sort.o stack.o statistics.o strengthen.o substitute.o sweep.o terminate.o trail.o utilities.o vector.o vivify.o walk.o warmup.o watch.o weaken.o
gcc -W -Wall -O3 -DNDEBUG -c ../src/main.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/application.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/handle.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/parse.c
gcc -W -Wall -O3 -DNDEBUG -c ../src/witness.c
gcc -o kissat main.o application.o handle.o parse.o witness.o libkissat.a -lm
Undefined symbols for architecture x86_64:
  "_kissat_new_focused_restart_limit", referenced from:
      _kissat_init_limits in libkissat.a(limits.o)
ld: symbol(s) not found for architecture x86_64
clang: error: linker command failed with exit code 1 (use -v to see invocation)
make[1]: *** [kissat] Error 1
make: *** [test] Error 2

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia
Top
User avatar
pipsqueek
Posts: 304
Joined: September 10th, 2022, 4:42 pm
Location: Abstract mathematical space

Re: ikpx 2.2

Post by pipsqueek »

ikpx is certainly one of the most advanced spaceship search programs out there. but one thing I've always wondered, if we can set the search width, why can't we set the search height?

Code: Select all

x=17,y=16,rule=B3/S23
3bo3bobo2bob2o$bobo4bo4b4o$bobo5bobo2b3o$b2obob2o3b2o$3o4b2ob2o2b2o$4b
o4bo$4b2obobob2ob3o$3ob3o2b2o$b3o2bobobo5bo$o3b2o3bobo2b2o$4bo3bob2o3b
o$2obo2bobobo2b2o$3b3o5bo2b2o$2obo4bo2bob2o$o3bob2obo3b2o$2bo8bobobo![[ STOP 3 GPS 4 ]]
Top
User avatar
pzq_alex
Posts: 801
Joined: May 1st, 2021, 9:00 pm
Location: tell me if you know

Re: ikpx 2.2

Post by pzq_alex »

pipsqueek wrote: February 3rd, 2023, 8:26 pm ikpx is certainly one of the most advanced spaceship search programs out there. but one thing I've always wondered, if we can set the search width, why can't we set the search height?
WLS and other cell-by-cell search programs are (trivially) able to search fixed heights; in addition, both afind (which is gfind-like) and amling's rlife (LSSS-like) can perform side-to-side searches. I also suspect that since you can search back-to-front by inputting -kc/p to ikpx, you should be able to search side-to-side by inputting (0,k)c/p -- however I don't know if that feature is implemented.
\sum_{n=1}^\infty H_n/n^2 = \zeta(3)

How much of current CA technology can I redevelop "on a desert island"?
Top
yoleo
Posts: 140
Joined: October 26th, 2021, 11:48 pm

Re: ikpx 2.2

Post by yoleo »

From amling's wave searches:
Diagonal is still TBD. LLSSS's basic structure could support it but I would need to write a bunch of custom edge code to implement diagonal symmetries and I've been putting it off.
Could ikpx be reworked to search for waves and agar stretchers (at fixed width), including diagonal waves and knight waves?
Top
User avatar
LaundryPizza03
Posts: 2623
Joined: December 15th, 2017, 12:05 am
Location: Unidentified location "https://en.wikipedia.org/wiki/Texas"

Re: ikpx 2.2

Post by LaundryPizza03 »

pzq_alex wrote: February 3rd, 2023, 11:14 pm
pipsqueek wrote: February 3rd, 2023, 8:26 pm ikpx is certainly one of the most advanced spaceship search programs out there. but one thing I've always wondered, if we can set the search width, why can't we set the search height?
WLS and other cell-by-cell search programs are (trivially) able to search fixed heights; in addition, both afind (which is gfind-like) and amling's rlife (LSSS-like) can perform side-to-side searches. I also suspect that since you can search back-to-front by inputting -kc/p to ikpx, you should be able to search side-to-side by inputting (0,k)c/p -- however I don't know if that feature is implemented.
Sideways searches don't work, but back-end searches do.

Code: Select all

./ikpx2 -v 0,1c/2 -n 10000 -k <your key>

<...>

Instruction set AVX2 detected
ikpx2 has been compiled for the rule b3567s26  (955 prime implicants).

Checking SAT solver...
...check complete!

sizeof(workitem) = 32
sizeof(iterator) = 8
Error: vertical displacement and period must be positive

Code: Select all

x = 4, y = 3, rule = B3-q4z5y/S234k5j
2b2o$b2o$2o!
LaundryPizza03 at Wikipedia
Top
User avatar
May13
Posts: 1082
Joined: March 11th, 2021, 8:33 am

Re: ikpx 2.2

Post by May13 »

I ran into a problem when searching for a (2,1)c/7 knightship. Three times the program crashed due to some kind of error. Two recent stackdumps:

Code: Select all

Exception: STATUS_ACCESS_VIOLATION at rip=0010046151A
rax=00000000FFFFFFFF rbx=000000081D3056C0 rcx=000000081D406610
rdx=00000000FFFFFFFE rsi=000000081CF89950 rdi=000000081D5A38A0
r8 =000000081D5A38A0 r9 =00006E87980FD88C r10=000000081D3056C0
r11=0000000000000002 r12=000000081D3056C0 r13=000000081D3056C0
r14=000000081CF89730 r15=000000081CF89B30
rbp=0000000000000022 rsp=00000000FFDFC8B0
program=D:\BASH\cygwin64\home\User\C\ikpx2i\ikpx2.exe, pid 729, thread ikpx2
cs=0033 ds=002B es=002B fs=0053 gs=002B ss=002B

Code: Select all

Exception: STATUS_ACCESS_VIOLATION at rip=0010046151A
rax=00000000FFFFFFFF rbx=000000081BB306E0 rcx=000000081BB80E60
rdx=00000000FFFFFFFE rsi=000000081BB0EF60 rdi=000000081BB0C480
r8 =000000081BB0C480 r9 =00006FC4671FD88C r10=000000081BB306E0
r11=0000000000000002 r12=000000081BB306E0 r13=000000081BB306E0
r14=000000081BB0ED40 r15=000000081BB0F140
rbp=0000000000000022 rsp=00000000FFDFC8B0
program=D:\BASH\cygwin64\home\User\C\ikpx2i\ikpx2.exe, pid 731, thread ikpx2
cs=0033 ds=002B es=002B fs=0053 gs=002B ss=002B
I wonder what exactly the problem is - in the ikpx2, backup file or Cygwin?
As for ikpx2, I use the current version.
Output from Cygwin:

Code: Select all

$ ./ikpx2 -v "(2,1)c7" -m 1500 -w 17 -b 300 --threads 4 backup_b356s3568_velocity_2_1_7_width_17_odd.bin | tee -i newp7k_1.txt

           :'',
          ,: '' '' ,,
         :     : ,, ' ,
        :    ,:   : : :
         : , : , ', ,
              ,,' ' ':  ,,
                  ,  :'''',
                 ,: :,'' ,,
                    :, :',
                  ,, :  '' :
                   '''','': ,
                          ',:
                   '''     '  :
                   ,    :'  , '
                   ''', ',:,
          *---*   *---*  '*---------*   *---*   *---*
         /   /|  /   /'   |\         \   \   \ /   /
        /   / * /   *---*:* \   v2.2  \   \   v   /
       /   / / /         \ \ \         *   *     *
      /   / / /       *---* \ \   *---*   /       \
     /   / / /   / \   \  ,,,\ \   \,    /   / \   \
    *---* / *---* | *---* : ,:\ *---*   *---* | *---*
    |   |/  |   |/ \|   | '   :\|   |'' |   |/ \|   |
    *---*   *---*   *---*  '''  *---*   *---*   *---*
                           ,''',
                            ' ::,
                         ::' , ,:'
                           '',  '
                         ,''''':'',
                          , ,:  :,:
                                ''' ,,
                              ':  , :
                            ':,  ': :'
                             ':',,' :
                              ' ' :   ,
                               ::,, '
                                  :::
                                ,,,''
                                ',,

Instruction set AVX2 detected
ikpx2 has been compiled for the rule b356s3568  (339 prime implicants).

Checking SAT solver...
...check complete!

sizeof(workitem) = 32
sizeof(iterator) = 8
# Valid velocity: (2,1)c/7
# Jacobian: [(-1, 3), (2, 1), (0, 1)]
# lookahead = 26; jumpahead = 3
# Profile: depth0 = 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 0/1 0/3 0/4 0/6 0/5 0/7 0/28 0/30 0/52 0/63 0/66 0/69 0/79 0/72 0/62 0/57 0/49 0/40 0/35 0/36 0/32 0/33 0/28 0/23 0/21 0/19 0/18 0/19 0/24 0/28 0/33 0/51 0/55 0/61 0/64 0/64 0/70 0/73 0/91 0/119 0/156 0/233 0/373 0/465 0/511 0/546 0/554 0/727 0/1223 2/2241 7/3138 9/4120 9/4886 104/5629 444/6161 1113/6675 1816/6897 2298/6634 2507/6208 2192/5760 1785/5503 1471/5346 1340/5186 1320/5026 1282/4780 1167/4496 1050/4352 993/4230 933/4173 883/4207 833/4252 879/4345 965/4342 1103/4331 1094/4350 1176/4401 1288/4609 1547/4624 1714/4411 1928/4249 1996/3932 1973/3689 1844/3305 1697/3072 1605/2925 1521/2818 1490/2684 1543/2628 1599/2566 1559/2480 1519/2497 1468/2541 1356/2681 1342/2886 1261/3085 1175/3094 1125/3211 1117/3484 1052/3739 1012/3801 978/3773 981/3649 947/3377 915/3166 874/2912 869/2681 879/2506 938/2426 956/2348 924/2269 961/2266 1023/2316 1076/2408 1124/2459 1197/2481 1297/2461 1399/2457 1385/2361 1323/2288 1252/2236 1207/2181 1172/2153 1122/2165 1060/2169 1070/2193 1034/2142 1080/2151 1087/2106 1072/1987 986/1838 894/1725 800/1641 747/1577 687/1523 618/1468 590/1474 582/1497 566/1503 549/1489 524/1491 508/1489 482/1490 487/1490 478/1484 467/1459 485/1512 483/1568 472/1566 478/1534 454/1498 440/1499 404/1475 388/1518 357/1489 352/1565 335/1543 308/1562 294/1552 289/1609 284/1700 329/1902 321/2028 379/2262 461/2622 606/2904 693/2999 788/2974 753/2855 694/2691 617/2680 547/2653 506/2616 473/2679 444/2815 412/3425 396/3889 364/4385 331/4738 302/5093 275/5050 265/5022 271/5044 256/4956 243/4715 238/4562 214/4308 199/4136 191/4004 175/3945 172/3835 167/3736 158/3698 154/3591 151/3643 142/3618 139/3590 131/3705 120/3897 115/4043 115/4137 119/4270 124/4379 132/4519 133/4718 151/4722 165/4825 221/4742 258/4611 354/4455 402/4328 468/4265 477/4112 470/4094 436/3913 426/3755 420/3592 391/3459 384/3293 350/3156 347/2994 353/2968 389/2850 395/2768 412/2767 462/2891 477/2837 503/3061 540/3160 562/3223 611/3383 654/3473 658/3394 630/3336 634/3407 621/3444 599/3936 558/4816 517/5799 528/6460 517/6662 541/6544 527/6224 533/6109 520/5973 504/5655 512/5161 508/4903 488/4713 463/4495 455/4395 447/4311 464/4252 485/4259 543/4244 539/4388 585/4493 546/4674 663/4757 778/4762 991/4828 1077/4703 1206/4516 1261/4166 1317/3990 1323/3828 1303/3638 1275/3428 1233/3268 1146/3053 1077/2867 1021/2701 985/2687 898/2631 951/2654 965/2677 1042/2736 1093/2687 1076/2693 1064/2570 1047/2501 1061/2413 1042/2287 1036/2241 1062/2230 1103/2188 1184/2193 1181/2108 1116/2005 1097/1910 1057/1795 1039/1705 1017/1607 1041/1578 1109/1594 1103/1530 1121/1494 1119/1434 1067/1324 990/1216 951/1150 898/1077 856/1009 836/957 826/912 823/873 783/822 786/817 774/800 749/781 720/779 669/740 655/746 657/771 681/773 723/790 733/775 684/707 695/710 710/714 757/760 772/790 791/871 774/1099 863/1783 968/2950 1627/4189 2378/4959 3605/5639 4511/5765 5047/5729 4955/5304 4635/4843 4321/4448 4101/4240 3917/4083 3866/4034 3778/3917 3709/3816 3516/3578 3353/3392 3204/3232 3096/3141 3018/3067 2991/3022 2963/3003 2994/3028 2963/2986 2923/2942 2830/2853 2671/2714 2537/2604 2411/2477 2363/2455 2295/2409 2298/2399 2271/2350 2281/2348 2230/2298 2158/2230 2112/2189 2082/2164 2102/2202 2093/2218 2114/2246 2143/2264 2156/2237 2164/2189 2120/2127 2019/2029 1941/1954 1905/1917 1856/1874 1864/1883 1772/1789 1708/1731 1673/1720 1636/1728 1554/1705 1539/1745 1562/1783 1587/1787 1561/1745 1579/1719 1603/1697 1576/1644 1535/1570 1497/1525 1505/1519 1502/1511 1500/1505 1490/1503 1481/1494 1463/1486 1466/1494 1459/1480 1412/1431 1368/1382 1320/1328 1247/1255 1201/1210 1131/1145 1084/1099 993/1014 950/969 906/926 877/896 842/859 807/820 815/818 844/845 856 868 869 847 842/844 800/802 794/801 779/787 784/789 843/849 914/918 979/983 1004/1006 1015/1016 1017/1018 976 994 1012 1005 985 978 962 928 889/891 893/905 879/904 899/940 894/952 895/978 894/979 923/975 961/982 968/985 1043/1071 1085/1109 1096/1125 1101/1124 1079/1090 1076/1087 1059/1071 998/1010 939/949 901/907 861/864 834/840 778/799 773/791 779/804 747/770 718/747 667/727 741/815 778/893 791/932 849/968 931/1022 959/1030 976/1026 971/997 939/975 927/1014 923/1074 976/1189 1025/1335 1123/1587 1282/2006 1580/2483 2013/3001 2722/3535 3299/3968 3491/3982 3461/3771 3327/3515 3175/3288 2958/3023 2733/2771 2594/2619 2423/2447 2266/2286 2160/2179 2030/2050 1946/1961 1855/1867 1822/1833 1850/1873 1842/1929 1863/1978 1904/2057 2006/2187 2027/2228 2097/2239 2090/2233 2109/2225 2086/2203 2027/2153 2036/2126 2082/2141 2150/2208 2239/2354 2419/2658 2647/2955 2884/3152 3191/3428 3472/3763 3764/3993 4042/4219 4124/4254 4277/4372 4200/4359 4085/4294 4117/4399 4145/4416 4258/4500 4319/4486 4292/4416 4207/4297 4146/4193 4020/4059 3902/3941 3749/3788 3599/3632 3511/3537 3360/3386 3289/3309 3210/3248 3081/3144 3035/3091 2936/3002 2883/2961 2825/2915 2823/2915 2830/2905 2835/2864 2777/2789 2775/2782 2740/2743 2736 2646/2653 2588/2605 2568/2592 2586/2647 2568/2657 2678/2754 2681/2765 2762/2819 2825/2867 2860/2909 2803/2858 2911/2956 2909/2969 2939/3001 2907/3006 2897/2996 2864/2953 2838/2927 2815/2878 2742/2786 2692/2729 2651/2690 2604/2664 2577/2621 2505/2544 2469/2488 2424/2441 2329/2357 2258/2292 2154/2198 2181/2224 2139/2177 2111/2156 2120/2170 2108/2154 2144/2187 2125/2180 2216/2277 2291/2362 2431/2503 2495/2548 2499/2533 2548/2591 2563/2630 2575/2691 2570/2719 2582/2718 2532/2624 2383/2432 2345/2371 2254/2266 2184/2191 2164/2172 2139/2171 2156/2204 2116/2174 2094/2125 2031/2054 1965/1981 1897/1908 1819/1830 1766/1774 1720/1730 1646/1655 1634/1639 1592/1595 1542/1545 1517/1519 1481/1488 1482/1495 1441/1463 1351/1387 1328/1390 1285/1358 1317/1416 1378/1456 1493/1566 1557/1591 1581/1629 1568/1625 1655/1739 1702/1792 1752/1841 1796/1857 1832/1863 1769/1789 1687/1716 1651/1700 1591/1665 1594/1683 1514/1613 1493/1579 1447/1522 1409/1471 1352/1454 1357/1482 1359/1504 1354/1502 1413/1546 1441/1546 1464/1561 1456/1525 1481/1541 1444/1497 1417/1473 1396/1449 1334/1373 1303/1329 1315/1329 1304/1310 1325/1335 1279/1291 1253/1272 1230/1268 1222/1256 1177/1221 1131/1168 1040/1065 1001/1020 999/1015 970/978 932/942 929/935 882 828 777 771/772 762/763 732/733 694/699 684/687 643/646 616/618 622/623 632/633 626 583 571 542 510/511 487 465/476 432/458 436/462 433/461 470/486 477/488 455/469 427/436 424/435 440/445 440/445 445/447 261/431 293/527 343/668 330/846 403/895 430/934 433/955 482/997 502/1003 530/974 530/941 519/871 500/830 480/790 441/745 415/719 376/686 346/684 331/747 323/769 316/827 355/856 404/871 380/896 348/914 324/1006 364/1288 439/1505 578/1709 633/1916 693/2041 654/2093 698/2135 657/2135 663/2159 629/2366 687/2617 761/2822 903/3094 1060/3414 1323/3630 1476/3567 1437/3441 1333/3192 1204/2968 1129/2870 1111/2834 1067/2880 1089/2797 1096/2739 1159/2703 1153/2661 1128/2586 1134/2583 1116/2536 1136/2655 1202/2661 1234/2650 1278/2640 1204/2608 1209/2653 1214/2658 1146/2645 1205/2639 1276/2730 1303/2738 1306/2668 1251/2513 1192/2385 1153/2298 1115/2300 1126/2310 1121/2399 1091/2588 1020/2645 970/2732 1078/2835 1201/2878 1181/2883 1236/2839 1243/2751 1158/2734 1133/2651 1067/2674 1096/2838 1092/2921 1189/3038 1256/3060 1336/3107 1363/3116 1333/3068 1166/2949 1107/2872 1044/2762 1034/2648 1016/2553 1052/2470 1008/2374 988/2337 970/2300 0/2249 0/2419 0/2642 0/3006 0/3204 0/3364 0/3355 0/3370 0/3411 0/3405 0/3415 0/3417 0/3445 0/3418 0/3386 0/3380 0/3369 0/3464 0/3557 0/3554 0/3511 0/3439 0/3379 0/3297 0/3267 0/3172 0/3100 0/3002 0/2935 0/2925 0/3056 0/3123 0/3152 0/3174 0/3177 0/3119 0/2982 0/2897 0/2836 0/2749 0/2706 0/2639 0/2571 0/2551 0/2515 0/2468 0/2388 0/2327 0/2291 0/2287 0/2283 0/2240 0/2262 0/2238 0/2200 0/2202 0/2175 0/2210 0/2254 0/2310 0/2368 0/2427 0/2466 0/2470 0/2459 0/2401 0/2347 0/2312 0/2298 0/2226 0/2127 0/2070 0/2008 0/1926 0/1847 0/1762 0/1697 0/1625 0/1515 0/1472 0/1403 0/1353 0/1307 0/1237 0/1205 0/1174 0/1200 0/1277 0/1363 0/1430 0/1490 0/1603 0/1630 0/1714 0/1782 0/1762 0/1794 0/1771 0/1761 0/1760 0/1715 0/1699 0/1733 0/1750 0/1664 0/1556 0/1466 0/1380 0/1329 0/1224 0/1218 0/1222 0/1278 0/1342 0/1419 0/1482 0/1517 0/1530 0/1489 0/1485 0/1458 0/1535 0/1585 0/1668 0/1706 0/1707 0/1717 0/1702 0/1709 0/1707 0/1748 0/1808 0/1851 0/1850 0/1871 0/1809 0/1807 0/1801 1/1754 1/1773 2/1802 4/1945 16/2024 32/2046 81/2026 129/1954 193/1876 272/1803 314/1723 316/1651 285/1541 292/1521 316/1447 334/1364 375/1267 420/1202 456/1162 475/1110 468/1073 432/1016 421/983 389/959 357/950 363/977 376/1015 377/1019 372/1025 371/1070 359/1079 414/1158 454/1199 483/1194 499/1197 488/1151 484/1137 468/1125 467/1118 455/1109 421/1097 384/1065 346/1010 332/1018 311/991 294/1037 280/1070 267/1090 250/1065 235/1024 224/1017 207/1025 200/1001 189/976 185/933 171/865 163/843 147/846 141/846 139/866 138/864 122/852 113/840 106/844 117/857 123/844 116/818 105/794 104/799 101/810 93/811 90/794 87/745 82/763 79/763 70/778 68/754 63/744 65/728 89/714 122/712 160/735 212/762 225/743 232/729 206/660 205/647 186/592 162/568 149/530 143/532 131/515 125/535 132/552 132/563 120/553 131/565 136/599 134/622 138/678 125/722 119/751 117/755 112/743 100/732 106/701 91/697 89/669 82/693 71/819 70/995 72/1247 79/1390 84/1501 151/1507 267/1469 357/1391 372/1340 334/1221 305/1132 259/1091 211/1043 178/1034 157/1048 132/1041 137/1047 134/1048 110/1096 130/1200 123/1306 180/1430 248/1595 329/1625 384/1586 413/1504 397/1440 366/1354 339/1291 338/1251 316/1235 266/1173 251/1183 220/1170 211/1214 213/1236 226/1215 293/1293 305/1294 351/1294 413/1304 410/1266 398/1194 353/1126 323/1095 300/1107 288/1101 298/1146 300/1166 298/1207 317/1171 335/1183 385/1226 396/1248 446/1307 498/1285 531/1248 528/1213 506/1166 465/1099 462/1120 494/1153 492/1168 484/1212 500/1246 513/1278 520/1286 551/1278 538/1253 547/1213 505/1120 475/1043 448/974 413/889 363/831 330/798 296/801 294/793 273/811 300/833 337/803 351/752 339/751 322/702 343/727 304/722 296/753 270/754 261/788 244/798 248/871 243/892 321/1013 430/1151 534/1205 604/1266 671/1326 719/1334 775/1394 809/1452 819/1480 833/1524 845/1589 834/1669 846/1715 856/1782 898/1772 849/1743 867/1734 914/1809 972/1824 952/1729 927/1625 922/1553 870/1494 852/1463 807/1375 767/1339 707/1256 708/1248 684/1207 690/1194 674/1173 632/1117 577/1049 540/1042 510/1047 511/1074 535/1075 566/1056 587/1049 592/996 573/937 569/885 558/841 516/787 498/757 459/714 438/702 432/698 376/670 354/677 358/686 353/679 346/658 330/628 358/613 355/600 376/580 353/579 346/581 321/608 296/629 284/666 272/663 266/664 255/706 244/822 288/907 335/963 389/1016 405/1024 464/1054 472/1130 462/1305 389/1729 367/2884 357/4133 379/5022 523/5421 1016/5406 1894/5274 2559/4940 2929/4396 2612/3646 2104/2868 1628/2237 1354/1873 1174/1607 1027/1409 909/1271 820/1154 779/1120 723/1097 670/1064 649/1030 598/1015 576/1032 545/1062 565/1118 610/1194 584/1205 632/1191 622/1168 647/1136 659/1072 619/987 592/953 558/887 537/852 493/827 481/824 503/873 488/931 489/965 496/1058 569/1264 579/1470 643/1590 649/1636 837/1691 911/1767 941/1767 1009/1691 958/1636 1000/1508 932/1365 912/1310 868/1212 871/1184 888/1142 883/1124 865/1091 825/1077 737/1014 687/1020 662/1039 606/1034 563/1044 525/1017 515/1069 555/1082 599/1081 638/1057 650/1016 681/998 677/958 666/903 647/798 553/675 489/600 460/544 424/523 410/508 411/510 387/511 369/517 384/546 369/545 329/539 327/546 329/572 299/588 139/628 147/712 138/884 161/1032 196/1277 260/1546 317/1724 368/1849 363/1930 353/1921 366/2008 429/2034 463/2043 494/2035 538/2032 592/1998 566/1863 581/1808 564/1742 524/1659 506/1604 471/1524 392/1459 368/1424 325/1407 335/1424 324/1399 319/1417 341/1467 327/1490 330/1516 270/1501 262/1465 278/1479 275/1507 295/1502 286/1489 311/1463 281/1391 253/1367 244/1358 254/1377 242/1355 266/1403 228/1352 244/1384 243/1362 306/1359 355/1340 366/1232 75/1143 89/1164 57/1210 32/1314 19/1314 20/1301 24/1264 15/1222 18/1185 13/1179 15/1120 8/1100 9/1101 6/1063 9/1056 7/1041 10/1033 15/1057 21/1110 28/1115 19/1055 7/986 1/946 0/906 0/869 0/824 0/815 0/785 0/771 0/764 0/752 0/763 0/767 0/737 0/735 0/678 0/646 0/601 0/514 4/448 3/406 2/367 0/330 0/295 0/271 0/241 0/223 0/204 0/192 0/182 0/181 0/165 0/141 0/118 0/101 0/85 0/80 0/79 0/70 0/59 0/54 0/53 0/45 0/41 0/41 0/36 0/28 0/28 0/28 0/31 0/27 0/26 0/22 0/20 0/17 0/17 0/18 0/17 0/16 0/17 0/15 0/13 0/8 0/6 0/5 0/6 0/4 0/2 0/2 0/1 0/1 = depth1640

#C depth = 1552
#C breadth = 12
#CLL state-numbering golly
x = 219, y = 455, rule = B356/S3568
2o$obo$bobo$4o$2bo$2b4o$4bo$2b2obo$4bo$3bo$2bo$b2obo$2bo$2bobo$2bo
$2b2o$2bo$2b2obo2$4bobo$6bo$8b2obo$6b2ob3o$8b5o$6b2o2b3o$8bo2b2o$
8b6o$7b6o$9b2obo$11b2o$9b6o$11bobo$11b3o$12bobo$11b5o$13b3o$11b2ob
o$12b3obo$12bo3bo$14b3o$14b2obo$17b2o$14bobobo$16b2o$14bo2bo$17b2o
2$16b3o$15b2o$16bo$16b3o$16bo$17b2o$18b2o$16b4o$18b2o$19bo$20b2o$
19bobo$21b3o$19bo$21b3o$21b2o$23b4o$22b3o$23b4o$22bo2bobo$26bo$25b
ob2o$24b2obobo$23b5o$25b2o$28bo$27b2o$26b2o$26bobo$27b4o$26bo2b2o$
27b4obo$29bob2o$31b3o$29bobobo$32bob3o$32b2obo$34b2obo$33b5o$33b2o
b2o$33bob2o$33b3o$35bo$35bobo$35b3obo$37bobo$37b3o$38bo$37b2o$37bo
b2o$40b2obo$39b3obo$39bo3bo$40bo4b2o$41bo2b2o$42b2ob2o$45b2o$45bob
2o$44b3o$44b4o$44b4o$47b2o2$47b3o$47b3o$47b4o$47bob2o$47b2o$49b4o$
50bobo$51b2o$49b2o2bo$50b2o$49b5o$51bo$49b3obo$51bobo$51b2o$50bob
2o$51b5o$54bo$53b3o$54b4o$55b3o$55bob2o$54bob3o$56b4o$56b2o$56b4ob
o$57bo2bo$61b3o$59b3obo$60b2o2bo$61b3o$61b3obo$62bobobo$63b3o$66bo
$65b2o$64bo2b2o$64b2o2bo$67b2obo2$68b2o2$69bo$68b3o$69bo$69b2ob2o$
70b4o$70bo$69b4o$69bobobobo$70bob4o$72b4o$71bobo$76bo$74b3o$74b3o$
74b2o$77bo$76b3o$75b3o$78bo$77bob2o$76b3o2bo$76b6o$77bob2o2bo$77bo
b2obo$77b5o$79bobo$82bo$83b2o$82bobobo$84bobo$85b5o$85b4o$84bob3ob
o$85b5o$88b2o$90bo$88b3obo$91bo$90b2o2$91bobo$92b2o$91b4o$94bo$93b
2obo$94b2o$94bob2o$98bo$96b4o$97b4o$98b3o$100b3o$98b2o$99b2o$98b3o
$99bo$98b2obo$99b3o$99b4o$99b5o$100b2obo$100b4o$101b3o$100bo$101b
3o$102b3o$101bob3obo$102bob4o$104b2ob2o$104b2ob2o$105b3o$105bob3o$
106b5o$105b2ob3o$105b2o2b2o$110b2o$109bobo$109bo$108b3o$110bob3o$
111bo2bo$110b2o$110b3o$110b4o$109b5o$111bob2obo$111b5o$111b4o$112b
ob2o$114b5o$113bob2o$116b3o$115bobo$115b2o$118bo$115b5o$115b5o$
114b2obo$116b6o$118bo2bo$118bob3o$117bo3b2o$120b2obo$121bo3bo$121b
3o$121bo2bo$123b2o$122b3o$123bo2bo$122bobobo$122bob2o$123b3obo$
123b3o$125b2o$126bobo$124b4obo$126b3o$124b3obobo$126bo2bo$126b3ob
2o$128b4o$128b2obo$131b3o$130b5o$131b2o$131b2o2bo$132b3o$131bob2o$
134b2o$132bob4o$135b2o$134b2o2bo$133b2ob2o$134bob2obo$134b2obobo$
134b3o2bo$135b4o$137bo$140b2o$139bob2o2bo$140b5obo$141b2o2b2o$144b
5o$144b3o$144b4o$147bobo$146bobo$147b3o$146b4o$148b2o$145bob4o$
148b2o2bo$146bo2bo$146b4ob2o$148b3o$151b2o$149b2o$150b4o$149b2obo$
149b2ob4o$150bob3obo$152b2o2bo$152bobobo$153b4o$152b6o$157bo$154b
2ob2o$155b4obo$156b2ob2o$158b2o$158b4o$159b2o$158b3o$158b3ob2o$
159b2ob2o$158b3obo$160b3o$159b5o$162b2o$161b2o$161b2obo$161b4o$
162b3o$162b3o$165bo$162b5o$164bobobo$163b6o$165b4o$165b6o$165b5obo
$164bo2b4o$167b2obobo$166bo3bobo2$169bobo$168b3ob2o$168bob2obo$
170bob2o$169b2ob2o$169b3o$171bobobo$171b6o$175bo$171bo3bo$173bob2o
$174bob2o$175bobo$176b2o$178bo$176b2o$176bobo$177bob2o$179bo$179bo
$178bo$178b3o$178b2o$180bo$179bo$178b2o$178b3o$180b4o$179b3obo$
179b4ob2o$181b3o$179b2o2b3o$180b2obo$180b3ob2o$181b3obo$182bob2o$
182bo2b2o$183bobo$183b3o$182b3obo$183b2obo$182bo$184bob2o$184bob2o
$186bob2o$189bo$188bo$189bobo$189b2o$190b3o$188b2o2b2o$190bobo$
189bob2o$191b4o$192b2ob2o$192bobobo$194b2o$193bobo$193b3o$194b3o$
196bo$193b2ob2o2$193bobo$195b4o$194b4o$195bob3o$194b2obobo$198bo$
195bobobo$199bobo$201bo$203bo$200b2o$200b4o$200b3obo$199bo2b2o$
200b3o2bo$200bo2b4o$203b4o$203b5o$204bob2o$203b3o$204b3o$205b3o$
206bo2b2o$205b3obo$210bo$205b2o3bo$207bo$209b2o$208b2o$211b2o$208b
4o$209bob2o$208b2ob2o$208b2ob3o$207b5obo$209b2obo$215bo$213bo$212b
4o$212b2ob2o$212b2o2bo$211bo2bo$211b4o2b2o$212bob4o$212bo2bo!


#C depth = 1553
#C breadth = 12
#CLL state-numbering golly
x = 220, y = 456, rule = B356/S3568
2o$obo$bobo$4o$2bo$2b4o$4bo$2b2obo$4bo$3bo$2bo$b2obo$2bo$2bobo$2bo
$2b2o$2bo$2b2obo2$4bobo$6bo$8b2obo$6b2ob3o$8b5o$6b2o2b3o$8bo2b2o$
8b6o$7b6o$9b2obo$11b2o$9b6o$11bobo$11b3o$12bobo$11b5o$13b3o$11b2ob
o$12b3obo$12bo3bo$14b3o$14b2obo$17b2o$14bobobo$16b2o$14bo2bo$17b2o
2$16b3o$15b2o$16bo$16b3o$16bo$17b2o$18b2o$16b4o$18b2o$19bo$20b2o$
19bobo$21b3o$19bo$21b3o$21b2o$23b4o$22b3o$23b4o$22bo2bobo$26bo$25b
ob2o$24b2obobo$23b5o$25b2o$28bo$27b2o$26b2o$26bobo$27b4o$26bo2b2o$
27b4obo$29bob2o$31b3o$29bobobo$32bob3o$32b2obo$34b2obo$33b5o$33b2o
b2o$33bob2o$33b3o$35bo$35bobo$35b3obo$37bobo$37b3o$38bo$37b2o$37bo
b2o$40b2obo$39b3obo$39bo3bo$40bo4b2o$41bo2b2o$42b2ob2o$45b2o$45bob
2o$44b3o$44b4o$44b4o$47b2o2$47b3o$47b3o$47b4o$47bob2o$47b2o$49b4o$
50bobo$51b2o$49b2o2bo$50b2o$49b5o$51bo$49b3obo$51bobo$51b2o$50bob
2o$51b5o$54bo$53b3o$54b4o$55b3o$55bob2o$54bob3o$56b4o$56b2o$56b4ob
o$57bo2bo$61b3o$59b3obo$60b2o2bo$61b3o$61b3obo$62bobobo$63b3o$66bo
$65b2o$64bo2b2o$64b2o2bo$67b2obo2$68b2o2$69bo$68b3o$69bo$69b2ob2o$
70b4o$70bo$69b4o$69bobobobo$70bob4o$72b4o$71bobo$76bo$74b3o$74b3o$
74b2o$77bo$76b3o$75b3o$78bo$77bob2o$76b3o2bo$76b6o$77bob2o2bo$77bo
b2obo$77b5o$79bobo$82bo$83b2o$82bobobo$84bobo$85b5o$85b4o$84bob3ob
o$85b5o$88b2o$90bo$88b3obo$91bo$90b2o2$91bobo$92b2o$91b4o$94bo$93b
2obo$94b2o$94bob2o$98bo$96b4o$97b4o$98b3o$100b3o$98b2o$99b2o$98b3o
$99bo$98b2obo$99b3o$99b4o$99b5o$100b2obo$100b4o$101b3o$100bo$101b
3o$102b3o$101bob3obo$102bob4o$104b2ob2o$104b2ob2o$105b3o$105bob3o$
106b5o$105b2ob3o$105b2o2b2o$110b2o$109bobo$109bo$108b3o$110bob3o$
111bo2bo$110b2o$110b3o$110b4o$109b5o$111bob2obo$111b5o$111b4o$112b
ob2o$114b5o$113bob2o$116b3o$115bobo$115b2o$118bo$115b5o$115b5o$
114b2obo$116b6o$118bo2bo$118bob3o$117bo3b2o$120b2obo$121bo3bo$121b
3o$121bo2bo$123b2o$122b3o$123bo2bo$122bobobo$122bob2o$123b3obo$
123b3o$125b2o$126bobo$124b4obo$126b3o$124b3obobo$126bo2bo$126b3ob
2o$128b4o$128b2obo$131b3o$130b5o$131b2o$131b2o2bo$132b3o$131bob2o$
134b2o$132bob4o$135b2o$134b2o2bo$133b2ob2o$134bob2obo$134b2obobo$
134b3o2bo$135b4o$137bo$140b2o$139bob2o2bo$140b5obo$141b2o2b2o$144b
5o$144b3o$144b4o$147bobo$146bobo$147b3o$146b4o$148b2o$145bob4o$
148b2o2bo$146bo2bo$146b4ob2o$148b3o$151b2o$149b2o$150b4o$149b2obo$
149b2ob4o$150bob3obo$152b2o2bo$152bobobo$153b4o$152b6o$157bo$154b
2ob2o$155b4obo$156b2ob2o$158b2o$158b4o$159b2o$158b3o$158b3ob2o$
159b2ob2o$158b3obo$160b3o$159b5o$162b2o$161b2o$161b2obo$161b4o$
162b3o$162b3o$165bo$162b5o$164bobobo$163b6o$165b4o$165b6o$165b5obo
$164bo2b4o$167b2obobo$166bo3bobo2$169bobo$168b3ob2o$168bob2obo$
170bob2o$169b2ob2o$169b3o$171bobobo$171b6o$175bo$171bo3bo$173bob2o
$174bob2o$175bobo$176b2o$178bo$176b2o$176bobo$177bob2o$179bo$179bo
$178bo$178b3o$178b2o$180bo$179bo$178b2o$178b3o$180b4o$179b3obo$
179b4ob2o$181b3o$179b2o2b3o$180b2obo$180b3ob2o$181b3obo$182bob2o$
182bo2b2o$183bobo$183b3o$182b3obo$183b2obo$182bo$184bob2o$184bob2o
$186bob2o$189bo$188bo$189bobo$189b2o$190b3o$188b2o2b2o$190bobo$
189bob2o$191b4o$192b2ob2o$192bobobo$194b2o$193bobo$193b3o$194b3o$
196bo$193b2ob2o2$193bobo$195b4o$194b4o$195bob3o$194b2obobo$198bo$
195bobobo$199bobo$201bo$203bo$200b2o$200b4o$200b3obo$199bo2b2o$
200b3o2bo$200bo2b4o$203b4o$203b5o$204bob2o$203b3o$204b3o$205b3o$
206bo2b2o$205b3obo$210bo$205b2o3bo$207bo$209b2o$208b2o$211b2o$208b
4o$209bob2o$208b2ob2o$208b2ob3o$207b5obo$209b2obo$215bo$213bo$212b
4o$212b2ob2o$212b2o2bo$211bo2bo$214bo$211bobobob3o$213bo2bo$212bo!


#C depth = 1560
#C breadth = 11
#CLL state-numbering golly
x = 223, y = 457, rule = B356/S3568
2o$obo$bobo$4o$2bo$2b4o$4bo$2b2obo$4bo$3bo$2bo$b2obo$2bo$2bobo$2bo
$2b2o$2bo$2b2obo2$4bobo$6bo$8b2obo$6b2ob3o$8b5o$6b2o2b3o$8bo2b2o$
8b6o$7b6o$9b2obo$11b2o$9b6o$11bobo$11b3o$12bobo$11b5o$13b3o$11b2ob
o$12b3obo$12bo3bo$14b3o$14b2obo$17b2o$14bobobo$16b2o$14bo2bo$17b2o
2$16b3o$15b2o$16bo$16b3o$16bo$17b2o$18b2o$16b4o$18b2o$19bo$20b2o$
19bobo$21b3o$19bo$21b3o$21b2o$23b4o$22b3o$23b4o$22bo2bobo$26bo$25b
ob2o$24b2obobo$23b5o$25b2o$28bo$27b2o$26b2o$26bobo$27b4o$26bo2b2o$
27b4obo$29bob2o$31b3o$29bobobo$32bob3o$32b2obo$34b2obo$33b5o$33b2o
b2o$33bob2o$33b3o$35bo$35bobo$35b3obo$37bobo$37b3o$38bo$37b2o$37bo
b2o$40b2obo$39b3obo$39bo3bo$40bo4b2o$41bo2b2o$42b2ob2o$45b2o$45bob
2o$44b3o$44b4o$44b4o$47b2o2$47b3o$47b3o$47b4o$47bob2o$47b2o$49b4o$
50bobo$51b2o$49b2o2bo$50b2o$49b5o$51bo$49b3obo$51bobo$51b2o$50bob
2o$51b5o$54bo$53b3o$54b4o$55b3o$55bob2o$54bob3o$56b4o$56b2o$56b4ob
o$57bo2bo$61b3o$59b3obo$60b2o2bo$61b3o$61b3obo$62bobobo$63b3o$66bo
$65b2o$64bo2b2o$64b2o2bo$67b2obo2$68b2o2$69bo$68b3o$69bo$69b2ob2o$
70b4o$70bo$69b4o$69bobobobo$70bob4o$72b4o$71bobo$76bo$74b3o$74b3o$
74b2o$77bo$76b3o$75b3o$78bo$77bob2o$76b3o2bo$76b6o$77bob2o2bo$77bo
b2obo$77b5o$79bobo$82bo$83b2o$82bobobo$84bobo$85b5o$85b4o$84bob3ob
o$85b5o$88b2o$90bo$88b3obo$91bo$90b2o2$91bobo$92b2o$91b4o$94bo$93b
2obo$94b2o$94bob2o$98bo$96b4o$97b4o$98b3o$100b3o$98b2o$99b2o$98b3o
$99bo$98b2obo$99b3o$99b4o$99b5o$100b2obo$100b4o$101b3o$100bo$101b
3o$102b3o$101bob3obo$102bob4o$104b2ob2o$104b2ob2o$105b3o$105bob3o$
106b5o$105b2ob3o$105b2o2b2o$110b2o$109bobo$109bo$108b3o$110bob3o$
111bo2bo$110b2o$110b3o$110b4o$109b5o$111bob2obo$111b5o$111b4o$112b
ob2o$114b5o$113bob2o$116b3o$115bobo$115b2o$118bo$115b5o$115b5o$
114b2obo$116b6o$118bo2bo$118bob3o$117bo3b2o$120b2obo$121bo3bo$121b
3o$121bo2bo$123b2o$122b3o$123bo2bo$122bobobo$122bob2o$123b3obo$
123b3o$125b2o$126bobo$124b4obo$126b3o$124b3obobo$126bo2bo$126b3ob
2o$128b4o$128b2obo$131b3o$130b5o$131b2o$131b2o2bo$132b3o$131bob2o$
134b2o$132bob4o$135b2o$134b2o2bo$133b2ob2o$134bob2obo$134b2obobo$
134b3o2bo$135b4o$137bo$140b2o$139bob2o2bo$140b5obo$141b2o2b2o$144b
5o$144b3o$144b4o$147bobo$146bobo$147b3o$146b4o$148b2o$145bob4o$
148b2o2bo$146bo2bo$146b4ob2o$148b3o$151b2o$149b2o$150b4o$149b2obo$
149b2ob4o$150bob3obo$152b2o2bo$152bobobo$153b4o$152b6o$157bo$154b
2ob2o$155b4obo$156b2ob2o$158b2o$158b4o$159b2o$158b3o$158b3ob2o$
159b2ob2o$158b3obo$160b3o$159b5o$162b2o$161b2o$161b2obo$161b4o$
162b3o$162b3o$165bo$162b5o$164bobobo$163b6o$165b4o$165b6o$165b5obo
$164bo2b4o$167b2obobo$166bo3bobo2$169bobo$168b3ob2o$168bob2obo$
170bob2o$169b2ob2o$169b3o$171bobobo$171b6o$175bo$171bo3bo$173bob2o
$174bob2o$175bobo$176b2o$178bo$176b2o$176bobo$177bob2o$179bo$179bo
$178bo$178b3o$178b2o$180bo$179bo$178b2o$178b3o$180b4o$179b3obo$
179b4ob2o$181b3o$179b2o2b3o$180b2obo$180b3ob2o$181b3obo$182bob2o$
182bo2b2o$183bobo$183b3o$184b2o$186b2o$183b5o$183bob4o$185b4o$184b
5o$187b3o2$187bo$185bobobo$188b2o$185bo2bo$189bo$186bob3o$189bobo$
186b3o2bo$187b3obo$189b2o$187bobo$188bo$190bo2$190b3o$189b2o$189b
2o$188bobo$189b2obo$191b3o$192b3o$192b4o$192b5o$194b4o$195bo$198bo
bo$197bob2o$196b4o$197b5o$198b3obo$199b2o$200b3o$201bo$199bo$200bo
bo$200bobo$200b4o$200b4obo$200bo2b2o$201b2ob2o$202b2o$202bo2bo$
202b4o$205bo$204b2o$203b3o2bo$205bobobobo$207bob3o$208bo2b2o$208b
2obo2bo$211b4o$209bob5o$212b3o$212bo$215b4o$213b5o$216b2o$213b4o2b
o$214bo3b2o$214bo2b4o$216b4ob2o$218bobo$218bo!


#C depth = 1561
#C breadth = 11
#CLL state-numbering golly
x = 223, y = 457, rule = B356/S3568
2o$obo$bobo$4o$2bo$2b4o$4bo$2b2obo$4bo$3bo$2bo$b2obo$2bo$2bobo$2bo
$2b2o$2bo$2b2obo2$4bobo$6bo$8b2obo$6b2ob3o$8b5o$6b2o2b3o$8bo2b2o$
8b6o$7b6o$9b2obo$11b2o$9b6o$11bobo$11b3o$12bobo$11b5o$13b3o$11b2ob
o$12b3obo$12bo3bo$14b3o$14b2obo$17b2o$14bobobo$16b2o$14bo2bo$17b2o
2$16b3o$15b2o$16bo$16b3o$16bo$17b2o$18b2o$16b4o$18b2o$19bo$20b2o$
19bobo$21b3o$19bo$21b3o$21b2o$23b4o$22b3o$23b4o$22bo2bobo$26bo$25b
ob2o$24b2obobo$23b5o$25b2o$28bo$27b2o$26b2o$26bobo$27b4o$26bo2b2o$
27b4obo$29bob2o$31b3o$29bobobo$32bob3o$32b2obo$34b2obo$33b5o$33b2o
b2o$33bob2o$33b3o$35bo$35bobo$35b3obo$37bobo$37b3o$38bo$37b2o$37bo
b2o$40b2obo$39b3obo$39bo3bo$40bo4b2o$41bo2b2o$42b2ob2o$45b2o$45bob
2o$44b3o$44b4o$44b4o$47b2o2$47b3o$47b3o$47b4o$47bob2o$47b2o$49b4o$
50bobo$51b2o$49b2o2bo$50b2o$49b5o$51bo$49b3obo$51bobo$51b2o$50bob
2o$51b5o$54bo$53b3o$54b4o$55b3o$55bob2o$54bob3o$56b4o$56b2o$56b4ob
o$57bo2bo$61b3o$59b3obo$60b2o2bo$61b3o$61b3obo$62bobobo$63b3o$66bo
$65b2o$64bo2b2o$64b2o2bo$67b2obo2$68b2o2$69bo$68b3o$69bo$69b2ob2o$
70b4o$70bo$69b4o$69bobobobo$70bob4o$72b4o$71bobo$76bo$74b3o$74b3o$
74b2o$77bo$76b3o$75b3o$78bo$77bob2o$76b3o2bo$76b6o$77bob2o2bo$77bo
b2obo$77b5o$79bobo$82bo$83b2o$82bobobo$84bobo$85b5o$85b4o$84bob3ob
o$85b5o$88b2o$90bo$88b3obo$91bo$90b2o2$91bobo$92b2o$91b4o$94bo$93b
2obo$94b2o$94bob2o$98bo$96b4o$97b4o$98b3o$100b3o$98b2o$99b2o$98b3o
$99bo$98b2obo$99b3o$99b4o$99b5o$100b2obo$100b4o$101b3o$100bo$101b
3o$102b3o$101bob3obo$102bob4o$104b2ob2o$104b2ob2o$105b3o$105bob3o$
106b5o$105b2ob3o$105b2o2b2o$110b2o$109bobo$109bo$108b3o$110bob3o$
111bo2bo$110b2o$110b3o$110b4o$109b5o$111bob2obo$111b5o$111b4o$112b
ob2o$114b5o$113bob2o$116b3o$115bobo$115b2o$118bo$115b5o$115b5o$
114b2obo$116b6o$118bo2bo$118bob3o$117bo3b2o$120b2obo$121bo3bo$121b
3o$121bo2bo$123b2o$122b3o$123bo2bo$122bobobo$122bob2o$123b3obo$
123b3o$125b2o$126bobo$124b4obo$126b3o$124b3obobo$126bo2bo$126b3ob
2o$128b4o$128b2obo$131b3o$130b5o$131b2o$131b2o2bo$132b3o$131bob2o$
134b2o$132bob4o$135b2o$134b2o2bo$133b2ob2o$134bob2obo$134b2obobo$
134b3o2bo$135b4o$137bo$140b2o$139bob2o2bo$140b5obo$141b2o2b2o$144b
5o$144b3o$144b4o$147bobo$146bobo$147b3o$146b4o$148b2o$145bob4o$
148b2o2bo$146bo2bo$146b4ob2o$148b3o$151b2o$149b2o$150b4o$149b2obo$
149b2ob4o$150bob3obo$152b2o2bo$152bobobo$153b4o$152b6o$157bo$154b
2ob2o$155b4obo$156b2ob2o$158b2o$158b4o$159b2o$158b3o$158b3ob2o$
159b2ob2o$158b3obo$160b3o$159b5o$162b2o$161b2o$161b2obo$161b4o$
162b3o$162b3o$165bo$162b5o$164bobobo$163b6o$165b4o$165b6o$165b5obo
$164bo2b4o$167b2obobo$166bo3bobo2$169bobo$168b3ob2o$168bob2obo$
170bob2o$169b2ob2o$169b3o$171bobobo$171b6o$175bo$171bo3bo$173bob2o
$174bob2o$175bobo$176b2o$178bo$176b2o$176bobo$177bob2o$179bo$179bo
$178bo$178b3o$178b2o$180bo$179bo$178b2o$178b3o$180b4o$179b3obo$
179b4ob2o$181b3o$179b2o2b3o$180b2obo$180b3ob2o$181b3obo$182bob2o$
182bo2b2o$183bobo$183b3o$184b2o$186b2o$183b5o$183bob4o$185b4o$184b
5o$187b3o2$187bo$185bobobo$188b2o$185bo2bo$189bo$186bob3o$189bobo$
186b3o2bo$187b3obo$189b2o$187bobo$188bo$190bo2$190b3o$189b2o$189b
2o$188bobo$189b2obo$191b3o$192b3o$192b4o$192b5o$194b4o$195bo$198bo
bo$197bob2o$196b4o$197b5o$198b3obo$199b2o$200b3o$201bo$199bo$200bo
bo$200bobo$200b4o$200b4obo$200bo2b2o$201b2ob2o$202b2o$202bo2bo$
202b4o$205bo$204b2o$203b3o2bo$205bobobobo$207bob3o$208bo2b2o$208b
2obo2bo$211b4o$209bob5o$212b3o$212bo$215b4o$213b5o$216b2o$213b4o2b
o$214bo3b2o$214bo2b4o$216b4ob2o$218bo2bo$218bo!


#C depth = 1567
#C breadth = 12
#CLL state-numbering golly
x = 227, y = 457, rule = B356/S3568
2o$obo$bobo$4o$2bo$2b4o$4bo$2b2obo$4bo$3bo$2bo$b2obo$2bo$2bobo$2bo
$2b2o$2bo$2b2obo2$4bobo$6bo$8b2obo$6b2ob3o$8b5o$6b2o2b3o$8bo2b2o$
8b6o$7b6o$9b2obo$11b2o$9b6o$11bobo$11b3o$12bobo$11b5o$13b3o$11b2ob
o$12b3obo$12bo3bo$14b3o$14b2obo$17b2o$14bobobo$16b2o$14bo2bo$17b2o
2$16b3o$15b2o$16bo$16b3o$16bo$17b2o$18b2o$16b4o$18b2o$19bo$20b2o$
19bobo$21b3o$19bo$21b3o$21b2o$23b4o$22b3o$23b4o$22bo2bobo$26bo$25b
ob2o$24b2obobo$23b5o$25b2o$28bo$27b2o$26b2o$26bobo$27b4o$26bo2b2o$
27b4obo$29bob2o$31b3o$29bobobo$32bob3o$32b2obo$34b2obo$33b5o$33b2o
b2o$33bob2o$33b3o$35bo$35bobo$35b3obo$37bobo$37b3o$38bo$37b2o$37bo
b2o$40b2obo$39b3obo$39bo3bo$40bo4b2o$41bo2b2o$42b2ob2o$45b2o$45bob
2o$44b3o$44b4o$44b4o$47b2o2$47b3o$47b3o$47b4o$47bob2o$47b2o$49b4o$
50bobo$51b2o$49b2o2bo$50b2o$49b5o$51bo$49b3obo$51bobo$51b2o$50bob
2o$51b5o$54bo$53b3o$54b4o$55b3o$55bob2o$54bob3o$56b4o$56b2o$56b4ob
o$57bo2bo$61b3o$59b3obo$60b2o2bo$61b3o$61b3obo$62bobobo$63b3o$66bo
$65b2o$64bo2b2o$64b2o2bo$67b2obo2$68b2o2$69bo$68b3o$69bo$69b2ob2o$
70b4o$70bo$69b4o$69bobobobo$70bob4o$72b4o$71bobo$76bo$74b3o$74b3o$
74b2o$77bo$76b3o$75b3o$78bo$77bob2o$76b3o2bo$76b6o$77bob2o2bo$77bo
b2obo$77b5o$79bobo$82bo$83b2o$82bobobo$84bobo$85b5o$85b4o$84bob3ob
o$85b5o$88b2o$90bo$88b3obo$91bo$90b2o2$91bobo$92b2o$91b4o$94bo$93b
2obo$94b2o$94bob2o$98bo$96b4o$97b4o$98b3o$100b3o$98b2o$99b2o$98b3o
$99bo$98b2obo$99b3o$99b4o$99b5o$100b2obo$100b4o$101b3o$100bo$101b
3o$102b3o$101bob3obo$102bob4o$104b2ob2o$104b2ob2o$105b3o$105bob3o$
106b5o$105b2ob3o$105b2o2b2o$110b2o$109bobo$109bo$108b3o$110bob3o$
111bo2bo$110b2o$110b3o$110b4o$109b5o$111bob2obo$111b5o$111b4o$112b
ob2o$114b5o$113bob2o$116b3o$115bobo$115b2o$118bo$115b5o$115b5o$
114b2obo$116b6o$118bo2bo$118bob3o$117bo3b2o$120b2obo$121bo3bo$121b
3o$121bo2bo$123b2o$122b3o$123bo2bo$122bobobo$122bob2o$123b3obo$
123b3o$125b2o$126bobo$124b4obo$126b3o$124b3obobo$126bo2bo$126b3ob
2o$128b4o$128b2obo$131b3o$130b5o$131b2o$131b2o2bo$132b3o$131bob2o$
134b2o$132bob4o$135b2o$134b2o2bo$133b2ob2o$134bob2obo$134b2obobo$
134b3o2bo$135b4o$137bo$140b2o$139bob2o2bo$140b5obo$141b2o2b2o$144b
5o$144b3o$144b4o$147bobo$146bobo$147b3o$146b4o$148b2o$145bob4o$
148b2o2bo$146bo2bo$146b4ob2o$148b3o$151b2o$149b2o$150b4o$149b2obo$
149b2ob4o$150bob3obo$152b2o2bo$152bobobo$153b4o$152b6o$157bo$154b
2ob2o$155b4obo$156b2ob2o$158b2o$158b4o$159b2o$158b3o$158b3ob2o$
159b2ob2o$158b3obo$160b3o$159b5o$162b2o$161b2o$161b2obo$161b4o$
162b3o$162b3o$165bo$162b5o$164bobobo$163b6o$165b4o$165b6o$165b5obo
$164bo2b4o$167b2obobo$166bo3bobo2$169bobo$168b3ob2o$168bob2obo$
170bob2o$169b2ob2o$169b3o$171bobobo$171b6o$175bo$171bo3bo$173bob2o
$174bob2o$175bobo$176b2o$178bo$176b2o$176bobo$177bob2o$179bo$179bo
$178bo$178b3o$178b2o$180bo$179bo$178b2o$178b3o$180b4o$179b3obo$
179b4ob2o$181b3o$179b2o2b3o$180b2obo$180b3ob2o$181b3obo$182bob2o$
182bo2b2o$183bobo$183b3o$182b3obo$183b2obo$182bo$184bob2o$184bob2o
$186bob2o$189bo$188bo$189bobo$189b2o$190b3o$188b2o2b2o$190bobo$
189bob2o$191b4o$192b2ob2o$192bobobo$194b2o$193bobo$193b3o$194b3o$
196bo$193b2ob2o2$193bobo$195b4o$194b4o$195bob3o$194b2obobo$198bo$
195bobobo$199bobo$201bo$203bo$200b2o$200b4o$200b3obo$199bo2b2o$
200b3o2bo$200bo2b4o$203b4o$203b5o$204bob2o$203b3o$204b3o$205b3o$
206bo2b2o$205b3obo$210bo$205b2o3bo$207bo$209b2o$208b3o$208bob3o$
209bob4o$208bob2o2bo$210b2obob2o$211bo4bo$215bobo$214bo2bo$213b5o$
216bobo$215bob2obo$220bo$217b2ob3o$217bobob2o$218b3ob3o$217b3o2bob
o$219bo2b2o$220bo4b2o$220b5o!

# 256 iterations (162 problems, 840 subproblems, 94 solutions) completed: queuesize = 4000; heapsize = 13033; treesize = 2672998
# 512 iterations (321 problems, 1589 subproblems, 191 solutions) completed: queuesize = 3999; heapsize = 12998; treesize = 2673132
# 768 iterations (468 problems, 2183 subproblems, 300 solutions) completed: queuesize = 4000; heapsize = 12993; treesize = 2673278

#C depth = 1571
#C breadth = 13
#CLL state-numbering golly
x = 228, y = 459, rule = B356/S3568
2o$obo$bobo$4o$2bo$2b4o$4bo$2b2obo$4bo$3bo$2bo$b2obo$2bo$2bobo$2bo
$2b2o$2bo$2b2obo2$4bobo$6bo$8b2obo$6b2ob3o$8b5o$6b2o2b3o$8bo2b2o$
8b6o$7b6o$9b2obo$11b2o$9b6o$11bobo$11b3o$12bobo$11b5o$13b3o$11b2ob
o$12b3obo$12bo3bo$14b3o$14b2obo$17b2o$14bobobo$16b2o$14bo2bo$17b2o
2$16b3o$15b2o$16bo$16b3o$16bo$17b2o$18b2o$16b4o$18b2o$19bo$20b2o$
19bobo$21b3o$19bo$21b3o$21b2o$23b4o$22b3o$23b4o$22bo2bobo$26bo$25b
ob2o$24b2obobo$23b5o$25b2o$28bo$27b2o$26b2o$26bobo$27b4o$26bo2b2o$
27b4obo$29bob2o$31b3o$29bobobo$32bob3o$32b2obo$34b2obo$33b5o$33b2o
b2o$33bob2o$33b3o$35bo$35bobo$35b3obo$37bobo$37b3o$38bo$37b2o$37bo
b2o$40b2obo$39b3obo$39bo3bo$40bo4b2o$41bo2b2o$42b2ob2o$45b2o$45bob
2o$44b3o$44b4o$44b4o$47b2o2$47b3o$47b3o$47b4o$47bob2o$47b2o$49b4o$
50bobo$51b2o$49b2o2bo$50b2o$49b5o$51bo$49b3obo$51bobo$51b2o$50bob
2o$51b5o$54bo$53b3o$54b4o$55b3o$55bob2o$54bob3o$56b4o$56b2o$56b4ob
o$57bo2bo$61b3o$59b3obo$60b2o2bo$61b3o$61b3obo$62bobobo$63b3o$66bo
$65b2o$64bo2b2o$64b2o2bo$67b2obo2$68b2o2$69bo$68b3o$69bo$69b2ob2o$
70b4o$70bo$69b4o$69bobobobo$70bob4o$72b4o$71bobo$76bo$74b3o$74b3o$
74b2o$77bo$76b3o$75b3o$78bo$77bob2o$76b3o2bo$76b6o$77bob2o2bo$77bo
b2obo$77b5o$79bobo$82bo$83b2o$82bobobo$84bobo$85b5o$85b4o$84bob3ob
o$85b5o$88b2o$90bo$88b3obo$91bo$90b2o2$91bobo$92b2o$91b4o$94bo$93b
2obo$94b2o$94bob2o$98bo$96b4o$97b4o$98b3o$100b3o$98b2o$99b2o$98b3o
$99bo$98b2obo$99b3o$99b4o$99b5o$100b2obo$100b4o$101b3o$100bo$101b
3o$102b3o$101bob3obo$102bob4o$104b2ob2o$104b2ob2o$105b3o$105bob3o$
106b5o$105b2ob3o$105b2o2b2o$110b2o$109bobo$109bo$108b3o$110bob3o$
111bo2bo$110b2o$110b3o$110b4o$109b5o$111bob2obo$111b5o$111b4o$112b
ob2o$114b5o$113bob2o$116b3o$115bobo$115b2o$118bo$115b5o$115b5o$
114b2obo$116b6o$118bo2bo$118bob3o$117bo3b2o$120b2obo$121bo3bo$121b
3o$121bo2bo$123b2o$122b3o$123bo2bo$122bobobo$122bob2o$123b3obo$
123b3o$125b2o$126bobo$124b4obo$126b3o$124b3obobo$126bo2bo$126b3ob
2o$128b4o$128b2obo$131b3o$130b5o$131b2o$131b2o2bo$132b3o$131bob2o$
134b2o$132bob4o$135b2o$134b2o2bo$133b2ob2o$134bob2obo$134b2obobo$
134b3o2bo$135b4o$137bo$140b2o$139bob2o2bo$140b5obo$141b2o2b2o$144b
5o$144b3o$144b4o$147bobo$146bobo$147b3o$146b4o$148b2o$145bob4o$
148b2o2bo$146bo2bo$146b4ob2o$148b3o$151b2o$149b2o$150b4o$149b2obo$
149b2ob4o$150bob3obo$152b2o2bo$152bobobo$153b4o$152b6o$157bo$154b
2ob2o$155b4obo$156b2ob2o$158b2o$158b4o$159b2o$158b3o$158b3ob2o$
159b2ob2o$158b3obo$160b3o$159b5o$162b2o$161b2o$161b2obo$161b4o$
162b3o$162b3o$165bo$162b5o$164bobobo$163b6o$165b4o$165b6o$165b5obo
$164bo2b4o$167b2obobo$166bo3bobo2$169bobo$168b3ob2o$168bob2obo$
170bob2o$169b2ob2o$169b3o$171bobobo$171b6o$175bo$171bo3bo$173bob2o
$174bob2o$175bobo$176b2o$178bo$176b2o$176bobo$177bob2o$179bo$179bo
$178bo$178b3o$178b2o$180bo$179bo$178b2o$178b3o$180b4o$179b3obo$
179b4ob2o$181b3o$179b2o2b3o$180b2obo$180b3ob2o$181b3obo$182bob2o$
182bo2b2o$183bobo$183b3o$182b3obo$183b2obo$182bo$184bob2o$184bob2o
$186bob2o$189bo$188bo$189bobo$189b2o$190b3o$188b2o2b2o$190bobo$
189bob2o$191b4o$192b2ob2o$192bobobo$194b2o$193bobo$193b3o$194b3o$
196bo$193b2ob2o2$193bobo$195b4o$194b4o$195bob3o$194b2obobo$198bo$
195bobobo$199bobo$201bo$199bobo$199b4o$201b2o$200b5o$201b3obo$203b
obobo$206bo$203b2obo$203b3o$203bo$204bob2o$204b4o$205b4o$207b3o$
207b2o$208bob2o$207b3obo$207bo2b2obo$211b3o$209b6o$209bo3bo$210b5o
$213bo$212bobo2bo$214bo$214b3o2bo$213bo2b2o$213b2o2b3o$218b3o$217b
4o$217bob2o$220b3o$220bob2o$221b2ob2o$219bobo2bo$219b2o2b2obo$220b
o3bobo$221b2o4bo$221b2o2bo$221bobo!

# 1024 iterations (619 problems, 2806 subproblems, 405 solutions) completed: queuesize = 4000; heapsize = 12966; treesize = 2673415
# 1280 iterations (775 problems, 3433 subproblems, 505 solutions) completed: queuesize = 3999; heapsize = 12930; treesize = 2673544
# 1536 iterations (935 problems, 4045 subproblems, 601 solutions) completed: queuesize = 4000; heapsize = 12866; treesize = 2673651
# 1792 iterations (1090 problems, 4635 subproblems, 702 solutions) completed: queuesize = 3999; heapsize = 12837; treesize = 2673777
# 2048 iterations (1252 problems, 5192 subproblems, 796 solutions) completed: queuesize = 3999; heapsize = 12790; treesize = 2673894
# 2304 iterations (1412 problems, 5735 subproblems, 892 solutions) completed: queuesize = 3999; heapsize = 12773; treesize = 2674042
# 2560 iterations (1576 problems, 6241 subproblems, 984 solutions) completed: queuesize = 4000; heapsize = 12727; treesize = 2674163
# 2816 iterations (1738 problems, 6694 subproblems, 1078 solutions) completed: queuesize = 3999; heapsize = 12690; treesize = 2674289
# 3072 iterations (1894 problems, 7117 subproblems, 1178 solutions) completed: queuesize = 3999; heapsize = 12664; treesize = 2674423
# 3328 iterations (2055 problems, 7519 subproblems, 1273 solutions) completed: queuesize = 4000; heapsize = 12626; treesize = 2674553
# 3584 iterations (2203 problems, 7896 subproblems, 1381 solutions) completed: queuesize = 4000; heapsize = 12599; treesize = 2674685
# 3840 iterations (2329 problems, 8343 subproblems, 1511 solutions) completed: queuesize = 4000; heapsize = 12565; treesize = 2674786
# Performing backup...
# ...saved backup file ./backup_b356s3568_velocity_2_1_7_width_17_odd.bin successfully.
# 4096 iterations (2456 problems, 8865 subproblems, 1640 solutions) completed: queuesize = 3999; heapsize = 12522; treesize = 2674876
# solvers invoked: trivial=1329, kissat=7543
# 4352 iterations (2583 problems, 9350 subproblems, 1769 solutions) completed: queuesize = 3999; heapsize = 12496; treesize = 2674986
# 4608 iterations (2710 problems, 9790 subproblems, 1898 solutions) completed: queuesize = 3999; heapsize = 12470; treesize = 2675094
# 4864 iterations (2834 problems, 10244 subproblems, 2030 solutions) completed: queuesize = 4000; heapsize = 12428; treesize = 2675190
# 5120 iterations (2957 problems, 10721 subproblems, 2163 solutions) completed: queuesize = 3999; heapsize = 12400; treesize = 2675303
# 5376 iterations (3081 problems, 11200 subproblems, 2295 solutions) completed: queuesize = 3999; heapsize = 12346; treesize = 2675384
# 5632 iterations (3200 problems, 11689 subproblems, 2432 solutions) completed: queuesize = 4000; heapsize = 12312; treesize = 2675482
Has anyone else experienced this?
Edit: I found a way to upload this backup.
After rebooting my computer, this error did not disappear:

Code: Select all

Exception: STATUS_ACCESS_VIOLATION at rip=0010046151A
rax=00000000FFFFFFFF rbx=000000081B90F170 rcx=000000081C1F4CB0
rdx=00000000FFFFFFFE rsi=0000000819DF72A0 rdi=000000081BAF8D00
r8 =000000081BAF8D00 r9 =00006FD66E4DD88C r10=000000081B90F170
r11=0000000000000002 r12=000000081B90F170 r13=000000081B90F170
r14=0000000819DF7080 r15=0000000819DF7480
rbp=0000000000000022 rsp=00000000FFDFC8B0
program=D:\BASH\cygwin64\home\User\C\ikpx2i\ikpx2.exe, pid 899, thread ikpx2
cs=0033 ds=002B es=002B fs=0053 gs=002B ss=002B
How to assemble this backup:
  1. Download both files to one folder
  2. Remove .txt extensions (not .001 and .002!)
  3. Extract archive ...7z.001
Attachments
backup_b356s3568_velocity_2_1_7_width_17_odd.7z.002.txt
(9.22 MiB) Downloaded 215 times
backup_b356s3568_velocity_2_1_7_width_17_odd.7z.001.txt
(10 MiB) Downloaded 209 times
Spaceship databases:
new-gliders.db (30683 gliders, square grid)
hex-gliders.db (668 gliders, hexagonal grid)
My scripts: new-glider.py v0.2, nbsearch2a.py, collector.py v0.3

-Dmitry Maitak
Top
User avatar
whatislife
Posts: 77
Joined: June 24th, 2023, 5:47 am

Re: ikpx 2.2

Post by whatislife »

I'm another user that would appreciate hex support in ikpx2. As is it squishes hex onto a square grid, so 'c/4d' gives me orthogonal ships. You can search for diagonal ships by telling it to look for knightships, but then the search doesn't take advantage of symmetry. I have also seen it immediately reach depth 60 and give up like mentioned earlier on the page, in my case on b25s34h c/2d. In both cases we were searching speeds that are too fast for regular life, maybe that's part of it...
:cursed:
Top
Post Reply

Return to “Scripts”