stuff
This commit is contained in:
Shelvacu
3
.gitignore
vendored
Normal file
3
.gitignore
vendored
Normal file
@@ -0,0 +1,3 @@
|
||||
/target
|
||||
.z3-trace
|
||||
/flow-free
|
||||
377
Cargo.lock
generated
Normal file
377
Cargo.lock
generated
Normal file
@@ -0,0 +1,377 @@
|
||||
# This file is automatically @generated by Cargo.
|
||||
# It is not intended for manual editing.
|
||||
version = 3
|
||||
|
||||
[[package]]
|
||||
name = "aho-corasick"
|
||||
version = "1.1.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8e60d3430d3a69478ad0993f19238d2df97c507009a52b3c10addcd7f6bcb916"
|
||||
dependencies = [
|
||||
"memchr",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "autocfg"
|
||||
version = "1.4.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26"
|
||||
|
||||
[[package]]
|
||||
name = "bindgen"
|
||||
version = "0.70.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f49d8fed880d473ea71efb9bf597651e77201bdd4893efe54c9e5d65ae04ce6f"
|
||||
dependencies = [
|
||||
"bitflags",
|
||||
"cexpr",
|
||||
"clang-sys",
|
||||
"itertools",
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"regex",
|
||||
"rustc-hash",
|
||||
"shlex",
|
||||
"syn",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "bitflags"
|
||||
version = "2.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
|
||||
|
||||
[[package]]
|
||||
name = "cexpr"
|
||||
version = "0.6.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "6fac387a98bb7c37292057cffc56d62ecb629900026402633ae9160df93a8766"
|
||||
dependencies = [
|
||||
"nom",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "cfg-if"
|
||||
version = "1.0.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
|
||||
|
||||
[[package]]
|
||||
name = "clang-sys"
|
||||
version = "1.8.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0b023947811758c97c59bf9d1c188fd619ad4718dcaa767947df1cadb14f39f4"
|
||||
dependencies = [
|
||||
"glob",
|
||||
"libc",
|
||||
"libloading",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "either"
|
||||
version = "1.13.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0"
|
||||
|
||||
[[package]]
|
||||
name = "glob"
|
||||
version = "0.3.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b"
|
||||
|
||||
[[package]]
|
||||
name = "itertools"
|
||||
version = "0.13.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186"
|
||||
dependencies = [
|
||||
"either",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "libc"
|
||||
version = "0.2.159"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "561d97a539a36e26a9a5fad1ea11a3039a67714694aaa379433e580854bc3dc5"
|
||||
|
||||
[[package]]
|
||||
name = "libloading"
|
||||
version = "0.8.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "4979f22fdb869068da03c9f7528f8297c6fd2606bc3a4affe42e6a823fdb8da4"
|
||||
dependencies = [
|
||||
"cfg-if",
|
||||
"windows-targets",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "log"
|
||||
version = "0.4.22"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24"
|
||||
|
||||
[[package]]
|
||||
name = "memchr"
|
||||
version = "2.7.4"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3"
|
||||
|
||||
[[package]]
|
||||
name = "minimal-lexical"
|
||||
version = "0.2.1"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
|
||||
|
||||
[[package]]
|
||||
name = "nom"
|
||||
version = "7.1.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a"
|
||||
dependencies = [
|
||||
"memchr",
|
||||
"minimal-lexical",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num"
|
||||
version = "0.4.3"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23"
|
||||
dependencies = [
|
||||
"num-bigint",
|
||||
"num-complex",
|
||||
"num-integer",
|
||||
"num-iter",
|
||||
"num-rational",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-bigint"
|
||||
version = "0.4.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
|
||||
dependencies = [
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-complex"
|
||||
version = "0.4.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495"
|
||||
dependencies = [
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-integer"
|
||||
version = "0.1.46"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f"
|
||||
dependencies = [
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-iter"
|
||||
version = "0.1.45"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "1429034a0490724d0075ebb2bc9e875d6503c3cf69e235a8941aa757d83ef5bf"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-rational"
|
||||
version = "0.4.2"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824"
|
||||
dependencies = [
|
||||
"num-bigint",
|
||||
"num-integer",
|
||||
"num-traits",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "num-traits"
|
||||
version = "0.2.19"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841"
|
||||
dependencies = [
|
||||
"autocfg",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "numberlink-solver"
|
||||
version = "0.1.0"
|
||||
dependencies = [
|
||||
"itertools",
|
||||
"z3",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "pkg-config"
|
||||
version = "0.3.31"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "953ec861398dccce10c670dfeaf3ec4911ca479e9c02154b3a215178c5f566f2"
|
||||
|
||||
[[package]]
|
||||
name = "proc-macro2"
|
||||
version = "1.0.86"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "5e719e8df665df0d1c8fbfd238015744736151d4445ec0836b8e628aae103b77"
|
||||
dependencies = [
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "quote"
|
||||
version = "1.0.37"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex"
|
||||
version = "1.11.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "38200e5ee88914975b69f657f0801b6f6dccafd44fd9326302a4aaeecfacb1d8"
|
||||
dependencies = [
|
||||
"aho-corasick",
|
||||
"memchr",
|
||||
"regex-automata",
|
||||
"regex-syntax",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex-automata"
|
||||
version = "0.4.8"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "368758f23274712b504848e9d5a6f010445cc8b87a7cdb4d7cbee666c1288da3"
|
||||
dependencies = [
|
||||
"aho-corasick",
|
||||
"memchr",
|
||||
"regex-syntax",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "regex-syntax"
|
||||
version = "0.8.5"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "2b15c43186be67a4fd63bee50d0303afffcef381492ebe2c5d87f324e1b8815c"
|
||||
|
||||
[[package]]
|
||||
name = "rustc-hash"
|
||||
version = "1.1.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2"
|
||||
|
||||
[[package]]
|
||||
name = "shlex"
|
||||
version = "1.3.0"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
|
||||
|
||||
[[package]]
|
||||
name = "syn"
|
||||
version = "2.0.79"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "89132cd0bf050864e1d38dc3bbc07a0eb8e7530af26344d3d2bbbef83499f590"
|
||||
dependencies = [
|
||||
"proc-macro2",
|
||||
"quote",
|
||||
"unicode-ident",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "unicode-ident"
|
||||
version = "1.0.13"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe"
|
||||
|
||||
[[package]]
|
||||
name = "windows-targets"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
|
||||
dependencies = [
|
||||
"windows_aarch64_gnullvm",
|
||||
"windows_aarch64_msvc",
|
||||
"windows_i686_gnu",
|
||||
"windows_i686_gnullvm",
|
||||
"windows_i686_msvc",
|
||||
"windows_x86_64_gnu",
|
||||
"windows_x86_64_gnullvm",
|
||||
"windows_x86_64_msvc",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_gnullvm"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"
|
||||
|
||||
[[package]]
|
||||
name = "windows_aarch64_msvc"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_gnu"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_gnullvm"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"
|
||||
|
||||
[[package]]
|
||||
name = "windows_i686_msvc"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnu"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_gnullvm"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"
|
||||
|
||||
[[package]]
|
||||
name = "windows_x86_64_msvc"
|
||||
version = "0.52.6"
|
||||
source = "registry+https://github.com/rust-lang/crates.io-index"
|
||||
checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
|
||||
|
||||
[[package]]
|
||||
name = "z3"
|
||||
version = "0.13.0"
|
||||
dependencies = [
|
||||
"log",
|
||||
"num",
|
||||
"z3-sys",
|
||||
]
|
||||
|
||||
[[package]]
|
||||
name = "z3-sys"
|
||||
version = "0.9.0"
|
||||
dependencies = [
|
||||
"bindgen",
|
||||
"pkg-config",
|
||||
]
|
||||
12
Cargo.toml
Normal file
12
Cargo.toml
Normal file
@@ -0,0 +1,12 @@
|
||||
[package]
|
||||
name = "numberlink-solver"
|
||||
version = "0.1.0"
|
||||
edition = "2021"
|
||||
|
||||
# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
|
||||
|
||||
[dependencies]
|
||||
itertools = "0.13.0"
|
||||
# z3 = { git = "https://github.com/shelvacu/z3.rs", branch = "fix-ur-shit" }
|
||||
z3 = { path = "../z3.rs/z3" }
|
||||
|
||||
1705
flake.lock
generated
Normal file
1705
flake.lock
generated
Normal file
File diff suppressed because it is too large
Load Diff
24
flake.nix
Normal file
24
flake.nix
Normal file
@@ -0,0 +1,24 @@
|
||||
{
|
||||
inputs.nixpkgs.url = "nixpkgs/nixos-24.05";
|
||||
outputs = { nixpkgs, vacu, ... }: let
|
||||
pkgs = import nixpkgs { system = "x86_64-linux"; };
|
||||
in {
|
||||
devShells.x86_64-linux.default = pkgs.mkShell {
|
||||
nativeBuildInputs = (with pkgs; [
|
||||
rustup
|
||||
clang
|
||||
valgrind
|
||||
# cmake
|
||||
# gnumake
|
||||
# python3
|
||||
# gdb
|
||||
]) ++ [ vacu.packages.x86_64-linux.z3 ];
|
||||
|
||||
shellHook = ''
|
||||
export CC=${pkgs.lib.getExe pkgs.clang}
|
||||
export RUST_BACKTRACE=1
|
||||
export LIBCLANG_PATH=${pkgs.libclang.lib}/lib
|
||||
'';
|
||||
};
|
||||
};
|
||||
}
|
||||
5
impossible-level.txt
Normal file
5
impossible-level.txt
Normal file
@@ -0,0 +1,5 @@
|
||||
# 0 1 2
|
||||
# 3 4 5
|
||||
# 6 7 8
|
||||
|
||||
3,0,1,2;1,2,0,3,6,8;7,4,5
|
||||
6
multi-solution-level.txt
Normal file
6
multi-solution-level.txt
Normal file
@@ -0,0 +1,6 @@
|
||||
# 0 1 2 3
|
||||
# 4 5 6 7
|
||||
# 8 9 10 11
|
||||
# 12 13 14 15
|
||||
4,0,1,2;12,8,4,0,1,5,9,10,6,2;3,7,11,15,14,13
|
||||
4,0,1,2;12,8,4,0,1,5,9,10,6,2;3,7,11,15,14,13
|
||||
394
notes.txt
Normal file
394
notes.txt
Normal file
@@ -0,0 +1,394 @@
|
||||
(assert (=> generic_node_not_empty_0_0 (not ((_ is Empty) node_color_000_000))))
|
||||
(assert (=> generic_conn_empty_or_same_0_0_to_1_0
|
||||
(or (= connection_000_000_to_001_000 node_color_001_000)
|
||||
((_ is Empty) connection_000_000_to_001_000))))
|
||||
(assert (=> generic_conn_empty_or_same_0_0_to_0_1
|
||||
(or (= connection_000_000_to_000_001 node_color_000_001)
|
||||
((_ is Empty) connection_000_000_to_000_001))))
|
||||
(assert (=> generic_node_at_least_1_connection_0_0
|
||||
(or (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))))
|
||||
(assert (=> generic_node_not_empty_0_1 (not ((_ is Empty) node_color_000_001))))
|
||||
(assert (=> generic_conn_empty_or_same_0_1_to_1_1
|
||||
(or (= connection_000_001_to_001_001 node_color_001_001)
|
||||
((_ is Empty) connection_000_001_to_001_001))))
|
||||
(assert (=> generic_conn_empty_or_same_0_1_to_0_0
|
||||
(or (= connection_000_000_to_000_001 node_color_000_000)
|
||||
((_ is Empty) connection_000_000_to_000_001))))
|
||||
(assert (=> generic_conn_empty_or_same_0_1_to_0_2
|
||||
(or (= connection_000_001_to_000_002 node_color_000_002)
|
||||
((_ is Empty) connection_000_001_to_000_002))))
|
||||
(assert (=> generic_node_at_least_1_connection_0_1
|
||||
(or (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))))
|
||||
(assert (let ((a!1 (or (and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))))))
|
||||
(=> generic_node_less_than_3_connections_0_1 (not a!1))))
|
||||
(assert (=> generic_node_not_empty_0_2 (not ((_ is Empty) node_color_000_002))))
|
||||
(assert (=> generic_conn_empty_or_same_0_2_to_1_2
|
||||
(or (= connection_000_002_to_001_002 node_color_001_002)
|
||||
((_ is Empty) connection_000_002_to_001_002))))
|
||||
(assert (=> generic_conn_empty_or_same_0_2_to_0_1
|
||||
(or (= connection_000_001_to_000_002 node_color_000_001)
|
||||
((_ is Empty) connection_000_001_to_000_002))))
|
||||
(assert (=> generic_node_at_least_1_connection_0_2
|
||||
(or (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))))
|
||||
(assert (=> generic_node_not_empty_1_0 (not ((_ is Empty) node_color_001_000))))
|
||||
(assert (=> generic_conn_empty_or_same_1_0_to_0_0
|
||||
(or (= connection_000_000_to_001_000 node_color_000_000)
|
||||
((_ is Empty) connection_000_000_to_001_000))))
|
||||
(assert (=> generic_conn_empty_or_same_1_0_to_2_0
|
||||
(or (= connection_001_000_to_002_000 node_color_002_000)
|
||||
((_ is Empty) connection_001_000_to_002_000))))
|
||||
(assert (=> generic_conn_empty_or_same_1_0_to_1_1
|
||||
(or (= connection_001_000_to_001_001 node_color_001_001)
|
||||
((_ is Empty) connection_001_000_to_001_001))))
|
||||
(assert (=> generic_node_at_least_1_connection_1_0
|
||||
(or (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))))
|
||||
(assert (let ((a!1 (or (and (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_000_000_to_001_000)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_001_000))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))))))
|
||||
(=> generic_node_less_than_3_connections_1_0 (not a!1))))
|
||||
(assert (=> generic_node_not_empty_1_1 (not ((_ is Empty) node_color_001_001))))
|
||||
(assert (=> generic_conn_empty_or_same_1_1_to_0_1
|
||||
(or (= connection_000_001_to_001_001 node_color_000_001)
|
||||
((_ is Empty) connection_000_001_to_001_001))))
|
||||
(assert (=> generic_conn_empty_or_same_1_1_to_2_1
|
||||
(or (= connection_001_001_to_002_001 node_color_002_001)
|
||||
((_ is Empty) connection_001_001_to_002_001))))
|
||||
(assert (=> generic_conn_empty_or_same_1_1_to_1_0
|
||||
(or (= connection_001_000_to_001_001 node_color_001_000)
|
||||
((_ is Empty) connection_001_000_to_001_001))))
|
||||
(assert (=> generic_conn_empty_or_same_1_1_to_1_2
|
||||
(or (= connection_001_001_to_001_002 node_color_001_002)
|
||||
((_ is Empty) connection_001_001_to_001_002))))
|
||||
(assert (=> generic_node_at_least_1_connection_1_1
|
||||
(or (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))))
|
||||
(assert (let ((a!1 (or (and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_000_to_001_001))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))))))
|
||||
(=> generic_node_less_than_3_connections_1_1 (not a!1))))
|
||||
(assert (=> generic_node_not_empty_1_2 (not ((_ is Empty) node_color_001_002))))
|
||||
(assert (=> generic_conn_empty_or_same_1_2_to_0_2
|
||||
(or (= connection_000_002_to_001_002 node_color_000_002)
|
||||
((_ is Empty) connection_000_002_to_001_002))))
|
||||
(assert (=> generic_conn_empty_or_same_1_2_to_2_2
|
||||
(or (= connection_001_002_to_002_002 node_color_002_002)
|
||||
((_ is Empty) connection_001_002_to_002_002))))
|
||||
(assert (=> generic_conn_empty_or_same_1_2_to_1_1
|
||||
(or (= connection_001_001_to_001_002 node_color_001_001)
|
||||
((_ is Empty) connection_001_001_to_001_002))))
|
||||
(assert (=> generic_node_at_least_1_connection_1_2
|
||||
(or (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))))
|
||||
(assert (let ((a!1 (or (and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))))))
|
||||
(=> generic_node_less_than_3_connections_1_2 (not a!1))))
|
||||
(assert (=> generic_node_not_empty_2_0 (not ((_ is Empty) node_color_002_000))))
|
||||
(assert (=> generic_conn_empty_or_same_2_0_to_1_0
|
||||
(or (= connection_001_000_to_002_000 node_color_001_000)
|
||||
((_ is Empty) connection_001_000_to_002_000))))
|
||||
(assert (=> generic_conn_empty_or_same_2_0_to_2_1
|
||||
(or (= connection_002_000_to_002_001 node_color_002_001)
|
||||
((_ is Empty) connection_002_000_to_002_001))))
|
||||
(assert (=> generic_node_at_least_1_connection_2_0
|
||||
(or (not ((_ is Empty) connection_001_000_to_002_000))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001)))))
|
||||
(assert (=> generic_node_not_empty_2_1 (not ((_ is Empty) node_color_002_001))))
|
||||
(assert (=> generic_conn_empty_or_same_2_1_to_1_1
|
||||
(or (= connection_001_001_to_002_001 node_color_001_001)
|
||||
((_ is Empty) connection_001_001_to_002_001))))
|
||||
(assert (=> generic_conn_empty_or_same_2_1_to_2_0
|
||||
(or (= connection_002_000_to_002_001 node_color_002_000)
|
||||
((_ is Empty) connection_002_000_to_002_001))))
|
||||
(assert (=> generic_conn_empty_or_same_2_1_to_2_2
|
||||
(or (= connection_002_001_to_002_002 node_color_002_002)
|
||||
((_ is Empty) connection_002_001_to_002_002))))
|
||||
(assert (=> generic_node_at_least_1_connection_2_1
|
||||
(or (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))))
|
||||
(assert (let ((a!1 (or (and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_002_001))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001)))
|
||||
(and (not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_002_000_to_002_001))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_002_001_to_002_002))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002))))))
|
||||
(=> generic_node_less_than_3_connections_2_1 (not a!1))))
|
||||
(assert (=> generic_node_not_empty_2_2 (not ((_ is Empty) node_color_002_002))))
|
||||
(assert (=> generic_conn_empty_or_same_2_2_to_1_2
|
||||
(or (= connection_001_002_to_002_002 node_color_001_002)
|
||||
((_ is Empty) connection_001_002_to_002_002))))
|
||||
(assert (=> generic_conn_empty_or_same_2_2_to_2_1
|
||||
(or (= connection_002_001_to_002_002 node_color_002_001)
|
||||
((_ is Empty) connection_002_001_to_002_002))))
|
||||
(assert (=> generic_node_at_least_1_connection_2_2
|
||||
(or (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_002_001_to_002_002)))))
|
||||
)
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(assert (let ((a!1 (or (and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002)))
|
||||
(and (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_002_to_002_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002)))
|
||||
(and (not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))
|
||||
(not ((_ is Empty) connection_001_001_to_001_002))))))
|
||||
(=> generic_node_less_than_3_connections_1_2 (not a!1))))
|
||||
|
||||
(assert
|
||||
(let
|
||||
((a!1
|
||||
(or
|
||||
(and
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
)
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_001_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_000_to_000_001))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))
|
||||
(and (not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002))))))
|
||||
(=> generic_node_less_than_3_connections_0_1 (not a!1))))
|
||||
|
||||
(assert (=> generic_node_at_least_1_connection_0_2
|
||||
(or (not ((_ is Empty) connection_000_002_to_001_002))
|
||||
(not ((_ is Empty) connection_000_001_to_000_002)))))
|
||||
|
||||
[src/main.rs:205:17] self.solver.get_unsat_core() = [
|
||||
Bool(generic_node_less_than_3_connections_1_2),
|
||||
bool(generic_node_at_least_1_connection_0_2),
|
||||
bool(generic_node_less_than_3_connections_0_1),
|
||||
]
|
||||
|
||||
00 01 02
|
||||
10 11 12
|
||||
20 21 22
|
||||
|
||||
1
problematic-level.txt
Normal file
1
problematic-level.txt
Normal file
@@ -0,0 +1 @@
|
||||
10,0,2,8;23,24,34,35,36,46,56,66,76,86,85,84,83,82,81,80,90;91,92,93,94,95,96,97,87,88,78,68,58,48,38,28,18,17,16,6,5,4;53,43,33;0,10,20,30,40,50,60,70;54,64,63,62,52,42,32;3,2,1,11,21,31,41,51,61,71,72,73,74,75,65,55,45,44;98,99,89,79,69,59,49,39,29,19,9,8,7;22,12,13,14,15,25,26,27,37,47,57,67,77
|
||||
6
some-levels.txt
Normal file
6
some-levels.txt
Normal file
@@ -0,0 +1,6 @@
|
||||
# 0 1 2
|
||||
# 3 4 5
|
||||
# 6 7 8
|
||||
|
||||
3,0,1,2;6,7,8,5,2,1;0,3,4
|
||||
3,0,2,3;0,3,6;1,4,7;2,5,8
|
||||
423
src/main.rs
Normal file
423
src/main.rs
Normal file
@@ -0,0 +1,423 @@
|
||||
use std::fs::File;
|
||||
use std::io::{prelude::*, BufReader, Write};
|
||||
use std::collections::HashMap;
|
||||
use std::collections::HashSet;
|
||||
use std::boxed::Box;
|
||||
use std::time::Instant;
|
||||
use core::num::NonZeroU64;
|
||||
|
||||
use itertools::Itertools;
|
||||
|
||||
use z3::*;
|
||||
use z3::ast::*;
|
||||
|
||||
fn main() {
|
||||
// let ctx = Context::default();
|
||||
// for tactic in Tactic::list_all(&ctx) {
|
||||
// println!("{tactic}");
|
||||
// }
|
||||
// return;
|
||||
let mut args = std::env::args_os();
|
||||
let _ = args.next(); // argv[0] - dont care
|
||||
let filename = args.next().unwrap();
|
||||
let handle = File::open(filename).unwrap();
|
||||
let buf = BufReader::new(handle);
|
||||
|
||||
let mut thingy = Thingy::new();
|
||||
|
||||
let mut levels = vec![];
|
||||
|
||||
for (zidx_lineno, mut line) in buf.lines().map(Result::unwrap).enumerate() {
|
||||
let lineno = zidx_lineno + 1;
|
||||
if let Some(idx) = line.find('#') {
|
||||
line.truncate(idx);
|
||||
}
|
||||
line.retain(|c| c != ' ' && c != '\t' && c != '\n' && c != '\r');
|
||||
if line.len() == 0 {
|
||||
continue;
|
||||
}
|
||||
let level = parseline(&line);
|
||||
level.sanity_check().unwrap();
|
||||
levels.push((lineno, level));
|
||||
}
|
||||
|
||||
levels.sort_unstable_by_key(|(_, lvl)| (lvl.size, lvl.num_pipes));
|
||||
|
||||
for (lineno, level) in levels {
|
||||
println!("Attempting to solve line#{lineno}, a {}x{} with {} pipes", level.size, level.size, level.num_pipes);
|
||||
let start = Instant::now();
|
||||
let solution_count = thingy.solve(level);
|
||||
let runtime = start.elapsed();
|
||||
println!("Line {lineno} had {solution_count} solutions{}, took {runtime:?}", if solution_count != 1 { "!!!" } else {""});
|
||||
}
|
||||
}
|
||||
|
||||
struct Thingy<'ctx> {
|
||||
solver: z3::Solver<'ctx>,
|
||||
lvl: Level,
|
||||
color_enum_cache: HashMap<u64, (Sort<'ctx>, Vec<FuncDecl<'ctx>>, Vec<FuncDecl<'ctx>>)>,
|
||||
setup_size: u64,
|
||||
last_color_count: u64,
|
||||
}
|
||||
|
||||
impl Thingy<'static> {
|
||||
fn new() -> Thingy<'static> {
|
||||
let mut cfg = z3::Config::default();
|
||||
cfg.set_bool_param_value("unsat_core", true);
|
||||
let ctx = z3::Context::new(cfg);
|
||||
let ctx = Box::leak(Box::new(ctx));
|
||||
// let tactic = Tactic::new(ctx, "sat-preprocess").and_then(&Tactic::new(ctx, "psat")).and_then(&Tactic::new(ctx, "sat"));
|
||||
// let solver = tactic.solver();
|
||||
let solver = Solver::new(ctx);
|
||||
solver.push();
|
||||
Self {
|
||||
solver,
|
||||
lvl: Level::unlevel(),
|
||||
color_enum_cache: HashMap::new(),
|
||||
setup_size: 0,
|
||||
last_color_count: 0,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
impl<'ctx> Thingy<'ctx> {
|
||||
fn ctx(&self) -> &'ctx z3::Context {
|
||||
self.solver.ctx()
|
||||
}
|
||||
|
||||
fn node_color(&mut self, x: u64, y: u64) -> Dynamic<'ctx> {
|
||||
let name = format!("node_color_{x:03}_{y:03}");
|
||||
let res = Dynamic::new_const(self.ctx(), name, &self.color_sort());
|
||||
res
|
||||
}
|
||||
|
||||
// fn node_connection_count(&mut self, x:u64, y:u64) -> Int<'ctx> {
|
||||
// let name = format!("note_connections_{x:03}_{y:03}");
|
||||
// Int::new_const(self.ctx(), name)
|
||||
// }
|
||||
|
||||
fn connection_color(&mut self, ax: u64, ay: u64, bx: u64, by: u64) -> Dynamic<'ctx> {
|
||||
if (ax == bx) && (ay == by) {
|
||||
panic!("self connection requested");
|
||||
}
|
||||
let mut sorted_coords:[(u64, u64); 2] = [(ax, ay), (bx, by)];
|
||||
sorted_coords.sort_unstable();
|
||||
let name = format!("connection_{:03}_{:03}_to_{:03}_{:03}", sorted_coords[0].0, sorted_coords[0].1, sorted_coords[1].0, sorted_coords[1].1);
|
||||
Dynamic::new_const(self.ctx(), name, &self.color_sort())
|
||||
}
|
||||
|
||||
fn connection(&mut self, my_x:u64, my_y:u64, other_x:u64, other_y:u64) -> (Dynamic<'ctx>, Dynamic<'ctx>) {
|
||||
let other = self.node_color(other_x, other_y);
|
||||
let conn = self.connection_color(my_x, my_y, other_x, other_y);
|
||||
(other, conn)
|
||||
}
|
||||
|
||||
// fn color_empty(&mut self) -> Dynamic<'ctx> {
|
||||
// self.color_const(None)
|
||||
// }
|
||||
|
||||
fn color_to_idx(color: Option<NonZeroU64>) -> usize {
|
||||
color.map(Into::into).unwrap_or(0u64).try_into().unwrap()
|
||||
}
|
||||
|
||||
// fn color_const(&mut self, color: Option<NonZeroU64>) -> Dynamic<'ctx> {
|
||||
// self.color_enum().1[Self::color_to_idx(color)].apply_empty()
|
||||
// }
|
||||
|
||||
fn color_is(&mut self, color: Option<NonZeroU64>, tested_color: &Dynamic<'ctx>) -> Bool<'ctx> {
|
||||
self.color_enum().2[Self::color_to_idx(color)].apply(&[tested_color]).as_bool().unwrap()
|
||||
}
|
||||
|
||||
fn color_is_empty(&mut self, tested_color: &Dynamic<'ctx>) -> Bool<'ctx> {
|
||||
self.color_is(None, tested_color)
|
||||
}
|
||||
|
||||
fn color_sort(&mut self) -> &Sort<'ctx> {
|
||||
&self.color_enum().0
|
||||
}
|
||||
|
||||
fn color_enum(&mut self) -> &(Sort<'ctx>, Vec<FuncDecl<'ctx>>, Vec<FuncDecl<'ctx>>) {
|
||||
let num_pipes = self.lvl.num_pipes;
|
||||
let ctx = self.ctx();
|
||||
self.color_enum_cache.entry(num_pipes).or_insert_with(move || Self::color_enum_impl(ctx, num_pipes))
|
||||
}
|
||||
|
||||
fn color_enum_impl(ctx: &'ctx Context, num_pipes:u64) -> (Sort<'ctx>, Vec<FuncDecl<'ctx>>, Vec<FuncDecl<'ctx>>) {
|
||||
let mut pipe_colors = Vec::new();
|
||||
pipe_colors.push("Empty".to_string());
|
||||
for i in 0..num_pipes {
|
||||
let c:char = (('A' as u32) + (i as u32)).try_into().unwrap();
|
||||
let mut color_str = std::string::String::with_capacity(1);
|
||||
color_str.push(c);
|
||||
pipe_colors.push(color_str);
|
||||
}
|
||||
let res = Sort::enumeration(
|
||||
ctx,
|
||||
format!("Color{}", num_pipes),
|
||||
pipe_colors,
|
||||
);
|
||||
res
|
||||
}
|
||||
|
||||
fn assert_and_track(&self, name: String, cond: &Bool<'ctx>) {
|
||||
let tracker_bool = Bool::new_const(self.ctx(), name);
|
||||
self.solver.assert_and_track(cond, &tracker_bool);
|
||||
}
|
||||
|
||||
fn index_to_coord(&self, idx: u64) -> (u64, u64) {
|
||||
(idx / self.lvl.size, idx % self.lvl.size)
|
||||
}
|
||||
|
||||
fn setup_board_generic(&mut self) {
|
||||
if self.lvl.size == self.setup_size && self.lvl.num_pipes == self.last_color_count { return; }
|
||||
self.solver.pop(1);
|
||||
self.solver.push();
|
||||
self.setup_size = self.lvl.size;
|
||||
for node in self.nodes_connections() {
|
||||
let color_not_empty_expr = self.color_is_empty(&node.color).not();
|
||||
self.assert_and_track(format!("generic_node_not_empty_{}_{}", node.x, node.y), &color_not_empty_expr);
|
||||
for conn in &node.connections {
|
||||
let color_empty_expr = self.color_is_empty(&conn.color);
|
||||
self.assert_and_track(
|
||||
format!("generic_conn_empty_or_same_{}_{}_to_{}_{}", node.x, node.y, conn.x, conn.y),
|
||||
&(conn.color._eq(&conn.other_color) | color_empty_expr.clone())
|
||||
);
|
||||
}
|
||||
let connected_bools_refs:Vec<_> = node.connections.iter().map(|c| &c.connected).collect();
|
||||
// node count is at least 1
|
||||
self.assert_and_track(format!("generic_node_at_least_1_connection_{}_{}", node.x, node.y), &Bool::or(self.ctx(), connected_bools_refs.as_slice()));
|
||||
if connected_bools_refs.len() >= 3 {
|
||||
// and is less than 3; ie no set of 3 connections are all connected
|
||||
let any_3:Vec<_> = connected_bools_refs.iter().copied().combinations(3).map(|comb| {
|
||||
Bool::and(self.ctx(), comb.as_slice())
|
||||
}).collect();
|
||||
let any_3_ref:Vec<_> = any_3.iter().collect();
|
||||
self.assert_and_track(format!("generic_node_less_than_3_connections_{}_{}", node.x, node.y), &Bool::or(self.ctx(), any_3_ref.as_slice()).not());
|
||||
}
|
||||
}
|
||||
// Try to 'optimize' this board internally
|
||||
let start = Instant::now();
|
||||
let res = self.solver.check();
|
||||
let dur = start.elapsed();
|
||||
println!("sanity check step for {}x{} took {dur:?} and gave {res:?}", self.lvl.size, self.lvl.size);
|
||||
match res {
|
||||
z3::SatResult::Unsat => {
|
||||
dbg!(&self.solver);
|
||||
dbg!(self.solver.get_unsat_core());
|
||||
panic!("Unsat at optimize step, wtf");
|
||||
},
|
||||
z3::SatResult::Unknown => {
|
||||
panic!("Unknown with reason {:?}, that shouldnt happen", self.solver.get_reason_unknown())
|
||||
},
|
||||
z3::SatResult::Sat => (),
|
||||
}
|
||||
}
|
||||
|
||||
fn setup_board_level_specific(&mut self) {
|
||||
let mut start_end_points = HashMap::new();
|
||||
for (idx, pipe) in self.lvl.pipes.iter().enumerate() {
|
||||
let idx_u64:u64 = idx.try_into().unwrap();
|
||||
let color:NonZeroU64 = (idx_u64 + 1).try_into().unwrap();
|
||||
for idx in [pipe.first().unwrap(), pipe.last().unwrap()] {
|
||||
start_end_points.insert(self.index_to_coord(*idx), color);
|
||||
}
|
||||
}
|
||||
|
||||
for node in self.nodes_connections() {
|
||||
let connecteds_iter = node.connections.iter().map(|c| &c.connected);
|
||||
let pairs:Vec<_> = connecteds_iter.combinations(2).map(|comb| {
|
||||
Bool::and(self.ctx(), comb.as_slice())
|
||||
}).collect();
|
||||
let pairs_refs:Vec<_> = pairs.iter().collect();
|
||||
let has_a_pair = Bool::or(self.ctx(), pairs_refs.as_slice());
|
||||
// We already asserted in _level_generic that each node has either 1 or 2 connections,
|
||||
// so now...
|
||||
if let Some(color) = start_end_points.get(&(node.x, node.y)) {
|
||||
// ...assert it has less than 2 (for exactly 1), ie no two connections are both
|
||||
// connected
|
||||
self.solver.assert(&has_a_pair.not());
|
||||
// and this node should be the correct color
|
||||
let color_is_expr = self.color_is(Some(*color), &node.color);
|
||||
self.solver.assert(&color_is_expr);
|
||||
} else {
|
||||
// ...assert it has at least 2 (for exactly 2), ie at one pair of two connections
|
||||
// are both connected
|
||||
self.solver.assert(&has_a_pair);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
fn solve(&mut self, lvl: Level) -> u64 {
|
||||
self.lvl = lvl;
|
||||
self.setup_board_generic();
|
||||
self.solver.push();
|
||||
self.setup_board_level_specific();
|
||||
let mut solution_count = 0;
|
||||
loop {
|
||||
let start = Instant::now();
|
||||
let res = self.solver.check();
|
||||
let dur = start.elapsed();
|
||||
match res {
|
||||
z3::SatResult::Sat => {
|
||||
solution_count += 1;
|
||||
println!("Found solution#{solution_count}, took {dur:?}");
|
||||
},
|
||||
z3::SatResult::Unsat => {
|
||||
// dbg!(self.solver.get_unsat_core());
|
||||
println!("Proved no more solutions, took {dur:?}");
|
||||
break;
|
||||
},
|
||||
z3::SatResult::Unknown => {
|
||||
let reason = self.solver.get_reason_unknown();
|
||||
if reason == Some("cancelled".into()) {
|
||||
// likely a ctrl-c
|
||||
std::process::exit(1);
|
||||
}
|
||||
panic!("got SatResult::Unknown with reason {:?} after {dur:?}, that shouldnt happen", self.solver.get_reason_unknown())
|
||||
},
|
||||
}
|
||||
if solution_count > 10 {
|
||||
println!("More than 10 solutions found!");
|
||||
self.solver.pop(1);
|
||||
return 10;
|
||||
}
|
||||
let model = self.solver.get_model().unwrap();
|
||||
let mut any_different = Vec::new();
|
||||
for x in 0..(self.lvl.size) {
|
||||
for y in 0..(self.lvl.size) {
|
||||
let this_color = self.node_color(x, y);
|
||||
let solution_node_color = model.get_const_interp(&this_color).unwrap();
|
||||
any_different.push(this_color._eq(&solution_node_color).not());
|
||||
}
|
||||
}
|
||||
let any_different_refs:Vec<&Bool> = any_different.iter().collect();
|
||||
self.solver.assert(&Bool::or(self.ctx(), any_different_refs.as_slice()));
|
||||
};
|
||||
self.solver.pop(1);
|
||||
solution_count
|
||||
}
|
||||
}
|
||||
|
||||
struct Connection<'ctx> {
|
||||
x: u64,
|
||||
y: u64,
|
||||
color: Dynamic<'ctx>,
|
||||
other_color: Dynamic<'ctx>,
|
||||
connected: Bool<'ctx>,
|
||||
}
|
||||
|
||||
struct NodeWithConnections<'ctx> {
|
||||
x: u64,
|
||||
y: u64,
|
||||
color: Dynamic<'ctx>,
|
||||
connections: Vec<Connection<'ctx>>,
|
||||
}
|
||||
|
||||
impl<'ctx> Thingy<'ctx> {
|
||||
fn nodes_connections(&mut self) -> Vec<NodeWithConnections<'ctx>> {
|
||||
let size = self.lvl.size;
|
||||
(0..size).map(|x| (0..size).map(move |y| (x,y))).flatten().map(|(x,y)| {
|
||||
let color = self.node_color(x, y);
|
||||
let mut connections = Vec::new();
|
||||
if x > 0 {
|
||||
connections.push((x-1,y));
|
||||
}
|
||||
if x < (self.lvl.size - 1) {
|
||||
connections.push((x+1,y));
|
||||
}
|
||||
if y > 0 {
|
||||
connections.push((x,y-1));
|
||||
}
|
||||
if y < (self.lvl.size - 1) {
|
||||
connections.push((x,y+1));
|
||||
}
|
||||
let connections = connections.into_iter().map(|(bx, by)| {
|
||||
let (other_color, color) = self.connection(x,y,bx,by);
|
||||
let connected = self.color_is_empty(&color).not();
|
||||
Connection {
|
||||
x: bx,
|
||||
y: by,
|
||||
color,
|
||||
other_color,
|
||||
connected,
|
||||
}
|
||||
}).collect();
|
||||
|
||||
NodeWithConnections {
|
||||
x, y,
|
||||
color,
|
||||
connections,
|
||||
}
|
||||
}).collect()
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
#[derive(Debug, Hash, PartialEq, Eq, Clone)]
|
||||
struct Level {
|
||||
size: u64,
|
||||
unk_always_zero: u64,
|
||||
level_num: u64,
|
||||
num_pipes: u64,
|
||||
pipes: Vec<Vec<u64>>,
|
||||
}
|
||||
|
||||
impl Level {
|
||||
fn unlevel() -> Self {
|
||||
Self {
|
||||
size: 2,
|
||||
unk_always_zero: 0,
|
||||
level_num: 1,
|
||||
num_pipes: 2,
|
||||
pipes: vec![
|
||||
vec![0, 1],
|
||||
vec![2, 3],
|
||||
],
|
||||
}
|
||||
}
|
||||
|
||||
fn sanity_check(&self) -> Result<(), &'static str> {
|
||||
let board_node_count = self.size * self.size;
|
||||
if self.num_pipes != self.pipes.len().try_into().unwrap() {
|
||||
return Err("num_pipes did not match pipes.len()");
|
||||
}
|
||||
let nums:Vec<u64> = self.pipes.iter().flatten().copied().collect();
|
||||
let len_before = nums.len();
|
||||
let mut nums_set = HashSet::new();
|
||||
for num in nums {
|
||||
nums_set.insert(num);
|
||||
}
|
||||
let len_after = nums_set.len();
|
||||
if len_before != len_after {
|
||||
return Err("Non-unique positions (overlapping pipes?)");
|
||||
}
|
||||
if len_after != board_node_count.try_into().unwrap() {
|
||||
return Err("More numbers than size of board");
|
||||
}
|
||||
for num in nums_set.iter().copied() {
|
||||
if num >= board_node_count {
|
||||
return Err("Invalid position number");
|
||||
}
|
||||
}
|
||||
Ok(())
|
||||
}
|
||||
}
|
||||
|
||||
fn parseline(line: &str) -> Level {
|
||||
let segs:Vec<&str> = line.split(';').collect();
|
||||
if segs.len() == 1 {
|
||||
panic!("bad line");
|
||||
}
|
||||
let maybe_metadata:Result<Vec<u64>, _> = segs[0].split(',').map(str::parse).collect();
|
||||
let metadata = maybe_metadata.unwrap();
|
||||
if metadata.len() != 4 {
|
||||
panic!("metadata wrong size");
|
||||
}
|
||||
let size = metadata[0];
|
||||
let unk_always_zero = metadata[1];
|
||||
let level_num = metadata[2];
|
||||
let num_pipes = metadata[3];
|
||||
let pipes = segs[1..].iter().map(|seg| seg.split(',').map(str::parse).map(Result::unwrap).collect()).collect();
|
||||
Level { size, unk_always_zero, level_num, num_pipes, pipes }
|
||||
}
|
||||
Reference in New Issue
Block a user