diff --git a/Cargo.lock b/Cargo.lock index 83be6df..80c48e1 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1,6 +1,6 @@ # This file is automatically @generated by Cargo. # It is not intended for manual editing. -version = 3 +version = 4 [[package]] name = "ahash" @@ -43,9 +43,9 @@ checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" [[package]] name = "bitflags" -version = "2.6.0" +version = "2.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" +checksum = "8f68f53c83ab957f72c32642f3868eec03eb974d1fb82e453128456482613d36" [[package]] name = "bumpalo" @@ -76,9 +76,9 @@ dependencies = [ [[package]] name = "cc" -version = "1.2.1" +version = "1.2.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fd9de9f2205d5ef3fd67e685b0df337994ddd4495e2a28d185500d0e1edfea47" +checksum = "13208fcbb66eaeffe09b99fffbe1af420f00a7b35aa99ad683dfc1aa76145229" dependencies = [ "jobserver", "libc", @@ -126,18 +126,18 @@ dependencies = [ [[package]] name = "clap" -version = "4.5.21" +version = "4.5.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb3b4b9e5a7c7514dfa52869339ee98b3156b0bfb4e8a77c4ff4babb64b1604f" +checksum = "769b0145982b4b48713e01ec42d61614425f27b7058bda7180a3a41f30104796" dependencies = [ "clap_builder", ] [[package]] name = "clap_builder" -version = "4.5.21" +version = "4.5.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b17a95aa67cc7b5ebd32aa5370189aa0d79069ef1c64ce893bd30fb24bff20ec" +checksum = "1b26884eb4b57140e4d2d93652abfa49498b938b3c9179f9fc487b0acc3edad7" dependencies = [ "anstyle", "clap_lex", @@ -145,9 +145,9 @@ dependencies = [ [[package]] name = "clap_lex" -version = "0.7.3" +version = "0.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "afb84c814227b90d6895e01398aee0d8033c00e7466aca416fb6a8e0eb19d8a7" +checksum = "f46ad14479a25103f283c0f10005961cf086d8dc42205bb44c46ac563475dca6" [[package]] name = "codspeed" @@ -173,12 +173,12 @@ dependencies = [ [[package]] name = "colored" -version = "2.1.0" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cbf2150cce219b664a8a70df7a1f933836724b503f8a413af9365b4dcc4d90b8" +checksum = "117725a109d387c937a1533ce01b450cbde6b88abceea8473c4d7a85853cda3c" dependencies = [ "lazy_static", - "windows-sys 0.48.0", + "windows-sys", ] [[package]] @@ -219,9 +219,9 @@ dependencies = [ [[package]] name = "crossbeam-deque" -version = "0.8.5" +version = "0.8.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d" +checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51" dependencies = [ "crossbeam-epoch", "crossbeam-utils", @@ -238,15 +238,15 @@ dependencies = [ [[package]] name = "crossbeam-utils" -version = "0.8.20" +version = "0.8.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" +checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28" [[package]] name = "crunchy" -version = "0.2.2" +version = "0.2.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7a81dae078cea95a014a339291cec439d2f232ebe854a9d672b796c6afafa9b7" +checksum = "43da5946c66ffcc7745f48db692ffbb10a83bfe0afd96235c5c2a4fb23994929" [[package]] name = "ctrlc" @@ -255,7 +255,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "90eeab0aa92f3f9b4e87f258c72b139c207d251f9cbc1080a0086b86a8870dd3" dependencies = [ "nix", - "windows-sys 0.59.0", + "windows-sys", ] [[package]] @@ -318,9 +318,9 @@ checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" [[package]] name = "expect-test" -version = "1.5.0" +version = "1.5.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9e0be0a561335815e06dab7c62e50353134c796e7a6155402a64bcff66b6a5e0" +checksum = "63af43ff4431e848fb47472a920f14fa71c24de13255a5692e93d4e90302acb0" dependencies = [ "dissimilar", "once_cell", @@ -411,13 +411,13 @@ checksum = "44faf5bb8861a9c72e20d3fb0fdbd59233e43056e2b80475ab0aacdc2e781355" [[package]] name = "is-terminal" -version = "0.4.13" +version = "0.4.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "261f68e344040fbd0edea105bef17c66edf46f984ddb1115b775ce31be948f4b" +checksum = "e19b23d53f35ce9f56aebc7d1bb4e6ac1e9c0db7ac85c8d1760c04379edced37" dependencies = [ "hermit-abi", "libc", - "windows-sys 0.52.0", + "windows-sys", ] [[package]] @@ -446,9 +446,9 @@ dependencies = [ [[package]] name = "itoa" -version = "1.0.13" +version = "1.0.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "540654e97a3f4470a492cd30ff187bc95d89557a903a2bbf112e2fae98104ef2" +checksum = "d75a2a4b1b190afb6f5425f10f6a8f959d2ea0b9c2b1d79553551850539e4674" [[package]] name = "jobserver" @@ -461,10 +461,11 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.72" +version = "0.3.77" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6a88f1bda2bd75b0452a14784937d796722fdebfe50df998aeb3f0b7603019a9" +checksum = "1cfaf33c695fc6e08064efbc1f72ec937429614f25eef83af942d0e227c3a28f" dependencies = [ + "once_cell", "wasm-bindgen", ] @@ -476,9 +477,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.164" +version = "0.2.169" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "433bfe06b8c75da9b2e3fbea6e5329ff87748f0b144ef75306e674c3f6f7c13f" +checksum = "b5aba8db14291edd000dfcc4d620c7ebfb122c613afb886ca8803fa4e128a20a" [[package]] name = "lock_api" @@ -492,9 +493,9 @@ dependencies = [ [[package]] name = "log" -version = "0.4.22" +version = "0.4.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" +checksum = "04cbf5b083de1c7e0222a7a51dbfdba1cbe1c6ab0b15e29fff3f6c077fd9cd9f" [[package]] name = "matchers" @@ -644,7 +645,7 @@ dependencies = [ "libc", "redox_syscall", "smallvec", - "windows-targets 0.52.6", + "windows-targets", ] [[package]] @@ -661,14 +662,14 @@ checksum = "5be167a7af36ee22fe3115051bc51f6e6c7054c9348e28deb4f49bd6f705a315" [[package]] name = "pin-project-lite" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "915a1e146535de9163f3987b8944ed8cf49a18bb0056bcebcdcece385cece4ff" +checksum = "3b3cff922bd51709b605d9ead9aa71031d81447142d828eb4a6eba76fe619f9b" [[package]] name = "pindakaas" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" +source = "git+https://github.com/pindakaashq/pindakaas.git#acd50aedde2ed8e4e34b66379957189427857199" dependencies = [ "iset", "itertools 0.13.0", @@ -680,7 +681,7 @@ dependencies = [ [[package]] name = "pindakaas-build-macros" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" +source = "git+https://github.com/pindakaashq/pindakaas.git#acd50aedde2ed8e4e34b66379957189427857199" dependencies = [ "cc", "paste", @@ -688,8 +689,8 @@ dependencies = [ [[package]] name = "pindakaas-cadical" -version = "2.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" +version = "2.1.2" +source = "git+https://github.com/pindakaashq/pindakaas.git#acd50aedde2ed8e4e34b66379957189427857199" dependencies = [ "cc", "pindakaas-build-macros", @@ -698,7 +699,7 @@ dependencies = [ [[package]] name = "pindakaas-derive" version = "0.1.0" -source = "git+https://github.com/pindakaashq/pindakaas.git#424559578c95d714f9fd44b6f81c4eaa437cd83c" +source = "git+https://github.com/pindakaashq/pindakaas.git#acd50aedde2ed8e4e34b66379957189427857199" dependencies = [ "darling", "quote", @@ -735,18 +736,18 @@ dependencies = [ [[package]] name = "proc-macro2" -version = "1.0.92" +version = "1.0.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "37d3544b3f2748c54e147655edb5025752e2303145b5aefb3c3ea2c78b973bb0" +checksum = "60946a68e5f9d28b0dc1c21bb8a97ee7d018a8b322fa57838ba31cc878e22d99" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.37" +version = "1.0.38" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" +checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" dependencies = [ "proc-macro2", ] @@ -783,9 +784,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.7" +version = "0.5.8" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" +checksum = "03a862b389f93e68874fbf580b9de08dd02facb9a788ebadaf4a3fd33cf58834" dependencies = [ "bitflags", ] @@ -836,15 +837,15 @@ checksum = "2b15c43186be67a4fd63bee50d0303afffcef381492ebe2c5d87f324e1b8815c" [[package]] name = "rustc-hash" -version = "2.0.0" +version = "2.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "583034fd73374156e66797ed8e5b0d5690409c9226b22d87cb7f19821c05d152" +checksum = "c7fb8039b3032c191086b10f11f319a6e99e1e82889c5cc6046f515c9db1d497" [[package]] name = "rustversion" -version = "1.0.18" +version = "1.0.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" +checksum = "f7c45b9784283f1b2e7fb61b42047c2fd678ef0960d4f6f1eba131594cc369d4" [[package]] name = "ryu" @@ -869,18 +870,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.215" +version = "1.0.217" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" +checksum = "02fc4265df13d6fa1d00ecff087228cc0a2b5f3c0e87e258d8b94a156e984c70" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.215" +version = "1.0.217" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" +checksum = "5a9bf7cf98d04a2b28aead066b7496853d4779c9cc183c440dbac457641e19a0" dependencies = [ "proc-macro2", "quote", @@ -889,9 +890,9 @@ dependencies = [ [[package]] name = "serde_json" -version = "1.0.133" +version = "1.0.137" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c7fceb2473b9166b2294ef05efcb65a3db80803f0b03ef86a5fc88a2b85ee377" +checksum = "930cfb6e6abf99298aaad7d29abbef7a9999a9a8806a40088f55f0dcec03146b" dependencies = [ "itoa", "memchr", @@ -928,9 +929,9 @@ checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" [[package]] name = "syn" -version = "2.0.89" +version = "2.0.96" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "44d46482f1c1c87acd84dea20c1bf5ebff4c757009ed6bf19cfd36fb10e92c4e" +checksum = "d5d0adab1ae378d7f53bdebc67a39f1f151407ef230f0ce2883572f5d8985c80" dependencies = [ "proc-macro2", "quote", @@ -939,18 +940,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "2.0.3" +version = "2.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c006c85c7651b3cf2ada4584faa36773bd07bac24acfb39f3c431b36d7e667aa" +checksum = "d452f284b73e6d76dd36758a0c8684b1d5be31f92b89d07fd5822175732206fc" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "2.0.3" +version = "2.0.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f077553d607adc1caf65430528a576c757a71ed73944b66ebb58ef2bbd243568" +checksum = "26afc1baea8a989337eeb52b6e72a039780ce45c3edfcc9c5b9d112feeb173c2" dependencies = [ "proc-macro2", "quote", @@ -979,9 +980,9 @@ dependencies = [ [[package]] name = "tracing" -version = "0.1.40" +version = "0.1.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef" +checksum = "784e0ac535deb450455cbfa28a6f0df145ea1bb7ae51b821cf5e7927fdcfbdd0" dependencies = [ "pin-project-lite", "tracing-attributes", @@ -990,9 +991,9 @@ dependencies = [ [[package]] name = "tracing-attributes" -version = "0.1.27" +version = "0.1.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" +checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" dependencies = [ "proc-macro2", "quote", @@ -1001,9 +1002,9 @@ dependencies = [ [[package]] name = "tracing-core" -version = "0.1.32" +version = "0.1.33" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c06d3da6113f116aaee68e4d601191614c9053067f9ab7f6edbcb161237daa54" +checksum = "e672c95779cf947c5311f83787af4fa8fffd12fb27e4993211a84bdfd9610f9c" dependencies = [ "once_cell", "valuable", @@ -1022,9 +1023,9 @@ dependencies = [ [[package]] name = "tracing-subscriber" -version = "0.3.18" +version = "0.3.19" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad0f048c97dbd9faa9b7df56362b8ebcaa52adb06b498c050d2f4e32f90a7a8b" +checksum = "e8189decb5ac0fa7bc8b96b7cb9b2701d60d48805aca84a238004d665fcc4008" dependencies = [ "matchers", "nu-ansi-term", @@ -1061,9 +1062,9 @@ dependencies = [ [[package]] name = "unicode-ident" -version = "1.0.14" +version = "1.0.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "adb9e6ca4f869e1180728b7950e35922a7fc6397f7b641499e8f3ef06e50dc83" +checksum = "11cd88e12b17c6494200a9c1b683a04fcac9573ed74cd1b62aeb2727c5592243" [[package]] name = "ustr" @@ -1080,9 +1081,9 @@ dependencies = [ [[package]] name = "valuable" -version = "0.1.0" +version = "0.1.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" +checksum = "ba73ea9cf16a25df0c8caa16c51acb937d5712a8429db78a3ee29d5dcacd3a65" [[package]] name = "version_check" @@ -1102,24 +1103,24 @@ dependencies = [ [[package]] name = "wasm-bindgen" -version = "0.2.95" +version = "0.2.100" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "128d1e363af62632b8eb57219c8fd7877144af57558fb2ef0368d0087bddeb2e" +checksum = "1edc8929d7499fc4e8f0be2262a241556cfc54a0bea223790e71446f2aab1ef5" dependencies = [ "cfg-if", "once_cell", + "rustversion", "wasm-bindgen-macro", ] [[package]] name = "wasm-bindgen-backend" -version = "0.2.95" +version = "0.2.100" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cb6dd4d3ca0ddffd1dd1c9c04f94b868c37ff5fac97c30b97cff2d74fce3a358" +checksum = "2f0a0651a5c2bc21487bde11ee802ccaf4c51935d0d3d42a6101f98161700bc6" dependencies = [ "bumpalo", "log", - "once_cell", "proc-macro2", "quote", "syn", @@ -1128,9 +1129,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.95" +version = "0.2.100" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e79384be7f8f5a9dd5d7167216f022090cf1f9ec128e6e6a482a2cb5c5422c56" +checksum = "7fe63fc6d09ed3792bd0897b314f53de8e16568c2b3f7982f468c0bf9bd0b407" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1138,9 +1139,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.95" +version = "0.2.100" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" +checksum = "8ae87ea40c9f689fc23f209965b6fb8a99ad69aeeb0231408be24920604395de" dependencies = [ "proc-macro2", "quote", @@ -1151,15 +1152,18 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.95" +version = "0.2.100" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "65fc09f10666a9f147042251e0dda9c18f166ff7de300607007e96bdebc1068d" +checksum = "1a05d73b933a847d6cccdda8f838a22ff101ad9bf93e33684f39c1f5f0eece3d" +dependencies = [ + "unicode-ident", +] [[package]] name = "web-sys" -version = "0.3.72" +version = "0.3.77" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f6488b90108c040df0fe62fa815cbdee25124641df01814dd7282749234c6112" +checksum = "33b6dd2ef9186f1f2072e409e99cd22a975331a6b3591b12c764e0e55c60d5d2" dependencies = [ "js-sys", "wasm-bindgen", @@ -1187,7 +1191,7 @@ version = "0.1.9" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "cf221c93e13a30d793f7645a0e7762c55d169dbb0a49671918a2319d289b10bb" dependencies = [ - "windows-sys 0.59.0", + "windows-sys", ] [[package]] @@ -1196,46 +1200,13 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" -[[package]] -name = "windows-sys" -version = "0.48.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "677d2418bec65e3338edb076e806bc1ec15693c5d0104683f2efe857f61056a9" -dependencies = [ - "windows-targets 0.48.5", -] - -[[package]] -name = "windows-sys" -version = "0.52.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" -dependencies = [ - "windows-targets 0.52.6", -] - [[package]] name = "windows-sys" version = "0.59.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" dependencies = [ - "windows-targets 0.52.6", -] - -[[package]] -name = "windows-targets" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9a2fa6e2155d7247be68c096456083145c183cbbbc2764150dda45a87197940c" -dependencies = [ - "windows_aarch64_gnullvm 0.48.5", - "windows_aarch64_msvc 0.48.5", - "windows_i686_gnu 0.48.5", - "windows_i686_msvc 0.48.5", - "windows_x86_64_gnu 0.48.5", - "windows_x86_64_gnullvm 0.48.5", - "windows_x86_64_msvc 0.48.5", + "windows-targets", ] [[package]] @@ -1244,46 +1215,28 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" dependencies = [ - "windows_aarch64_gnullvm 0.52.6", - "windows_aarch64_msvc 0.52.6", - "windows_i686_gnu 0.52.6", + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", "windows_i686_gnullvm", - "windows_i686_msvc 0.52.6", - "windows_x86_64_gnu 0.52.6", - "windows_x86_64_gnullvm 0.52.6", - "windows_x86_64_msvc 0.52.6", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", ] -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2b38e32f0abccf9987a4e3079dfb67dcd799fb61361e53e2882c3cbaf0d905d8" - [[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.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc35310971f3b2dbbf3f0690a219f40e2d9afcf64f9ab7cc1be722937c26b4bc" - [[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.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a75915e7def60c94dcef72200b9a8e58e5091744960da64ec734a6c6e9b3743e" - [[package]] name = "windows_i686_gnu" version = "0.52.6" @@ -1296,48 +1249,24 @@ version = "0.52.6" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" -[[package]] -name = "windows_i686_msvc" -version = "0.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8f55c233f70c4b27f66c523580f78f1004e8b5a8b659e05a4eb49d4166cca406" - [[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.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "53d40abd2583d23e4718fddf1ebec84dbff8381c07cae67ff7768bbf19c6718e" - [[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.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b7b52767868a23d5bab768e390dc5f5c55825b6d30b86c844ff2dc7414044cc" - [[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.48.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ed94fce61571a4006852b7389a063ab983c02eb1bb37b47f8272ce92d06d9538" - [[package]] name = "windows_x86_64_msvc" version = "0.52.6" diff --git a/crates/huub/src/actions.rs b/crates/huub/src/actions.rs index 576d0b4..156d9d2 100644 --- a/crates/huub/src/actions.rs +++ b/crates/huub/src/actions.rs @@ -1,21 +1,26 @@ //! Traits that encapsulate different sets of actions that can be performed at //! different phases and by different objects in the solving process. +use std::ops::AddAssign; + +use pindakaas::{AsDynClauseDatabase, ClauseDatabase}; + use crate::{ - constraints::{Conflict, LazyReason, ReasonBuilder}, + branchers::BoxedBrancher, + constraints::{BoxedPropagator, Conflict, LazyReason, ReasonBuilder}, + model::{self, int::IntExpr}, solver::{ activation_list::IntPropCond, - engine::{BoxedBrancher, BoxedPropagator, PropRef}, + engine::PropRef, int_var::IntVarRef, queue::PriorityLevel, trail::TrailedInt, - view::{BoolViewInner, IntViewInner}, + view::{BoolView, BoolViewInner, IntViewInner}, }, - BoolView, IntVal, IntView, LitMeaning, ReformulationError, SolverView, + IntSetVal, IntVal, IntView, LitMeaning, Model, ReformulationError, SolverView, }; -/// Actions that can be performed during the initlization of propagators and -/// branchers. +/// Actions that can be performed during the initialization of branchers. pub trait BrancherInitActions: DecisionActions { /// Ensure that any relevant decision variable are marked internally as a /// decidable variable. @@ -29,6 +34,18 @@ pub trait BrancherInitActions: DecisionActions { fn push_brancher(&mut self, brancher: BoxedBrancher); } +/// Actions that can be performed when a constraint is initialized within a +/// model object. +pub trait ConstraintInitActions { + /// Schedule the simplify method of the calling constraint when the given + /// boolean expression changes. + fn simplify_on_change_bool(&mut self, var: model::bool::BoolView); + + /// Schedule the simplify method of the calling constraint when the given + /// integer expression changes. + fn simplify_on_change_int(&mut self, var: IntExpr); +} + /// Actions that can be performed by a [`crate::branchers::Brancher`] when /// making search decisions. pub trait DecisionActions: InspectionActions { @@ -195,13 +212,7 @@ pub trait PropagationActions: ExplanationActions + DecisionActions { } /// Actions that can be performed during the initialization of propagators. -pub trait PropagatorInitActions: DecisionActions { - /// Add a clause to the solver. - fn add_clause>( - &mut self, - clause: I, - ) -> Result<(), ReformulationError>; - +pub trait PropagatorInitActions: AsDynClauseDatabase + ClauseDatabase + DecisionActions { /// Add a propagator to the solver. fn add_propagator(&mut self, propagator: BoxedPropagator, priority: PriorityLevel) -> PropRef; @@ -219,6 +230,94 @@ pub trait PropagatorInitActions: DecisionActions { fn enqueue_on_int_change(&mut self, prop: PropRef, var: IntView, condition: IntPropCond); } +/// Actions that can be performed when reformulating a [`Model`] object into a +/// [`Solver`] object. +pub trait ReformulationActions: PropagatorInitActions { + /// Lookup the solver [`BoolView`] to which the given model + /// [`model::bool::BoolView`] maps. + fn get_solver_bool(&mut self, bv: model::bool::BoolView) -> BoolView; + + /// Lookup the solver [`IntExpr`] to which the given model + /// [`model::int::IntView`] maps. + fn get_solver_int(&mut self, iv: IntExpr) -> IntView; + + /// Create a new Boolean decision variable to use in the encoding. + fn new_bool_var(&mut self) -> BoolView; +} + +/// Actions that can be performed to simplify a Model considering a given +/// constraint. +pub trait SimplificationActions { + /// Add a constraint to the model (to replace the current constraint). + fn add_constraint(&mut self, constraint: C) + where + Model: AddAssign; + + /// Check whether a given integer view can take a given value. + fn check_int_in_domain(&self, var: IntExpr, val: IntVal) -> bool; + + /// Get the current value of a [`BoolView`], if it has been assigned. + fn get_bool_val(&self, bv: model::bool::BoolView) -> Option; + + /// Get the minimum value that an integer view is guaranteed to take. + fn get_int_lower_bound(&self, var: IntExpr) -> IntVal; + + /// Get the maximum value that an integer view is guaranteed to take. + fn get_int_upper_bound(&self, var: IntExpr) -> IntVal; + + /// Convenience method to get both the lower and upper bounds of an integer + /// view. + fn get_int_bounds(&self, var: IntExpr) -> (IntVal, IntVal) { + (self.get_int_lower_bound(var), self.get_int_upper_bound(var)) + } + + /// Get the current value of an integer view, if it has been assigned. + fn get_int_val(&self, var: IntExpr) -> Option { + let (lb, ub) = self.get_int_bounds(var); + if lb == ub { + Some(lb) + } else { + None + } + } + + /// Enforce a boolean view to be `true`. + /// + /// Note that it is possible to enforce that a boolean view is `false` by + /// negating the view, i.e. `!bv`. + fn set_bool(&mut self, bv: model::bool::BoolView) -> Result<(), ReformulationError>; + + /// Enforce that the given integer expression takes a value in in the given + /// set. + fn set_int_in_set( + &mut self, + var: IntExpr, + values: &IntSetVal, + ) -> Result<(), ReformulationError>; + + /// Enforce that a an integer view takes a value that is greater or equal to + /// `val`. + fn set_int_lower_bound(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>; + + /// Enforce that a an integer view takes a value that is less or equal to + /// `val`. + fn set_int_upper_bound(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>; + + /// Enforce that a an integer view takes a value `val`. + fn set_int_val(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>; + + /// Enforce that a an integer view cannot take a value `val`. + fn set_int_not_eq(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError>; + + /// Enforce that a given integer expression cannot take any of the values in + /// the given set. + fn set_int_not_in_set( + &mut self, + var: IntExpr, + values: &IntSetVal, + ) -> Result<(), ReformulationError>; +} + /// Basic actions that can be performed when the trailing infrastructure is /// available. pub trait TrailingActions { diff --git a/crates/huub/src/branchers.rs b/crates/huub/src/branchers.rs index e08685e..c04fb56 100644 --- a/crates/huub/src/branchers.rs +++ b/crates/huub/src/branchers.rs @@ -8,12 +8,11 @@ use crate::{ actions::{BrancherInitActions, DecisionActions}, model::branching::{ValueSelection, VariableSelection}, solver::{ - engine::BoxedBrancher, solving_context::SolvingContext, trail::TrailedInt, - view::{BoolViewInner, IntView, IntViewInner}, + view::{BoolView, BoolViewInner, IntView, IntViewInner}, }, - BoolView, LitMeaning, SolverView, + LitMeaning, SolverView, }; #[derive(Clone, Debug, Eq, Hash, PartialEq)] @@ -32,8 +31,12 @@ pub struct BoolBrancher { next: TrailedInt, } +/// Type alias to represent [`Brancher`] contained in a [`Box`], that is used by +/// [`Engine`]. +pub(crate) type BoxedBrancher = Box Brancher>>; + /// A trait for making search decisions in the solver -pub trait Brancher: DynBranchClone + Debug { +pub trait Brancher: DynBrancherClone + Debug { /// Make a next search decision using the given decision actions. fn decide(&mut self, actions: &mut D) -> Decision; } @@ -54,9 +57,9 @@ pub enum Decision { /// A trait to allow the cloning of boxed branchers. /// /// This trait allows us to implement [`Clone`] for [`BoxedBrancher`]. -pub trait DynBranchClone { +pub trait DynBrancherClone { /// Clone the object and store it as a boxed trait object. - fn clone_dyn_branch(&self) -> BoxedBrancher; + fn clone_dyn_brancher(&self) -> BoxedBrancher; } #[derive(Clone, Debug, PartialEq, Eq)] @@ -86,8 +89,8 @@ pub struct WarmStartBrancher { conflicts: u64, } -impl Brancher> + Clone + 'static> DynBranchClone for B { - fn clone_dyn_branch(&self) -> BoxedBrancher { +impl Brancher> + Clone + 'static> DynBrancherClone for B { + fn clone_dyn_brancher(&self) -> BoxedBrancher { Box::new(self.clone()) } } @@ -168,7 +171,7 @@ impl Brancher for BoolBrancher { impl Clone for BoxedBrancher { fn clone(&self) -> BoxedBrancher { - self.clone_dyn_branch() + self.clone_dyn_brancher() } } diff --git a/crates/huub/src/constraints.rs b/crates/huub/src/constraints.rs index 03cc544..63a99a1 100644 --- a/crates/huub/src/constraints.rs +++ b/crates/huub/src/constraints.rs @@ -1,15 +1,17 @@ //! Module containing the definitions for propagators and their implementations. pub mod all_different_int; +pub mod array_int_element; pub mod array_int_minimum; +pub mod array_var_bool_element; pub mod array_var_int_element; pub mod disjunctive_strict; pub mod int_abs; pub mod int_div; -pub mod int_lin_le; -pub mod int_lin_ne; +pub mod int_linear; pub mod int_pow; pub mod int_times; +pub mod set_in_reif; pub mod table_int; use std::{ @@ -24,15 +26,24 @@ use index_vec::IndexVec; use pindakaas::Lit as RawLit; use crate::{ - actions::{ExplanationActions, PropagationActions}, + actions::{ + ConstraintInitActions, ExplanationActions, PropagationActions, ReformulationActions, + SimplificationActions, + }, solver::{ - engine::{BoxedPropagator, PropRef, State}, + engine::{PropRef, State}, solving_context::SolvingContext, - view::BoolViewInner, + view::{BoolView, BoolViewInner}, }, - BoolView, Conjunction, + Conjunction, Model, ReformulationError, }; +pub(crate) type BoxedConstraint = Box>; + +/// Type alias to represent [`Propagator`] contained in a [`Box`], that is used +/// by [`Engine`]. +pub(crate) type BoxedPropagator = Box Propagator, State>>; + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// A `ReasonBuilder` whose result is cached so it can be used multiple times, /// and is only evaluated once used. @@ -56,12 +67,52 @@ pub struct Conflict { pub(crate) reason: Reason, } +/// A trait for constraints that can be placed in a [`Model`] object. +/// +/// Constraints specified in the library implement this trait, but are using +/// their explicit type in an enumerated type to allow for global model +/// analysis. +pub trait Constraint: Debug + DynConstraintClone { + /// Method called when a constraint is added to the model, allowing the + /// constraint to request addtional calls to its [`Constraint::simplify`] + /// method when decision variables change. + fn initialize(&self, actions: &mut dyn ConstraintInitActions) { + let _ = actions; + // Default implementation does nothing + } + + /// Simplify the [`Model`] given the current constraint. + /// + /// This method is expected to reduce the domains of decision variables, + /// rewrite the constraint to a simpler form, or detect when the constraint is + /// already subsumed by the current state of the model. + fn simplify(&mut self, actions: &mut S) -> Result { + let _ = actions; + Ok(SimplificationStatus::Fixpoint) + } + + /// Encode the constraint using [`Propagator`] objects or clauses for a + /// [`Solver`] object. + /// + /// This method is should place all required propagators and/or clauses in a + /// [`Solver`] object to ensure the constraint will not be violated. + fn to_solver(&self, actions: &mut dyn ReformulationActions) -> Result<(), ReformulationError>; +} + +/// A trait to allow the cloning of user boxed constraint. +/// +/// This trait allows us to implement [`Clone`] for [`BoxedConstraint`]. +pub trait DynConstraintClone { + /// Clone the object and store it as a boxed trait object. + fn clone_dyn_constraint(&self) -> BoxedConstraint; +} + /// A trait to allow the cloning of boxed propagators. /// /// This trait allows us to implement [`Clone`] for [`BoxedPropagator`]. -pub trait DynPropClone { +pub trait DynPropagatorClone { /// Clone the object and store it as a boxed trait object. - fn clone_dyn_prop(&self) -> BoxedPropagator; + fn clone_dyn_propagator(&self) -> BoxedPropagator; } #[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] @@ -78,7 +129,11 @@ pub struct LazyReason(pub(crate) PropRef, pub(crate) u64); /// [`PropagationActions::deferred_reason`]. If the explanation is needed, then /// the propagation engine will revert the state of the solver and call /// [`Propagator::explain`] to receive the explanation. -pub trait Propagator: Debug + DynPropClone { +pub trait Propagator: Debug + DynPropagatorClone +where + P: PropagationActions, + E: ExplanationActions, +{ /// The propagate method is called during the search process to allow the /// propagator to enforce fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> { @@ -128,6 +183,22 @@ pub trait ReasonBuilder { fn build_reason(self, actions: &mut A) -> Result; } +#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)] +/// Status returned by the [`SimplificationActions::simplify`] method, +/// indicating whether the constraint has been subsumed (such that it can be +/// removed from the [`Model`]) or not. +pub enum SimplificationStatus { + /// The constraint has been simplified as much as possible, but should be kept + /// in the [`Model`]. + /// + /// Simplification can be triggered again if any of the decision variables the + /// constraint depends on change. + Fixpoint, + /// The constraint has been simplified to the point where it is subsumed. The + /// constraint can be removed from the [`Model`]. + Subsumed, +} + impl ReasonBuilder for BoolView { fn build_reason(self, _: &mut A) -> Result { match self.0 { @@ -143,9 +214,21 @@ impl ReasonBuilder for &[BoolView] { } } +impl Clone for BoxedConstraint { + fn clone(&self) -> BoxedConstraint { + self.clone_dyn_constraint() + } +} + impl Clone for BoxedPropagator { fn clone(&self) -> BoxedPropagator { - self.clone_dyn_prop() + self.clone_dyn_propagator() + } +} + +impl + Clone + 'static> DynConstraintClone for C { + fn clone_dyn_constraint(&self) -> BoxedConstraint { + Box::new(self.clone()) } } @@ -228,8 +311,8 @@ impl ReasonBuilder for LazyReason { } } -impl Propagator, State> + Clone + 'static> DynPropClone for P { - fn clone_dyn_prop(&self) -> BoxedPropagator { +impl Propagator, State> + Clone + 'static> DynPropagatorClone for P { + fn clone_dyn_propagator(&self) -> BoxedPropagator { Box::new(self.clone()) } } @@ -250,8 +333,8 @@ impl Reason { let reason = props[*prop].explain(actions, lit, *data); reason.into_iter().map(|l| !l).chain(lit).collect() } - Reason::Eager(v) => v.iter().map(|l| !l).chain(lit).collect(), - Reason::Simple(reason) => once(!reason).chain(lit).collect(), + Reason::Eager(v) => v.iter().map(|&l| !l).chain(lit).collect(), + &Reason::Simple(reason) => once(!reason).chain(lit).collect(), } } diff --git a/crates/huub/src/constraints/all_different_int.rs b/crates/huub/src/constraints/all_different_int.rs index fdf9974..f6e7945 100644 --- a/crates/huub/src/constraints/all_different_int.rs +++ b/crates/huub/src/constraints/all_different_int.rs @@ -1,17 +1,33 @@ -//! Propagators for the `all_different_int` constraint, which enforces that a -//! list of integer variables each take a different value. +//! Structure and algorithms for the `all_different_int` constraint, which +//! enforces that a list of integer variables each take a different value. + +use rangelist::{IntervalIterator, RangeList}; use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{Conflict, PropagationActions, Propagator}, + actions::{ + ExplanationActions, PropagatorInitActions, ReformulationActions, SimplificationActions, + }, + constraints::{Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus}, + model::int::IntExpr, solver::{ activation_list::IntPropCond, int_var::LitMeaning, queue::PriorityLevel, view::{IntView, IntViewInner}, }, + ReformulationError, }; +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Representation of the `all_different_int` constraint within a model. +/// +/// This constraint enforces that all the given integer decisions take different +/// values. +pub struct AllDifferentInt { + /// List of integer decision variables that must take different values. + pub(crate) vars: Vec, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Value consistent propagator for the `all_different_int` constraint. pub struct AllDifferentIntValue { @@ -19,10 +35,43 @@ pub struct AllDifferentIntValue { vars: Vec, } +impl Constraint for AllDifferentInt { + fn simplify(&mut self, actions: &mut S) -> Result { + let (vals, vars): (Vec<_>, Vec<_>) = self + .vars + .iter() + .partition(|v| matches!(v, IntExpr::Const(_))); + self.vars = vars; + let neg_dom = RangeList::from_iter(vals.iter().map(|i| { + let IntExpr::Const(i) = i else { unreachable!() }; + *i..=*i + })); + if neg_dom.card() != vals.len() { + return Err(ReformulationError::TrivialUnsatisfiable); + } + if self.vars.is_empty() { + return Ok(SimplificationStatus::Subsumed); + } + if vals.is_empty() { + return Ok(SimplificationStatus::Fixpoint); + } + for v in &self.vars { + actions.set_int_not_in_set(*v, &neg_dom)?; + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let vars: Vec<_> = self.vars.iter().map(|v| slv.get_solver_int(*v)).collect(); + AllDifferentIntValue::new_in(slv, vars); + Ok(()) + } +} + impl AllDifferentIntValue { /// Create a new [`AllDifferentIntValue`] propagator and post it in the /// solver. - pub fn new_in(solver: &mut impl PropagatorInitActions, vars: Vec) { + pub fn new_in(solver: &mut P, vars: Vec) { let enqueue = vars .iter() .any(|v| matches!(v, IntView(IntViewInner::Const(_)))); @@ -173,7 +222,7 @@ mod tests { assert_eq!( slv.solve(|val| { (0..9).for_each(|r| { - let row = all_vars[r].iter().map(|v| val(v.into())).collect_vec(); + let row = all_vars[r].iter().map(|&v| val(v.into())).collect_vec(); assert!( row.iter().all_unique(), "Values in row {} are not all different: {:?}", diff --git a/crates/huub/src/constraints/array_int_element.rs b/crates/huub/src/constraints/array_int_element.rs new file mode 100644 index 0000000..1d16429 --- /dev/null +++ b/crates/huub/src/constraints/array_int_element.rs @@ -0,0 +1,60 @@ +//! Structures and algorithms for the `array_int_element` constraint, which +//! enforces that a resulting variable equals an element of an array of integer +//! values, chosen by an index variable. + +use std::iter::once; + +use itertools::Itertools; +use pindakaas::ClauseDatabaseTools; + +use crate::{ + actions::{ReformulationActions, SimplificationActions}, + constraints::Constraint, + model::int::IntExpr, + IntVal, LitMeaning, ReformulationError, +}; + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `array_int_element` constraint within a model. +/// +/// This constraint enforces that a result integer decision variable takes the +/// value equal the element of the given array of integer values at the given +/// index decision variable. +pub struct ArrayIntElement { + /// The array of integer values + pub(crate) array: Vec, + /// The index variable + pub(crate) index: IntExpr, + /// The resulting variable + pub(crate) result: IntExpr, +} + +impl Constraint for ArrayIntElement { + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let index = slv.get_solver_int(self.index); + let result = slv.get_solver_int(self.result); + + let idx_map = self + .array + .iter() + .enumerate() + .map(|(i, v)| (*v, i as IntVal)) + .into_group_map(); + + for (val, idxs) in idx_map { + let val_eq = slv.get_int_lit(result, LitMeaning::Eq(val)); + let idxs: Vec<_> = idxs + .into_iter() + .map(|i| slv.get_int_lit(index, LitMeaning::Eq(i))) + .collect(); + + for i in idxs.iter() { + // (idx = i) -> (val = arr[i]) + slv.add_clause([!i, val_eq])?; + } + // (idx not in idxs) -> (val != arr[i]) + slv.add_clause(idxs.into_iter().chain(once(!val_eq)))?; + } + Ok(()) + } +} diff --git a/crates/huub/src/constraints/array_int_minimum.rs b/crates/huub/src/constraints/array_int_minimum.rs index 827e394..b5063a8 100644 --- a/crates/huub/src/constraints/array_int_minimum.rs +++ b/crates/huub/src/constraints/array_int_minimum.rs @@ -1,28 +1,86 @@ -//! Propagators for the `array_int_minimum` constraint, which enforces that a -//! variable takes the minimum value of an array of variables. +//! Structures and algorithms for the `array_int_minimum` constraint, which +//! enforces that a variable takes the minimum value of an array of variables. use itertools::Itertools; use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{Conflict, PropagationActions, Propagator}, + actions::{ + ConstraintInitActions, ExplanationActions, PropagatorInitActions, ReformulationActions, + SimplificationActions, + }, + constraints::{Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus}, + model::int::IntExpr, solver::{activation_list::IntPropCond, queue::PriorityLevel, value::IntVal, view::IntView}, - LitMeaning, + LitMeaning, ReformulationError, }; +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `array_int_minimum` constraint within a model. +/// +/// This constraint enforces that an integer decision variable takes the minimum +/// value of an array of integer decision variables. +pub struct ArrayIntMinimum { + /// Set of decision variables from which the mimimum must be taken + pub(crate) vars: Vec, + /// Decision variable that represents the minimum value + pub(crate) min: IntExpr, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Bounds cosistent propagator for the `array_int_minimum` constraint. pub struct ArrayIntMinimumBounds { - /// Set of variable from which the mimimum must be taken + /// Set of decision variables from which the mimimum must be taken vars: Vec, - /// Variable that represents the minimum value + /// Decision variable that represents the minimum value min: IntView, } +impl Constraint for ArrayIntMinimum { + fn initialize(&self, actions: &mut dyn ConstraintInitActions) { + for v in &self.vars { + actions.simplify_on_change_int(*v); + } + actions.simplify_on_change_int(self.min); + } + + fn simplify(&mut self, actions: &mut S) -> Result { + let min_lb = self + .vars + .iter() + .map(|&v| actions.get_int_lower_bound(v)) + .min() + .unwrap(); + let min_ub = self + .vars + .iter() + .map(|&v| actions.get_int_upper_bound(v)) + .min() + .unwrap(); + actions.set_int_lower_bound(self.min, min_lb)?; + actions.set_int_upper_bound(self.min, min_ub)?; + + let lb = actions.get_int_lower_bound(self.min); + for &v in &self.vars { + actions.set_int_lower_bound(v, lb)?; + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let vars: Vec<_> = self.vars.iter().map(|v| slv.get_solver_int(*v)).collect(); + let min = slv.get_solver_int(self.min); + ArrayIntMinimumBounds::new_in(slv, vars, min); + Ok(()) + } +} + impl ArrayIntMinimumBounds { /// Create a new [`ArrayIntMinimumBounds`] propagator and post it in the /// solver. - pub fn new_in(solver: &mut impl PropagatorInitActions, vars: Vec, min: IntView) { + pub fn new_in

(solver: &mut P, vars: Vec, min: IntView) + where + P: PropagatorInitActions + ?Sized, + { let prop = solver.add_propagator( Box::new(Self { vars: vars.clone(), @@ -91,7 +149,9 @@ mod tests { use itertools::Itertools; use tracing_test::traced_test; - use crate::{model::ModelView, Constraint, InitConfig, Model}; + use crate::{ + array_int_maximum, array_int_minimum, model::reformulate::ModelView, InitConfig, Model, + }; #[test] #[traced_test] @@ -102,7 +162,7 @@ mod tests { let c = prb.new_int_var((2..=5).into()); let y = prb.new_int_var((1..=3).into()); - prb += Constraint::ArrayIntMaximum(vec![a.clone(), b.clone(), c.clone()], y.clone()); + prb += array_int_maximum(vec![a, b, c], y); let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap(); let vars = vec![a, b, c, y] .into_iter() @@ -130,7 +190,7 @@ mod tests { let c = prb.new_int_var((4..=10).into()); let y = prb.new_int_var((13..=20).into()); - prb += Constraint::ArrayIntMaximum(vec![a, b, c], y); + prb += array_int_maximum(vec![a, b, c], y); prb.assert_unsatisfiable(); } @@ -143,7 +203,7 @@ mod tests { let c = prb.new_int_var((2..=3).into()); let y = prb.new_int_var((3..=4).into()); - prb += Constraint::ArrayIntMinimum(vec![a.clone(), b.clone(), c.clone()], y.clone()); + prb += array_int_minimum(vec![a, b, c], y); let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap(); let vars = vec![a, b, c, y] .into_iter() @@ -166,7 +226,7 @@ mod tests { let c = prb.new_int_var((4..=10).into()); let y = prb.new_int_var((1..=2).into()); - prb += Constraint::ArrayIntMinimum(vec![a, b, c], y); + prb += array_int_minimum(vec![a, b, c], y); prb.assert_unsatisfiable(); } } diff --git a/crates/huub/src/constraints/array_var_bool_element.rs b/crates/huub/src/constraints/array_var_bool_element.rs new file mode 100644 index 0000000..cb7aab4 --- /dev/null +++ b/crates/huub/src/constraints/array_var_bool_element.rs @@ -0,0 +1,65 @@ +//! Structures and algorithms for the `array_var_bool_element` constraint, which +//! enforces that a resulting variable equals an element of an array of Boolean +//! decision variables, chosen by an index variable. + +use std::iter::once; + +use pindakaas::{propositional_logic::Formula, ClauseDatabaseTools}; + +use crate::{ + actions::{ReformulationActions, SimplificationActions}, + constraints::{Constraint, SimplificationStatus}, + model::{bool::BoolView, int::IntExpr}, + IntVal, LitMeaning, ReformulationError, +}; + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `array_var_bool_element` constraint within a model. +/// +/// This constraint enforces that a result Boolean decision variable takes the +/// value equal the element of the given array of Boolean decision varaibles at +/// the index given by the index integer decision variable. +pub struct ArrayVarBoolElement { + /// The array of Boolean decision expressions + pub(crate) array: Vec, + /// The index variable + pub(crate) index: IntExpr, + /// The resulting variable + pub(crate) result: BoolView, +} + +impl Constraint for ArrayVarBoolElement { + fn simplify(&mut self, actions: &mut S) -> Result { + if let Some(i) = actions.get_int_val(self.index) { + actions.add_constraint(Formula::Equiv(vec![ + self.array[i as usize].into(), + self.result.into(), + ])); + return Ok(SimplificationStatus::Subsumed); + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let result = slv.get_solver_bool(self.result); + let index = slv.get_solver_int(self.index); + + // Evaluate result literal + let arr: Vec<_> = self.array.iter().map(|&v| slv.get_solver_bool(v)).collect(); + + for (i, l) in arr.iter().enumerate() { + // Evaluate array literal + let idx_eq = slv.get_int_lit(index, LitMeaning::Eq(i as IntVal)); + // add clause (idx = i + 1 /\ arr[i]) => val + slv.add_clause([!idx_eq, !l, result])?; + // add clause (idx = i + 1 /\ !arr[i]) => !val + slv.add_clause([!idx_eq, *l, !result])?; + } + + // add clause (arr[1] /\ arr[2] /\ ... /\ arr[n]) => val + slv.add_clause(arr.iter().map(|l| !l).chain(once(result)))?; + // add clause (!arr[1] /\ !arr[2] /\ ... /\ !arr[n]) => !val + slv.add_clause(arr.into_iter().chain(once(!result)))?; + Ok(()) + } +} diff --git a/crates/huub/src/constraints/array_var_int_element.rs b/crates/huub/src/constraints/array_var_int_element.rs index 02e4e13..2d6480f 100644 --- a/crates/huub/src/constraints/array_var_int_element.rs +++ b/crates/huub/src/constraints/array_var_int_element.rs @@ -1,18 +1,38 @@ -//! Propagators for the `array_var_int_element` constraint, which enforces that -//! a resulting variable equals an element of an array of variables, chosen by -//! an index variable. +//! Structures and algorithms for the `array_var_int_element` constraint, which +//! enforces that a resulting variable equals an element of an array of +//! variables, chosen by an index variable. use itertools::Itertools; use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{Conflict, PropagationActions, Propagator}, + actions::{ + ConstraintInitActions, ExplanationActions, PropagatorInitActions, ReformulationActions, + SimplificationActions, + }, + constraints::{Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus}, + model::int::IntExpr, solver::{ activation_list::IntPropCond, queue::PriorityLevel, trail::TrailedInt, value::IntVal, view::IntView, }, LitMeaning, ReformulationError, }; +use pindakaas::ClauseDatabaseTools; + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `array_var_int_element` constraint within a model. +/// +/// This constraint enforces that a result integer decision variable takes the +/// value equal the element of the given array of integer decision variable at +/// the given index decision variable. +pub struct ArrayVarIntElement { + /// The array of integer values + pub(crate) array: Vec, + /// The index variable + pub(crate) index: IntExpr, + /// The resulting variable + pub(crate) result: IntExpr, +} #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Bounds consistent propagator for the `array_var_int_element` constraint. @@ -29,20 +49,62 @@ pub struct ArrayVarIntElementBounds { max_support: TrailedInt, } +impl Constraint for ArrayVarIntElement { + fn initialize(&self, actions: &mut dyn ConstraintInitActions) { + for &a in &self.array { + actions.simplify_on_change_int(a); + } + actions.simplify_on_change_int(self.result); + actions.simplify_on_change_int(self.index); + } + + fn simplify(&mut self, actions: &mut S) -> Result { + // make sure idx is within the range of args + actions.set_int_lower_bound(self.index, 0)?; + actions.set_int_upper_bound(self.index, self.array.len() as IntVal - 1)?; + let (min_lb, max_ub) = + self.array + .iter() + .fold((IntVal::MAX, IntVal::MIN), |(min_lb, max_ub), &v| { + ( + min_lb.min(actions.get_int_lower_bound(v)), + max_ub.max(actions.get_int_upper_bound(v)), + ) + }); + if min_lb > actions.get_int_lower_bound(self.result) { + actions.set_int_lower_bound(self.result, min_lb)?; + } + if max_ub < actions.get_int_upper_bound(self.result) { + actions.set_int_upper_bound(self.result, max_ub)?; + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let array = self.array.iter().map(|&v| slv.get_solver_int(v)).collect(); + let result = slv.get_solver_int(self.result); + let index = slv.get_solver_int(self.index); + ArrayVarIntElementBounds::new_in(slv, array, result, index) + } +} + impl ArrayVarIntElementBounds { /// Create a new [`ArrayVarIntElementBounds`] propagator and post it in the /// solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, + pub fn new_in

( + solver: &mut P, collection: Vec, result: IntView, index: IntView, - ) -> Result<(), ReformulationError> { + ) -> Result<(), ReformulationError> + where + P: PropagatorInitActions + ?Sized, + { // Remove out-of-bound values from the index variables let index_ub = solver.get_int_lit(index, LitMeaning::Less(collection.len() as IntVal)); let index_lb = solver.get_int_lit(index, LitMeaning::GreaterEq(0)); - solver.add_clause(vec![index_ub])?; - solver.add_clause(vec![index_lb])?; + solver.add_clause([index_ub])?; + solver.add_clause([index_lb])?; // Initialize the min_support and max_support variables let mut min_support = -1; @@ -244,9 +306,10 @@ mod tests { use tracing_test::traced_test; use crate::{ + array_var_int_element, constraints::array_var_int_element::ArrayVarIntElementBounds, solver::int_var::{EncodingType, IntVar}, - Constraint, Model, Solver, + Model, Solver, }; #[test] @@ -355,10 +418,10 @@ mod tests { let a = prb.new_int_var((3..=5).into()); let b = prb.new_int_var((4..=5).into()); let c = prb.new_int_var((4..=10).into()); - let y = prb.new_int_var((1..=2).into()); + let result = prb.new_int_var((1..=2).into()); let index = prb.new_int_var((0..=2).into()); - prb += Constraint::ArrayVarIntElement(vec![a, b, c], index, y); + prb += array_var_int_element(index, vec![a, b, c], result); prb.assert_unsatisfiable(); } } diff --git a/crates/huub/src/constraints/disjunctive_strict.rs b/crates/huub/src/constraints/disjunctive_strict.rs index 1769c71..546b0ed 100644 --- a/crates/huub/src/constraints/disjunctive_strict.rs +++ b/crates/huub/src/constraints/disjunctive_strict.rs @@ -1,30 +1,49 @@ -//! Propagators for the `disjunctive_strict` constraint, which enforces that no -//! two tasks overlap from a list of tasks. +//! Structures and algorithms for the `disjunctive_strict` constraint, which +//! enforces that no two tasks overlap from a list of tasks. use itertools::Itertools; use pindakaas::Lit as RawLit; use tracing::trace; use crate::{ - actions::{ExplanationActions, InspectionActions, PropagatorInitActions}, - constraints::{Conflict, PropagationActions, Propagator, ReasonBuilder}, + actions::{ + ExplanationActions, InspectionActions, PropagatorInitActions, ReformulationActions, + SimplificationActions, + }, + constraints::{ + Conflict, Constraint, PropagationActions, Propagator, ReasonBuilder, SimplificationStatus, + }, + model::int::IntExpr, solver::{ activation_list::IntPropCond, queue::PriorityLevel, trail::TrailedInt, view::{BoolViewInner, IntView}, }, - Conjunction, LitMeaning, + Conjunction, IntVal, LitMeaning, ReformulationError, }; +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `disjunctive_strict` constraint within a model. +/// +/// This constraint enforces that the given a list of integer decision variables +/// representing the start times of tasks and a list of integer values +/// representing the durations of tasks, the tasks do not overlap in time. +pub struct DisjunctiveStrict { + /// Start time variables of each task. + pub(crate) start_times: Vec, + /// Durations of each task. + pub(crate) durations: Vec, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// A propagator for the `disjunctive` constraint using the Strict Edge Finding -/// algorithm. +/// A propagator for the `disjunctive_strict` constraint using the Strict Edge +/// Finding algorithm. pub struct DisjunctiveStrictEdgeFinding { /// Start time variables of each task. start_times: Vec, /// Durations of each task. - durations: Vec, + durations: Vec, // Internal state for propagation /// Indexes of the tasks sorted by earliest start time. @@ -77,6 +96,54 @@ struct TaskInfo { latest_completion: TrailedInt, } +impl Constraint for DisjunctiveStrict { + fn simplify(&mut self, actions: &mut S) -> Result { + // return TrivialUnsatisfiable if overload is detected + let (earliest_start, latest_completion) = + self.start_times.iter().zip(self.durations.iter()).fold( + (IntVal::MAX, IntVal::MIN), + |(earliest_start, latest_completion), (&start, &duration)| { + ( + i64::min( + earliest_start.min(actions.get_int_lower_bound(start)), + earliest_start, + ), + i64::max( + latest_completion.max(actions.get_int_upper_bound(start) + duration), + latest_completion, + ), + ) + }, + ); + let total_duration = self.durations.iter().sum::(); + if earliest_start + total_duration > latest_completion { + return Err(ReformulationError::TrivialUnsatisfiable); + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let start_times = self + .start_times + .iter() + .map(|&v| slv.get_solver_int(v)) + .collect_vec(); + // Add propagator for lower bound propagation + DisjunctiveStrictEdgeFinding::new_in(slv, start_times.clone(), self.durations.clone()); + + // Add symmetric propagator for upper bound propagation + let iter = start_times.iter().zip(self.durations.iter()); + let horizon = iter + .clone() + .map(|(v, d)| slv.get_int_upper_bound(*v) + d) + .max() + .unwrap(); + let symmetric_vars = iter.map(|(v, d)| -*v + (horizon - d)).collect(); + DisjunctiveStrictEdgeFinding::new_in(slv, symmetric_vars, self.durations.clone()); + Ok(()) + } +} + impl DisjunctiveStrictEdgeFinding { #[inline] /// Return the (current) earliest start time of task `i`. @@ -123,7 +190,7 @@ impl DisjunctiveStrictEdgeFinding { .flat_map(|&i| { let (bv, _) = actions.get_int_lit_relaxed( self.start_times[i], - LitMeaning::Less((time_bound - slack) as i64 - self.durations[i]), + LitMeaning::Less((time_bound - slack) as IntVal - self.durations[i]), ); [actions.get_int_lower_bound_lit(self.start_times[i]), bv] }) @@ -139,11 +206,10 @@ impl DisjunctiveStrictEdgeFinding { /// Create a new [`DisjunctiveStrictEdgeFinding`] propagator and post it in /// the solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, - start_times: Vec, - durations: Vec, - ) { + pub fn new_in

(solver: &mut P, start_times: Vec, durations: Vec) + where + P: PropagatorInitActions + ?Sized, + { let n = start_times.len(); let trailed_info = (0..n) .map(|_| TaskInfo { diff --git a/crates/huub/src/constraints/int_abs.rs b/crates/huub/src/constraints/int_abs.rs index 67c44f7..b397aec 100644 --- a/crates/huub/src/constraints/int_abs.rs +++ b/crates/huub/src/constraints/int_abs.rs @@ -1,15 +1,30 @@ -//! Propagators for the `int_abs` constraint, which enforces that one variable -//! is takes absolute value of another. +//! Structures and algorithms for the `int_abs` constraint, which enforces that +//! one variable is takes absolute value of another. use std::iter::once; use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{Conflict, PropagationActions, Propagator}, + actions::{ + ExplanationActions, PropagatorInitActions, ReformulationActions, SimplificationActions, + }, + constraints::{Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus}, + model::int::IntExpr, solver::{activation_list::IntPropCond, queue::PriorityLevel}, - IntView, LitMeaning, + IntView, LitMeaning, ReformulationError, }; +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `int_abs` constraint within a model. +/// +/// This constraint enforces that the second integer decision variable takes the +/// absolute value of the first integer decision variable. +pub struct IntAbs { + /// The integer decision variable whose absolute value is being taken + pub(crate) origin: IntExpr, + /// The integer decision variable representing the absolute value + pub(crate) abs: IntExpr, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Bounds propagator for one integer variable being the absolute value of another pub struct IntAbsBounds { @@ -19,9 +34,46 @@ pub struct IntAbsBounds { abs: IntView, } +impl Constraint for IntAbs { + fn simplify(&mut self, actions: &mut S) -> Result { + let (lb, ub) = actions.get_int_bounds(self.origin); + if ub < 0 { + actions.set_int_lower_bound(self.abs, -ub)?; + actions.set_int_upper_bound(self.abs, -lb)?; + } else if lb >= 0 { + actions.set_int_lower_bound(self.abs, lb)?; + actions.set_int_upper_bound(self.abs, ub)?; + } else { + actions.set_int_lower_bound(self.abs, 0)?; + let abs_max = ub.max(-lb); + actions.set_int_upper_bound(self.abs, abs_max)?; + } + let abs_ub = actions.get_int_upper_bound(self.abs); + actions.set_int_lower_bound(self.origin, -abs_ub)?; + actions.set_int_upper_bound(self.abs, abs_ub)?; + if lb >= 0 { + // TODO: Unify + actions.add_constraint((self.origin - self.abs).eq(0)); + return Ok(SimplificationStatus::Subsumed); + } + + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let origin = slv.get_solver_int(self.origin); + let abs = slv.get_solver_int(self.abs); + IntAbsBounds::new_in(slv, origin, abs); + Ok(()) + } +} + impl IntAbsBounds { /// Create a new [`IntAbsBounds`] propagator and post it in the solver. - pub fn new_in(solver: &mut impl PropagatorInitActions, origin: IntView, abs: IntView) { + pub fn new_in

(solver: &mut P, origin: IntView, abs: IntView) + where + P: PropagatorInitActions + ?Sized, + { let prop = solver.add_propagator(Box::new(Self { origin, abs }), PriorityLevel::Highest); // Subscribe to both bounds of the origin variable solver.enqueue_on_int_change(prop, origin, IntPropCond::Bounds); diff --git a/crates/huub/src/constraints/int_div.rs b/crates/huub/src/constraints/int_div.rs index 11eafc4..6e25ba5 100644 --- a/crates/huub/src/constraints/int_div.rs +++ b/crates/huub/src/constraints/int_div.rs @@ -1,17 +1,40 @@ -//! Propagators for the `int_div` constraint, which enforces that a numerator, a -//! denominator, and a result variable are correctly related by integer -//! division. +//! Structures and algorithms for the `int_div` constraint, which enforces that +//! a numerator, a denominator, and a result variable are correctly related by +//! integer division. use std::mem; use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{Conflict, PropagationActions, Propagator}, + actions::{ + ExplanationActions, PropagatorInitActions, ReformulationActions, SimplificationActions, + }, + constraints::{Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus}, helpers::div_ceil, + model::int::IntExpr, solver::{activation_list::IntPropCond, queue::PriorityLevel}, IntView, LitMeaning, NonZeroIntVal, ReformulationError, }; +use pindakaas::ClauseDatabaseTools; + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `int_div` constraint within a model. +/// +/// This constraint enforces that a numerator decision integer variable divided +/// by a denominator integer decision variable is equal to a result integer +/// decision variable. +/// +/// Note that the division is integer division, i.e. the result is rounded +/// towards zero. +pub struct IntDiv { + /// The numerator of the division + pub(crate) numerator: IntExpr, + /// The denominator of the division + pub(crate) denominator: IntExpr, + /// Result of the division + pub(crate) result: IntExpr, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Bounds propagator for the division of two integer variables. /// @@ -26,14 +49,31 @@ pub struct IntDivBounds { result: IntView, } +impl Constraint for IntDiv { + fn simplify(&mut self, actions: &mut S) -> Result { + actions.set_int_not_eq(self.denominator, 0)?; + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let numerator = slv.get_solver_int(self.numerator); + let denominator = slv.get_solver_int(self.denominator); + let result = slv.get_solver_int(self.result); + IntDivBounds::new_in(slv, numerator, denominator, result) + } +} + impl IntDivBounds { /// Create a new [`IntDivBounds`] propagator and post it in the solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, + pub fn new_in

( + solver: &mut P, numerator: IntView, denominator: IntView, result: IntView, - ) -> Result<(), ReformulationError> { + ) -> Result<(), ReformulationError> + where + P: PropagatorInitActions + ?Sized, + { let prop = solver.add_propagator( Box::new(Self { numerator, @@ -60,13 +100,13 @@ impl IntDivBounds { let res_neg = solver.get_int_lit(result, LitMeaning::Less(1)); // num >= 0 /\ denom > 0 => res >= 0 - solver.add_clause(vec![!num_pos, !denom_pos, res_pos])?; + solver.add_clause([!num_pos, !denom_pos, res_pos])?; // num <= 0 /\ denom < 0 => res >= 0 - solver.add_clause(vec![!num_neg, !denom_neg, res_pos])?; + solver.add_clause([!num_neg, !denom_neg, res_pos])?; // num >= 0 /\ denom < 0 => res < 0 - solver.add_clause(vec![!num_pos, !denom_neg, res_neg])?; + solver.add_clause([!num_pos, !denom_neg, res_neg])?; // num < 0 /\ denom >= 0 => res < 0 - solver.add_clause(vec![!num_neg, !denom_pos, res_neg])?; + solver.add_clause([!num_neg, !denom_pos, res_neg])?; } Ok(()) diff --git a/crates/huub/src/constraints/int_lin_le.rs b/crates/huub/src/constraints/int_lin_le.rs deleted file mode 100644 index f0eebb7..0000000 --- a/crates/huub/src/constraints/int_lin_le.rs +++ /dev/null @@ -1,383 +0,0 @@ -//! Propagator for the `int_lin_le` constraint, and its reification. This -//! constraint enforce that the sum of the products of the variables is less or -//! equal to a given value. - -use itertools::Itertools; -use pindakaas::Lit as RawLit; - -use crate::{ - actions::PropagatorInitActions, - constraints::{Conflict, ExplanationActions, PropagationActions, Propagator}, - helpers::opt_field::OptField, - solver::{ - activation_list::IntPropCond, - queue::PriorityLevel, - value::IntVal, - view::{BoolViewInner, IntView, IntViewInner}, - }, - BoolView, Conjunction, -}; - -/// Type alias for the non-reified version of the [`IntLinearLessEqBoundsImpl`] -/// propagator. -pub(crate) type IntLinearLessEqBounds = IntLinearLessEqBoundsImpl<0>; - -#[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// Value consistent propagator for the `int_lin_le` or `int_lin_le_imp` -/// constraint. -/// -/// `R` should be `0` if the propagator is not refied, or `1` if it is. Other -/// values are invalid. -pub struct IntLinearLessEqBoundsImpl { - /// Variables that are being summed - vars: Vec, - /// Maximum value of the sum can take - max: IntVal, - /// Reified variable, if any - reification: OptField, -} - -/// Type alias for the reified version of the [`IntLinearLessEqBoundsImpl`] -/// propagator. -pub(crate) type IntLinearLessEqImpBounds = IntLinearLessEqBoundsImpl<1>; - -impl IntLinearLessEqBounds { - /// Create a new [`IntLinearLessEqBounds`] propagator and post it in the - /// solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, - vars: impl IntoIterator, - mut max: IntVal, - ) { - let vars: Vec = vars - .into_iter() - .filter(|v| { - if let IntViewInner::Const(c) = v.0 { - max -= c; - false - } else { - true - } - }) - .collect(); - - let prop = solver.add_propagator( - Box::new(Self { - vars: vars.clone(), - max, - reification: Default::default(), - }), - PriorityLevel::Low, - ); - solver.enqueue_now(prop); - for &v in vars.iter() { - solver.enqueue_on_int_change(prop, v, IntPropCond::UpperBound); - } - } -} - -impl Propagator for IntLinearLessEqBoundsImpl -where - P: PropagationActions, - E: ExplanationActions, -{ - fn explain(&mut self, actions: &mut E, _: Option, data: u64) -> Conjunction { - let i = data as usize; - let mut var_lits: Vec = self - .vars - .iter() - .enumerate() - .filter_map(|(j, v)| { - if j == i { - return None; - } - if let BoolView(BoolViewInner::Lit(lit)) = actions.get_int_lower_bound_lit(*v) { - Some(lit) - } else { - None - } - }) - .collect(); - if let Some(r) = self.reification.get() { - var_lits.push(*r); - } - var_lits - } - // propagation rule: x[i] <= rhs - sum_{j != i} x[j].lower_bound - #[tracing::instrument(name = "int_lin_le", level = "trace", skip(self, actions))] - fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> { - // If the reified variable is false, skip propagation - if let Some(&r) = self.reification.get() { - if !actions.get_bool_val(r.into()).unwrap_or(true) { - return Ok(()); - } - } - - // get the difference between the right-hand-side value and the sum of variable lower bounds - let sum = self - .vars - .iter() - .map(|v| actions.get_int_lower_bound(*v)) - .fold(self.max, |sum, val| sum - val); - - // propagate the reified variable if the sum of lower bounds is greater than the right-hand-side value - if let Some(&r) = self.reification.get() { - if sum < 0 { - actions.set_bool((!r).into(), |a: &mut P| { - self.vars - .iter() - .map(|v| a.get_int_lower_bound_lit(*v)) - .collect_vec() - })?; - } - // skip the remaining propagation if the reified variable is not assigned to true - if !actions.get_bool_val(r.into()).unwrap_or(false) { - return Ok(()); - } - } - - // propagate the upper bound of the variables - for (j, &v) in self.vars.iter().enumerate() { - let reason = actions.deferred_reason(j as u64); - let ub = sum + actions.get_int_lower_bound(v); - actions.set_int_upper_bound(v, ub, reason)?; - } - Ok(()) - } -} - -impl IntLinearLessEqImpBounds { - /// Create a new [`IntLinearLessEqImpBounds`] propagator and post it in the - /// solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, - vars: impl IntoIterator, - mut max: IntVal, - reification: BoolView, - ) { - let reification = match reification.0 { - BoolViewInner::Lit(r) => r, - BoolViewInner::Const(true) => return IntLinearLessEqBounds::new_in(solver, vars, max), - BoolViewInner::Const(false) => return, - }; - let vars: Vec = vars - .into_iter() - .filter(|v| { - if let IntViewInner::Const(c) = v.0 { - max -= c; - false - } else { - true - } - }) - .collect(); - - let prop = solver.add_propagator( - Box::new(Self { - vars: vars.clone(), - max, - reification: OptField::new(reification), - }), - PriorityLevel::Low, - ); - solver.enqueue_now(prop); - for &v in vars.iter() { - solver.enqueue_on_int_change(prop, v, IntPropCond::UpperBound); - } - solver.enqueue_on_bool_change(prop, reification.into()); - } -} - -#[cfg(test)] -mod tests { - use expect_test::expect; - use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; - use rangelist::RangeList; - use tracing_test::traced_test; - - use crate::{ - constraints::int_lin_le::IntLinearLessEqBounds, - solver::int_var::{EncodingType, IntVar}, - Constraint, InitConfig, Model, NonZeroIntVal, Solver, - }; - - #[test] - #[traced_test] - fn test_linear_ge_sat() { - let mut slv = Solver::>::from(&Cnf::default()); - let a = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Lazy, - ); - let b = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Lazy, - ); - let c = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Lazy, - ); - - IntLinearLessEqBounds::new_in( - &mut slv, - vec![a * NonZeroIntVal::new(-2).unwrap(), -b, -c], - -6, - ); - - slv.expect_solutions( - &[a, b, c], - expect![[r#" - 1, 2, 2 - 2, 1, 1 - 2, 1, 2 - 2, 2, 1 - 2, 2, 2"#]], - ); - } - - #[test] - #[traced_test] - fn test_linear_ge_unsat() { - let mut prb = Model::default(); - let a = prb.new_int_var((1..=2).into()); - let b = prb.new_int_var((1..=2).into()); - let c = prb.new_int_var((1..=2).into()); - - prb += Constraint::IntLinLessEq(vec![a * -2, -b, -c], -10); - prb.assert_unsatisfiable(); - } - - #[test] - #[traced_test] - fn test_linear_le_sat() { - let mut slv = Solver::>::from(&Cnf::default()); - let a = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Lazy, - ); - let b = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Lazy, - ); - let c = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Lazy, - ); - - IntLinearLessEqBounds::new_in(&mut slv, vec![a * NonZeroIntVal::new(2).unwrap(), b, c], 6); - - slv.expect_solutions( - &[a, b, c], - expect![[r#" - 1, 1, 1 - 1, 1, 2 - 1, 2, 1 - 1, 2, 2 - 2, 1, 1"#]], - ); - } - - #[test] - #[traced_test] - fn test_linear_le_unsat() { - let mut prb = Model::default(); - let a = prb.new_int_var((1..=4).into()); - let b = prb.new_int_var((1..=4).into()); - let c = prb.new_int_var((1..=4).into()); - - prb += Constraint::IntLinLessEq(vec![a * 2, b, c], 3); - prb.assert_unsatisfiable(); - } - - #[test] - #[traced_test] - fn test_reified_linear_ge_sat() { - let mut prb = Model::default(); - let r = prb.new_bool_var(); - let a = prb.new_int_var((1..=2).into()); - let b = prb.new_int_var((1..=2).into()); - let c = prb.new_int_var((1..=2).into()); - - prb += Constraint::IntLinLessEqImp( - vec![ - a.clone() * NonZeroIntVal::new(-2).unwrap(), - -b.clone(), - -c.clone(), - ], - -7, - r.clone().into(), - ); - let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); - let a = map.get(&mut slv, &a.into()); - let b = map.get(&mut slv, &b.into()); - let c = map.get(&mut slv, &c.into()); - let r = map.get(&mut slv, &r.into()); - slv.expect_solutions( - &[r, a, b, c], - expect![[r#" - false, 1, 1, 1 - false, 1, 1, 2 - false, 1, 2, 1 - false, 1, 2, 2 - false, 2, 1, 1 - false, 2, 1, 2 - false, 2, 2, 1 - false, 2, 2, 2 - true, 2, 1, 2 - true, 2, 2, 1 - true, 2, 2, 2"#]], - ); - } - - #[test] - #[traced_test] - fn test_reified_linear_le_sat() { - let mut prb = Model::default(); - let r = prb.new_bool_var(); - let a = prb.new_int_var((1..=2).into()); - let b = prb.new_int_var((1..=2).into()); - let c = prb.new_int_var((1..=2).into()); - - prb += Constraint::IntLinLessEqImp( - vec![ - a.clone() * NonZeroIntVal::new(2).unwrap(), - b.clone(), - c.clone(), - ], - 5, - r.clone().into(), - ); - let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); - let a = map.get(&mut slv, &a.into()); - let b = map.get(&mut slv, &b.into()); - let c = map.get(&mut slv, &c.into()); - let r = map.get(&mut slv, &r.into()); - slv.expect_solutions( - &[r, a, b, c], - expect![[r#" - false, 1, 1, 1 - false, 1, 1, 2 - false, 1, 2, 1 - false, 1, 2, 2 - false, 2, 1, 1 - false, 2, 1, 2 - false, 2, 2, 1 - false, 2, 2, 2 - true, 1, 1, 1 - true, 1, 1, 2 - true, 1, 2, 1"#]], - ); - } -} diff --git a/crates/huub/src/constraints/int_lin_ne.rs b/crates/huub/src/constraints/int_lin_ne.rs deleted file mode 100644 index a505ed1..0000000 --- a/crates/huub/src/constraints/int_lin_ne.rs +++ /dev/null @@ -1,292 +0,0 @@ -//! Propagator for the `int_lin_ne` constraint, and its reification. This -//! constraint enforce that the sum of the products of the variables is not -//! equal to a given value. - -use pindakaas::Lit as RawLit; - -use crate::{ - actions::PropagatorInitActions, - constraints::{Conflict, ExplanationActions, PropagationActions, Propagator, ReasonBuilder}, - helpers::opt_field::OptField, - solver::{ - activation_list::IntPropCond, - queue::PriorityLevel, - trail::TrailedInt, - value::IntVal, - view::{BoolViewInner, IntView, IntViewInner}, - }, - BoolView, -}; - -/// Type alias for the reified version of the [`IntLinearNotEqValueImpl`] -/// propagator. -pub type IntLinearNotEqImpValue = IntLinearNotEqValueImpl<1>; - -/// Type alias for the non-reified version of the [`IntLinearNotEqValueImpl`] -/// propagator. -pub type IntLinearNotEqValue = IntLinearNotEqValueImpl<0>; - -#[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// Value consistent propagator for the `int_lin_ne` or `int_lin_ne_imp` -/// constraint. -/// -/// `R` should be `0` if the propagator is not refied, or `1` if it is. Other -/// values are invalid. -pub struct IntLinearNotEqValueImpl { - /// Variables in the sumation - vars: Vec, - /// The value the sumation should not equal - violation: IntVal, - /// Reified variable, if any - reification: OptField, - /// Number of variables currently fixed - num_fixed: TrailedInt, -} - -impl IntLinearNotEqImpValue { - /// Create a new [`IntLinearNotEqImpValue`] propagator and post it in the - /// solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, - vars: impl IntoIterator, - mut violation: IntVal, - reification: BoolView, - ) { - let reification = match reification.0 { - BoolViewInner::Lit(r) => r, - BoolViewInner::Const(true) => { - return IntLinearNotEqValue::new_in(solver, vars, violation) - } - BoolViewInner::Const(false) => return, - }; - - let vars: Vec = vars - .into_iter() - .filter(|v| { - if let IntViewInner::Const(c) = v.0 { - violation -= c; - false - } else { - true - } - }) - .collect(); - - let num_fixed = solver.new_trailed_int(0); - let prop = solver.add_propagator( - Box::new(Self { - vars: vars.clone(), - violation, - reification: OptField::new(reification), - num_fixed, - }), - PriorityLevel::Low, - ); - - for &v in vars.iter() { - solver.enqueue_on_int_change(prop, v, IntPropCond::Fixed); - } - solver.enqueue_on_bool_change(prop, reification.into()); - } -} - -impl IntLinearNotEqValue { - /// Create a new [`IntLinearNotEqImpValue`] propagator and post it in the - /// solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, - vars: impl IntoIterator, - mut violation: IntVal, - ) { - let vars: Vec = vars - .into_iter() - .filter(|v| { - if let IntViewInner::Const(c) = v.0 { - violation -= c; - false - } else { - true - } - }) - .collect(); - - let num_fixed = solver.new_trailed_int(0); - let prop = solver.add_propagator( - Box::new(Self { - vars: vars.clone(), - violation, - reification: Default::default(), - num_fixed, - }), - PriorityLevel::Low, - ); - - for &v in vars.iter() { - solver.enqueue_on_int_change(prop, v, IntPropCond::Fixed); - } - } -} - -impl IntLinearNotEqValueImpl { - /// Helper function to construct the reason for propagation given the index of - /// the variable in the list of variables to sum or the length of the list, if - /// explaining the reification. - fn reason(&self, data: usize) -> impl ReasonBuilder + '_ { - move |actions: &mut A| { - let mut conj: Vec<_> = self - .vars - .iter() - .enumerate() - .filter_map(|(i, v)| { - if data != i { - Some(actions.get_int_val_lit(*v).unwrap()) - } else { - None - } - }) - .collect(); - if let Some(&r) = self.reification.get() { - if data != self.vars.len() { - conj.push(r.into()); - } - } - conj - } - } -} - -impl Propagator for IntLinearNotEqValueImpl -where - P: PropagationActions, - E: ExplanationActions, -{ - #[tracing::instrument(name = "int_lin_ne", level = "trace", skip(self, actions))] - fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> { - let (r, r_fixed) = if let Some(&r) = self.reification.get() { - let r_bv = r.into(); - match actions.get_bool_val(r_bv) { - Some(false) => return Ok(()), - Some(true) => (r_bv, true), - None => (r_bv, false), - } - } else { - (true.into(), true) - }; - let mut sum = 0; - let mut unfixed = None; - for (i, v) in self.vars.iter().enumerate() { - if let Some(val) = actions.get_int_val(*v) { - sum += val; - } else if unfixed.is_some() { - return Ok(()); - } else { - unfixed = Some((i, v)); - } - } - if let Some((i, v)) = unfixed { - if !r_fixed { - return Ok(()); - } - let val = self.violation - sum; - actions.set_int_not_eq(*v, val, self.reason(i)) - } else if sum == self.violation { - actions.set_bool(!r, self.reason(self.vars.len())) - } else { - Ok(()) - } - } -} - -#[cfg(test)] -mod tests { - use expect_test::expect; - use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; - use rangelist::RangeList; - use tracing_test::traced_test; - - use crate::{ - constraints::int_lin_ne::IntLinearNotEqValue, - solver::int_var::{EncodingType, IntVar}, - Constraint, InitConfig, Model, NonZeroIntVal, Solver, - }; - - #[test] - #[traced_test] - fn test_linear_ne_sat() { - let mut slv = Solver::>::from(&Cnf::default()); - let a = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Eager, - ); - let b = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Eager, - ); - let c = IntVar::new_in( - &mut slv, - RangeList::from_iter([1..=2]), - EncodingType::Eager, - EncodingType::Eager, - ); - - IntLinearNotEqValue::new_in(&mut slv, vec![a * NonZeroIntVal::new(2).unwrap(), b, c], 6); - - slv.expect_solutions( - &[a, b, c], - expect![[r#" - 1, 1, 1 - 1, 1, 2 - 1, 2, 1 - 2, 1, 2 - 2, 2, 1 - 2, 2, 2"#]], - ); - } - - #[test] - #[traced_test] - fn test_reified_linear_ne_sat() { - let mut prb = Model::default(); - let r = prb.new_bool_var(); - let a = prb.new_int_var((1..=2).into()); - let b = prb.new_int_var((1..=2).into()); - let c = prb.new_int_var((1..=2).into()); - - prb += Constraint::IntLinNotEqImp( - vec![ - a.clone() * NonZeroIntVal::new(2).unwrap(), - b.clone(), - c.clone(), - ], - 6, - r.clone().into(), - ); - let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); - let a = map.get(&mut slv, &a.into()); - let b = map.get(&mut slv, &b.into()); - let c = map.get(&mut slv, &c.into()); - let r = map.get(&mut slv, &r.into()); - slv.expect_solutions( - &[r, a, b, c], - expect![[r#" - false, 1, 1, 1 - false, 1, 1, 2 - false, 1, 2, 1 - false, 1, 2, 2 - false, 2, 1, 1 - false, 2, 1, 2 - false, 2, 2, 1 - false, 2, 2, 2 - true, 1, 1, 1 - true, 1, 1, 2 - true, 1, 2, 1 - true, 2, 1, 2 - true, 2, 2, 1 - true, 2, 2, 2"#]], - ); - } -} diff --git a/crates/huub/src/constraints/int_linear.rs b/crates/huub/src/constraints/int_linear.rs new file mode 100644 index 0000000..88ea0d2 --- /dev/null +++ b/crates/huub/src/constraints/int_linear.rs @@ -0,0 +1,884 @@ +//! Structures and algorithms for the integer linear constraint, including +//! `int_lin_eq`, `int_lin_le`, `int_lin_ne` and their reification. These +//! constraint enforce a condition on the sum of (linear transformations of) +//! integer decision variables. + +use itertools::Itertools; +use pindakaas::Lit as RawLit; + +use crate::{ + actions::{PropagatorInitActions, ReformulationActions, SimplificationActions}, + constraints::{ + Conflict, Constraint, ExplanationActions, PropagationActions, Propagator, ReasonBuilder, + SimplificationStatus, + }, + helpers::opt_field::OptField, + model::{bool::BoolView as ModelBoolView, int::IntExpr}, + solver::{ + activation_list::IntPropCond, + queue::PriorityLevel, + value::IntVal, + view::{BoolView, BoolViewInner, IntView, IntViewInner}, + }, + Conjunction, ReformulationError, +}; + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +/// Possible operators that can be used for in a linear constraint. +pub(crate) enum LinOperator { + /// Sum is equal to the constant + Equal, + /// Sum is less than or equal to the constant + LessEq, + /// Sum is not equal to the constant + NotEqual, +} + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Representation of an integer linear constraint within a model. +/// +/// This constraint enforces that a sum of (linear transformations of) integer +/// decision variables is less than, equal, or not equal to a constant value, or +/// the implication or reification or whether this is so. +pub struct IntLinear { + /// The integer linear terms that are being summed. + pub(crate) terms: Vec, + /// The operator that is used to compare the sum to the right-hand side. + pub(crate) operator: LinOperator, + /// The constant right-hand side value. + pub(crate) rhs: IntVal, + /// Boolean decision varaible that (half-)reifies the constraint, if any. + pub(crate) reif: Option, +} + +/// Type alias for the non-reified version of the [`IntLinearLessEqBoundsImpl`] +/// propagator. +pub type IntLinearLessEqBounds = IntLinearLessEqBoundsImpl<0>; + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Value consistent propagator for the `int_lin_le` or `int_lin_le_imp` +/// constraint. +/// +/// `R` should be `0` if the propagator is not refied, or `1` if it is. Other +/// values are invalid. +pub struct IntLinearLessEqBoundsImpl { + /// Variables that are being summed + terms: Vec, + /// Maximum value of the sum can take + max: IntVal, + /// Reified variable, if any + reification: OptField, +} + +/// Type alias for the reified version of the [`IntLinearLessEqBoundsImpl`] +/// propagator. +pub type IntLinearLessEqImpBounds = IntLinearLessEqBoundsImpl<1>; + +/// Type alias for the reified version of the [`IntLinearNotEqValueImpl`] +/// propagator. +pub type IntLinearNotEqImpValue = IntLinearNotEqValueImpl<1>; + +/// Type alias for the non-reified version of the [`IntLinearNotEqValueImpl`] +/// propagator. +pub type IntLinearNotEqValue = IntLinearNotEqValueImpl<0>; + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Value consistent propagator for the `int_lin_ne` or `int_lin_ne_imp` +/// constraint. +/// +/// `R` should be `0` if the propagator is not refied, or `1` if it is. Other +/// values are invalid. +pub struct IntLinearNotEqValueImpl { + /// Variables in the sumation + terms: Vec, + /// The value the sumation should not equal + violation: IntVal, + /// Reified variable, if any + reification: OptField, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] +/// Reification possibilities for a linear constraint. +pub(crate) enum Reification { + /// The constraint is half-reified by the given [`ModelBoolView`]. + ImpliedBy(ModelBoolView), + /// The constraint is reified by the given [`ModelBoolView`]. + ReifiedBy(ModelBoolView), +} + +impl IntLinear { + /// Change the integer linear constraint to be implied by the given Boolean + /// decision variable. + /// + /// The integer linear constraint must hold when the given Boolean decision + /// variable is `true`. If the constraint does not hold, then the Boolean + /// decision variable must be `false`. + pub fn implied_by(self, b: ModelBoolView) -> Self { + assert!( + self.reif.is_none(), + "IntLinear is already implied or reified." + ); + Self { + reif: Some(Reification::ImpliedBy(b)), + ..self + } + } + + /// Change the integer linear constraint to be reified by the given Boolean + /// decision variable. + /// + /// The integer linear constraint must hold if-and-only-if the given Boolean + /// decision variable is `true`. + pub fn reified_by(self, b: ModelBoolView) -> Self { + assert!( + self.reif.is_none(), + "IntLinear is already implied or reified." + ); + Self { + reif: Some(Reification::ReifiedBy(b)), + ..self + } + } + + /// Internal method to negate the linear constraint. + fn negate(self) -> Self { + match self.operator { + LinOperator::Equal => Self { + operator: LinOperator::NotEqual, + ..self + }, + LinOperator::LessEq => Self { + terms: self.terms.into_iter().map(|v| -v).collect(), + rhs: -self.rhs, + ..self + }, + LinOperator::NotEqual => Self { + operator: LinOperator::Equal, + ..self + }, + } + } +} + +impl Constraint for IntLinear { + fn simplify(&mut self, actions: &mut S) -> Result { + // If the reification of the constriant is known, simplify to non-reified version + if let Some(Reification::ImpliedBy(r) | Reification::ReifiedBy(r)) = self.reif { + match actions.get_bool_val(r) { + Some(true) => { + let mut lin = self.clone(); + lin.reif = None; + actions.add_constraint(lin); + return Ok(SimplificationStatus::Subsumed); + } + Some(false) => { + if matches!(self.reif.unwrap(), Reification::ReifiedBy(_)) { + let mut lin = self.clone().negate(); + lin.reif = None; + actions.add_constraint(lin); + } + return Ok(SimplificationStatus::Subsumed); + } + None => {} + } + } + + // Collect variable bounds and create their sums + let lb = self + .terms + .iter() + .map(|v| actions.get_int_lower_bound(*v)) + .collect_vec(); + let ub = self + .terms + .iter() + .map(|v| actions.get_int_upper_bound(*v)) + .collect_vec(); + + let lb_sum: IntVal = lb.iter().sum(); + let ub_sum: IntVal = ub.iter().sum(); + + // Detection for not-equal constraints. Mark as subsumed, unsatisfiable, or + // stop. + if self.operator == LinOperator::NotEqual { + if self.rhs < lb_sum || self.rhs > ub_sum { + if let Some(Reification::ReifiedBy(r)) = self.reif { + actions.set_bool(r)?; + } + return Ok(SimplificationStatus::Subsumed); + } else if lb_sum == ub_sum && lb_sum == self.rhs { + if let Some(Reification::ImpliedBy(r) | Reification::ReifiedBy(r)) = self.reif { + actions.set_bool(!r)?; + return Ok(SimplificationStatus::Subsumed); + } + return Err(ReformulationError::TrivialUnsatisfiable); + } + return Ok(SimplificationStatus::Fixpoint); + } + debug_assert_ne!(self.operator, LinOperator::NotEqual); + + // Check whether LessEq constraint are already subsumed + if ub_sum < self.rhs || (self.operator == LinOperator::Equal && lb_sum > self.rhs) { + if let Some(Reification::ReifiedBy(r)) = self.reif { + actions.set_bool(if self.operator == LinOperator::LessEq { + r + } else { + !r + })?; + } + if self.operator == LinOperator::Equal { + return Err(ReformulationError::TrivialUnsatisfiable); + } + return Ok(SimplificationStatus::Subsumed); + } + + // The difference between the right-hand-side value and the sum of the lower + // bounds. The current lower bound plus this difference is an upper bound + // for each variable. + let lb_diff = self.rhs - lb_sum; + // Propagate the upper bounds of the variables + for (i, &v) in self.terms.iter().enumerate() { + let new_ub = lb_diff + lb[i]; + if let Some(Reification::ReifiedBy(r) | Reification::ImpliedBy(r)) = self.reif { + if lb[i] > new_ub { + actions.set_bool(!r)?; + return Ok(SimplificationStatus::Subsumed); + } + } else { + actions.set_int_upper_bound(v, new_ub)?; + } + } + + // For equality constriants, propagate the lower bounds of the variables + if self.operator == LinOperator::Equal { + if lb_sum == ub_sum { + assert_eq!(lb_sum, self.rhs); + return Ok(SimplificationStatus::Subsumed); + } + + // The amount the sum of the upper bounds exceeds the right-hand-side + // value (negated). Used to propagate lower bounds of each variable. + let ub_diff = self.rhs - ub_sum; + for (i, &v) in self.terms.iter().enumerate() { + let new_lb = ub_diff + ub[i]; + if let Some(Reification::ReifiedBy(r) | Reification::ImpliedBy(r)) = self.reif { + if ub[i] < new_lb { + actions.set_bool(!r)?; + return Ok(SimplificationStatus::Subsumed); + } + } else { + actions.set_int_lower_bound(v, new_lb)?; + } + } + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + use Reification::*; + + let terms = self + .terms + .iter() + .map(|&v| slv.get_solver_int(v)) + .collect_vec(); + let r = self.reif.as_ref().map(|&r| { + slv.get_solver_bool(match r { + ImpliedBy(r) | ReifiedBy(r) => r, + }) + }); + let full_reif = matches!(self.reif, Some(ReifiedBy(_))); + + match (self.operator, r) { + (LinOperator::Equal, None) => { + // coeffs * vars >= c <=> -coeffs * vars <= -c + IntLinearLessEqBounds::new_in(slv, terms.iter().map(|&v| -v), -self.rhs); + // coeffs * vars <= c + IntLinearLessEqBounds::new_in(slv, terms.clone(), self.rhs); + } + (LinOperator::Equal, Some(r)) => { + if full_reif { + IntLinearNotEqImpValue::new_in(slv, terms.clone(), self.rhs, !r); + } + IntLinearLessEqImpBounds::new_in(slv, terms.iter().map(|&v| -v), -self.rhs, r); + IntLinearLessEqImpBounds::new_in(slv, terms, self.rhs, r); + } + (LinOperator::LessEq, None) => { + IntLinearLessEqBounds::new_in(slv, terms, self.rhs); + } + (LinOperator::LessEq, Some(r)) => { + if full_reif { + IntLinearLessEqImpBounds::new_in( + slv, + terms.iter().map(|&v| -v), + -(self.rhs + 1), + !r, + ); + } + IntLinearLessEqImpBounds::new_in(slv, terms, self.rhs, r); + } + (LinOperator::NotEqual, None) => { + IntLinearNotEqValue::new_in(slv, terms, self.rhs); + } + (LinOperator::NotEqual, Some(r)) => { + if full_reif { + IntLinearLessEqImpBounds::new_in(slv, terms.clone(), self.rhs, !r); + IntLinearLessEqImpBounds::new_in(slv, terms.iter().map(|&v| -v), -self.rhs, !r); + } + IntLinearNotEqImpValue::new_in(slv, terms, self.rhs, r); + } + } + Ok(()) + } +} + +impl IntLinearLessEqBounds { + /// Create a new [`IntLinearLessEqBounds`] propagator and post it in the + /// solver. + pub fn new_in

(solver: &mut P, vars: impl IntoIterator, mut max: IntVal) + where + P: PropagatorInitActions + ?Sized, + { + let vars: Vec = vars + .into_iter() + .filter(|v| { + if let IntViewInner::Const(c) = v.0 { + max -= c; + false + } else { + true + } + }) + .collect(); + + let prop = solver.add_propagator( + Box::new(Self { + terms: vars.clone(), + max, + reification: Default::default(), + }), + PriorityLevel::Low, + ); + solver.enqueue_now(prop); + for &v in vars.iter() { + solver.enqueue_on_int_change(prop, v, IntPropCond::UpperBound); + } + } +} + +impl Propagator for IntLinearLessEqBoundsImpl +where + P: PropagationActions, + E: ExplanationActions, +{ + fn explain(&mut self, actions: &mut E, _: Option, data: u64) -> Conjunction { + let i = data as usize; + let mut var_lits: Vec = self + .terms + .iter() + .enumerate() + .filter_map(|(j, v)| { + if j == i { + return None; + } + if let BoolView(BoolViewInner::Lit(lit)) = actions.get_int_lower_bound_lit(*v) { + Some(lit) + } else { + None + } + }) + .collect(); + if let Some(r) = self.reification.get() { + var_lits.push(*r); + } + var_lits + } + // propagation rule: x[i] <= rhs - sum_{j != i} x[j].lower_bound + #[tracing::instrument(name = "int_lin_le", level = "trace", skip(self, actions))] + fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> { + // If the reified variable is false, skip propagation + if let Some(&r) = self.reification.get() { + if !actions.get_bool_val(r.into()).unwrap_or(true) { + return Ok(()); + } + } + + // get the difference between the right-hand-side value and the sum of variable lower bounds + let sum = self + .terms + .iter() + .map(|v| actions.get_int_lower_bound(*v)) + .fold(self.max, |sum, val| sum - val); + + // propagate the reified variable if the sum of lower bounds is greater than the right-hand-side value + if let Some(&r) = self.reification.get() { + if sum < 0 { + actions.set_bool((!r).into(), |a: &mut P| { + self.terms + .iter() + .map(|v| a.get_int_lower_bound_lit(*v)) + .collect_vec() + })?; + } + // skip the remaining propagation if the reified variable is not assigned to true + if !actions.get_bool_val(r.into()).unwrap_or(false) { + return Ok(()); + } + } + + // propagate the upper bound of the variables + for (j, &v) in self.terms.iter().enumerate() { + let reason = actions.deferred_reason(j as u64); + let ub = sum + actions.get_int_lower_bound(v); + actions.set_int_upper_bound(v, ub, reason)?; + } + Ok(()) + } +} + +impl IntLinearLessEqImpBounds { + /// Create a new [`IntLinearLessEqImpBounds`] propagator and post it in the + /// solver. + pub fn new_in

( + solver: &mut P, + vars: impl IntoIterator, + mut max: IntVal, + reification: BoolView, + ) where + P: PropagatorInitActions + ?Sized, + { + let reification = match reification.0 { + BoolViewInner::Lit(r) => r, + BoolViewInner::Const(true) => return IntLinearLessEqBounds::new_in(solver, vars, max), + BoolViewInner::Const(false) => return, + }; + let vars: Vec = vars + .into_iter() + .filter(|v| { + if let IntViewInner::Const(c) = v.0 { + max -= c; + false + } else { + true + } + }) + .collect(); + + let prop = solver.add_propagator( + Box::new(Self { + terms: vars.clone(), + max, + reification: OptField::new(reification), + }), + PriorityLevel::Low, + ); + solver.enqueue_now(prop); + for &v in vars.iter() { + solver.enqueue_on_int_change(prop, v, IntPropCond::UpperBound); + } + solver.enqueue_on_bool_change(prop, reification.into()); + } +} + +impl IntLinearNotEqImpValue { + /// Create a new [`IntLinearNotEqImpValue`] propagator and post it in the + /// solver. + pub fn new_in

( + solver: &mut P, + vars: impl IntoIterator, + mut violation: IntVal, + reification: BoolView, + ) where + P: PropagatorInitActions + ?Sized, + { + let reification = match reification.0 { + BoolViewInner::Lit(r) => r, + BoolViewInner::Const(true) => { + return IntLinearNotEqValue::new_in(solver, vars, violation) + } + BoolViewInner::Const(false) => return, + }; + + let vars: Vec = vars + .into_iter() + .filter(|v| { + if let IntViewInner::Const(c) = v.0 { + violation -= c; + false + } else { + true + } + }) + .collect(); + + let prop = solver.add_propagator( + Box::new(Self { + terms: vars.clone(), + violation, + reification: OptField::new(reification), + }), + PriorityLevel::Low, + ); + + for &v in vars.iter() { + solver.enqueue_on_int_change(prop, v, IntPropCond::Fixed); + } + solver.enqueue_on_bool_change(prop, reification.into()); + } +} + +impl IntLinearNotEqValue { + /// Create a new [`IntLinearNotEqImpValue`] propagator and post it in the + /// solver. + pub fn new_in

(solver: &mut P, vars: impl IntoIterator, mut violation: IntVal) + where + P: PropagatorInitActions + ?Sized, + { + let vars: Vec = vars + .into_iter() + .filter(|v| { + if let IntViewInner::Const(c) = v.0 { + violation -= c; + false + } else { + true + } + }) + .collect(); + + let prop = solver.add_propagator( + Box::new(Self { + terms: vars.clone(), + violation, + reification: Default::default(), + }), + PriorityLevel::Low, + ); + + for &v in vars.iter() { + solver.enqueue_on_int_change(prop, v, IntPropCond::Fixed); + } + } +} + +impl IntLinearNotEqValueImpl { + /// Helper function to construct the reason for propagation given the index of + /// the variable in the list of variables to sum or the length of the list, if + /// explaining the reification. + fn reason(&self, data: usize) -> impl ReasonBuilder + '_ { + move |actions: &mut A| { + let mut conj: Vec<_> = self + .terms + .iter() + .enumerate() + .filter_map(|(i, v)| { + if data != i { + Some(actions.get_int_val_lit(*v).unwrap()) + } else { + None + } + }) + .collect(); + if let Some(&r) = self.reification.get() { + if data != self.terms.len() { + conj.push(r.into()); + } + } + conj + } + } +} + +impl Propagator for IntLinearNotEqValueImpl +where + P: PropagationActions, + E: ExplanationActions, +{ + #[tracing::instrument(name = "int_lin_ne", level = "trace", skip(self, actions))] + fn propagate(&mut self, actions: &mut P) -> Result<(), Conflict> { + let (r, r_fixed) = if let Some(&r) = self.reification.get() { + let r_bv = r.into(); + match actions.get_bool_val(r_bv) { + Some(false) => return Ok(()), + Some(true) => (r_bv, true), + None => (r_bv, false), + } + } else { + (true.into(), true) + }; + let mut sum = 0; + let mut unfixed = None; + for (i, v) in self.terms.iter().enumerate() { + if let Some(val) = actions.get_int_val(*v) { + sum += val; + } else if unfixed.is_some() { + return Ok(()); + } else { + unfixed = Some((i, v)); + } + } + if let Some((i, v)) = unfixed { + if !r_fixed { + return Ok(()); + } + let val = self.violation - sum; + actions.set_int_not_eq(*v, val, self.reason(i)) + } else if sum == self.violation { + actions.set_bool(!r, self.reason(self.terms.len())) + } else { + Ok(()) + } + } +} + +#[cfg(test)] +mod tests { + use expect_test::expect; + use pindakaas::{solver::cadical::PropagatingCadical, Cnf}; + use rangelist::RangeList; + use tracing_test::traced_test; + + use crate::{ + constraints::int_linear::{IntLinearLessEqBounds, IntLinearNotEqValue}, + solver::int_var::{EncodingType, IntVar}, + InitConfig, Model, NonZeroIntVal, Solver, + }; + + #[test] + #[traced_test] + fn test_linear_ge_sat() { + let mut slv = Solver::>::from(&Cnf::default()); + let a = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Lazy, + ); + let b = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Lazy, + ); + let c = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Lazy, + ); + + IntLinearLessEqBounds::new_in( + &mut slv, + vec![a * NonZeroIntVal::new(-2).unwrap(), -b, -c], + -6, + ); + + slv.expect_solutions( + &[a, b, c], + expect![[r#" + 1, 2, 2 + 2, 1, 1 + 2, 1, 2 + 2, 2, 1 + 2, 2, 2"#]], + ); + } + + #[test] + #[traced_test] + fn test_linear_ge_unsat() { + let mut prb = Model::default(); + let a = prb.new_int_var((1..=2).into()); + let b = prb.new_int_var((1..=2).into()); + let c = prb.new_int_var((1..=2).into()); + + prb += (a * 2 + b + c).geq(10); + prb.assert_unsatisfiable(); + } + + #[test] + #[traced_test] + fn test_linear_le_sat() { + let mut slv = Solver::>::from(&Cnf::default()); + let a = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Lazy, + ); + let b = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Lazy, + ); + let c = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Lazy, + ); + + IntLinearLessEqBounds::new_in(&mut slv, vec![a * NonZeroIntVal::new(2).unwrap(), b, c], 6); + + slv.expect_solutions( + &[a, b, c], + expect![[r#" + 1, 1, 1 + 1, 1, 2 + 1, 2, 1 + 1, 2, 2 + 2, 1, 1"#]], + ); + } + + #[test] + #[traced_test] + fn test_linear_le_unsat() { + let mut prb = Model::default(); + let a = prb.new_int_var((1..=4).into()); + let b = prb.new_int_var((1..=4).into()); + let c = prb.new_int_var((1..=4).into()); + + prb += (a * 2 + b + c).leq(3); + prb.assert_unsatisfiable(); + } + + #[test] + #[traced_test] + fn test_linear_ne_sat() { + let mut slv = Solver::>::from(&Cnf::default()); + let a = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Eager, + ); + let b = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Eager, + ); + let c = IntVar::new_in( + &mut slv, + RangeList::from_iter([1..=2]), + EncodingType::Eager, + EncodingType::Eager, + ); + + IntLinearNotEqValue::new_in(&mut slv, vec![a * NonZeroIntVal::new(2).unwrap(), b, c], 6); + + slv.expect_solutions( + &[a, b, c], + expect![[r#" + 1, 1, 1 + 1, 1, 2 + 1, 2, 1 + 2, 1, 2 + 2, 2, 1 + 2, 2, 2"#]], + ); + } + + #[test] + #[traced_test] + fn test_reified_linear_ge_sat() { + let mut prb = Model::default(); + let r = prb.new_bool_var(); + let a = prb.new_int_var((1..=2).into()); + let b = prb.new_int_var((1..=2).into()); + let c = prb.new_int_var((1..=2).into()); + + prb += (a * 2 + b + c).geq(7).implied_by(r); + let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); + let a = map.get(&mut slv, &a.into()); + let b = map.get(&mut slv, &b.into()); + let c = map.get(&mut slv, &c.into()); + let r = map.get(&mut slv, &r.into()); + slv.expect_solutions( + &[r, a, b, c], + expect![[r#" + false, 1, 1, 1 + false, 1, 1, 2 + false, 1, 2, 1 + false, 1, 2, 2 + false, 2, 1, 1 + false, 2, 1, 2 + false, 2, 2, 1 + false, 2, 2, 2 + true, 2, 1, 2 + true, 2, 2, 1 + true, 2, 2, 2"#]], + ); + } + + #[test] + #[traced_test] + fn test_reified_linear_le_sat() { + let mut prb = Model::default(); + let r = prb.new_bool_var(); + let a = prb.new_int_var((1..=2).into()); + let b = prb.new_int_var((1..=2).into()); + let c = prb.new_int_var((1..=2).into()); + + prb += (a * 2 + b + c).leq(5).implied_by(r); + + let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); + let a = map.get(&mut slv, &a.into()); + let b = map.get(&mut slv, &b.into()); + let c = map.get(&mut slv, &c.into()); + let r = map.get(&mut slv, &r.into()); + slv.expect_solutions( + &[r, a, b, c], + expect![[r#" + false, 1, 1, 1 + false, 1, 1, 2 + false, 1, 2, 1 + false, 1, 2, 2 + false, 2, 1, 1 + false, 2, 1, 2 + false, 2, 2, 1 + false, 2, 2, 2 + true, 1, 1, 1 + true, 1, 1, 2 + true, 1, 2, 1"#]], + ); + } + + #[test] + #[traced_test] + fn test_reified_linear_ne_sat() { + let mut prb = Model::default(); + let r = prb.new_bool_var(); + let a = prb.new_int_var((1..=2).into()); + let b = prb.new_int_var((1..=2).into()); + let c = prb.new_int_var((1..=2).into()); + + prb += (a * 2 + b + c).ne(6).implied_by(r); + + let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); + let a = map.get(&mut slv, &a.into()); + let b = map.get(&mut slv, &b.into()); + let c = map.get(&mut slv, &c.into()); + let r = map.get(&mut slv, &r.into()); + slv.expect_solutions( + &[r, a, b, c], + expect![[r#" + false, 1, 1, 1 + false, 1, 1, 2 + false, 1, 2, 1 + false, 1, 2, 2 + false, 2, 1, 1 + false, 2, 1, 2 + false, 2, 2, 1 + false, 2, 2, 2 + true, 1, 1, 1 + true, 1, 1, 2 + true, 1, 2, 1 + true, 2, 1, 2 + true, 2, 2, 1 + true, 2, 2, 2"#]], + ); + } +} diff --git a/crates/huub/src/constraints/int_pow.rs b/crates/huub/src/constraints/int_pow.rs index bcd82d8..1823bfc 100644 --- a/crates/huub/src/constraints/int_pow.rs +++ b/crates/huub/src/constraints/int_pow.rs @@ -1,14 +1,38 @@ -//! Propagators for the `int_pow` constraint, which enforces that the result of -//! exponentiation of two integer variables is equal to a third integer -//! variable. +//! Structures and algorithms for the `int_pow` constraint, which enforces that +//! the result of exponentiation of two integer variables is equal to a third +//! integer variable. use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{CachedReason, Conflict, PropagationActions, Propagator}, + actions::{ + ExplanationActions, PropagatorInitActions, ReformulationActions, SimplificationActions, + }, + constraints::{CachedReason, Conflict, Constraint, PropagationActions, Propagator}, + model::int::IntExpr, solver::{activation_list::IntPropCond, queue::PriorityLevel}, IntVal, IntView, LitMeaning, ReformulationError, }; +use pindakaas::ClauseDatabaseTools; + +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `int_pow` constraint within a model. +/// +/// This constraint enforces that a base integer decision variable +/// exponentiated by an exponent integer decision variable is equal to a result +/// integer decision variable. +/// +/// Note that the exponentiation with negative exponents has similar behaviour +/// to integer division, including the fact the constraint will remove any +/// (semi-)division by zero. +pub struct IntPow { + /// The base in the exponentiation + pub(crate) base: IntExpr, + /// The exponent in the exponentiation + pub(crate) exponent: IntExpr, + /// The result of exponentiation + pub(crate) result: IntExpr, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Bounds propagator for the constraint `result = base^exponent`. pub struct IntPowBounds { @@ -43,14 +67,26 @@ fn pow(base: IntVal, exponent: IntVal) -> Option { }) } +impl Constraint for IntPow { + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let base = slv.get_solver_int(self.base); + let exponent = slv.get_solver_int(self.exponent); + let result = slv.get_solver_int(self.result); + IntPowBounds::new_in(slv, base, exponent, result) + } +} + impl IntPowBounds { /// Create a new [`IntPowBounds`] propagator and post it in the solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, + pub fn new_in

( + solver: &mut P, base: IntView, exponent: IntView, result: IntView, - ) -> Result<(), ReformulationError> { + ) -> Result<(), ReformulationError> + where + P: PropagatorInitActions + ?Sized, + { let prop = solver.add_propagator( Box::new(Self { base, @@ -70,7 +106,7 @@ impl IntPowBounds { let (base_lb, base_ub) = solver.get_int_bounds(base); if exp_lb < 0 || (base_lb..=base_ub).contains(&0) { // (exp < 0) -> (base != 0) - let clause = vec![ + let clause = [ solver.get_int_lit(exponent, LitMeaning::GreaterEq(0)), solver.get_int_lit(base, LitMeaning::NotEq(0)), ]; @@ -80,7 +116,7 @@ impl IntPowBounds { // Ensure that if the exponent is zero, then the result is one if (exp_lb..=exp_ub).contains(&0) { // (exp == 0) -> (res == 1) - let clause = vec![ + let clause = [ solver.get_int_lit(exponent, LitMeaning::NotEq(0)), solver.get_int_lit(result, LitMeaning::Eq(1)), ]; diff --git a/crates/huub/src/constraints/int_times.rs b/crates/huub/src/constraints/int_times.rs index c7b5781..df0b2ae 100644 --- a/crates/huub/src/constraints/int_times.rs +++ b/crates/huub/src/constraints/int_times.rs @@ -1,14 +1,34 @@ -//! Propagators for the `int_times` constraint, which enforces that the product -//! of two integer variables is equal to a third integer variable. +//! Structures and algorithms for the `int_times` constraint, which enforces +//! that the product of two integer variables is equal to a third integer +//! variable. use crate::{ - actions::{ExplanationActions, PropagatorInitActions}, - constraints::{CachedReason, Conflict, PropagationActions, Propagator}, + actions::{ + ExplanationActions, PropagatorInitActions, ReformulationActions, SimplificationActions, + }, + constraints::{ + CachedReason, Conflict, Constraint, PropagationActions, Propagator, SimplificationStatus, + }, helpers::{div_ceil, div_floor}, + model::int::IntExpr, solver::{activation_list::IntPropCond, queue::PriorityLevel}, - IntView, NonZeroIntVal, + IntView, NonZeroIntVal, ReformulationError, }; +#[derive(Clone, Debug, Eq, Hash, PartialEq)] +/// Representation of the `int_times` constraint within a model. +/// +/// This constraint enforces that the product of the two integer decision +/// variables is equal to a third. +pub struct IntTimes { + /// First factor variable + pub(crate) factor1: IntExpr, + /// Second factor variable + pub(crate) factor2: IntExpr, + /// Product variable + pub(crate) product: IntExpr, +} + #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Bounds propagator for the constraint `z = x * y`. pub struct IntTimesBounds { @@ -20,14 +40,89 @@ pub struct IntTimesBounds { product: IntView, } +impl Constraint for IntTimes { + fn simplify(&mut self, actions: &mut S) -> Result { + let (f1_lb, f1_ub) = actions.get_int_bounds(self.factor1); + let (f2_lb, f2_ub) = actions.get_int_bounds(self.factor2); + let (prd_lb, prd_ub) = actions.get_int_bounds(self.product); + + let bounds = [f1_lb * f2_lb, f1_lb * f2_ub, f1_ub * f2_lb, f1_ub * f2_ub]; + actions.set_int_lower_bound(self.product, *bounds.iter().min().unwrap())?; + actions.set_int_upper_bound(self.product, *bounds.iter().max().unwrap())?; + + if f2_lb > 0 || f2_ub < 0 { + let bounds = [ + (prd_lb, f2_lb), + (prd_lb, f2_ub), + (prd_ub, f2_lb), + (prd_ub, f2_ub), + ]; + let min = bounds + .iter() + .filter_map(|(z, y)| { + let y = NonZeroIntVal::new(*y)?; + Some(div_ceil(*z, y)) + }) + .min() + .unwrap(); + actions.set_int_lower_bound(self.factor1, min)?; + + let max = bounds + .iter() + .filter_map(|(z, y)| { + let y = NonZeroIntVal::new(*y)?; + Some(div_floor(*z, y)) + }) + .max() + .unwrap(); + actions.set_int_upper_bound(self.factor1, max)?; + } + + if f1_lb > 0 || f1_ub < 0 { + let bounds = [ + (prd_lb, f1_lb), + (prd_lb, f1_ub), + (prd_ub, f1_lb), + (prd_ub, f1_ub), + ]; + let min = bounds + .iter() + .filter_map(|(z, x)| { + let x = NonZeroIntVal::new(*x)?; + Some(div_ceil(*z, x)) + }) + .min() + .unwrap(); + actions.set_int_lower_bound(self.factor2, min)?; + + let max = bounds + .iter() + .filter_map(|(z, x)| { + let x = NonZeroIntVal::new(*x)?; + Some(div_floor(*z, x)) + }) + .max() + .unwrap(); + actions.set_int_upper_bound(self.factor2, max)?; + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let factor1 = slv.get_solver_int(self.factor1); + let factor2 = slv.get_solver_int(self.factor2); + let product = slv.get_solver_int(self.product); + IntTimesBounds::new_in(slv, factor1, factor2, product); + Ok(()) + } +} + impl IntTimesBounds { /// Create a new [`IntTimesBounds`] propagator and post it in the solver. - pub fn new_in( - solver: &mut impl PropagatorInitActions, - factor1: IntView, - factor2: IntView, - product: IntView, - ) { + pub fn new_in

(solver: &mut P, factor1: IntView, factor2: IntView, product: IntView) + where + P: PropagatorInitActions + ?Sized, + { let prop = solver.add_propagator( Box::new(Self { factor1, diff --git a/crates/huub/src/constraints/set_in_reif.rs b/crates/huub/src/constraints/set_in_reif.rs new file mode 100644 index 0000000..c161547 --- /dev/null +++ b/crates/huub/src/constraints/set_in_reif.rs @@ -0,0 +1,73 @@ +//! Structures and algorithms for the `set_in_reif` constraint, which +//! constraints that an integer decision variable is assigned to a member of a +//! given set if-and-only-if a given Boolean decision variable is assigned to +//! `true`. + +use pindakaas::propositional_logic::Formula; + +use crate::{ + actions::{ConstraintInitActions, ReformulationActions, SimplificationActions}, + constraints::{Constraint, SimplificationStatus}, + model::{bool::BoolView, int::IntExpr}, + IntSetVal, ReformulationError, +}; + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Representation of the `set_in_reif` constraint within a model. +/// +/// This constraint enforces that the given Boolean variable takes the value +/// `true` if-and-only-if an integer variable is in a given set. +pub struct SetInReif { + /// The integer decision variable monitored. + pub(crate) var: IntExpr, + /// The set of considered values for the integer decision variable. + pub(crate) set: IntSetVal, + /// The Boolean variable that indicates if the integer decision variable is in + /// the set. + pub(crate) reif: BoolView, +} + +impl Constraint for SetInReif { + fn initialize(&self, actions: &mut dyn ConstraintInitActions) { + actions.simplify_on_change_bool(self.reif); + } + + fn simplify(&mut self, actions: &mut S) -> Result { + match actions.get_bool_val(self.reif) { + Some(true) => { + actions.set_int_in_set(self.var, &self.set)?; + Ok(SimplificationStatus::Subsumed) + } + Some(false) => { + actions.set_int_not_in_set(self.var, &self.set)?; + Ok(SimplificationStatus::Subsumed) + } + None => Ok(SimplificationStatus::Fixpoint), + } + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + if self.set.iter().len() == 1 { + let lb = *self.set.lower_bound().unwrap(); + let ub = *self.set.upper_bound().unwrap(); + as Constraint>::to_solver( + &Formula::Equiv(vec![ + Formula::And(vec![self.var.geq(lb).into(), self.var.leq(ub).into()]), + self.reif.into(), + ]), + slv, + ) + } else { + let eq_lits = self + .set + .iter() + .flatten() + .map(|v| self.var.eq(v).into()) + .collect(); + as Constraint>::to_solver( + &Formula::Equiv(vec![self.reif.into(), Formula::Or(eq_lits)]), + slv, + ) + } + } +} diff --git a/crates/huub/src/constraints/table_int.rs b/crates/huub/src/constraints/table_int.rs index 3b4848e..079e316 100644 --- a/crates/huub/src/constraints/table_int.rs +++ b/crates/huub/src/constraints/table_int.rs @@ -1,78 +1,135 @@ -//! Propagation methods for the `table_int` constraint, which constraints a -//! sequence of integer decision variable to be assigned to a set of possible +//! Structures and algorithms for the `table_int` constraint, which constraints +//! a sequence of integer decision variable to be assigned to a set of possible //! sequences of integer values. use itertools::Itertools; -use pindakaas::{solver::propagation::PropagatingSolver, VarRange}; +use pindakaas::ClauseDatabaseTools; use crate::{ - actions::InspectionActions, - model::{int::IntView, reformulate::VariableMap}, - solver::engine::Engine, - BoolView, IntVal, LitMeaning, ReformulationError, Solver, + actions::{ReformulationActions, SimplificationActions}, + constraints::{Constraint, SimplificationStatus}, + model::int::IntExpr, + solver::view::BoolView, + IntVal, LitMeaning, ReformulationError, }; -/// Encode a [`Constraint::TableInt`] constraint into clauses in the solver such -/// that using clausal propagation will enforce global arc consistency. -pub(crate) fn encode_table_int_gac>( - slv: &mut Solver, - map: &mut VariableMap, - vars: &[IntView], - vals: &[Vec], -) -> Result<(), ReformulationError> { - assert!(vars.len() >= 2); - - let selector = if vars.len() != 2 { - slv.oracle.new_var_range(vals.len()) - } else { - VarRange::empty() - }; - let vars = vars.iter().map(|iv| map.get_int(slv, iv)).collect_vec(); - - // Create clauses that say foreach tuple i, if `selector[i]` is true, then the - // variable `j` equals `vals[i][j]`. - if vars.len() != 2 { - for (i, tup) in vals.iter().enumerate() { - assert!(tup.len() == vars.len()); - let lit: BoolView = selector.index(i).into(); - for (j, var) in vars.iter().enumerate() { - let clause = [!lit, slv.get_int_lit(*var, LitMeaning::Eq(tup[j]))]; - slv.add_clause(clause)?; +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Representation of the `table_int` constraint within a model. +/// +/// This constraint enforces that the given list of integer views take their +/// values according to one of the given lists of integer values. +pub struct TableInt { + /// List of variables that must take the values of a row in the table. + pub(crate) vars: Vec, + /// The table of possible values for the variables. + pub(crate) table: Vec>, +} + +impl Constraint for TableInt { + fn simplify(&mut self, actions: &mut S) -> Result { + match self.vars.len() { + 0 => return Ok(SimplificationStatus::Subsumed), + 1 => { + let dom = self.table.iter().map(|v| v[0]..=v[0]).collect(); + actions.set_int_in_set(self.vars[0], &dom)?; + return Ok(SimplificationStatus::Subsumed); } + _ => {} } - } - // Create clauses that map from the value taken by the variables back to the - // possible selectors that can be active. - for (j, var) in vars.iter().enumerate() { - let (lb, ub) = slv.get_int_bounds(*var); - let mut support_clauses: Vec> = vec![Vec::new(); (ub - lb + 1) as usize]; - for (i, tup) in vals.iter().enumerate() { - let k = tup[j] - lb; - if !(0..support_clauses.len() as IntVal).contains(&k) { - // Value is not in the domain of the variable, so this tuple should not - // be considered. - continue; + // Remove any tuples that contain values outside of the domain of the + // variables. + let table = self + .table + .iter() + .filter(|tup| { + tup.iter() + .enumerate() + .all(|(j, val)| actions.check_int_in_domain(self.vars[j], *val)) + }) + .collect_vec(); + + // If no tuples remain, then the problem is trivially unsatisfiable. + if table.is_empty() { + return Err(ReformulationError::TrivialUnsatisfiable); + } + + // Restrict the domain of the variables to the values it can take in the + // tuple. + if table.len() == 1 { + for (j, &var) in self.vars.iter().enumerate() { + actions.set_int_val(var, table[0][j])?; } - // Add tuple i to be in support of value `k`. - if vars.len() == 2 { - // Special case where we can use the values of the other variables as - // the selection variables directly. - support_clauses[k as usize] - .push(slv.get_int_lit(vars[1 - j], LitMeaning::Eq(tup[1 - j]))); - } else { - support_clauses[k as usize].push(selector.index(i).into()); + return Ok(SimplificationStatus::Subsumed); + } + + for (j, &var) in self.vars.iter().enumerate() { + let dom = (0..table.len()) + .map(|i| table[i][j]..=table[i][j]) + .collect(); + actions.set_int_in_set(var, &dom)?; + } + Ok(SimplificationStatus::Fixpoint) + } + + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + assert!(self.vars.len() >= 2); + + let selector = if self.vars.len() != 2 { + (0..self.table.len()).map(|_| slv.new_bool_var()).collect() + } else { + Vec::new() + }; + let vars = self + .vars + .iter() + .map(|&iv| slv.get_solver_int(iv)) + .collect_vec(); + + // Create clauses that say foreach tuple i, if `selector[i]` is true, then the + // variable `j` equals `vals[i][j]`. + if vars.len() != 2 { + for (i, tup) in self.table.iter().enumerate() { + assert!(tup.len() == vars.len()); + for (j, var) in vars.iter().enumerate() { + let clause = [!selector[i], slv.get_int_lit(*var, LitMeaning::Eq(tup[j]))]; + slv.add_clause(clause)?; + } } } - for (i, mut clause) in support_clauses.into_iter().enumerate() { - if slv.check_int_in_domain(*var, lb + i as IntVal) { - clause.push(slv.get_int_lit(vars[j], LitMeaning::NotEq(lb + i as IntVal))); - slv.add_clause(clause)?; + + // Create clauses that map from the value taken by the variables back to the + // possible selectors that can be active. + for (j, var) in vars.iter().enumerate() { + let (lb, ub) = slv.get_int_bounds(*var); + let mut support_clauses: Vec> = vec![Vec::new(); (ub - lb + 1) as usize]; + for (i, tup) in self.table.iter().enumerate() { + let k = tup[j] - lb; + if !(0..support_clauses.len() as IntVal).contains(&k) { + // Value is not in the domain of the variable, so this tuple should not + // be considered. + continue; + } + // Add tuple i to be in support of value `k`. + if vars.len() == 2 { + // Special case where we can use the values of the other variables as + // the selection variables directly. + support_clauses[k as usize] + .push(slv.get_int_lit(vars[1 - j], LitMeaning::Eq(tup[1 - j]))); + } else { + support_clauses[k as usize].push(selector[i]); + } + } + for (i, mut clause) in support_clauses.into_iter().enumerate() { + if slv.check_int_in_domain(*var, lb + i as IntVal) { + clause.push(slv.get_int_lit(vars[j], LitMeaning::NotEq(lb + i as IntVal))); + slv.add_clause(clause)?; + } } } - } - Ok(()) + Ok(()) + } } #[cfg(test)] @@ -80,7 +137,7 @@ mod tests { use expect_test::expect; use itertools::Itertools; - use crate::{model::ModelView, Constraint, InitConfig, Model}; + use crate::{model::reformulate::ModelView, table_int, InitConfig, Model}; #[test] fn test_binary_table_sat() { @@ -98,8 +155,8 @@ mod tests { vec![5, 2], vec![5, 3], ]; - prb += Constraint::TableInt(vec![vars[0].into(), vars[1].into()], table.clone()); - prb += Constraint::TableInt(vec![vars[1].into(), vars[2].into()], table.clone()); + prb += table_int(vec![vars[0].into(), vars[1].into()], table.clone()); + prb += table_int(vec![vars[1].into(), vars[2].into()], table.clone()); let (mut slv, map) = prb.to_solver(&InitConfig::default()).unwrap(); let vars = vars @@ -146,12 +203,12 @@ mod tests { vec![5, 3, 1], vec![5, 3, 5], ]; - prb += Constraint::TableInt( - vars[0..3].iter().cloned().map_into().collect_vec(), + prb += table_int( + vars[0..3].iter().cloned().map_into().collect(), table.clone(), ); - prb += Constraint::TableInt( - vars[2..5].iter().cloned().map_into().collect_vec(), + prb += table_int( + vars[2..5].iter().cloned().map_into().collect(), table.clone(), ); diff --git a/crates/huub/src/helpers/linear_transform.rs b/crates/huub/src/helpers/linear_transform.rs index 021ee67..6e77a97 100644 --- a/crates/huub/src/helpers/linear_transform.rs +++ b/crates/huub/src/helpers/linear_transform.rs @@ -17,6 +17,11 @@ pub struct LinearTransform { } impl LinearTransform { + /// Check whether the linear transformation is an identity transformation. + pub(crate) fn is_identity(&self) -> bool { + self.scale.get() == 1 && self.offset == 0 + } + /// Creates a new linear transformation with the given scale and offset. pub fn new(scale: NonZeroIntVal, offset: IntVal) -> Self { Self { scale, offset } diff --git a/crates/huub/src/lib.rs b/crates/huub/src/lib.rs index af8e481..06f9536 100644 --- a/crates/huub/src/lib.rs +++ b/crates/huub/src/lib.rs @@ -18,21 +18,66 @@ pub(crate) mod solver; #[cfg(test)] pub(crate) mod tests; -pub use helpers::linear_transform::LinearTransform; -pub use model::{ - bool::BoolExpr, - constraint::Constraint, - flatzinc::{FlatZincError, FlatZincStatistics}, - reformulate::{InitConfig, ReformulationError}, - Model, +use std::{ + any::Any, + collections::{HashSet, VecDeque}, + iter::{repeat, Sum}, + ops::{Add, AddAssign, Mul, Sub}, }; + +use index_vec::IndexVec; +use itertools::Itertools; pub use pindakaas::solver::SlvTermSignal; -use pindakaas::Lit as RawLit; -pub use solver::{ - int_var::LitMeaning, - value::{IntSetVal, IntVal, NonZeroIntVal, Valuation, Value}, - view::{BoolView, IntView, SolverView}, - Goal, SolveResult, Solver, +use pindakaas::{ + propositional_logic::Formula, + solver::{cadical::Cadical, propagation::PropagatingSolver}, + ClauseDatabase, ClauseDatabaseTools, Cnf, Lit as RawLit, Unsatisfiable, +}; +use rangelist::IntervalIterator; +use tracing::warn; + +// TODO: Remove this re-export +pub(crate) use crate::model::constraint::ConstraintStore; +use crate::{ + constraints::{ + all_different_int::AllDifferentInt, + array_int_element::ArrayIntElement, + array_int_minimum::ArrayIntMinimum, + array_var_bool_element::ArrayVarBoolElement, + array_var_int_element::ArrayVarIntElement, + disjunctive_strict::DisjunctiveStrict, + int_abs::IntAbs, + int_div::IntDiv, + int_linear::{IntLinear, LinOperator}, + int_pow::IntPow, + int_times::IntTimes, + set_in_reif::SetInReif, + table_int::TableInt, + BoxedConstraint, + }, + model::{ + bool::BoolView as ModelBoolView, + branching::Branching, + int::{IntExpr, IntVar, IntVarDef}, + reformulate::VariableMap, + }, + solver::{ + engine::Engine, + int_var::{EncodingType, IntVar as SlvIntVar}, + }, +}; +pub use crate::{ + helpers::linear_transform::LinearTransform, + model::{ + flatzinc::{FlatZincError, FlatZincStatistics}, + reformulate::{InitConfig, ReformulationError}, + }, + solver::{ + int_var::LitMeaning, + value::{IntSetVal, IntVal, NonZeroIntVal, Valuation, Value}, + view::{IntView, SolverView}, + Goal, SolveResult, Solver, + }, }; /// Type alias for a disjunction of literals (clause), used for internal type @@ -42,3 +87,557 @@ type Clause = Vec; /// Type alias for a conjunction of literals (clause), used for internal type /// documentation. type Conjunction = Vec; + +#[derive(Debug, Clone, PartialEq, Eq, Hash)] +/// Object to help with the creation of integer linear constriants. +/// +/// This object is generally created when [`IntExpr`] objects are added +/// together. Calling methods like [`Self::less_than`] or [`Self::equal_to`] +/// will create a [`IntLinear`] constriant object that can be added to a +/// [`Model`] object. +pub struct IntLinExpr { + /// The (linear transformation of) integer decision variables that are added + /// together. + terms: Vec, +} + +#[derive(Clone, Debug, Default)] +/// A formulation of a problem instance in terms of decisions and constraints. +pub struct Model { + /// A base [`Cnf`] object that contains pure Boolean parts of the problem. + pub(crate) cnf: Cnf, + /// An list of branching strategies that will be used by created [`Solver`] + /// instances to be used in order to make search decisions. + branchings: Vec, + /// A list of constraints that have been added to the model. + constraints: Vec>, + /// The definitions of the integer variables that have been created. + int_vars: IndexVec, + /// A queue of indexes of constraints that need to be propagated. + prop_queue: VecDeque, + /// A flag for each constraint whether it has been enqueued for propagation. + enqueued: Vec, +} + +/// Create a `all_different_int` constraint that enforces that all the given +/// integer decisions take different values. +pub fn all_different_int(vars: Iter) -> AllDifferentInt +where + Iter: IntoIterator, + Iter::Item: Into, +{ + AllDifferentInt { + vars: vars.into_iter().map_into().collect(), + } +} + +/// Create an `array_int_element` constraint that enforces that a result integer +/// decision variable takes the value equal the element of the given array of +/// integer values at the given index decision variable. +pub fn array_int_element(index: IntExpr, array: Vec, result: IntExpr) -> ArrayIntElement { + ArrayIntElement { + index, + array, + result, + } +} + +/// Create an `array_int_maximum` constraint that enforces that an integer +/// decision variable takes the minimum value of an array of integer decision +/// variables. +pub fn array_int_maximum(vars: Iter, max: IntExpr) -> ArrayIntMinimum +where + Iter: IntoIterator, + Iter::Item: Into, +{ + array_int_minimum(vars.into_iter().map(|v| -v.into()), -max) +} + +/// Create an `array_int_minimum` constraint that enforces that an integer +/// decision variable takes the minimum value of an array of integer decision +/// variables. +pub fn array_int_minimum(vars: Iter, min: IntExpr) -> ArrayIntMinimum +where + Iter: IntoIterator, + Iter::Item: Into, +{ + ArrayIntMinimum { + vars: vars.into_iter().map_into().collect(), + min, + } +} + +/// Create an `array_var_bool_element` constraint that enforces that a result +/// Boolean decision variable takes the value equal the element of the given +/// array of Boolean decision varaibles at the index given by the index integer +/// decision variable. +pub fn array_var_bool_element( + index: IntExpr, + array: Vec, + result: ModelBoolView, +) -> ArrayVarBoolElement { + ArrayVarBoolElement { + index, + array, + result, + } +} + +/// Create a `disjunctive_strict` constraint that enforces that the given a list +/// of integer decision variables representing the start times of tasks and a +/// list of integer values representing the durations of tasks, the tasks do not +/// overlap in time. +pub fn disjunctive_strict(start_times: Vec, durations: Vec) -> DisjunctiveStrict { + assert_eq!( + start_times.len(), + durations.len(), + "disjunctive_strict must be given the same number of start times and durations." + ); + assert!( + durations.iter().all(|&dur| dur >= 0), + "disjunctive_strict cannot be given any negative durations." + ); + DisjunctiveStrict { + start_times, + durations, + } +} + +/// Create an `array_var_int_element` constraint that enforces that a result +/// integer decision variable takes the value equal the element of the given +/// array of integer decision variable at the given index decision variable. +pub fn array_var_int_element( + index: IntExpr, + array: Vec, + result: IntExpr, +) -> ArrayVarIntElement { + ArrayVarIntElement { + index, + array, + result, + } +} + +/// Create an `int_abs` constraint that enforces that the second integer +/// decision variable takes the absolute value of the first integer decision +/// variable. +pub fn int_abs(origin: IntExpr, abs: IntExpr) -> IntAbs { + IntAbs { origin, abs } +} + +/// Create an `int_div` constraint that enforces that a numerator decision +/// integer variable divided by a denominator integer decision variable is equal +/// to a result integer decision variable. +pub fn int_div(numerator: IntExpr, denominator: IntExpr, result: IntExpr) -> IntDiv { + IntDiv { + numerator, + denominator, + result, + } +} + +/// Create an `int_pow` constraint that enforces that a base integer decision +/// variable exponentiated by an exponent integer decision variable is equal to +/// a result integer decision variable. +pub fn int_pow(base: IntExpr, exponent: IntExpr, result: IntExpr) -> IntPow { + IntPow { + base, + exponent, + result, + } +} + +/// Create an `int_times` constraint that enforces that the product of the two +/// integer decision variables is equal to a third. +pub fn int_times(factor1: IntExpr, factor2: IntExpr, product: IntExpr) -> IntTimes { + IntTimes { + factor1, + factor2, + product, + } +} + +/// Create a `set_in_reif` constraint that enforces that the given Boolean +/// variable takes the value `true` if-and-only-if an integer variable is in a +/// given set. +pub fn set_in_reif(var: IntExpr, set: IntSetVal, reif: ModelBoolView) -> SetInReif { + SetInReif { var, set, reif } +} + +/// Create a `table_int` constraint that enforces that given list of integer +/// views take their values according to one of the given lists of integer +/// values. +pub fn table_int(vars: Vec, table: Vec>) -> TableInt { + assert!(table.iter().all(|tup| tup.len() == vars.len()), "The number of values in each row of the table must be equal to the number of decision variables."); + TableInt { vars, table } +} + +impl IntLinExpr { + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is less than or equal to the given value. + pub fn lt(self, rhs: IntVal) -> IntLinear { + self.leq(rhs - 1) + } + + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is less than the given value. + pub fn leq(self, rhs: IntVal) -> IntLinear { + IntLinear { + terms: self.terms, + operator: LinOperator::LessEq, + rhs, + reif: None, + } + } + + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is equal to the given value. + pub fn eq(self, rhs: IntVal) -> IntLinear { + IntLinear { + terms: self.terms, + operator: LinOperator::Equal, + rhs, + reif: None, + } + } + + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is greater than or equal to the given value. + pub fn geq(mut self, rhs: IntVal) -> IntLinear { + self.terms = self.terms.into_iter().map(|x| -x).collect(); + self.leq(-rhs) + } + + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is greater than the given value. + pub fn gt(self, rhs: IntVal) -> IntLinear { + self.geq(rhs + 1) + } + /// Create a new integer linear constraint that enforces that the sum of the + /// expressions in the object is not equal to the given value. + pub fn ne(self, rhs: IntVal) -> IntLinear { + IntLinear { + terms: self.terms, + operator: LinOperator::NotEqual, + rhs, + reif: None, + } + } +} + +impl Add for IntLinExpr { + type Output = IntLinExpr; + + fn add(self, rhs: IntExpr) -> Self::Output { + let mut terms = self.terms; + terms.push(rhs); + IntLinExpr { terms } + } +} + +impl Add for IntLinExpr { + type Output = IntLinExpr; + + fn add(mut self, rhs: IntVal) -> Self::Output { + self.terms[0] = self.terms[0] + rhs; + self + } +} + +impl Mul for IntLinExpr { + type Output = IntLinExpr; + + fn mul(self, rhs: IntVal) -> Self::Output { + IntLinExpr { + terms: self.terms.into_iter().map(|x| x * rhs).collect(), + } + } +} + +impl Sub for IntLinExpr { + type Output = IntLinExpr; + + fn sub(self, rhs: IntExpr) -> Self::Output { + self + -rhs + } +} + +impl Sub for IntLinExpr { + type Output = IntLinExpr; + + fn sub(self, rhs: IntVal) -> Self::Output { + self + -rhs + } +} + +impl Sum for IntLinExpr { + fn sum>(iter: I) -> Self { + IntLinExpr { + terms: iter.collect(), + } + } +} + +impl Model { + /// Internal method to add a constraint to the model. + /// + /// Note that users will use either the `+=` operator or the + /// [`Self::add_custom_constraint`] method. + fn add_constraint(&mut self, constraint: ConstraintStore) { + self.constraints.push(Some(constraint)); + self.enqueued.push(false); + self.enqueue(self.constraints.len() - 1); + self.subscribe(self.constraints.len() - 1); + } + + /// Add a custom constraint to the model. + pub fn add_custom_constraint(&mut self, _: IntVal) { + todo!() + } + + /// Enqueue constraint that has index `constraint` to the propagation queue. + fn enqueue(&mut self, constraint: usize) { + if !self.enqueued[constraint] { + self.prop_queue.push_back(constraint); + self.enqueued[constraint] = true; + } + } + + /// Create a new Boolean variable. + pub fn new_bool_var(&mut self) -> ModelBoolView { + ModelBoolView::Lit(self.cnf.new_lit()) + } + + /// Create `len` new Boolean variables. + pub fn new_bool_vars(&mut self, len: usize) -> Vec { + self.cnf + .new_var_range(len) + .map(|v| ModelBoolView::Lit(v.into())) + .collect() + } + + /// Create a new integer variable with the given domain. + pub fn new_int_var(&mut self, domain: IntSetVal) -> IntExpr { + IntExpr::Var(self.int_vars.push(IntVarDef::with_domain(domain))) + } + + /// Create `len` new integer variables with the given domain. + pub fn new_int_vars(&mut self, len: usize, domain: IntSetVal) -> Vec { + repeat(IntVarDef::with_domain(domain)) + .take(len) + .map(|v| self.int_vars.push(v)) + .collect() + } + + /// Process the model to create a [`Solver`] instance that can be used to + /// solve it. + /// + /// This method will return a [`Solver`] instance in addition to a + /// [`VariableMap`], which can be used to map from [`ModelView`] + /// to [`crate::SolverView`]. If an error occurs during the reformulation + /// process, or if it is found to be trivially unsatisfiable, then an error + /// will be returned. + pub fn to_solver>( + &mut self, + config: &InitConfig, + ) -> Result<(Solver, VariableMap), ReformulationError> + where + Solver: for<'a> From<&'a Cnf>, + Oracle::Slv: 'static, + { + let mut map = VariableMap::default(); + + // TODO: run SAT simplification + let mut slv = Solver::::from(&self.cnf); + let any_slv: &mut dyn Any = slv.oracle.solver_mut(); + if let Some(r) = any_slv.downcast_mut::() { + r.set_option("restart", config.restart() as i32); + r.set_option("vivify", config.vivification() as i32); + } else { + warn!("unknown solver: vivification and restart options are ignored"); + } + + while let Some(con) = self.prop_queue.pop_front() { + self.propagate(con)?; + self.enqueued[con] = false; + } + + // TODO: Detect Views From Model + + // Determine encoding types for integer variables + let eager_order = HashSet::::new(); + let mut eager_direct = HashSet::::new(); + + for c in self.constraints.iter().flatten() { + match c { + ConstraintStore::AllDifferentInt(c) => { + for v in &c.vars { + if let IntExpr::Var(iv) | IntExpr::Linear(_, iv) = v { + if self.int_vars[*iv].domain.card() <= (c.vars.len() * 100 / 80) { + let _ = eager_direct.insert(*iv); + } + } + } + } + ConstraintStore::ArrayIntElement(c) => { + if let IntExpr::Var(iv) | IntExpr::Linear(_, iv) = c.index { + let _ = eager_direct.insert(iv); + } + } + ConstraintStore::ArrayVarBoolElement(c) => { + if let IntExpr::Var(iv) | IntExpr::Linear(_, iv) = c.index { + let _ = eager_direct.insert(iv); + } + } + ConstraintStore::ArrayVarIntElement(c) => { + if let IntExpr::Var(iv) | IntExpr::Linear(_, iv) = c.index { + let _ = eager_direct.insert(iv); + } + } + ConstraintStore::TableInt(con) => { + for &v in &con.vars { + if let IntExpr::Var(iv) | IntExpr::Linear(_, iv) = v { + let _ = eager_direct.insert(iv); + } + } + } + _ => {} + } + } + + // Create integer data structures within the solver + for (i, var) in self.int_vars.iter_enumerated() { + let direct_enc = if eager_direct.contains(&i) { + EncodingType::Eager + } else { + EncodingType::Lazy + }; + let order_enc = if eager_order.contains(&i) + || eager_direct.contains(&i) + || var.domain.card() <= config.int_eager_limit() + { + EncodingType::Eager + } else { + EncodingType::Lazy + }; + let view = SlvIntVar::new_in(&mut slv, var.domain.clone(), order_enc, direct_enc); + map.insert_int(i, view); + } + + // Create constraint data structures within the solver + for c in self.constraints.iter().flatten() { + c.to_solver(&mut slv, &mut map)?; + } + // Add branching data structures to the solver + for b in self.branchings.iter() { + b.to_solver(&mut slv, &mut map); + } + + Ok((slv, map)) + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: AllDifferentInt) { + self.add_constraint(ConstraintStore::AllDifferentInt(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: ArrayIntElement) { + self.add_constraint(ConstraintStore::ArrayIntElement(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: ArrayIntMinimum) { + self.add_constraint(ConstraintStore::ArrayIntMinimum(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: ArrayVarBoolElement) { + self.add_constraint(ConstraintStore::ArrayVarBoolElement(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: ArrayVarIntElement) { + self.add_constraint(ConstraintStore::ArrayVarIntElement(constraint)); + } +} + +impl AddAssign> for Model { + fn add_assign(&mut self, constraint: Formula) { + self.add_constraint(ConstraintStore::PropLogic(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, rhs: Branching) { + self.branchings.push(rhs); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: BoxedConstraint) { + self.add_constraint(ConstraintStore::UserCustom(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: DisjunctiveStrict) { + self.add_constraint(ConstraintStore::DisjunctiveStrict(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntAbs) { + self.add_constraint(ConstraintStore::IntAbs(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntDiv) { + self.add_constraint(ConstraintStore::IntDiv(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntLinear) { + self.add_constraint(ConstraintStore::IntLinear(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntPow) { + self.add_constraint(ConstraintStore::IntPow(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: IntTimes) { + self.add_constraint(ConstraintStore::IntTimes(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: SetInReif) { + self.add_constraint(ConstraintStore::SetInReif(constraint)); + } +} + +impl AddAssign for Model { + fn add_assign(&mut self, constraint: TableInt) { + self.add_constraint(ConstraintStore::TableInt(constraint)); + } +} + +impl ClauseDatabase for Model { + fn add_clause_from_slice(&mut self, clause: &[RawLit]) -> Result<(), Unsatisfiable> { + self.cnf.add_clause_from_slice(clause) + } + fn new_var_range(&mut self, len: usize) -> pindakaas::VarRange { + self.cnf.new_var_range(len) + } +} diff --git a/crates/huub/src/model.rs b/crates/huub/src/model.rs index 0bb97b5..b4f462b 100644 --- a/crates/huub/src/model.rs +++ b/crates/huub/src/model.rs @@ -7,241 +7,3 @@ pub(crate) mod constraint; pub(crate) mod flatzinc; pub(crate) mod int; pub(crate) mod reformulate; - -use std::{ - any::Any, - collections::{HashSet, VecDeque}, - iter::repeat, - ops::AddAssign, -}; - -use pindakaas::{ - solver::{cadical::Cadical, propagation::PropagatingSolver}, - ClauseDatabase, Cnf, ConditionalDatabase, Lit as RawLit, Unsatisfiable, -}; -use rangelist::{IntervalIterator, RangeList}; -use tracing::warn; - -use crate::{ - model::{ - bool::{BoolExpr, BoolView}, - branching::Branching, - int::{IntVar, IntVarDef, IntView}, - reformulate::{InitConfig, ReformulationError, VariableMap}, - }, - solver::{ - engine::Engine, - int_var::{EncodingType, IntVar as SlvIntVar}, - }, - Constraint, Solver, -}; - -#[derive(Debug, Default)] -/// A formulation of a problem instance in terms of decisions and constraints. -pub struct Model { - /// A base [`Cnf`] object that contains pure Boolean parts of the problem. - pub(crate) cnf: Cnf, - /// An list of branching strategies that will be used by created [`Solver`] - /// instances to be used in order to make search decisions. - branchings: Vec, - /// A list of constraints that have been added to the model. - constraints: Vec, - /// The definitions of the integer variables that have been created. - int_vars: Vec, - /// A queue of indexes of constraints that need to be propagated. - prop_queue: VecDeque, - /// A flag for each constraint whether it has been enqueued for propagation. - enqueued: Vec, -} - -#[derive(Clone, Debug, PartialEq, Eq, Hash)] -/// Reference to a decision in a [`Model`]. -pub enum ModelView { - /// Reference to a Boolean decision. - Bool(BoolView), - /// Reference to an integer decision. - Int(IntView), -} - -impl Model { - /// Enqueue constraint that has index `constraint` to the propagation queue. - fn enqueue(&mut self, constraint: usize) { - if !self.enqueued[constraint] { - self.prop_queue.push_back(constraint); - self.enqueued[constraint] = true; - } - } - - /// Create a new Boolean variable. - pub fn new_bool_var(&mut self) -> BoolView { - BoolView::Lit(self.cnf.new_lit()) - } - - /// Create `len` new Boolean variables. - pub fn new_bool_vars(&mut self, len: usize) -> Vec { - self.cnf - .new_var_range(len) - .map(|v| BoolView::Lit(v.into())) - .collect() - } - - /// Create a new integer variable with the given domain. - pub fn new_int_var(&mut self, domain: RangeList) -> IntView { - let iv = IntVar(self.int_vars.len() as u32); - self.int_vars.push(IntVarDef::with_domain(domain)); - IntView::Var(iv) - } - - /// Create `len` new integer variables with the given domain. - pub fn new_int_vars(&mut self, len: usize, domain: RangeList) -> Vec { - let iv = IntVar(self.int_vars.len() as u32); - self.int_vars - .extend(repeat(IntVarDef::with_domain(domain)).take(len)); - (0..len).map(|i| IntVar(iv.0 + i as u32)).collect() - } - - /// Process the model to create a [`Solver`] instance that can be used to - /// solve it. - /// - /// This method will return a [`Solver`] instance in addition to a - /// [`VariableMap`], which can be used to map from [`ModelView`] - /// to [`crate::SolverView`]. If an error occurs during the reformulation - /// process, or if it is found to be trivially unsatisfiable, then an error - /// will be returned. - pub fn to_solver>( - &mut self, - config: &InitConfig, - ) -> Result<(Solver, VariableMap), ReformulationError> - where - Solver: for<'a> From<&'a Cnf>, - Oracle::Slv: 'static, - { - let mut map = VariableMap::default(); - - // TODO: run SAT simplification - let mut slv = Solver::::from(&self.cnf); - let any_slv: &mut dyn Any = slv.oracle.solver_mut(); - if let Some(r) = any_slv.downcast_mut::() { - r.set_option("restart", config.restart() as i32); - r.set_option("vivify", config.vivification() as i32); - } else { - warn!("unknown solver: vivification and restart options are ignored"); - } - - while let Some(con) = self.prop_queue.pop_front() { - self.propagate(con)?; - self.enqueued[con] = false; - } - - // TODO: Detect Views From Model - - // Determine encoding types for integer variables - let eager_order = HashSet::::new(); - let mut eager_direct = HashSet::::new(); - - for c in &self.constraints { - match c { - Constraint::AllDifferentInt(vars) => { - for v in vars { - if let IntView::Var(iv) | IntView::Linear(_, iv) = v { - if self.int_vars[iv.0 as usize].domain.card() <= (vars.len() * 100 / 80) - { - let _ = eager_direct.insert(*iv); - } - } - } - } - Constraint::ArrayVarIntElement(_, IntView::Var(iv) | IntView::Linear(_, iv), _) => { - let _ = eager_direct.insert(*iv); - } - Constraint::TableInt(vars, _) => { - for v in vars { - if let IntView::Var(iv) | IntView::Linear(_, iv) = v { - let _ = eager_direct.insert(*iv); - } - } - } - _ => {} - } - } - - // Create integer data structures within the solver - for i in 0..self.int_vars.len() { - let var = &self.int_vars[i]; - let direct_enc = if eager_direct.contains(&IntVar(i as u32)) { - EncodingType::Eager - } else { - EncodingType::Lazy - }; - let order_enc = if eager_order.contains(&IntVar(i as u32)) - || eager_direct.contains(&IntVar(i as u32)) - || var.domain.card() <= config.int_eager_limit() - { - EncodingType::Eager - } else { - EncodingType::Lazy - }; - let view = SlvIntVar::new_in(&mut slv, var.domain.clone(), order_enc, direct_enc); - map.insert_int(IntVar(i as u32), view); - } - - // Create constraint data structures within the solver - for c in self.constraints.iter() { - c.to_solver(&mut slv, &mut map)?; - } - // Add branching data structures to the solver - for b in self.branchings.iter() { - b.to_solver(&mut slv, &mut map); - } - - Ok((slv, map)) - } -} -impl AddAssign for Model { - fn add_assign(&mut self, rhs: BoolExpr) { - self.add_assign(Constraint::PropLogic(rhs)); - } -} - -impl AddAssign for Model { - fn add_assign(&mut self, rhs: Branching) { - self.branchings.push(rhs); - } -} - -impl AddAssign for Model { - fn add_assign(&mut self, rhs: Constraint) { - self.constraints.push(rhs); - self.enqueued.push(false); - self.enqueue(self.constraints.len() - 1); - self.subscribe(self.constraints.len() - 1); - } -} - -impl ClauseDatabase for Model { - type CondDB = Model; - - fn add_clause>(&mut self, cl: I) -> Result<(), Unsatisfiable> { - self.cnf.add_clause(cl) - } - - fn new_var_range(&mut self, len: usize) -> pindakaas::VarRange { - self.cnf.new_var_range(len) - } - - fn with_conditions(&mut self, conditions: Vec) -> ConditionalDatabase { - ConditionalDatabase::new(self, conditions) - } -} - -impl From for ModelView { - fn from(value: BoolView) -> Self { - Self::Bool(value) - } -} - -impl From for ModelView { - fn from(value: IntView) -> Self { - Self::Int(value) - } -} diff --git a/crates/huub/src/model/bool.rs b/crates/huub/src/model/bool.rs index b28f5a8..0d92480 100644 --- a/crates/huub/src/model/bool.rs +++ b/crates/huub/src/model/bool.rs @@ -1,57 +1,22 @@ //! Representation and manipulation of Boolean decision variable and expressions //! in [`Model`]. -use std::{iter::once, ops::Not}; +use std::ops::Not; use pindakaas::{ propositional_logic::{Formula, TseitinEncoder}, - solver::propagation::PropagatingSolver, - Lit as RawLit, + ClauseDatabaseTools, Encoder, Lit as RawLit, }; use crate::{ - model::{ - int, - reformulate::{ReformulationError, VariableMap}, - }, - solver::{ - engine::Engine, - view::{self, BoolViewInner}, - }, - IntVal, Solver, + actions::{ReformulationActions, SimplificationActions}, + constraints::{Constraint, SimplificationStatus}, + model::{int::IntVar, reformulate::ReformulationError}, + solver::view::BoolViewInner, + IntVal, }; -#[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// A propositional logic formula that can be used as part of a [`crate::Constraint`] -/// in a [`crate::Model`]. -pub enum BoolExpr { - /// Direct Boolean view - View(BoolView), - /// Logical negation of a Boolean expression. - Not(Box), - /// Disjunction of a list of Boolean expressions. - Or(Vec), - /// Conjunction of a list of Boolean expressions. - And(Vec), - /// Logical implication of the first Boolean expression to the second. - Implies(Box, Box), - /// Logical equivalence of a list of Boolean expressions. - Equiv(Vec), - /// Exclusive disjunction of a list of Boolean expressions. - Xor(Vec), - /// If-then-else expression: if the condition holds, then the `then` - /// expression must also hold, otherwise the `els` expression must hold. - IfThenElse { - /// Condition expression, choosing between the `then` and `els`. - cond: Box, - /// Expression that must hold if the condition holds. - then: Box, - /// Expression that must hold if the condition does not hold. - els: Box, - }, -} - -#[derive(Clone, Debug, PartialEq, Eq, Hash)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] #[allow( variant_size_differences, reason = "`bool` is smaller than all other variants" @@ -64,390 +29,43 @@ pub enum BoolView { /// A constant Boolean value. Const(bool), /// Wether an integer is equal to a constant. - IntEq(Box, IntVal), - /// Wether an integer is greater than a constant. - IntGreater(Box, IntVal), + IntEq(IntVar, IntVal), /// Wether an integer is greater or equal to a constant. - IntGreaterEq(Box, IntVal), + IntGreaterEq(IntVar, IntVal), /// Wether an integer is less than a constant. - IntLess(Box, IntVal), - /// Wether an integer is less or equal to a constant. - IntLessEq(Box, IntVal), + IntLess(IntVar, IntVal), /// Wether an integer is not equal to a constant. - IntNotEq(Box, IntVal), + IntNotEq(IntVar, IntVal), } -impl BoolExpr { - /// Add clauses to the solver to enforce the Boolean expression. - pub(crate) fn constrain>( - &self, - slv: &mut Solver, - map: &mut VariableMap, - ) -> Result<(), ReformulationError> { - match self { - BoolExpr::View(bv) => { - let v = map.get_bool(slv, bv); - slv.add_clause([v]) - } - BoolExpr::Not(x) => { - if let Some(y) = x.push_not_inward() { - y.constrain(slv, map) - } else { - let r = x.to_arg(slv, map, None)?; - slv.add_clause([!r]) - } - } - BoolExpr::Or(es) => { - let mut lits = Vec::with_capacity(es.len()); - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(false) => {} - BoolViewInner::Const(true) => return Ok(()), - BoolViewInner::Lit(l) => lits.push(l), - } - } - slv.oracle - .add_clause(lits) - .map_err(|_| ReformulationError::TrivialUnsatisfiable) - } - BoolExpr::And(es) => { - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(false) => { - return Err(ReformulationError::TrivialUnsatisfiable) - } - BoolViewInner::Const(true) => {} - BoolViewInner::Lit(l) => slv - .oracle - .add_clause([l]) - .map_err(|_| ReformulationError::TrivialUnsatisfiable)?, - } - } - Ok(()) - } - BoolExpr::Implies(a, b) => { - let a = match a.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => { - return b.constrain(slv, map); - } - BoolViewInner::Const(false) => { - return Ok(()); - } - BoolViewInner::Lit(l) => l, - }; - - // TODO: Conditional Compilation - match b.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => Ok(()), - BoolViewInner::Const(false) => slv - .oracle - .add_clause([!a]) - .map_err(|_| ReformulationError::TrivialUnsatisfiable), - BoolViewInner::Lit(b) => slv - .oracle - .add_clause([!a, b]) - .map_err(|_| ReformulationError::TrivialUnsatisfiable), - } - } - BoolExpr::Equiv(es) => { - // Try and find some constant or literal to start binding to - let mut res = es.iter().find_map(|e| { - if let BoolExpr::View(b) = e { - Some(map.get_bool(slv, b)) - } else { - None - } - }); - for e in es { - match res { - Some(view::BoolView(BoolViewInner::Const(false))) => { - (!e).constrain(slv, map)?; - } - Some(view::BoolView(BoolViewInner::Const(true))) => { - e.constrain(slv, map)?; - } - Some(view::BoolView(BoolViewInner::Lit(name))) => { - res = Some(e.to_arg(slv, map, Some(name))?); - } - None => res = Some(e.to_arg(slv, map, None)?), - } - } - Ok(()) - } - BoolExpr::Xor(es) => { - let mut lits = Vec::with_capacity(es.len()); - let mut count = 0; - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => count += 1, - BoolViewInner::Const(false) => {} - BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), - } - } - let mut formula = Formula::Xor(lits); - if count % 2 == 1 { - formula = !formula; - } - slv.oracle - .encode(&formula, &TseitinEncoder) - .map_err(|_| ReformulationError::TrivialUnsatisfiable) - } - BoolExpr::IfThenElse { cond, then, els } => match cond.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => then.constrain(slv, map), - BoolViewInner::Const(false) => els.constrain(slv, map), - BoolViewInner::Lit(_) => BoolExpr::And(vec![ - BoolExpr::Or(vec![!*cond.clone(), *then.clone()]), - BoolExpr::Or(vec![*cond.clone(), *els.clone()]), - ]) - .constrain(slv, map), - }, - } +impl Constraint for Formula { + fn simplify(&mut self, _: &mut S) -> Result { + Ok(SimplificationStatus::Fixpoint) } - /// Helper function that takes an expression that was contains in a - /// [`BoolExpr::Not`] and return an equivalent expression that is equivalent - /// to the negation of the original expression by pushing the negation - /// inwards. If this is not possible, then `None` is returned. - fn push_not_inward(&self) -> Option { - Some(match self { - BoolExpr::View(v) => BoolExpr::View(!v), - BoolExpr::Not(e) => *e.clone(), - BoolExpr::Or(es) => BoolExpr::And(es.iter().map(|e| !e).collect()), - BoolExpr::And(es) => BoolExpr::Or(es.iter().map(|e| !e).collect()), - BoolExpr::Implies(a, b) => BoolExpr::And(vec![*a.clone(), !*b.clone()]), - BoolExpr::IfThenElse { cond, then, els } => BoolExpr::IfThenElse { - cond: cond.clone(), - then: Box::new(!*then.clone()), - els: Box::new(!*els.clone()), - }, - BoolExpr::Xor(es) => { - BoolExpr::Xor(once(true.into()).chain(es.iter().cloned()).collect()) + fn to_solver(&self, slv: &mut dyn ReformulationActions) -> Result<(), ReformulationError> { + let mut resolver = |bv: BoolView| { + let inner = slv.get_solver_bool(bv); + match inner.0 { + BoolViewInner::Const(b) => Err(b), + BoolViewInner::Lit(l) => Ok(l), } - BoolExpr::Equiv(es) => { - if let [a, b] = es.as_slice() { - BoolExpr::Xor(vec![a.clone(), b.clone()]) - } else { - return None; - } - } - }) - } - - /// Reifies the Boolean expression into a Boolean view (which will be a - /// literal or constant in the oracle solver). - pub(crate) fn to_arg>( - &self, - slv: &mut Solver, - map: &mut VariableMap, - name: Option, - ) -> Result { - let bind_lit = |oracle: &mut Oracle, lit| { - Ok(view::BoolView(BoolViewInner::Lit( - if let Some(name) = name { - oracle - .encode( - &Formula::Equiv(vec![Formula::Atom(name), Formula::Atom(lit)]), - &TseitinEncoder, - ) - .map_err(|_| ReformulationError::TrivialUnsatisfiable)?; - name - } else { - lit - }, - ))) }; - let bind_const = |oracle: &mut Oracle, val| { - if let Some(name) = name { - oracle - .add_clause([if val { name } else { !name }]) - .map_err(|_| ReformulationError::TrivialUnsatisfiable)?; - } - Ok(view::BoolView(BoolViewInner::Const(val))) - }; - let bind_view = |oracle: &mut Oracle, view: view::BoolView| match view.0 { - BoolViewInner::Lit(l) => bind_lit(oracle, l), - BoolViewInner::Const(c) => bind_const(oracle, c), - }; - match self { - BoolExpr::View(v) => { - let view = map.get_bool(slv, v); - bind_view(&mut slv.oracle, view) - } - BoolExpr::Not(x) => { - if let Some(y) = x.push_not_inward() { - y.to_arg(slv, map, name) - } else { - let r = x.to_arg(slv, map, name.map(|e| !e))?; - Ok(!r) - } - } - BoolExpr::Or(es) => { - let mut lits = Vec::with_capacity(es.len()); - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(false) => {} - BoolViewInner::Const(true) => return bind_const(&mut slv.oracle, true), - BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), - } - } - let r = name.unwrap_or_else(|| slv.oracle.new_lit()); - slv.oracle - .encode( - &Formula::Equiv(vec![Formula::Atom(r), Formula::Or(lits)]), - &TseitinEncoder, - ) - .unwrap(); - Ok(view::BoolView(BoolViewInner::Lit(r))) - } - BoolExpr::And(es) => { - let mut lits = Vec::with_capacity(es.len()); - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => {} - BoolViewInner::Const(false) => return bind_const(&mut slv.oracle, false), - BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), - } - } - let name = name.unwrap_or_else(|| slv.oracle.new_lit()); - slv.oracle - .encode( - &Formula::Equiv(vec![Formula::Atom(name), Formula::And(lits)]), - &TseitinEncoder, - ) - .unwrap(); - Ok(view::BoolView(BoolViewInner::Lit(name))) - } - BoolExpr::Implies(a, b) => { - let a = match a.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => return b.to_arg(slv, map, name), - BoolViewInner::Const(false) => return bind_const(&mut slv.oracle, true), - BoolViewInner::Lit(l) => l, - }; - - // TODO: Conditional encoding - match b.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => bind_const(&mut slv.oracle, true), - BoolViewInner::Const(false) => bind_lit(&mut slv.oracle, !a), - BoolViewInner::Lit(b) => { - let name = name.unwrap_or_else(|| slv.oracle.new_lit()); - slv.oracle - .encode( - &Formula::Equiv(vec![ - Formula::Atom(name), - Formula::Implies( - Box::new(Formula::Atom(a)), - Box::new(Formula::Atom(b)), - ), - ]), - &TseitinEncoder, - ) - .unwrap(); - Ok(view::BoolView(BoolViewInner::Lit(name))) - } - } - } - BoolExpr::Equiv(es) => { - let mut lits = Vec::with_capacity(es.len()); - let mut res = None; - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(b) => match res { - None => res = Some(b), - Some(b2) if b != b2 => { - return bind_const(&mut slv.oracle, false); - } - Some(_) => {} - }, - BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), - } - } - let name = name.unwrap_or_else(|| slv.oracle.new_lit()); - let f = match res { - Some(b) => { - Formula::And(lits.into_iter().map(|e| if b { e } else { !e }).collect()) - } - None => Formula::Equiv(lits), - }; - slv.oracle - .encode( - &Formula::Equiv(vec![Formula::Atom(name), f]), - &TseitinEncoder, - ) - .unwrap(); - Ok(view::BoolView(BoolViewInner::Lit(name))) - } - BoolExpr::Xor(es) => { - let mut lits = Vec::with_capacity(es.len()); - let mut count = 0; - for e in es { - match e.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => count += 1, - BoolViewInner::Const(false) => {} - BoolViewInner::Lit(l) => lits.push(Formula::Atom(l)), - } - } - let name = name.unwrap_or_else(|| slv.oracle.new_lit()); - let mut formula = Formula::Xor(lits); - if count % 2 == 1 { - formula = !formula; - } - slv.oracle - .encode( - &Formula::Equiv(vec![Formula::Atom(name), formula]), - &TseitinEncoder, - ) - .unwrap(); - Ok(view::BoolView(BoolViewInner::Lit(name))) - } - BoolExpr::IfThenElse { cond, then, els } => { - match cond.to_arg(slv, map, None)?.0 { - BoolViewInner::Const(true) => then.to_arg(slv, map, name), - BoolViewInner::Const(false) => then.to_arg(slv, map, name), - // TODO: Conditional encoding - BoolViewInner::Lit(_) => BoolExpr::And(vec![ - BoolExpr::Or(vec![!*cond.clone(), *then.clone()]), - BoolExpr::Or(vec![*cond.clone(), *els.clone()]), - ]) - .to_arg(slv, map, name), - } + let result: Result, _> = self.clone().simplify_with(&mut resolver); + match result { + Err(false) => Err(ReformulationError::TrivialUnsatisfiable), + Err(true) => Ok(()), + Ok(f) => { + let mut wrapper = slv.with_conditions(vec![]); + Ok(TseitinEncoder.encode(&mut wrapper, &f)?) } } } } -impl From<&BoolView> for BoolExpr { - fn from(v: &BoolView) -> Self { - Self::View(v.clone()) - } -} -impl From for BoolExpr { - fn from(v: BoolView) -> Self { - Self::View(v) - } -} - -impl From for BoolExpr { - fn from(v: bool) -> Self { - Self::View(v.into()) - } -} - -impl Not for BoolExpr { - type Output = BoolExpr; - - fn not(self) -> Self::Output { - match self { - BoolExpr::View(v) => BoolExpr::View(!v), - BoolExpr::Not(e) => *e, - _ => BoolExpr::Not(Box::new(self)), - } - } -} - -impl Not for &BoolExpr { - type Output = BoolExpr; - fn not(self) -> Self::Output { - !self.clone() +impl From for Formula { + fn from(v: BoolView) -> Self { + Self::Atom(v) } } @@ -465,29 +83,20 @@ impl Not for BoolView { BoolView::Lit(l) => BoolView::Lit(!l), BoolView::Const(b) => BoolView::Const(!b), BoolView::IntEq(v, i) => BoolView::IntNotEq(v, i), - BoolView::IntGreater(v, i) => BoolView::IntLessEq(v, i), BoolView::IntGreaterEq(v, i) => BoolView::IntLess(v, i), BoolView::IntLess(v, i) => BoolView::IntGreaterEq(v, i), - BoolView::IntLessEq(v, i) => BoolView::IntGreater(v, i), BoolView::IntNotEq(v, i) => BoolView::IntEq(v, i), } } } -impl Not for &BoolView { - type Output = BoolView; - - fn not(self) -> Self::Output { - !(self.clone()) - } -} - #[cfg(test)] mod tests { use expect_test::expect; use itertools::Itertools; - use crate::{model::bool::BoolView, BoolExpr, InitConfig, Model, Solver}; + use crate::{InitConfig, Model, Solver}; + use pindakaas::propositional_logic::Formula; #[test] fn test_bool_and() { @@ -495,7 +104,7 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::And(b.iter().cloned().map_into().collect()); + m += Formula::And(b.iter().cloned().map_into().collect()); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b .into_iter() @@ -507,8 +116,8 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::And(b.iter().cloned().map_into().collect()); - m += BoolExpr::from(!b[0].clone()); + m += Formula::And(b.iter().cloned().map_into().collect()); + m += Formula::from(!b[0]); let (mut slv, _): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); slv.assert_unsatisfiable(); @@ -516,9 +125,13 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_var(); - m += BoolExpr::Equiv(vec![ - b.clone().into(), - BoolExpr::And(vec![true.into(), true.into(), true.into()]), + m += Formula::Equiv(vec![ + b.into(), + Formula::And(vec![ + Formula::Atom(true.into()), + Formula::Atom(true.into()), + Formula::Atom(true.into()), + ]), ]); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars = vec![map.get(&mut slv, &b.into())]; @@ -531,9 +144,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Equiv(vec![ - b[0].clone().into(), - BoolExpr::And(vec![b[1].clone().into(), b[2].clone().into()]), + m += Formula::Equiv(vec![ + b[0].into(), + Formula::And(vec![b[1].into(), b[2].into()]), ]); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b @@ -556,9 +169,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Equiv(vec![ - b[0].clone().into(), - BoolExpr::Or(vec![b[1].clone().into(), b[2].clone().into()]), + m += Formula::Equiv(vec![ + b[0].into(), + Formula::Or(vec![b[1].into(), b[2].into()]), ]); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b @@ -581,9 +194,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Equiv(vec![ - b[0].clone().into(), - BoolExpr::Equiv(vec![b[1].clone().into(), b[2].clone().into()]), + m += Formula::Equiv(vec![ + b[0].into(), + Formula::Equiv(vec![b[1].into(), b[2].into()]), ]); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b @@ -606,7 +219,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(2); - m += BoolExpr::Not(Box::new(BoolExpr::Xor(b.iter().map_into().collect()))); + m += Formula::Not(Box::new(Formula::Xor( + b.iter().copied().map_into().collect(), + ))); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b .into_iter() @@ -623,7 +238,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Not(Box::new(BoolExpr::Equiv(b.iter().map_into().collect()))); + m += Formula::Not(Box::new(Formula::Equiv( + b.iter().copied().map_into().collect(), + ))); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b .into_iter() @@ -647,7 +264,7 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Or(b.iter().cloned().map_into().collect()); + m += Formula::Or(b.iter().cloned().map_into().collect()); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b .into_iter() @@ -669,8 +286,8 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Or(b.iter().cloned().map_into().collect()); - m += BoolExpr::And(b.iter().cloned().map(|l| (!l).into()).collect()); + m += Formula::Or(b.iter().cloned().map_into().collect()); + m += Formula::And(b.iter().cloned().map(|l| (!l).into()).collect()); let (mut slv, _): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); slv.assert_unsatisfiable(); @@ -678,9 +295,13 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_var(); - m += BoolExpr::Equiv(vec![ - b.clone().into(), - BoolExpr::Or(vec![false.into(), false.into(), false.into()]), + m += Formula::Equiv(vec![ + b.into(), + Formula::Or(vec![ + Formula::Atom(false.into()), + Formula::Atom(false.into()), + Formula::Atom(false.into()), + ]), ]); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars = vec![map.get(&mut slv, &b.into())]; @@ -693,7 +314,7 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(3); - m += BoolExpr::Xor(b.iter().cloned().map_into().collect()); + m += Formula::Xor(b.iter().cloned().map_into().collect()); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b .into_iter() @@ -712,12 +333,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(2); - m += BoolExpr::Equiv(vec![ - BoolExpr::View(b[1].clone()), - BoolExpr::Xor(vec![ - BoolExpr::View(BoolView::Const(true)), - BoolExpr::View(b[0].clone()), - ]), + m += Formula::Equiv(vec![ + b[1].into(), + Formula::Xor(vec![Formula::Atom(true.into()), b[0].into()]), ]); let (mut slv, map): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); let vars: Vec<_> = b @@ -735,9 +353,9 @@ mod tests { let mut m = Model::default(); let b = m.new_bool_vars(2); - m += BoolExpr::Xor(b.iter().cloned().map_into().collect()); - m += BoolExpr::from(!b[0].clone()); - m += BoolExpr::from(!b[1].clone()); + m += Formula::Xor(b.iter().cloned().map_into().collect()); + m += Formula::from(!b[0]); + m += Formula::from(!b[1]); let (mut slv, _): (Solver, _) = m.to_solver(&InitConfig::default()).unwrap(); slv.assert_unsatisfiable(); } diff --git a/crates/huub/src/model/branching.rs b/crates/huub/src/model/branching.rs index 5906533..2dd6c58 100644 --- a/crates/huub/src/model/branching.rs +++ b/crates/huub/src/model/branching.rs @@ -4,7 +4,7 @@ use pindakaas::solver::propagation::PropagatingSolver; use crate::{ branchers::{BoolBrancher, IntBrancher, WarmStartBrancher}, - model::{bool::BoolView, int::IntView, reformulate::VariableMap}, + model::{bool::BoolView, int::IntExpr, reformulate::VariableMap}, solver::engine::Engine, Solver, }; @@ -19,7 +19,7 @@ pub enum Branching { /// Make a search decision by using the [`VariableSelection`] to select a /// integer decision variable, and then limit the domain of the variable by /// using the [`ValueSelection`]. - Int(Vec, VariableSelection, ValueSelection), + Int(Vec, VariableSelection, ValueSelection), /// Search by sequentially applying the given branching strategies. Seq(Vec), /// Search by enforcing the given Boolean expressions, but abandon the search @@ -73,11 +73,11 @@ impl Branching { ) { match self { Branching::Bool(vars, var_sel, val_sel) => { - let vars = vars.iter().map(|v| map.get_bool(slv, v)).collect(); + let vars = vars.iter().map(|v| map.get_bool(slv, *v)).collect(); BoolBrancher::new_in(slv, vars, *var_sel, *val_sel); } Branching::Int(v, var_sel, val_sel) => { - let vars: Vec<_> = v.iter().map(|v| v.to_arg(slv, map)).collect(); + let vars: Vec<_> = v.iter().map(|v| v.as_solver_arg(slv, map)).collect(); IntBrancher::new_in(slv, vars, *var_sel, *val_sel); } Branching::Seq(branchings) => { @@ -86,7 +86,7 @@ impl Branching { } } Branching::WarmStart(exprs) => { - let decisions = exprs.iter().map(|v| map.get_bool(slv, v)).collect(); + let decisions = exprs.iter().map(|v| map.get_bool(slv, *v)).collect(); WarmStartBrancher::new_in(slv, decisions); } } diff --git a/crates/huub/src/model/constraint.rs b/crates/huub/src/model/constraint.rs index 7795f5d..6d6e314 100644 --- a/crates/huub/src/model/constraint.rs +++ b/crates/huub/src/model/constraint.rs @@ -1,129 +1,85 @@ //! Definitions of constraints that can be used as part of a model. -use std::iter::once; +use std::ops::AddAssign; -use itertools::Itertools; -use pindakaas::solver::propagation::PropagatingSolver; -use rangelist::RangeList; +use pindakaas::{ + propositional_logic::Formula, solver::propagation::PropagatingSolver, ClauseDatabaseTools, +}; +use rangelist::{IntervalIterator, RangeList}; use crate::{ - actions::InspectionActions, + actions::{ConstraintInitActions, SimplificationActions}, constraints::{ - all_different_int::AllDifferentIntValue, - array_int_minimum::ArrayIntMinimumBounds, - array_var_int_element::ArrayVarIntElementBounds, - disjunctive_strict::DisjunctiveStrictEdgeFinding, - int_abs::IntAbsBounds, - int_div::IntDivBounds, - int_lin_le::{IntLinearLessEqBounds, IntLinearLessEqImpBounds}, - int_lin_ne::{IntLinearNotEqImpValue, IntLinearNotEqValue}, - int_pow::IntPowBounds, - int_times::IntTimesBounds, - table_int::encode_table_int_gac, + all_different_int::AllDifferentInt, array_int_element::ArrayIntElement, + array_int_minimum::ArrayIntMinimum, array_var_bool_element::ArrayVarBoolElement, + array_var_int_element::ArrayVarIntElement, disjunctive_strict::DisjunctiveStrict, + int_abs::IntAbs, int_div::IntDiv, int_linear::IntLinear, int_pow::IntPow, + int_times::IntTimes, set_in_reif::SetInReif, table_int::TableInt, BoxedConstraint, + Constraint, SimplificationStatus, + }, + model::{ + bool::BoolView, + int::IntExpr, + reformulate::{ReformulationContext, VariableMap}, }, - helpers::{div_ceil, div_floor}, - model::{bool::BoolView, int::IntView, reformulate::VariableMap}, - solver::{engine::Engine, view::IntViewInner}, - BoolExpr, IntSetVal, IntVal, LitMeaning, Model, NonZeroIntVal, ReformulationError, Solver, + solver::engine::Engine, + IntSetVal, IntVal, LitMeaning, Model, ReformulationError, Solver, }; -#[derive(Debug, Clone, PartialEq, Eq, Hash)] -/// The collection of possible constraint that can be part of a [`Model`]. -pub enum Constraint { - /// `all_different_int` constraint, which enforces that all the given integer - /// decision variables take different values. - AllDifferentInt(Vec), - /// `array_int_element` which enforces that the final integer decision - /// variable takes the value equal the element of the given array of integer - /// integer values at the index given by the integer decision variable. - ArrayIntElement(Vec, IntView, IntView), - /// `array_int_maximum` constraint, which enforces that the final integer - /// decision variable takes the maximum value of the given array of integer - /// decision variables. - ArrayIntMaximum(Vec, IntView), - /// `array_int_minimum` constraint, which enforces that the final integer - /// decision variable takes the minimum value of the given array of integer - /// decision variables. - ArrayIntMinimum(Vec, IntView), - /// `array_var_bool_element` constraint, which enforces that the final Boolean - /// decision variable takes the value equal the element of the given array of - /// Boolean decision variables at the index given by the integer decision - /// variable. - ArrayVarBoolElement(Vec, IntView, BoolExpr), - /// `array_var_int_element` constraint, which enforces that final integer - /// decision variable takes the value equal the element of the given array of - /// integer decision variables at the index given by the second integer - /// decision variable. - ArrayVarIntElement(Vec, IntView, IntView), - /// `disjuctive_strict` constraint, which enforces that the given a list of - /// integer decision variables representing the start times of tasks and a - /// list of integer values representing the durations of tasks, the tasks do - /// not overlap in time. - DisjunctiveStrict(Vec, Vec), - /// `int_abs` constraint, which enforces that the second integer decision - /// variable takes the absolute value of the first integer decision variable. - IntAbs(IntView, IntView), - /// `int_div` constraint, which enforces that the first integer variable - /// divided by the second integer variable is equal to the third integer - /// variable. - /// - /// Note that the division is integer division, i.e. the result is rounded - /// towards zero. - IntDiv(IntView, IntView, IntView), - /// `int_lin_eq` constraint, which enforces that the sum of the integer views - /// is equal to the given integer value. - IntLinEq(Vec, IntVal), - /// `int_lin_eq_imp` constraint, which enforces that if the given Boolean - /// decision variable is `true`, then the sum of the integer views is equal to - /// the given integer value. - IntLinEqImp(Vec, IntVal, BoolExpr), - /// `int_lin_eq_reif` constraint, which enforces that the given Boolean - /// decision variable is `true` if-and-only-if the sum of the integer views is - /// equal to the given integer value. - IntLinEqReif(Vec, IntVal, BoolExpr), - /// `int_lin_le` constraint, which enforces that the sum of the integer views - /// is less than or equal to the given integer value. - IntLinLessEq(Vec, IntVal), - /// `int_lin_le_imp` constraint, which enforces that if the given Boolean - /// decision variable is `true`, then the sum of the integer views is less - /// than or equal to the given integer value. - IntLinLessEqImp(Vec, IntVal, BoolExpr), - /// `int_lin_le_reif` constraint, which enforces that the given Boolean - /// decision variable is `true` if-and-only-if the sum of the integer views is - /// less than or equal to the given integer value. - IntLinLessEqReif(Vec, IntVal, BoolExpr), - /// `int_lin_ne` constraint, which enforces that the sum of the integer views - /// is not equal to the given integer value. - IntLinNotEq(Vec, IntVal), - /// `int_lin_ne_imp` constraint, which enforces that if the given Boolean - /// decision variable is `true`, then the sum of the integer views is not - /// equal to the given integer value. - IntLinNotEqImp(Vec, IntVal, BoolExpr), - /// `int_lin_ne_reif` constraint, which enforces that the given Boolean - /// variable is `true` if-and-only-if the sum of the integer views is not - /// equal to the given integer value. - IntLinNotEqReif(Vec, IntVal, BoolExpr), - /// `int_pow` constraint, which enforces that the first (base) integer - /// variable exponentiated by the second (exponent) integer variable is equal - /// to the third (result) integer variable. - IntPow(IntView, IntView, IntView), - /// `int_times` constraint, which enforces that the product of the first two - /// integer variables is equal to a third. - IntTimes(IntView, IntView, IntView), +/// Wrapper around [`Model`] that knows the constraint being initialized. +struct ConstraintInitContext<'a> { + /// Index of the constraint being initialized. + con: usize, + /// Reference to the Model in which the constraint exists. + model: &'a mut Model, +} + +#[allow( + clippy::missing_docs_in_private_items, + reason = "constraints are generally documented on their own types" +)] +#[derive(Clone, Debug)] +/// An disambiguation of the different constraints objects that can be used in a +/// [`Model`] object. +/// +/// This enum type is used to store and analyze the constraints in a [`Model`]. +pub(crate) enum ConstraintStore { + AllDifferentInt(AllDifferentInt), + ArrayIntElement(ArrayIntElement), + ArrayIntMinimum(ArrayIntMinimum), + ArrayVarBoolElement(ArrayVarBoolElement), + ArrayVarIntElement(ArrayVarIntElement), + DisjunctiveStrict(DisjunctiveStrict), + IntAbs(IntAbs), + IntDiv(IntDiv), + IntLinear(IntLinear), + IntPow(IntPow), + IntTimes(IntTimes), /// A constraint given as a propasitional logic formula, which is enforced to /// be `true`. - PropLogic(BoolExpr), - /// `set_in_reif` constraint, which enforces that the given Boolean variable - /// takes the value `true` if-and-only-if an integer variable is in a given - /// set. - SetInReif(IntView, IntSetVal, BoolExpr), - /// `table_int` constraint, which enforces that the given list of integer - /// views take their values according to one of the given list of integer - /// values. - TableInt(Vec, Vec>), + PropLogic(Formula), + SetInReif(SetInReif), + TableInt(TableInt), + UserCustom(BoxedConstraint), +} + +impl ConstraintInitActions for ConstraintInitContext<'_> { + fn simplify_on_change_bool(&mut self, _var: BoolView) { + todo!() + } + + fn simplify_on_change_int(&mut self, var: IntExpr) { + match var { + IntExpr::Bool(_, v) => self.simplify_on_change_bool(v), + IntExpr::Linear(_, v) | IntExpr::Var(v) => { + self.model.int_vars[v].constraints.push(self.con); + } + IntExpr::Const(_) => {} + } + } } -impl Constraint { +impl ConstraintStore { /// Map the constraint into propagators and clauses to be added to the given /// solver, using the variable mapping provided. pub(crate) fn to_solver>( @@ -131,541 +87,471 @@ impl Constraint { slv: &mut Solver, map: &mut VariableMap, ) -> Result<(), ReformulationError> { + let mut actions = ReformulationContext { slv, map }; match self { - Constraint::AllDifferentInt(v) => { - let vars: Vec<_> = v.iter().map(|v| v.to_arg(slv, map)).collect(); - AllDifferentIntValue::new_in(slv, vars); - Ok(()) + ConstraintStore::AllDifferentInt(con) => { + >::to_solver(con, &mut actions) } - Constraint::ArrayIntElement(arr, idx, y) => { - let idx = idx.to_arg(slv, map); - let y = y.to_arg(slv, map); - - let idx_map = arr - .iter() - .enumerate() - .map(|(i, v)| (*v, (i + 1) as IntVal)) - .into_group_map(); - - for (val, idxs) in idx_map { - let val_eq = slv.get_int_lit(y, LitMeaning::Eq(val)); - let idxs: Vec<_> = idxs - .into_iter() - .map(|i| slv.get_int_lit(idx, LitMeaning::Eq(i))) - .collect(); - - for i in idxs.iter() { - // (idx = i) -> (val = arr[i]) - slv.add_clause([!i, val_eq])?; - } - // (idx not in idxs) -> (val != arr[i]) - slv.add_clause(idxs.into_iter().chain(once(!val_eq)))?; - } - Ok(()) + ConstraintStore::ArrayIntElement(con) => { + >::to_solver(con, &mut actions) } - Constraint::ArrayIntMinimum(vars, y) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let y = y.to_arg(slv, map); - ArrayIntMinimumBounds::new_in(slv, vars, y); - Ok(()) + ConstraintStore::ArrayIntMinimum(con) => { + >::to_solver(con, &mut actions) } - Constraint::ArrayIntMaximum(vars, y) => { - let vars: Vec<_> = vars.iter().map(|v| -v.to_arg(slv, map)).collect(); - let y = -y.to_arg(slv, map); - ArrayIntMinimumBounds::new_in(slv, vars, y); - Ok(()) + ConstraintStore::ArrayVarBoolElement(con) => { + >::to_solver(con, &mut actions) } - Constraint::ArrayVarIntElement(vars, idx, y) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let y = y.to_arg(slv, map); - let idx = idx.to_arg(slv, map); - // tranform 1-based index into 0-based index array - ArrayVarIntElementBounds::new_in(slv, vars, y, idx + (-1)) - } - Constraint::ArrayVarBoolElement(vars, idx, y) => { - let idx = idx.to_arg(slv, map); - // If the index is already fixed, implement simple equivalence - if let IntViewInner::Const(idx) = idx.0 { - let idx = idx as usize; - return BoolExpr::Equiv(vec![vars[idx - 1].clone(), y.clone()]) - .constrain(slv, map); - } - - // Evaluate result literal - let y = y.to_arg(slv, map, None)?; - let arr: Vec<_> = vars - .iter() - .map(|v| v.to_arg(slv, map, None)) - .try_collect()?; + ConstraintStore::ArrayVarIntElement(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::DisjunctiveStrict(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntAbs(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntDiv(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntLinear(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntPow(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::IntTimes(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::PropLogic(exp) => { + as Constraint>::to_solver(exp, &mut actions) + } + ConstraintStore::SetInReif(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::TableInt(con) => { + >::to_solver(con, &mut actions) + } + ConstraintStore::UserCustom(con) => con.to_solver(&mut actions), + } + } +} - for (i, l) in arr.iter().enumerate() { - // Evaluate array literal - let idx_eq = slv.get_int_lit(idx, LitMeaning::Eq((i + 1) as IntVal)); - // add clause (idx = i + 1 /\ arr[i]) => val - slv.add_clause([!idx_eq, !l, y])?; - // add clause (idx = i + 1 /\ !arr[i]) => !val - slv.add_clause([!idx_eq, *l, !y])?; - } +impl Model { + /// Propagate the constraint at index `con`, updating the domains of the + /// variables and rewriting the constraint if necessary. + pub(crate) fn propagate(&mut self, con: usize) -> Result<(), ReformulationError> { + let Some(mut con_obj) = self.constraints[con].take() else { + return Ok(()); + }; - // add clause (arr[1] /\ arr[2] /\ ... /\ arr[n]) => val - slv.add_clause(arr.iter().map(|l| !l).chain(once(y)))?; - // add clause (!arr[1] /\ !arr[2] /\ ... /\ !arr[n]) => !val - slv.add_clause(arr.into_iter().chain(once(!y)))?; - Ok(()) + let status = match &mut con_obj { + ConstraintStore::AllDifferentInt(c) => c.simplify(self), + ConstraintStore::ArrayIntElement(c) => c.simplify(self), + ConstraintStore::ArrayIntMinimum(c) => c.simplify(self), + ConstraintStore::ArrayVarBoolElement(c) => c.simplify(self), + ConstraintStore::ArrayVarIntElement(c) => c.simplify(self), + ConstraintStore::DisjunctiveStrict(c) => c.simplify(self), + ConstraintStore::IntAbs(c) => c.simplify(self), + ConstraintStore::IntDiv(c) => c.simplify(self), + ConstraintStore::IntLinear(c) => c.simplify(self), + ConstraintStore::IntPow(c) => c.simplify(self), + ConstraintStore::IntTimes(c) => c.simplify(self), + ConstraintStore::PropLogic(exp) => exp.simplify(self), + ConstraintStore::SetInReif(c) => c.simplify(self), + ConstraintStore::TableInt(con) => con.simplify(self), + ConstraintStore::UserCustom(con) => con.simplify(self), + }?; + match status { + SimplificationStatus::Subsumed => { + // Constraint is known to be satisfied, no need to place back. + } + SimplificationStatus::Fixpoint => { + self.constraints[con] = Some(con_obj); } - Constraint::DisjunctiveStrict(v, d) => { - let vars: Vec<_> = v.iter().map(|v| v.to_arg(slv, map)).collect(); - let durs = d - .iter() - .map(|d| { - assert!( - *d >= 0, - "duration of tasks in disjunctive constraint must be non-negative" - ); - *d - }) - .collect_vec(); - // Add propagator for lower bound propagation - DisjunctiveStrictEdgeFinding::new_in(slv, vars.clone(), durs.clone()); + } + Ok(()) + } - // Add symmetric propagator for upper bound propagation - let horizon = vars - .iter() - .zip(durs.iter()) - .map(|(v, d)| slv.engine().state.get_int_upper_bound(*v) + d) - .max() - .unwrap(); - let symmetric_vars = vars - .iter() - .zip(durs.iter()) - .map(|(v, d)| -*v + (horizon - d)) - .collect(); - DisjunctiveStrictEdgeFinding::new_in(slv, symmetric_vars, durs); - Ok(()) + /// Subscribe the constraint located at index `con` to changes in the + /// variables it depends on. + pub(crate) fn subscribe(&mut self, con: usize) { + let con_store = self.constraints[con].take().unwrap(); + let mut ctx = ConstraintInitContext { con, model: self }; + match &con_store { + ConstraintStore::AllDifferentInt(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntAbs(origin, abs) => { - let origin = origin.to_arg(slv, map); - let abs = abs.to_arg(slv, map); - IntAbsBounds::new_in(slv, origin, abs); - Ok(()) + ConstraintStore::ArrayIntElement(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntDiv(numerator, denominator, result) => { - let numerator = numerator.to_arg(slv, map); - let denominator = denominator.to_arg(slv, map); - let result = result.to_arg(slv, map); - IntDivBounds::new_in(slv, numerator, denominator, result) - } - Constraint::IntLinEq(vars, c) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - // coeffs * vars <= c - IntLinearLessEqBounds::new_in(slv, vars.clone(), *c); - // coeffs * vars >= c <=> -coeffs * vars <= -c - IntLinearLessEqBounds::new_in(slv, vars.into_iter().map(|v| -v), -c); - Ok(()) + ConstraintStore::ArrayIntMinimum(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinEqImp(vars, c, r) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let r = r.to_arg(slv, map, None)?; - IntLinearLessEqImpBounds::new_in(slv, vars.clone(), *c, r); - IntLinearLessEqImpBounds::new_in(slv, vars.into_iter().map(|v| -v), -c, r); - Ok(()) + ConstraintStore::ArrayVarBoolElement(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinEqReif(vars, c, r) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let r = r.to_arg(slv, map, None)?; - IntLinearLessEqImpBounds::new_in(slv, vars.clone(), *c, r); - IntLinearLessEqImpBounds::new_in(slv, vars.iter().map(|v| -(*v)), -c, r); - IntLinearNotEqImpValue::new_in(slv, vars, *c, !r); - Ok(()) + ConstraintStore::ArrayVarIntElement(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinLessEq(vars, c) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - IntLinearLessEqBounds::new_in(slv, vars, *c); - Ok(()) + ConstraintStore::DisjunctiveStrict(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinLessEqImp(vars, c, r) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let r = r.to_arg(slv, map, None)?; - IntLinearLessEqImpBounds::new_in(slv, vars, *c, r); - Ok(()) + ConstraintStore::IntAbs(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinLessEqReif(vars, c, r) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let r = r.to_arg(slv, map, None)?; - IntLinearLessEqImpBounds::new_in(slv, vars.clone(), *c, r); - IntLinearLessEqImpBounds::new_in(slv, vars.into_iter().map(|v| -v), -(c + 1), !r); - Ok(()) + ConstraintStore::IntDiv(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinNotEq(vars, c) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - IntLinearNotEqValue::new_in(slv, vars, *c); - Ok(()) + ConstraintStore::IntLinear(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinNotEqImp(vars, c, r) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let r = r.to_arg(slv, map, None)?; - IntLinearNotEqImpValue::new_in(slv, vars, *c, r); - Ok(()) + ConstraintStore::IntPow(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntLinNotEqReif(vars, c, r) => { - let vars: Vec<_> = vars.iter().map(|v| v.to_arg(slv, map)).collect(); - let r = r.to_arg(slv, map, None)?; - IntLinearNotEqImpValue::new_in(slv, vars.clone(), *c, r); - IntLinearLessEqImpBounds::new_in(slv, vars.clone(), *c, !r); - IntLinearLessEqImpBounds::new_in(slv, vars.iter().map(|v| -(*v)), -c, !r); - Ok(()) + ConstraintStore::IntTimes(con) => { + >::initialize(con, &mut ctx) } - Constraint::IntPow(base, exponent, res) => { - let base = base.to_arg(slv, map); - let exponent = exponent.to_arg(slv, map); - let result = res.to_arg(slv, map); - IntPowBounds::new_in(slv, base, exponent, result) - } - Constraint::IntTimes(x, y, z) => { - let x = x.to_arg(slv, map); - let y = y.to_arg(slv, map); - let z = z.to_arg(slv, map); - IntTimesBounds::new_in(slv, x, y, z); - Ok(()) + ConstraintStore::PropLogic(exp) => { + as Constraint>::initialize(exp, &mut ctx) } - Constraint::PropLogic(exp) => exp.constrain(slv, map), - Constraint::SetInReif(x, s, r) => { - if s.iter().len() == 1 { - let lb = *s.lower_bound().unwrap(); - let ub = *s.upper_bound().unwrap(); - BoolExpr::Equiv(vec![ - BoolExpr::And(vec![ - BoolView::IntGreaterEq(Box::from(x.clone()), lb).into(), - BoolView::IntLessEq(Box::from(x.clone()), ub).into(), - ]), - r.clone(), - ]) - .constrain(slv, map) - } else { - let eq_lits = s - .iter() - .flatten() - .map(|v| BoolView::IntEq(Box::new(x.clone()), v).into()) - .collect(); - BoolExpr::Equiv(vec![r.clone(), BoolExpr::Or(eq_lits)]).constrain(slv, map) - } + ConstraintStore::SetInReif(con) => { + >::initialize(con, &mut ctx) + } + ConstraintStore::TableInt(con) => { + >::initialize(con, &mut ctx) } - Constraint::TableInt(vars, vals) => encode_table_int_gac(slv, map, vars, vals), + ConstraintStore::UserCustom(con) => con.initialize(&mut ctx), } + self.constraints[con] = Some(con_store); } } -impl Model { - /// Propagate the constraint at index `con`, updating the domains of the - /// variables and rewriting the constraint if necessary. - pub(crate) fn propagate(&mut self, con: usize) -> Result<(), ReformulationError> { - let simplified = match self.constraints[con].clone() { - Constraint::AllDifferentInt(vars) => { - let (vals, vars): (Vec<_>, Vec<_>) = vars - .into_iter() - .partition(|v| matches!(v, IntView::Const(_))); - if vals.is_empty() { - return Ok(()); - } - let neg_dom = RangeList::from_iter(vals.iter().map(|i| { - let IntView::Const(i) = i else { unreachable!() }; - *i..=*i - })); - for v in &vars { - self.diff_int_domain(v, &neg_dom, con)?; - } - Some(Constraint::AllDifferentInt(vars)) - } - Constraint::ArrayIntMaximum(args, m) => { - let max_lb = args - .iter() - .map(|a| self.get_int_lower_bound(a)) - .max() - .unwrap(); - let max_ub = args - .iter() - .map(|a| self.get_int_upper_bound(a)) - .max() - .unwrap(); - self.set_int_lower_bound(&m, max_lb, con)?; - self.set_int_upper_bound(&m, max_ub, con)?; +impl SimplificationActions for Model { + fn add_constraint(&mut self, constraint: C) + where + Model: AddAssign, + { + *self += constraint; + } - let ub = self.get_int_upper_bound(&m); - for a in &args { - self.set_int_upper_bound(a, ub, con)?; - } - Some(Constraint::ArrayIntMaximum(args, m)) - } - Constraint::ArrayIntMinimum(args, m) => { - let min_lb = args - .iter() - .map(|a| self.get_int_lower_bound(a)) - .min() - .unwrap(); - let min_ub = args - .iter() - .map(|a| self.get_int_upper_bound(a)) - .min() - .unwrap(); - self.set_int_lower_bound(&m, min_lb, con)?; - self.set_int_upper_bound(&m, min_ub, con)?; + fn check_int_in_domain(&self, var: IntExpr, val: IntVal) -> bool { + match var { + IntExpr::Var(v) => self.int_vars[v].domain.contains(&val), + IntExpr::Const(v) => v == val, + IntExpr::Linear(t, v) => match t.rev_transform_lit(LitMeaning::Eq(val)) { + Ok(LitMeaning::Eq(val)) => self.int_vars[v].domain.contains(&val), + Err(false) => false, + _ => unreachable!(), + }, + IntExpr::Bool(t, _) => match t.rev_transform_lit(LitMeaning::Eq(val)) { + Ok(LitMeaning::Eq(val)) => val == 0 || val == 1, + Err(false) => false, + _ => unreachable!(), + }, + } + } - let lb = self.get_int_lower_bound(&m); - for a in &args { - self.set_int_lower_bound(a, lb, con)?; + fn get_bool_val(&self, _: BoolView) -> Option { + None // TODO + } + + fn get_int_lower_bound(&self, var: IntExpr) -> IntVal { + match var { + IntExpr::Var(v) => { + let def = &self.int_vars[v]; + *def.domain.lower_bound().unwrap() + } + IntExpr::Const(v) => v, + IntExpr::Linear(t, v) => { + let def = &self.int_vars[v]; + if t.positive_scale() { + t.transform(*def.domain.lower_bound().unwrap()) + } else { + t.transform(*def.domain.upper_bound().unwrap()) } - Some(Constraint::ArrayIntMinimum(args, m)) - } - Constraint::ArrayVarIntElement(args, idx, y) => { - // make sure idx is within the range of args - self.set_int_lower_bound(&idx, 1, con)?; - self.set_int_upper_bound(&idx, args.len() as IntVal, con)?; - let (min_lb, max_ub) = - args.iter() - .fold((IntVal::MAX, IntVal::MIN), |(min_lb, max_ub), v| { - ( - min_lb.min(self.get_int_lower_bound(v)), - max_ub.max(self.get_int_upper_bound(v)), - ) - }); - if min_lb > self.get_int_lower_bound(&y) { - self.set_int_lower_bound(&y, min_lb, con)?; + } + IntExpr::Bool(t, _) => { + if t.positive_scale() { + t.transform(0) + } else { + t.transform(1) } - if max_ub < self.get_int_upper_bound(&y) { - self.set_int_upper_bound(&y, max_ub, con)?; + } + } + } + + fn get_int_upper_bound(&self, var: IntExpr) -> IntVal { + match var { + IntExpr::Var(v) => { + let def = &self.int_vars[v]; + *def.domain.upper_bound().unwrap() + } + IntExpr::Const(v) => v, + IntExpr::Linear(t, v) => { + let def = &self.int_vars[v]; + if t.positive_scale() { + t.transform(*def.domain.upper_bound().unwrap()) + } else { + t.transform(*def.domain.lower_bound().unwrap()) + } + } + IntExpr::Bool(t, _) => { + if t.positive_scale() { + t.transform(1) + } else { + t.transform(0) } - Some(Constraint::ArrayVarIntElement(args, idx, y)) - } - Constraint::DisjunctiveStrict(starts, durations) => { - // return trivialunsatisfiable if overload is detected - let (earliest_start, latest_completion) = - starts.iter().zip(durations.clone()).fold( - (IntVal::MAX, IntVal::MIN), - |(earliest_start, latest_completion), (start, duration)| { - ( - i64::min( - earliest_start.min(self.get_int_lower_bound(start)), - earliest_start, - ), - i64::max( - latest_completion - .max(self.get_int_upper_bound(start) + duration), - latest_completion, - ), - ) - }, - ); - let total_duration = durations.iter().sum::(); - if earliest_start + total_duration > latest_completion { + } + } + } + + fn set_bool(&mut self, var: BoolView) -> Result<(), ReformulationError> { + match var { + BoolView::Lit(l) => Ok(self.cnf.add_clause([l])?), + BoolView::Const(true) => Ok(()), + BoolView::Const(false) => Err(ReformulationError::TrivialUnsatisfiable), + BoolView::IntEq(iv, val) => self.set_int_val(iv.into(), val), + BoolView::IntGreaterEq(iv, val) => self.set_int_lower_bound(iv.into(), val), + BoolView::IntLess(iv, val) => self.set_int_upper_bound(iv.into(), val - 1), + BoolView::IntNotEq(iv, val) => self.set_int_not_eq(iv.into(), val), + } + } + + fn set_int_in_set( + &mut self, + var: IntExpr, + values: &IntSetVal, + ) -> Result<(), ReformulationError> { + match var { + IntExpr::Var(v) => { + let intersect: RangeList<_> = self.int_vars[v].domain.intersect(values); + if intersect.is_empty() { return Err(ReformulationError::TrivialUnsatisfiable); + } else if self.int_vars[v].domain == intersect { + return Ok(()); } - Some(Constraint::DisjunctiveStrict(starts, durations)) - } - Constraint::IntAbs(origin, abs) => { - let lb = self.get_int_lower_bound(&origin); - let ub = self.get_int_upper_bound(&origin); - if ub < 0 { - self.set_int_lower_bound(&abs, -ub, con)?; - self.set_int_upper_bound(&abs, -lb, con)?; - } else if lb >= 0 { - self.set_int_lower_bound(&abs, lb, con)?; - self.set_int_upper_bound(&abs, ub, con)?; - } else { - self.set_int_lower_bound(&abs, 0, con)?; - let abs_max = ub.max(-lb); - self.set_int_upper_bound(&abs, abs_max, con)?; + self.int_vars[v].domain = intersect; + let constraints = self.int_vars[v].constraints.clone(); + for c in constraints { + self.enqueue(c); } - let abs_ub = ub.abs(); - debug_assert!(abs_ub >= 0); - self.set_int_lower_bound(&origin, -abs_ub, con)?; - self.set_int_upper_bound(&abs, abs_ub, con)?; - if lb >= 0 { - // TODO: Unify - Some(Constraint::IntLinEq(vec![origin, -abs], 0)) + Ok(()) + } + IntExpr::Const(v) => { + if !values.contains(&v) { + Err(ReformulationError::TrivialUnsatisfiable) } else { - Some(Constraint::IntAbs(origin, abs)) + Ok(()) } } - Constraint::IntDiv(num, denom, res) => { - self.diff_int_domain(&denom, &RangeList::from(0..=0), con)?; - Some(Constraint::IntDiv(num, denom, res)) + IntExpr::Linear(trans, iv) => { + let values = trans.rev_transform_int_set(values); + self.set_int_in_set(iv.into(), &values) } - Constraint::IntLinLessEq(args, cons) => { - let sum = args - .iter() - .map(|v| self.get_int_lower_bound(v)) - .fold(cons, |sum, val| sum - val); - - for v in &args { - let ub = sum + self.get_int_lower_bound(v); - self.set_int_upper_bound(v, ub, con)?; + IntExpr::Bool(trans, b) => { + let values = trans.rev_transform_int_set(values); + if !values.contains(&0) { + self.set_bool(b)?; + } + if !values.contains(&1) { + self.set_bool(!b)?; } - Some(Constraint::IntLinLessEq(args, cons)) + Ok(()) } - Constraint::IntLinEq(args, cons) => { - let lb_sum = args - .iter() - .map(|v| self.get_int_lower_bound(v)) - .fold(cons, |sum, val| sum - val); + } + } - for v in &args { - let ub = lb_sum + self.get_int_lower_bound(v); - self.set_int_upper_bound(v, ub, con)?; + fn set_int_lower_bound(&mut self, var: IntExpr, lb: IntVal) -> Result<(), ReformulationError> { + match var { + IntExpr::Var(v) => { + let def = &mut self.int_vars[v]; + if lb <= *def.domain.lower_bound().unwrap() { + return Ok(()); + } else if lb > *def.domain.upper_bound().unwrap() { + return Err(ReformulationError::TrivialUnsatisfiable); } - - let ub_sum = args - .iter() - .map(|v| self.get_int_upper_bound(v)) - .fold(cons, |sum, val| sum - val); - - for v in &args { - let lb = ub_sum + self.get_int_upper_bound(v); - self.set_int_lower_bound(v, lb, con)?; + def.domain = RangeList::from_iter(def.domain.iter().filter_map(|r| { + if *r.end() < lb { + None + } else if *r.start() < lb { + Some(lb..=*r.end()) + } else { + Some(r) + } + })); + let constraints = def.constraints.clone(); + for c in constraints { + self.enqueue(c); } - - Some(Constraint::IntLinEq(args, cons)) - } - Constraint::IntTimes(x, y, z) => { - let x_lb = self.get_int_lower_bound(&x); - let x_ub = self.get_int_upper_bound(&x); - let y_lb = self.get_int_lower_bound(&y); - let y_ub = self.get_int_upper_bound(&y); - let z_lb = self.get_int_lower_bound(&z); - let z_ub = self.get_int_upper_bound(&z); - - let bounds = [x_lb * y_lb, x_lb * y_ub, x_ub * y_lb, x_ub * y_ub]; - self.set_int_lower_bound(&z, *bounds.iter().min().unwrap(), con)?; - self.set_int_upper_bound(&z, *bounds.iter().max().unwrap(), con)?; - - if y_lb > 0 || y_ub < 0 { - let bounds = [(z_lb, y_lb), (z_lb, y_ub), (z_ub, y_lb), (z_ub, y_ub)]; - let min = bounds - .iter() - .filter_map(|(z, y)| { - let y = NonZeroIntVal::new(*y)?; - Some(div_ceil(*z, y)) - }) - .min() - .unwrap(); - self.set_int_lower_bound(&x, min, con)?; - - let max = bounds - .iter() - .filter_map(|(z, y)| { - let y = NonZeroIntVal::new(*y)?; - Some(div_floor(*z, y)) - }) - .max() - .unwrap(); - self.set_int_upper_bound(&x, max, con)?; + Ok(()) + } + IntExpr::Const(v) => { + if v < lb { + Err(ReformulationError::TrivialUnsatisfiable) + } else { + Ok(()) } - - if x_lb > 0 || x_ub < 0 { - let bounds = [(z_lb, x_lb), (z_lb, x_ub), (z_ub, x_lb), (z_ub, x_ub)]; - let min = bounds - .iter() - .filter_map(|(z, x)| { - let x = NonZeroIntVal::new(*x)?; - Some(div_ceil(*z, x)) - }) - .min() - .unwrap(); - self.set_int_lower_bound(&y, min, con)?; - - let max = bounds - .iter() - .filter_map(|(z, x)| { - let x = NonZeroIntVal::new(*x)?; - Some(div_floor(*z, x)) - }) - .max() - .unwrap(); - self.set_int_upper_bound(&y, max, con)?; + } + IntExpr::Linear(trans, iv) => { + match trans.rev_transform_lit(LitMeaning::GreaterEq(lb)) { + Ok(LitMeaning::GreaterEq(val)) => self.set_int_lower_bound(iv.into(), val), + Ok(LitMeaning::Less(val)) => self.set_int_upper_bound(iv.into(), val - 1), + _ => unreachable!(), } + } + IntExpr::Bool(trans, b) => match trans.rev_transform_lit(LitMeaning::GreaterEq(lb)) { + Ok(LitMeaning::GreaterEq(1)) => self.set_bool(b), + Ok(LitMeaning::GreaterEq(val)) if val >= 2 => { + Err(ReformulationError::TrivialUnsatisfiable) + } + Ok(LitMeaning::GreaterEq(_)) => Ok(()), + Ok(LitMeaning::Less(1)) => self.set_bool(!b), + Ok(LitMeaning::Less(val)) if val <= 0 => { + Err(ReformulationError::TrivialUnsatisfiable) + } + Ok(LitMeaning::Less(_)) => Ok(()), + _ => unreachable!(), + }, + } + } - Some(Constraint::IntTimes(x, y, z)) - } - Constraint::TableInt(vars, table) => { - debug_assert!(!vars.is_empty()); - if vars.len() == 1 { - let dom = table.into_iter().map(|v| v[0]..=v[0]).collect(); - self.intersect_int_domain(&vars[0], &dom, con)?; - None - } else { - // Remove any tuples that contain values outside of the domain of the - // variables. - let table = table - .into_iter() - .filter(|tup| { - tup.iter() - .enumerate() - .all(|(j, val)| self.check_int_in_domain(&vars[j], *val)) - }) - .collect_vec(); - - // If no tuples remain, then the problem is trivially unsatisfiable. - if table.is_empty() { - return Err(ReformulationError::TrivialUnsatisfiable); - } - - // Restrict the domain of the variables to the values it can take in the - // tuple. - if table.len() == 1 { - for (j, var) in vars.iter().enumerate() { - self.set_int_value(var, table[0][j], con)?; - } + fn set_int_upper_bound(&mut self, var: IntExpr, ub: IntVal) -> Result<(), ReformulationError> { + match var { + IntExpr::Var(v) => { + let def = &mut self.int_vars[v]; + if ub >= *def.domain.upper_bound().unwrap() { + return Ok(()); + } else if ub < *def.domain.lower_bound().unwrap() { + return Err(ReformulationError::TrivialUnsatisfiable); + } + def.domain = RangeList::from_iter(def.domain.iter().filter_map(|r| { + if ub < *r.start() { None + } else if ub < *r.end() { + Some(*r.start()..=ub) } else { - for (j, var) in vars.iter().enumerate() { - let dom = (0..table.len()) - .map(|i| table[i][j]..=table[i][j]) - .collect(); - self.intersect_int_domain(var, &dom, con)?; - } - Some(Constraint::TableInt(vars, table)) + Some(r) } + })); + let constraints = def.constraints.clone(); + for c in constraints { + self.enqueue(c); } + Ok(()) } - con => Some(con), - }; - match simplified { - Some(simplified) => self.constraints[con] = simplified, - None => { - self.constraints[con] = - Constraint::PropLogic(BoolExpr::View(BoolView::Const(true))); + IntExpr::Const(v) => { + if v > ub { + Err(ReformulationError::TrivialUnsatisfiable) + } else { + Ok(()) + } } + IntExpr::Linear(trans, iv) => match trans.rev_transform_lit(LitMeaning::Less(ub + 1)) { + Ok(LitMeaning::GreaterEq(val)) => self.set_int_lower_bound(iv.into(), val), + Ok(LitMeaning::Less(val)) => self.set_int_upper_bound(iv.into(), val - 1), + _ => unreachable!(), + }, + IntExpr::Bool(trans, b) => match trans.rev_transform_lit(LitMeaning::Less(ub + 1)) { + Ok(LitMeaning::GreaterEq(1)) => self.set_bool(b), + Ok(LitMeaning::GreaterEq(val)) if val >= 2 => { + Err(ReformulationError::TrivialUnsatisfiable) + } + Ok(LitMeaning::GreaterEq(_)) => Ok(()), + Ok(LitMeaning::Less(1)) => self.set_bool(!b), + Ok(LitMeaning::Less(val)) if val <= 0 => { + Err(ReformulationError::TrivialUnsatisfiable) + } + Ok(LitMeaning::Less(_)) => Ok(()), + _ => unreachable!(), + }, } - Ok(()) } - /// Subscribe the constraint located at index `con` to changes in the - /// variables it depends on. - pub(crate) fn subscribe(&mut self, con: usize) { - match &self.constraints[con] { - Constraint::ArrayIntMaximum(args, m) | Constraint::ArrayIntMinimum(args, m) => { - for a in args { - if let IntView::Var(a) = a { - self.int_vars[a.0 as usize].constraints.push(con); + fn set_int_val(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError> { + match var { + IntExpr::Var(v) => { + let def = &mut self.int_vars[v]; + if def.domain.contains(&val) { + def.domain = RangeList::from(val..=val); + let constraints = def.constraints.clone(); + for c in constraints { + self.enqueue(c); } + Ok(()) + } else { + Err(ReformulationError::TrivialUnsatisfiable) + } + } + IntExpr::Const(i) if i == val => Ok(()), + IntExpr::Const(_) => Err(ReformulationError::TrivialUnsatisfiable), + IntExpr::Linear(trans, iv) => match trans.rev_transform_lit(LitMeaning::Eq(val)) { + Ok(LitMeaning::Eq(val)) => self.set_int_val(iv.into(), val), + Err(b) => { + debug_assert!(!b); + Err(ReformulationError::TrivialUnsatisfiable) + } + _ => unreachable!(), + }, + IntExpr::Bool(trans, b) => match trans.rev_transform_lit(LitMeaning::Eq(val)) { + Ok(LitMeaning::Eq(val)) => match val { + 0 => self.set_bool(!b), + 1 => self.set_bool(b), + _ => Err(ReformulationError::TrivialUnsatisfiable), + }, + Err(b) => { + debug_assert!(!b); + Err(ReformulationError::TrivialUnsatisfiable) + } + _ => unreachable!(), + }, + } + } + + fn set_int_not_eq(&mut self, var: IntExpr, val: IntVal) -> Result<(), ReformulationError> { + self.set_int_in_set(var, &(val..=val).into()) + } + + fn set_int_not_in_set( + &mut self, + var: IntExpr, + values: &IntSetVal, + ) -> Result<(), ReformulationError> { + match var { + IntExpr::Var(v) => { + let diff: RangeList<_> = self.int_vars[v].domain.diff(values); + if diff.is_empty() { + return Err(ReformulationError::TrivialUnsatisfiable); + } else if self.int_vars[v].domain == diff { + return Ok(()); } - if let IntView::Var(m) = m { - self.int_vars[m.0 as usize].constraints.push(con); + self.int_vars[v].domain = diff; + let constraints = self.int_vars[v].constraints.clone(); + for c in constraints { + self.enqueue(c); } + Ok(()) } - Constraint::ArrayVarIntElement(args, idx, y) => { - for a in args { - if let IntView::Var(a) = a { - self.int_vars[a.0 as usize].constraints.push(con); - } + IntExpr::Const(v) => { + if values.contains(&v) { + Err(ReformulationError::TrivialUnsatisfiable) + } else { + Ok(()) } - if let IntView::Var(y) = y { - self.int_vars[y.0 as usize].constraints.push(con); + } + IntExpr::Linear(trans, iv) => { + let mask = trans.rev_transform_int_set(values); + self.set_int_not_in_set(iv.into(), &mask) + } + IntExpr::Bool(trans, b) => { + let values = trans.rev_transform_int_set(values); + if values.contains(&0) { + self.set_bool(b)?; } - if let IntView::Var(idx) = idx { - self.int_vars[idx.0 as usize].constraints.push(con); + if values.contains(&1) { + self.set_bool(!b)?; } + Ok(()) } - _ => {} } } } diff --git a/crates/huub/src/model/flatzinc.rs b/crates/huub/src/model/flatzinc.rs index 40e67f5..6c678ea 100644 --- a/crates/huub/src/model/flatzinc.rs +++ b/crates/huub/src/model/flatzinc.rs @@ -5,6 +5,7 @@ use std::{ collections::{hash_map::Entry, HashMap, HashSet}, fmt::{Debug, Display}, hash::Hash, + iter::once, ops::Deref, rc::Rc, }; @@ -14,21 +15,26 @@ use flatzinc_serde::{ Literal, Type, }; use itertools::Itertools; -use pindakaas::{solver::propagation::PropagatingSolver, Cnf}; +use pindakaas::{propositional_logic::Formula, solver::propagation::PropagatingSolver, Cnf}; use rangelist::{IntervalIterator, RangeList}; use thiserror::Error; use tracing::warn; use crate::{ + actions::SimplificationActions, + all_different_int, array_int_element, array_int_maximum, array_int_minimum, + array_var_bool_element, array_var_int_element, + constraints::table_int::TableInt, + disjunctive_strict, int_abs, int_div, int_pow, int_times, model::{ bool::BoolView, branching::{Branching, ValueSelection, VariableSelection}, - int::IntView, - reformulate::ReformulationError, - ModelView, + int::IntExpr, + reformulate::{ModelView, ReformulationError}, }, + set_in_reif, solver::engine::Engine, - BoolExpr, Constraint, InitConfig, IntSetVal, IntVal, Model, NonZeroIntVal, Solver, SolverView, + table_int, InitConfig, IntLinExpr, IntSetVal, IntVal, Model, NonZeroIntVal, Solver, SolverView, }; #[derive(Error, Debug)] @@ -265,7 +271,7 @@ where Ok(( vars.into_iter() .zip(vals) - .map(|(var, val)| BoolView::IntEq(Box::new(var), val)) + .map(|(var, val)| var.eq(val)) .collect(), Vec::new(), )) @@ -396,7 +402,7 @@ where /// Extract a integer decision variable from the an [`Argument`] in a /// [`FlatZinc`] instance. A [`FlatZincError::InvalidArgumentType`] will be /// returned if the argument was not a integer decision variable. - fn arg_int(&mut self, arg: &Argument) -> Result { + fn arg_int(&mut self, arg: &Argument) -> Result { match arg { Argument::Literal(l) => self.lit_int(l), _ => Err(FlatZincError::InvalidArgumentType { @@ -439,13 +445,12 @@ where /// [`Constraint::TableInt`] constraints. fn convert_regular_to_tables( &mut self, - vars: Vec, + vars: Vec, transitions: Vec>, init_state: IntVal, accept_states: HashSet, - ) -> Vec { + ) -> Vec { // TODO: Add the regular checking - // let mut table_constraints = Vec::new(); let mut start: Vec> = Vec::new(); @@ -481,30 +486,23 @@ where .prb .new_int_vars(vars.len() - 1, (1..=transitions.len() as IntVal).into()) .into_iter() - .map(IntView::from) + .map(IntExpr::from) .collect_vec(); // Add table constraint to force a transition for the starting state - let sx: Vec = vec![vars[0].clone(), state_vars[0].clone()]; - table_constraints.push(Constraint::TableInt(sx, start)); + let sx: Vec = vec![vars[0], state_vars[0]]; + table_constraints.push(table_int(sx, start)); // Add table constraint to force valid transition for the intermediate // states for i in 1..vars.len() - 1 { - let mx: Vec = vec![ - state_vars[i - 1].clone(), - vars[i].clone(), - state_vars[i].clone(), - ]; - table_constraints.push(Constraint::TableInt(mx, middle.clone())); + let mx: Vec = vec![state_vars[i - 1], vars[i], state_vars[i]]; + table_constraints.push(table_int(mx, middle.clone())); } // Add table constraint to force ending in an accepting state - let ex: Vec = vec![ - state_vars.last().unwrap().clone(), - vars.last().unwrap().clone(), - ]; - table_constraints.push(Constraint::TableInt(ex, end)); + let ex: Vec = vec![*state_vars.last().unwrap(), *vars.last().unwrap()]; + table_constraints.push(table_int(ex, end)); table_constraints } @@ -576,7 +574,7 @@ where } me.arg_bool(arg) }; - let lit_int_view = |me: &mut Self, lit: &Literal| -> Result { + let lit_int_view = |me: &mut Self, lit: &Literal| -> Result { if let Literal::Identifier(x) = lit { if !me.map.contains_key(x) && defined_by.contains_key(x) { me.extract_view(defined_by, defined_by[x])?; @@ -592,7 +590,7 @@ where if let [b, Argument::Literal(Literal::Identifier(x))] = c.args.as_slice() { if x == l { let b = arg_bool_view(self, b)?; - add_view(self, l.clone(), IntView::from(b).into()); + add_view(self, l.clone(), IntExpr::from(b).into()); } } } @@ -612,7 +610,7 @@ where if r == l => { let x = lit_int_view(self, x)?; - add_view(self, l.clone(), BoolView::IntEq(Box::new(x), *i).into()); + add_view(self, l.clone(), x.eq(*i).into()); } _ => {} }, @@ -621,17 +619,13 @@ where if r == l => { let x = lit_int_view(self, x)?; - add_view( - self, - l.clone(), - BoolView::IntGreaterEq(Box::new(x), *i).into(), - ); + add_view(self, l.clone(), x.geq(*i).into()); } [Argument::Literal(x), Argument::Literal(Literal::Int(i)), Argument::Literal(Literal::Identifier(r))] if r == l => { let x = lit_int_view(self, x)?; - add_view(self, l.clone(), BoolView::IntLessEq(Box::new(x), *i).into()); + add_view(self, l.clone(), x.leq(*i).into()); } _ => {} }, @@ -641,7 +635,7 @@ where if r == l => { let x = lit_int_view(self, x)?; - add_view(self, l.clone(), BoolView::IntNotEq(Box::new(x), *i).into()); + add_view(self, l.clone(), x.ne(*i).into()); } _ => {} }, @@ -675,7 +669,7 @@ where let y = lit_int_view(self, vy)?; y * scale + offset } else { - IntView::Const(offset) + IntExpr::Const(offset) }; add_view(self, l.clone(), view.into()); } @@ -732,7 +726,7 @@ where /// Extract a integer decision variable from a [`Literal`] in a [`FlatZinc`] /// instance. A [`FlatZincError::InvalidArgumentType`] will be returned if the /// argument was not a integer decision variable. - fn lit_int(&mut self, lit: &Literal) -> Result { + fn lit_int(&mut self, lit: &Literal) -> Result { match lit { Literal::Identifier(ident) => self.lookup_or_create_var(ident).map(|mv| match mv { ModelView::Int(iv) => Ok(iv), @@ -741,8 +735,8 @@ where found: "bool".to_owned(), }), })?, - Literal::Bool(v) => Ok(IntView::Const(if *v { 1 } else { 0 })), - Literal::Int(v) => Ok(IntView::Const(*v)), + Literal::Bool(v) => Ok(IntExpr::Const(if *v { 1 } else { 0 })), + Literal::Int(v) => Ok(IntExpr::Const(*v)), _ => todo!(), } } @@ -873,7 +867,7 @@ where .iter() .map(|l| self.lit_bool(l).map(Into::into)) .collect(); - self.prb += BoolExpr::Equiv(vec![r.into(), BoolExpr::And(es?)]); + self.prb += Formula::Equiv(vec![r.into(), Formula::And(es?)]); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_bool_and", @@ -885,11 +879,11 @@ where "array_bool_xor" => { if let [es] = c.args.as_slice() { let es = self.arg_array(es)?; - let es: Result, _> = es + let es: Vec> = es .iter() .map(|l| self.lit_bool(l).map(Into::into)) - .collect(); - self.prb += BoolExpr::Xor(es?); + .try_collect()?; + self.prb += Formula::Xor(es); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_bool_xor", @@ -927,8 +921,7 @@ where } assert_ne!(ranges.len(), 0, "unexpected empty range list"); - self.prb += - Constraint::SetInReif(idx, RangeList::from_iter(ranges), val.into()); + self.prb += set_in_reif(idx, RangeList::from_iter(ranges), val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_bool_element", @@ -946,7 +939,7 @@ where .collect(); let idx = self.arg_int(idx)?; let val = self.arg_int(val)?; - self.prb += Constraint::ArrayIntElement(arr?, idx, val); + self.prb += array_int_element(idx - 1, arr?, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_int_element", @@ -957,18 +950,15 @@ where } "array_var_bool_element" => { if let [idx, arr, val] = c.args.as_slice() { - let arr: Result, FlatZincError> = self + let arr = self .arg_array(arr)? .iter() - .map(|l| { - let x: BoolView = self.lit_bool(l)?; - Ok(x.into()) - }) - .collect(); + .map(|l| self.lit_bool(l)) + .try_collect()?; let idx = self.arg_int(idx)?; let val = self.arg_bool(val)?; - self.prb += Constraint::ArrayVarBoolElement(arr?, idx, val.into()); + self.prb += array_var_bool_element(idx - 1, arr, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_var_bool_element", @@ -986,7 +976,7 @@ where .collect(); let idx = self.arg_int(idx)?; let val = self.arg_int(val)?; - self.prb += Constraint::ArrayVarIntElement(arr?, idx, val); + self.prb += array_var_int_element(idx - 1, arr?, val); } else { return Err(FlatZincError::InvalidNumArgs { name: "array_var_int_element", @@ -999,7 +989,7 @@ where if let [b, i] = c.args.as_slice() { let b = self.arg_bool(b)?; let i = self.arg_int(i)?; - self.prb += Constraint::IntLinEq(vec![b.into(), -i], 0); + self.prb += (IntExpr::from(b) - i).eq(0); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool2int", @@ -1021,15 +1011,17 @@ where .map(|l| self.lit_bool(l)) .try_collect()?; let sum = self.arg_int(sum)?; - let vars: Vec = vars + + let lin_exp: IntLinExpr = vars .into_iter() .zip(coeffs.into_iter()) .filter_map(|(x, c)| { - NonZeroIntVal::new(c).map(|c| IntView::from(x) * c) + NonZeroIntVal::new(c).map(|c| IntExpr::from(x) * c) }) - .chain(Some(-sum)) - .collect(); - self.prb += Constraint::IntLinEq(vars, 0); + .chain(once(-sum)) + .sum(); + + self.prb += lin_exp.eq(0); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool_lin_eq", @@ -1051,7 +1043,7 @@ where let e = self.lit_bool(l)?; lits.push((!e).into()); } - self.prb += BoolExpr::Or(lits); + self.prb += Formula::Or(lits); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool_clause", @@ -1065,9 +1057,9 @@ where let a = self.arg_bool(a)?; let b = self.arg_bool(b)?; let r = self.arg_bool(r)?; - self.prb += BoolExpr::Equiv(vec![ + self.prb += Formula::Equiv(vec![ r.into(), - BoolExpr::Equiv(vec![a.into(), b.into()]), + Formula::Equiv(vec![a.into(), b.into()]), ]); } else { return Err(FlatZincError::InvalidNumArgs { @@ -1081,7 +1073,7 @@ where if let [a, b] = c.args.as_slice() { let a = self.arg_bool(a)?; let b = self.arg_bool(b)?; - self.prb += BoolExpr::Equiv(vec![b.into(), (!a).into()]); + self.prb += Formula::Equiv(vec![b.into(), (!a).into()]); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool_not", @@ -1094,10 +1086,10 @@ where if (2..=3).contains(&c.args.len()) { let a = self.arg_bool(&c.args[0])?; let b = self.arg_bool(&c.args[1])?; - let mut f = BoolExpr::Xor(vec![a.into(), b.into()]); + let mut f = Formula::Xor(vec![a.into(), b.into()]); if c.args.len() == 3 { let r = self.arg_bool(&c.args[2])?; - f = BoolExpr::Equiv(vec![r.into(), f]); + f = Formula::Equiv(vec![r.into(), f]); } self.prb += f; } else { @@ -1113,7 +1105,7 @@ where let args = self.arg_array(args)?; let args: Result, _> = args.iter().map(|l| self.lit_int(l)).collect(); - self.prb += Constraint::AllDifferentInt(args?); + self.prb += all_different_int(args?); } else { return Err(FlatZincError::InvalidNumArgs { name: "huub_all_different", @@ -1130,9 +1122,9 @@ where args.iter().map(|l| self.lit_int(l)).collect(); let m = self.arg_int(m)?; if is_maximum { - self.prb += Constraint::ArrayIntMaximum(args?, m); + self.prb += array_int_maximum(args?, m); } else { - self.prb += Constraint::ArrayIntMinimum(args?, m); + self.prb += array_int_minimum(args?, m); } } else { return Err(FlatZincError::InvalidNumArgs { @@ -1160,7 +1152,7 @@ where let e = self.lit_bool(l)?; lits.push((!e).into()); } - self.prb += BoolExpr::Equiv(vec![r.into(), BoolExpr::Or(lits)]); + self.prb += Formula::Equiv(vec![r.into(), Formula::Or(lits)]); } else { return Err(FlatZincError::InvalidNumArgs { name: "bool_clause_reif", @@ -1171,7 +1163,7 @@ where } "huub_disjunctive_strict" => { if let [starts, durations] = c.args.as_slice() { - let starts = self + let start_times = self .arg_array(starts)? .iter() .map(|l| self.lit_int(l)) @@ -1181,7 +1173,7 @@ where .iter() .map(|l| self.par_int(l)) .try_collect()?; - self.prb += Constraint::DisjunctiveStrict(starts, durations); + self.prb += disjunctive_strict(start_times, durations); } else { return Err(FlatZincError::InvalidNumArgs { name: "huub_disjunctive_strict", @@ -1257,7 +1249,7 @@ where .into_iter() .map(|c| c.collect()) .collect(); - self.prb += Constraint::TableInt(args, table); + self.prb += table_int(args, table); } else { return Err(FlatZincError::InvalidNumArgs { name: "huub_table_int", @@ -1270,7 +1262,7 @@ where if let [origin, abs] = c.args.as_slice() { let origin = self.arg_int(origin)?; let abs = self.arg_int(abs)?; - self.prb += Constraint::IntAbs(origin, abs); + self.prb += int_abs(origin, abs); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_abs", @@ -1284,7 +1276,7 @@ where let num = self.arg_int(num)?; let denom = self.arg_int(denom)?; let res = self.arg_int(res)?; - self.prb += Constraint::IntDiv(num, denom, res); + self.prb += int_div(num, denom, res); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_div", @@ -1293,27 +1285,23 @@ where }); } } - "int_le" => { - if let [a, b] = c.args.as_slice() { - let a = self.arg_int(a)?; - let b = self.arg_int(b)?; - self.prb += Constraint::IntLinLessEq(vec![a, -b], 0); - } else { - return Err(FlatZincError::InvalidNumArgs { - name: "int_le", - found: c.args.len(), - expected: 2, - }); - } - } - "int_ne" => { + "int_le" | "int_ne" => { if let [a, b] = c.args.as_slice() { let a = self.arg_int(a)?; let b = self.arg_int(b)?; - self.prb += Constraint::IntLinNotEq(vec![a, -b], 0); + let lin_exp = a - b; + self.prb += match c.id.deref() { + "int_le" => lin_exp.leq(0), + "int_ne" => lin_exp.ne(0), + _ => unreachable!(), + }; } else { return Err(FlatZincError::InvalidNumArgs { - name: "int_ne", + name: match c.id.deref() { + "int_le" => "int_le", + "int_ne" => "int_ne", + _ => unreachable!(), + }, found: c.args.len(), expected: 2, }); @@ -1325,15 +1313,19 @@ where let a = self.arg_int(a)?; let b = self.arg_int(b)?; let r = self.arg_bool(r)?; + + let lin_exp = a - b; + let lin = match c.id.deref() { + "int_eq_imp" | "int_eq_reif" => lin_exp.eq(0), + "int_le_imp" | "int_le_reif" => lin_exp.leq(0), + "int_ne_imp" | "int_ne_reif" => lin_exp.ne(0), + _ => unreachable!(), + }; self.prb += match c.id.deref() { - "int_eq_imp" => Constraint::IntLinEqImp, - "int_eq_reif" => Constraint::IntLinEqReif, - "int_le_imp" => Constraint::IntLinLessEqImp, - "int_le_reif" => Constraint::IntLinLessEqReif, - "int_ne_imp" => Constraint::IntLinNotEqImp, - "int_ne_reif" => Constraint::IntLinNotEqReif, + "int_eq_imp" | "int_le_imp" | "int_ne_imp" => lin.implied_by(r), + "int_eq_reif" | "int_le_reif" | "int_ne_reif" => lin.reified_by(r), _ => unreachable!(), - }(vec![a, -b], 0, r.into()); + }; } else { return Err(FlatZincError::InvalidNumArgs { name: match c.id.deref() { @@ -1363,18 +1355,18 @@ where .map(|l| self.lit_int(l)) .try_collect()?; let rhs = self.arg_par_int(rhs)?; - let vars: Vec = vars + let lin_exp: IntLinExpr = vars .into_iter() .zip(coeffs.into_iter()) .filter_map(|(x, c)| NonZeroIntVal::new(c).map(|c| x * c)) - .collect(); + .sum(); self.prb += match c.id.deref() { - "int_lin_eq" => Constraint::IntLinEq, - "int_lin_le" => Constraint::IntLinLessEq, - "int_lin_ne" => Constraint::IntLinNotEq, + "int_lin_eq" => lin_exp.eq(rhs), + "int_lin_le" => lin_exp.leq(rhs), + "int_lin_ne" => lin_exp.ne(rhs), _ => unreachable!(), - }(vars, rhs); + }; } else { return Err(FlatZincError::InvalidNumArgs { name: match c.id.deref() { @@ -1403,20 +1395,27 @@ where .try_collect()?; let rhs = self.arg_par_int(rhs)?; let reified = self.arg_bool(reified)?; - let vars: Vec = vars + let lin_exp: IntLinExpr = vars .into_iter() .zip(coeffs.into_iter()) .filter_map(|(x, c)| NonZeroIntVal::new(c).map(|c| x * c)) - .collect(); + .sum(); + + let lin = match c.id.deref() { + "int_lin_eq_imp" | "int_lin_eq_reif" => lin_exp.eq(rhs), + "int_lin_le_imp" | "int_lin_le_reif" => lin_exp.leq(rhs), + "int_lin_ne_imp" | "int_lin_ne_reif" => lin_exp.ne(rhs), + _ => unreachable!(), + }; self.prb += match c.id.deref() { - "int_lin_eq_imp" => Constraint::IntLinEqImp, - "int_lin_eq_reif" => Constraint::IntLinEqReif, - "int_lin_le_imp" => Constraint::IntLinLessEqImp, - "int_lin_le_reif" => Constraint::IntLinLessEqReif, - "int_lin_ne_imp" => Constraint::IntLinNotEqImp, - "int_lin_ne_reif" => Constraint::IntLinNotEqReif, + "int_lin_eq_imp" | "int_lin_le_imp" | "int_lin_ne_imp" => { + lin.implied_by(reified) + } + "int_lin_eq_reif" | "int_lin_le_reif" | "int_lin_ne_reif" => { + lin.reified_by(reified) + } _ => unreachable!(), - }(vars, rhs, reified.into()); + }; } else { return Err(FlatZincError::InvalidNumArgs { name: match c.id.deref() { @@ -1440,9 +1439,9 @@ where let b = self.arg_int(b)?; let m = self.arg_int(m)?; if is_maximum { - self.prb += Constraint::ArrayIntMaximum(vec![a, b], m); + self.prb += array_int_maximum(vec![a, b], m); } else { - self.prb += Constraint::ArrayIntMinimum(vec![a, b], m); + self.prb += array_int_minimum(vec![a, b], m); } } else { return Err(FlatZincError::InvalidNumArgs { @@ -1457,8 +1456,7 @@ where let base = self.arg_int(base)?; let exponent = self.arg_int(exponent)?; let res = self.arg_int(res)?; - - self.prb += Constraint::IntPow(base, exponent, res); + self.prb += int_pow(base, exponent, res); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_pow", @@ -1472,7 +1470,7 @@ where let a = self.arg_int(x)?; let b = self.arg_int(y)?; let m = self.arg_int(z)?; - self.prb += Constraint::IntTimes(a, b, m); + self.prb += int_times(a, b, m); } else { return Err(FlatZincError::InvalidNumArgs { name: "int_times", @@ -1486,8 +1484,7 @@ where let x = self.arg_int(x)?; let s = self.arg_par_set(s)?; - self.prb - .intersect_int_domain(&x, &s, self.prb.constraints.len())?; + self.prb.set_int_in_set(x, &s)?; } else { return Err(FlatZincError::InvalidNumArgs { name: "set_in", @@ -1502,7 +1499,7 @@ where let s = self.arg_par_set(s)?; let r = self.arg_bool(r)?; - self.prb += Constraint::SetInReif(x, s, r.into()); + self.prb += set_in_reif(x, s, r); } else { return Err(FlatZincError::InvalidNumArgs { name: "set_in_reif", @@ -1594,7 +1591,7 @@ where let arr = self.arg_array(arr)?; let idx = self.arg_int(idx)?; // unify if the index is constant - if let IntView::Const(idx) = idx { + if let IntExpr::Const(idx) = idx { let a = &arr[(idx - 1) as usize]; record_unify(&mut unify_map, a, b); mark_processed(self); @@ -1704,7 +1701,7 @@ where unreachable!() }; self.prb += - BoolExpr::Equiv(vec![new.into(), existing.into()]); + Formula::Equiv(vec![new.into(), existing.into()]); } Type::Int => { let (ModelView::Int(new), ModelView::Int(existing)) = @@ -1712,8 +1709,7 @@ where else { unreachable!() }; - self.prb += - Constraint::IntLinEq(vec![new, existing * -1], 0); + self.prb += (new - existing).eq(0); } _ => unreachable!(), } diff --git a/crates/huub/src/model/int.rs b/crates/huub/src/model/int.rs index e447b08..499f201 100644 --- a/crates/huub/src/model/int.rs +++ b/crates/huub/src/model/int.rs @@ -1,20 +1,21 @@ //! Representation and manipulation of integer decision variable in [`Model`]. -use std::ops::{Add, Mul, Neg}; +use std::ops::{Add, Mul, Neg, Sub}; -use pindakaas::{solver::propagation::PropagatingSolver, ClauseDatabase}; -use rangelist::{IntervalIterator, RangeList}; +use index_vec::define_index_type; +use pindakaas::solver::propagation::PropagatingSolver; use crate::{ helpers::linear_transform::LinearTransform, model::{bool::BoolView, reformulate::VariableMap}, solver::{engine::Engine, view}, - IntSetVal, IntVal, LitMeaning, Model, NonZeroIntVal, ReformulationError, Solver, + IntLinExpr, IntSetVal, IntVal, LitMeaning, NonZeroIntVal, Solver, }; -#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)] -/// Reference type for integer decision variables in a [`Model`]. -pub struct IntVar(pub(crate) u32); +define_index_type! { + /// Reference type for integer decision variables in a [`Model`]. + pub struct IntVar = u32; +} #[derive(Debug, Clone, PartialEq, Eq, Hash)] /// Defintition of an integer decision variable in a [`Model`]. @@ -28,9 +29,9 @@ pub(crate) struct IntVarDef { pub(crate) constraints: Vec, } -#[derive(Clone, Debug, PartialEq, Eq, Hash)] +#[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] /// A reference to an integer value or its transformation in a [`Model`]. -pub enum IntView { +pub enum IntExpr { /// Direct reference to an integer variable. Var(IntVar), /// Constant integer value. @@ -51,31 +52,157 @@ impl IntVarDef { } } -impl IntView { - /// Get the [`view::IntView`] to which the `IntView` will be mapped. - pub(crate) fn to_arg>( +impl IntExpr { + /// Get the [`view::IntView`] to which the expression will be mapped. + pub(crate) fn as_solver_arg>( &self, slv: &mut Solver, map: &mut VariableMap, ) -> view::IntView { - map.get_int(slv, self) + map.get_int(slv, *self) + } + + /// Get a Boolean view that represent whether the integer view is equal to the + /// given value. + pub fn eq(&self, v: IntVal) -> BoolView { + match self { + &Self::Var(x) => BoolView::IntEq(x, v), + &Self::Const(c) => BoolView::Const(c == v), + &Self::Linear(t, x) => match t.rev_transform_lit(LitMeaning::Eq(v)) { + Ok(LitMeaning::Eq(val)) => BoolView::IntEq(x, val), + Err(b) => { + // After the transformation, the value `v` does not remain an integer. + debug_assert!(!b); + BoolView::Const(false) + } + _ => unreachable!(), + }, + &Self::Bool(t, x) => match t.rev_transform_lit(LitMeaning::Eq(v)) { + Ok(LitMeaning::Eq(1)) => x, + Ok(LitMeaning::Eq(0)) => !x, + Ok(LitMeaning::Eq(_)) /* if val != 0 */ => BoolView::Const(false), + _ => unreachable!(), + }, + } + } + + /// Get a Boolean view that represent whether the integer view is greater than + /// the given value. + pub fn gt(&self, v: IntVal) -> BoolView { + self.geq(v + 1) + } + + /// Get a Boolean view that represent whether the integer view is greater than + /// or equal to the given value. + pub fn geq(&self, v: IntVal) -> BoolView { + match self { + &Self::Var(x) => BoolView::IntGreaterEq(x, v), + &Self::Const(c) => BoolView::Const(c >= v), + &Self::Linear(t, x) => match t.rev_transform_lit(LitMeaning::GreaterEq(v)) { + Ok(LitMeaning::GreaterEq(val)) => BoolView::IntGreaterEq(x, val), + Ok(LitMeaning::Less(val)) => BoolView::IntLess(x, val), + _ => unreachable!(), + }, + &Self::Bool(t, x) => match t.rev_transform_lit(LitMeaning::GreaterEq(v)) { + Ok(LitMeaning::GreaterEq(1)) => x, + Ok(LitMeaning::GreaterEq(val)) if val > 1 => BoolView::Const(true), + Ok(LitMeaning::GreaterEq(_)) /* if val <= 0 */ => BoolView::Const(false), + Ok(LitMeaning::Less(1)) => !x, + Ok(LitMeaning::Less(val)) if val > 1 => BoolView::Const(false), + Ok(LitMeaning::Less(_)) /* if val <= 0 */ => BoolView::Const(true), + _ => unreachable!(), + }, + } + } + + /// Get a Boolean view that represent whether the integer view is less than + /// the given value. + pub fn lt(&self, v: IntVal) -> BoolView { + match self { + &Self::Var(x) => BoolView::IntLess(x, v), + &Self::Const(c) => BoolView::Const(c <= v), + &Self::Linear(t, x) => match t.rev_transform_lit(LitMeaning::Less(v)) { + Ok(LitMeaning::GreaterEq(val)) => BoolView::IntGreaterEq(x, val), + Ok(LitMeaning::Less(val)) => BoolView::IntLess(x, val), + _ => unreachable!(), + }, + &Self::Bool(t, x) => match t.rev_transform_lit(LitMeaning::Less(v)) { + Ok(LitMeaning::GreaterEq(1)) => x, + Ok(LitMeaning::GreaterEq(val)) if val > 1 => BoolView::Const(false), + Ok(LitMeaning::GreaterEq(_)) /* if val <= 0 */ => BoolView::Const(true), + Ok(LitMeaning::Less(1)) => !x, + Ok(LitMeaning::Less(val)) if val > 1 => BoolView::Const(true), + Ok(LitMeaning::Less(_)) /* if val <= 0 */ => BoolView::Const(false), + _ => unreachable!(), + }, + } + } + + /// Get a Boolean view that represent whether the integer view is less than or + /// equal to the given value. + pub fn leq(&self, v: IntVal) -> BoolView { + self.lt(v + 1) + } + + /// Get a Boolean view that represent whether the integer view is not equal to + /// the given value. + pub fn ne(&self, v: IntVal) -> BoolView { + match self { + &Self::Var(x) => BoolView::IntNotEq(x, v), + &Self::Const(c) => BoolView::Const(c != v), + &Self::Linear(t, x) => match t.rev_transform_lit(LitMeaning::NotEq(v)) { + Ok(LitMeaning::NotEq(val)) => BoolView::IntNotEq(x, val), + Err(b) => { + // After the transformation, the value `v` does not remain an integer. + debug_assert!(b); + BoolView::Const(true) + } + _ => unreachable!(), + }, + &Self::Bool(t, x) => match t.rev_transform_lit(LitMeaning::NotEq(v)) { + Ok(LitMeaning::NotEq(1)) => !x, + Ok(LitMeaning::NotEq(0)) => x, + Ok(LitMeaning::NotEq(_)) /* if val != 0 */ => BoolView::Const(true), + _ => unreachable!(), + }, + } + } +} + +impl Add for IntExpr { + type Output = IntLinExpr; + + fn add(self, rhs: IntExpr) -> Self::Output { + IntLinExpr { + terms: vec![self, rhs], + } } } -impl Add for IntView { +impl Add for IntExpr { type Output = Self; fn add(self, rhs: IntVal) -> Self::Output { + if rhs == 0 { + return self; + } match self { Self::Var(x) => Self::Linear(LinearTransform::offset(rhs), x), Self::Const(v) => Self::Const(v + rhs), - Self::Linear(t, x) => Self::Linear(t + rhs, x), + Self::Linear(t, x) => { + let t = t + rhs; + if t.is_identity() { + Self::Var(x) + } else { + Self::Linear(t, x) + } + } Self::Bool(t, x) => Self::Bool(t + rhs, x), } } } -impl From for IntView { +impl From for IntExpr { fn from(value: BoolView) -> Self { match value { BoolView::Const(b) => Self::Const(b as IntVal), @@ -84,13 +211,13 @@ impl From for IntView { } } -impl From for IntView { +impl From for IntExpr { fn from(value: IntVar) -> Self { Self::Var(value) } } -impl Mul for IntView { +impl Mul for IntExpr { type Output = Self; fn mul(self, rhs: IntVal) -> Self::Output { @@ -102,7 +229,7 @@ impl Mul for IntView { } } -impl Mul for IntView { +impl Mul for IntExpr { type Output = Self; fn mul(self, rhs: NonZeroIntVal) -> Self::Output { @@ -115,7 +242,7 @@ impl Mul for IntView { } } -impl Neg for IntView { +impl Neg for IntExpr { type Output = Self; fn neg(self) -> Self::Output { @@ -130,370 +257,18 @@ impl Neg for IntView { } } -impl Model { - /// Check whether a given integer is within the set of possible values that a - /// given integer view can take. - pub(crate) fn check_int_in_domain(&self, iv: &IntView, val: IntVal) -> bool { - match iv { - IntView::Var(v) => self.int_vars[v.0 as usize].domain.contains(&val), - IntView::Const(v) => *v == val, - IntView::Linear(t, v) => match t.rev_transform_lit(LitMeaning::Eq(val)) { - Ok(LitMeaning::Eq(val)) => self.int_vars[v.0 as usize].domain.contains(&val), - Err(false) => false, - _ => unreachable!(), - }, - IntView::Bool(t, _) => match t.rev_transform_lit(LitMeaning::Eq(val)) { - Ok(LitMeaning::Eq(val)) => val == 0 || val == 1, - Err(false) => false, - _ => unreachable!(), - }, - } - } +impl Sub for IntExpr { + type Output = IntLinExpr; - /// Ensure that a given integer view cannot take any of the values in the - /// given set. - pub(crate) fn diff_int_domain( - &mut self, - iv: &IntView, - mask: &IntSetVal, - con: usize, - ) -> Result<(), ReformulationError> { - match iv { - IntView::Var(v) => { - let diff: RangeList<_> = self.int_vars[v.0 as usize].domain.diff(mask); - if diff.is_empty() { - return Err(ReformulationError::TrivialUnsatisfiable); - } else if self.int_vars[v.0 as usize].domain == diff { - return Ok(()); - } - self.int_vars[v.0 as usize].domain = diff; - let constraints = self.int_vars[v.0 as usize].constraints.clone(); - for c in constraints { - if c != con { - self.enqueue(c); - } - } - Ok(()) - } - IntView::Const(v) => { - if mask.contains(v) { - Err(ReformulationError::TrivialUnsatisfiable) - } else { - Ok(()) - } - } - IntView::Linear(trans, iv) => { - let mask = trans.rev_transform_int_set(mask); - self.diff_int_domain(&IntView::Var(*iv), &mask, con) - } - IntView::Bool(trans, b) => { - let mask = trans.rev_transform_int_set(mask); - if mask.contains(&0) { - self.set_bool(b, con)?; - } - if mask.contains(&1) { - self.set_bool(&!b, con)?; - } - Ok(()) - } - } - } - - /// Return the minimal value that the given integer view can take. - pub(crate) fn get_int_lower_bound(&self, iv: &IntView) -> IntVal { - match *iv { - IntView::Var(v) => { - let def = &self.int_vars[v.0 as usize]; - *def.domain.lower_bound().unwrap() - } - IntView::Const(v) => v, - IntView::Linear(t, v) => { - let def = &self.int_vars[v.0 as usize]; - if t.positive_scale() { - t.transform(*def.domain.lower_bound().unwrap()) - } else { - t.transform(*def.domain.upper_bound().unwrap()) - } - } - IntView::Bool(t, _) => { - if t.positive_scale() { - t.transform(0) - } else { - t.transform(1) - } - } - } - } - - /// Return the maximal value that the given integer view can take. - pub(crate) fn get_int_upper_bound(&self, iv: &IntView) -> IntVal { - match *iv { - IntView::Var(v) => { - let def = &self.int_vars[v.0 as usize]; - *def.domain.upper_bound().unwrap() - } - IntView::Const(v) => v, - IntView::Linear(t, v) => { - let def = &self.int_vars[v.0 as usize]; - if t.positive_scale() { - t.transform(*def.domain.upper_bound().unwrap()) - } else { - t.transform(*def.domain.lower_bound().unwrap()) - } - } - IntView::Bool(t, _) => { - if t.positive_scale() { - t.transform(1) - } else { - t.transform(0) - } - } - } - } - - /// Ensure that the given integer decision variable takes a value in in the - /// given set. - pub(crate) fn intersect_int_domain( - &mut self, - iv: &IntView, - mask: &IntSetVal, - con: usize, - ) -> Result<(), ReformulationError> { - match iv { - IntView::Var(v) => { - let intersect: RangeList<_> = self.int_vars[v.0 as usize].domain.intersect(mask); - if intersect.is_empty() { - return Err(ReformulationError::TrivialUnsatisfiable); - } else if self.int_vars[v.0 as usize].domain == intersect { - return Ok(()); - } - self.int_vars[v.0 as usize].domain = intersect; - let constraints = self.int_vars[v.0 as usize].constraints.clone(); - for c in constraints { - if c != con { - self.enqueue(c); - } - } - Ok(()) - } - IntView::Const(v) => { - if !mask.contains(v) { - Err(ReformulationError::TrivialUnsatisfiable) - } else { - Ok(()) - } - } - IntView::Linear(trans, iv) => { - let mask = trans.rev_transform_int_set(mask); - self.intersect_int_domain(&IntView::Var(*iv), &mask, con) - } - IntView::Bool(trans, b) => { - let mask = trans.rev_transform_int_set(mask); - if !mask.contains(&0) { - self.set_bool(b, con)?; - } - if !mask.contains(&1) { - self.set_bool(&!b, con)?; - } - Ok(()) - } - } - } - - /// Set the value of a boolean variable. - pub(crate) fn set_bool(&mut self, b: &BoolView, con: usize) -> Result<(), ReformulationError> { - match b { - BoolView::Lit(l) => self - .add_clause([*l]) - .map_err(|_| ReformulationError::TrivialUnsatisfiable), - BoolView::Const(true) => Ok(()), - BoolView::Const(false) => Err(ReformulationError::TrivialUnsatisfiable), - BoolView::IntEq(iv, val) => self.set_int_value(iv, *val, con), - BoolView::IntGreater(iv, val) => self.set_int_lower_bound(iv, val + 1, con), - BoolView::IntGreaterEq(iv, val) => self.set_int_lower_bound(iv, *val, con), - BoolView::IntLess(iv, val) => self.set_int_upper_bound(iv, val - 1, con), - BoolView::IntLessEq(iv, val) => self.set_int_upper_bound(iv, *val, con), - BoolView::IntNotEq(iv, val) => { - self.diff_int_domain(iv, &RangeList::from(*val..=*val), con) - } - } - } - - /// Ensure that a given integer variable cannot take a value lower than `lb`. - pub(crate) fn set_int_lower_bound( - &mut self, - iv: &IntView, - lb: IntVal, - con: usize, - ) -> Result<(), ReformulationError> { - match iv { - IntView::Var(v) => { - let def = &mut self.int_vars[v.0 as usize]; - if lb <= *def.domain.lower_bound().unwrap() { - return Ok(()); - } else if lb > *def.domain.upper_bound().unwrap() { - return Err(ReformulationError::TrivialUnsatisfiable); - } - def.domain = RangeList::from_iter(def.domain.iter().filter_map(|r| { - if *r.end() < lb { - None - } else if *r.start() < lb { - Some(lb..=*r.end()) - } else { - Some(r) - } - })); - let constraints = def.constraints.clone(); - for c in constraints { - if c != con { - self.enqueue(c); - } - } - Ok(()) - } - IntView::Const(v) => { - if *v < lb { - Err(ReformulationError::TrivialUnsatisfiable) - } else { - Ok(()) - } - } - IntView::Linear(trans, iv) => { - match trans.rev_transform_lit(LitMeaning::GreaterEq(lb)) { - Ok(LitMeaning::GreaterEq(val)) => { - self.set_int_lower_bound(&IntView::Var(*iv), val, con) - } - Ok(LitMeaning::Less(val)) => { - self.set_int_upper_bound(&IntView::Var(*iv), val - 1, con) - } - _ => unreachable!(), - } - } - IntView::Bool(trans, b) => match trans.rev_transform_lit(LitMeaning::GreaterEq(lb)) { - Ok(LitMeaning::GreaterEq(1)) => self.set_bool(b, con), - Ok(LitMeaning::GreaterEq(val)) if val >= 2 => { - Err(ReformulationError::TrivialUnsatisfiable) - } - Ok(LitMeaning::GreaterEq(_)) => Ok(()), - Ok(LitMeaning::Less(1)) => self.set_bool(&!b, con), - Ok(LitMeaning::Less(val)) if val <= 0 => { - Err(ReformulationError::TrivialUnsatisfiable) - } - Ok(LitMeaning::Less(_)) => Ok(()), - _ => unreachable!(), - }, - } + fn sub(self, rhs: IntExpr) -> Self::Output { + self + -rhs } +} - /// Ensure that an integer variable cannot take a value greater than `ub`. - pub(crate) fn set_int_upper_bound( - &mut self, - iv: &IntView, - ub: IntVal, - con: usize, - ) -> Result<(), ReformulationError> { - match iv { - IntView::Var(v) => { - let def = &mut self.int_vars[v.0 as usize]; - if ub >= *def.domain.upper_bound().unwrap() { - return Ok(()); - } else if ub < *def.domain.lower_bound().unwrap() { - return Err(ReformulationError::TrivialUnsatisfiable); - } - def.domain = RangeList::from_iter(def.domain.iter().filter_map(|r| { - if ub < *r.start() { - None - } else if ub < *r.end() { - Some(*r.start()..=ub) - } else { - Some(r) - } - })); - let constraints = def.constraints.clone(); - for c in constraints { - if c != con { - self.enqueue(c); - } - } - Ok(()) - } - IntView::Const(v) => { - if *v > ub { - Err(ReformulationError::TrivialUnsatisfiable) - } else { - Ok(()) - } - } - IntView::Linear(trans, iv) => match trans.rev_transform_lit(LitMeaning::Less(ub + 1)) { - Ok(LitMeaning::GreaterEq(val)) => { - self.set_int_lower_bound(&IntView::Var(*iv), val, con) - } - Ok(LitMeaning::Less(val)) => { - self.set_int_upper_bound(&IntView::Var(*iv), val - 1, con) - } - _ => unreachable!(), - }, - IntView::Bool(trans, b) => match trans.rev_transform_lit(LitMeaning::Less(ub + 1)) { - Ok(LitMeaning::GreaterEq(1)) => self.set_bool(b, con), - Ok(LitMeaning::GreaterEq(val)) if val >= 2 => { - Err(ReformulationError::TrivialUnsatisfiable) - } - Ok(LitMeaning::GreaterEq(_)) => Ok(()), - Ok(LitMeaning::Less(1)) => self.set_bool(&!b, con), - Ok(LitMeaning::Less(val)) if val <= 0 => { - Err(ReformulationError::TrivialUnsatisfiable) - } - Ok(LitMeaning::Less(_)) => Ok(()), - _ => unreachable!(), - }, - } - } +impl Sub for IntExpr { + type Output = Self; - /// Set the value of an integer decision variable. - pub(crate) fn set_int_value( - &mut self, - iv: &IntView, - val: IntVal, - con: usize, - ) -> Result<(), ReformulationError> { - match iv { - IntView::Var(v) => { - let def = &mut self.int_vars[v.0 as usize]; - if def.domain.contains(&val) { - def.domain = RangeList::from(val..=val); - let constraints = def.constraints.clone(); - for c in constraints { - if c != con { - self.enqueue(c); - } - } - Ok(()) - } else { - Err(ReformulationError::TrivialUnsatisfiable) - } - } - IntView::Const(i) if *i == val => Ok(()), - IntView::Const(_) => Err(ReformulationError::TrivialUnsatisfiable), - IntView::Linear(trans, iv) => match trans.rev_transform_lit(LitMeaning::Eq(val)) { - Ok(LitMeaning::Eq(val)) => self.set_int_value(&IntView::Var(*iv), val, con), - Err(b) => { - debug_assert!(!b); - Err(ReformulationError::TrivialUnsatisfiable) - } - _ => unreachable!(), - }, - IntView::Bool(trans, b) => match trans.rev_transform_lit(LitMeaning::Eq(val)) { - Ok(LitMeaning::Eq(val)) => match val { - 0 => self.set_bool(&!b, con), - 1 => self.set_bool(b, con), - _ => Err(ReformulationError::TrivialUnsatisfiable), - }, - Err(b) => { - debug_assert!(!b); - Err(ReformulationError::TrivialUnsatisfiable) - } - _ => unreachable!(), - }, - } + fn sub(self, rhs: IntVal) -> Self::Output { + self + -rhs } } diff --git a/crates/huub/src/model/reformulate.rs b/crates/huub/src/model/reformulate.rs index 1b597c2..8735e19 100644 --- a/crates/huub/src/model/reformulate.rs +++ b/crates/huub/src/model/reformulate.rs @@ -3,17 +3,29 @@ use std::collections::HashMap; -use pindakaas::{solver::propagation::PropagatingSolver, Var as RawVar}; +use delegate::delegate; +use pindakaas::{ + solver::propagation::PropagatingSolver, ClauseDatabase, ClauseDatabaseTools, Lit as RawLit, + Unsatisfiable, Var as RawVar, +}; use thiserror::Error; use crate::{ + actions::{ + DecisionActions, InspectionActions, PropagatorInitActions, ReformulationActions, + TrailingActions, + }, + constraints::BoxedPropagator, model::{ bool, - int::{self, IntVar}, - ModelView, + int::{IntExpr, IntVar}, }, solver::{ - engine::Engine, + activation_list::IntPropCond, + engine::{Engine, PropRef}, + int_var::IntVarRef, + queue::PriorityLevel, + trail::TrailedInt, view::{BoolView, BoolViewInner, IntViewInner, SolverView}, }, IntVal, IntView, LitMeaning, Solver, @@ -32,6 +44,25 @@ pub struct InitConfig { vivification: bool, } +#[derive(Clone, Debug, PartialEq, Eq, Hash)] +/// Reference to a decision in a [`Model`]. +pub enum ModelView { + /// Reference to a Boolean decision. + Bool(bool::BoolView), + /// Reference to an integer decision. + Int(IntExpr), +} + +/// Context object used during the reformulation process that creates a +/// [`Solver`] object from a [`crate::Model`]. +pub(crate) struct ReformulationContext<'a> { + /// The resulting [`Solver`] object. + pub(crate) slv: &'a mut dyn PropagatorInitActions, + /// The mapping from variable in the [`crate::Model`] to the corresponding + /// view in the [`Solver`]. + pub(crate) map: &'a mut VariableMap, +} + #[derive(Error, Debug, PartialEq, Eq)] /// Error type used during the reformulation process of creating a [`Solver`], /// e.g. when creating a [`Solver`] from a [`crate::Model`]. @@ -103,6 +134,88 @@ impl InitConfig { } } +impl From for ModelView { + fn from(value: bool::BoolView) -> Self { + Self::Bool(value) + } +} + +impl From for ModelView { + fn from(value: IntExpr) -> Self { + Self::Int(value) + } +} + +impl ClauseDatabase for ReformulationContext<'_> { + delegate! { + to self.slv { + fn add_clause_from_slice(&mut self, clause: &[RawLit]) -> Result<(), Unsatisfiable>; + fn new_var_range(&mut self, len: usize) -> pindakaas::VarRange; + } + } +} + +impl DecisionActions for ReformulationContext<'_> { + delegate! { + to self.slv { + fn get_intref_lit(&mut self, var: IntVarRef, meaning: LitMeaning) -> BoolView; + fn get_num_conflicts(&self) -> u64; + } + } +} + +impl InspectionActions for ReformulationContext<'_> { + delegate! { + to self.slv { + fn get_int_lower_bound(&self, var: IntView) -> IntVal; + fn get_int_upper_bound(&self, var: IntView) -> IntVal; + fn check_int_in_domain(&self, var: IntView, val: IntVal) -> bool; + } + } +} + +impl PropagatorInitActions for ReformulationContext<'_> { + delegate! { + to self.slv { + fn add_propagator(&mut self, propagator: BoxedPropagator, priority: PriorityLevel) -> PropRef; + fn new_trailed_int(&mut self, init: IntVal) -> TrailedInt; + fn enqueue_now(&mut self, prop: PropRef); + fn enqueue_on_bool_change(&mut self, prop: PropRef, var: BoolView); + fn enqueue_on_int_change(&mut self, prop: PropRef, var: IntView, condition: IntPropCond); + } + } +} + +impl ReformulationActions for ReformulationContext<'_> { + fn get_solver_bool(&mut self, bv: bool::BoolView) -> BoolView { + self.map.get_bool(self.slv, bv) + } + + fn get_solver_int(&mut self, iv: IntExpr) -> IntView { + self.map.get_int(self.slv, iv) + } + + fn new_bool_var(&mut self) -> BoolView { + self.slv.new_lit().into() + } +} + +impl TrailingActions for ReformulationContext<'_> { + delegate! { + to self.slv { + fn get_bool_val(&self, bv: BoolView) -> Option; + fn get_trailed_int(&self, i: TrailedInt) -> IntVal; + fn set_trailed_int(&mut self, i: TrailedInt, v: IntVal) -> IntVal; + } + } +} + +impl From for ReformulationError { + fn from(_: Unsatisfiable) -> Self { + Self::TrivialUnsatisfiable + } +} + impl From for Variable { fn from(value: IntVar) -> Self { Self::Int(value) @@ -123,22 +236,19 @@ impl VariableMap { index: &ModelView, ) -> SolverView { match index { - ModelView::Bool(b) => SolverView::Bool(self.get_bool(slv, b)), - ModelView::Int(i) => SolverView::Int(self.get_int(slv, i)), + ModelView::Bool(b) => SolverView::Bool(self.get_bool(slv, *b)), + ModelView::Int(i) => SolverView::Int(self.get_int(slv, *i)), } } /// Lookup the solver [`BoolView`] to which the given model [`bool::BoolView`] /// maps. - pub fn get_bool>( - &self, - slv: &mut Solver, - bv: &bool::BoolView, - ) -> BoolView { - let get_int_lit = |slv: &mut Solver, iv: &int::IntView, lit_meaning: LitMeaning| { - let iv = self.get_int(slv, iv); - slv.get_int_lit(iv, lit_meaning) - }; + pub fn get_bool(&self, slv: &mut dyn PropagatorInitActions, bv: bool::BoolView) -> BoolView { + let get_int_lit = + |slv: &mut dyn PropagatorInitActions, iv: IntVar, lit_meaning: LitMeaning| { + let iv = self.get_int(slv, IntExpr::Var(iv)); + slv.get_int_lit(iv, lit_meaning) + }; match bv { bool::BoolView::Lit(l) => { @@ -158,39 +268,33 @@ impl VariableMap { bv } } - bool::BoolView::Const(c) => (*c).into(), - bool::BoolView::IntEq(v, i) => get_int_lit(slv, v, LitMeaning::Eq(*i)), - bool::BoolView::IntGreater(v, i) => get_int_lit(slv, v, LitMeaning::GreaterEq(i + 1)), - bool::BoolView::IntGreaterEq(v, i) => get_int_lit(slv, v, LitMeaning::GreaterEq(*i)), - bool::BoolView::IntLess(v, i) => get_int_lit(slv, v, LitMeaning::Less(*i)), - bool::BoolView::IntLessEq(v, i) => get_int_lit(slv, v, LitMeaning::Less(i + 1)), - bool::BoolView::IntNotEq(v, i) => get_int_lit(slv, v, LitMeaning::NotEq(*i)), + bool::BoolView::Const(c) => c.into(), + bool::BoolView::IntEq(v, i) => get_int_lit(slv, v, LitMeaning::Eq(i)), + bool::BoolView::IntGreaterEq(v, i) => get_int_lit(slv, v, LitMeaning::GreaterEq(i)), + bool::BoolView::IntLess(v, i) => get_int_lit(slv, v, LitMeaning::Less(i)), + bool::BoolView::IntNotEq(v, i) => get_int_lit(slv, v, LitMeaning::NotEq(i)), } } /// Lookup the solver [`IntView`] to which the given model [`int::IntView`] /// maps. - pub fn get_int>( - &self, - slv: &mut Solver, - iv: &int::IntView, - ) -> IntView { - let get_int_var = |v: &IntVar| { - let SolverView::Int(i) = self.map.get(&Variable::Int(*v)).cloned().unwrap() else { + pub fn get_int(&self, slv: &mut dyn PropagatorInitActions, iv: IntExpr) -> IntView { + let get_int_var = |v: IntVar| { + let SolverView::Int(i) = self.map.get(&Variable::Int(v)).cloned().unwrap() else { unreachable!() }; i }; match iv { - int::IntView::Var(i) => get_int_var(i), - int::IntView::Const(c) => (*c).into(), - int::IntView::Linear(t, i) => get_int_var(i) * t.scale + t.offset, - int::IntView::Bool(t, bv) => { + IntExpr::Var(i) => get_int_var(i), + IntExpr::Const(c) => (c).into(), + IntExpr::Linear(t, i) => get_int_var(i) * t.scale + t.offset, + IntExpr::Bool(t, bv) => { let bv = self.get_bool(slv, bv); match bv.0 { BoolViewInner::Lit(lit) => IntView(IntViewInner::Bool { - transformer: *t, + transformer: t, lit, }), BoolViewInner::Const(b) => t.transform(b as IntVal).into(), diff --git a/crates/huub/src/solver.rs b/crates/huub/src/solver.rs index f9bdc33..d4ab2c0 100644 --- a/crates/huub/src/solver.rs +++ b/crates/huub/src/solver.rs @@ -20,7 +20,7 @@ use pindakaas::{ propagation::{PropagatingSolver, WithPropagator}, LearnCallback, SlvTermSignal, SolveResult as SatSolveResult, TermCallback, }, - Cnf, Lit as RawLit, Valuation as SatValuation, + ClauseDatabase, Cnf, Lit as RawLit, Unsatisfiable, Valuation as SatValuation, }; use tracing::{debug, trace}; @@ -29,18 +29,18 @@ use crate::{ BrancherInitActions, DecisionActions, ExplanationActions, InspectionActions, PropagatorInitActions, TrailingActions, }, + branchers::BoxedBrancher, + constraints::BoxedPropagator, solver::{ activation_list::IntPropCond, - engine::{ - trace_new_lit, BoxedBrancher, BoxedPropagator, Engine, PropRef, SearchStatistics, - }, + engine::{trace_new_lit, Engine, PropRef, SearchStatistics}, int_var::{IntVarRef, LazyLitDef, OrderStorage}, queue::PriorityLevel, trail::TrailedInt, value::{AssumptionChecker, NoAssumptions, Valuation, Value}, - view::{BoolViewInner, IntView, IntViewInner, SolverView}, + view::{BoolView, BoolViewInner, IntView, IntViewInner, SolverView}, }, - BoolView, IntVal, LitMeaning, ReformulationError, + IntVal, LitMeaning, ReformulationError, }; #[derive(Debug, Clone, Copy, PartialEq, Eq)] @@ -172,21 +172,15 @@ where impl> Solver { /// Add a clause to the solver - pub fn add_clause>( - &mut self, - iter: I, - ) -> Result<(), ReformulationError> { - let mut clause = Vec::new(); - for lit in iter { - match lit.0 { - BoolViewInner::Lit(l) => clause.push(l), - BoolViewInner::Const(true) => return Ok(()), - BoolViewInner::Const(false) => {} - } - } - self.oracle - .add_clause(clause) - .map_err(|_| ReformulationError::TrivialUnsatisfiable) + pub fn add_clause(&mut self, clause: Iter) -> Result<(), ReformulationError> + where + Iter: IntoIterator, + Iter::Item: Into, + { + Ok(pindakaas::ClauseDatabaseTools::add_clause( + self, + clause.into_iter().map(Into::into), + )?) } #[doc(hidden)] @@ -506,6 +500,15 @@ impl> BrancherInitActions for Solver { } } +impl ClauseDatabase for Solver { + delegate! { + to self.oracle { + fn add_clause_from_slice(&mut self, clause: &[RawLit]) -> Result<(), Unsatisfiable>; + fn new_var_range(&mut self, len: usize) -> pindakaas::VarRange; + } + } +} + impl> DecisionActions for Solver { fn get_intref_lit(&mut self, iv: IntVarRef, meaning: LitMeaning) -> BoolView { let mut clauses = Vec::new(); @@ -534,7 +537,7 @@ impl> DecisionActions for Solver { let bv = var.bool_lit(meaning, new_var); for cl in clauses { self.oracle - .add_clause(cl) + .add_clause_from_slice(&cl) .expect("functional definition cannot make the problem unsatisfiable"); } bv @@ -589,13 +592,6 @@ impl> InspectionActions for Solver { } impl> PropagatorInitActions for Solver { - fn add_clause>( - &mut self, - clause: I, - ) -> Result<(), ReformulationError> { - self.add_clause(clause) - } - fn add_propagator(&mut self, propagator: BoxedPropagator, priority: PriorityLevel) -> PropRef { let engine = self.engine_mut(); let prop_ref = engine.propagators.push(propagator); diff --git a/crates/huub/src/solver/engine.rs b/crates/huub/src/solver/engine.rs index 453a3be..f6e1214 100644 --- a/crates/huub/src/solver/engine.rs +++ b/crates/huub/src/solver/engine.rs @@ -36,8 +36,8 @@ use tracing::{debug, trace}; use crate::{ actions::{DecisionActions, ExplanationActions, InspectionActions, TrailingActions}, - branchers::{Brancher, Decision}, - constraints::{Propagator, Reason}, + branchers::{BoxedBrancher, Decision}, + constraints::{BoxedPropagator, Reason}, solver::{ activation_list::{ActivationList, IntEvent}, bool_to_int::BoolToIntMap, @@ -45,20 +45,12 @@ use crate::{ queue::{PriorityLevel, PriorityQueue}, solving_context::SolvingContext, trail::{Trail, TrailedInt}, - view::{BoolViewInner, IntViewInner}, + view::{BoolView, BoolViewInner, IntViewInner}, SolverConfiguration, }, - BoolView, Clause, Conjunction, IntVal, IntView, + Clause, Conjunction, IntVal, IntView, }; -/// Type alias to represent [`Brancher`] contained in a [`Box`], that is used by -/// [`Engine`]. -pub(crate) type BoxedBrancher = Box Brancher>>; - -/// Type alias to represent [`Propagator`] contained in a [`Box`], that is used -/// by [`Engine`]. -pub(crate) type BoxedPropagator = Box Propagator, State>>; - #[derive(Debug, Default, Clone)] /// A propagation engine implementing the [`Propagator`] trait. pub struct Engine { @@ -87,8 +79,15 @@ pub struct SearchStatistics { } #[derive(Clone, Debug, Default)] +/// Internal state representation of the propagation engine disconnected from +/// the storage of the propagators and branchers. +/// +/// Note that this structure is public to the user to allow the user to +/// construct [`BoxedPropgator`], but it is not intended to be constructed by +/// the user. It should merely be seen as the implementation of the +/// [`ExplanationActions`] trait. pub struct State { - /// Solver confifguration + /// Solver configuration pub(crate) config: SolverConfiguration, // ---- Trailed Value Infrastructure (e.g., decision variables) ---- @@ -342,8 +341,8 @@ impl PropagatorExtension for Engine { if let Some(reason) = self.state.reason_map.get(&lit).cloned() { let clause: Clause = reason.explain(&mut self.propagators, &mut self.state, Some(lit)); - for l in &clause { - if l == &lit { + for &l in &clause { + if l == lit { continue; } let val = self.state.trail.get_sat_value(!l); diff --git a/crates/huub/src/solver/int_var.rs b/crates/huub/src/solver/int_var.rs index 6436632..0c505ff 100644 --- a/crates/huub/src/solver/int_var.rs +++ b/crates/huub/src/solver/int_var.rs @@ -10,7 +10,10 @@ use std::{ }; use itertools::Itertools; -use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit, Var as RawVar, VarRange}; +use pindakaas::{ + solver::propagation::PropagatingSolver, ClauseDatabaseTools, Lit as RawLit, Var as RawVar, + VarRange, +}; use rangelist::RangeList; use crate::{ @@ -18,10 +21,10 @@ use crate::{ solver::{ engine::Engine, trail::TrailedInt, - view::{BoolViewInner, IntViewInner}, + view::{BoolView, BoolViewInner, IntViewInner}, IntView, }, - BoolView, Clause, IntSetVal, IntVal, LinearTransform, NonZeroIntVal, Solver, + Clause, IntSetVal, IntVal, LinearTransform, NonZeroIntVal, Solver, }; /// An entry in the [`DirectStorage`] that can be used to access the @@ -1284,9 +1287,9 @@ mod tests { use crate::{ solver::{ int_var::{EncodingType, IntVar}, - view::{BoolViewInner, IntViewInner}, + view::{BoolView, BoolViewInner, IntViewInner}, }, - BoolView, IntView, LitMeaning, Solver, + IntView, LitMeaning, Solver, }; #[test] diff --git a/crates/huub/src/solver/solving_context.rs b/crates/huub/src/solver/solving_context.rs index 39acdb4..9316c0c 100644 --- a/crates/huub/src/solver/solving_context.rs +++ b/crates/huub/src/solver/solving_context.rs @@ -15,12 +15,13 @@ use crate::{ }, constraints::{Conflict, LazyReason, ReasonBuilder}, solver::{ - engine::{trace_new_lit, BoxedPropagator, PropRef, State}, + engine::{trace_new_lit, PropRef, State}, int_var::{IntVarRef, LazyLitDef}, trail::TrailedInt, - view::{BoolViewInner, IntViewInner}, + view::{BoolView, BoolViewInner, IntViewInner}, + BoxedPropagator, }, - BoolView, Clause, IntVal, IntView, LitMeaning, + Clause, IntVal, IntView, LitMeaning, }; /// Type used to communicate whether a change is redundant, conflicting, or new. @@ -37,6 +38,11 @@ enum ChangeType { /// [`SolvingActions`] exposed by the SAT oracle. /// /// This structure is used to run the propagators that have been scheduled. +/// +/// Note that this structure is public to the user to allow the user to +/// construct [`BoxedPropgator`] and [`BoxedBrancher`], but it is not intended +/// to be constructed by the user. It should merely be seen as the +/// implementation of the [`PropagationActions`] trait. pub struct SolvingContext<'a> { /// Actions to create new variables in the oracle pub(crate) slv: &'a mut dyn SolvingActions, diff --git a/crates/huub/src/solver/trail.rs b/crates/huub/src/solver/trail.rs index 3d5a3e2..782ba5b 100644 --- a/crates/huub/src/solver/trail.rs +++ b/crates/huub/src/solver/trail.rs @@ -9,7 +9,11 @@ use index_vec::IndexVec; use pindakaas::{Lit as RawLit, Var as RawVar}; use tracing::trace; -use crate::{actions::TrailingActions, solver::view::BoolViewInner, BoolView, IntVal}; +use crate::{ + actions::TrailingActions, + solver::view::{BoolView, BoolViewInner}, + IntVal, +}; #[derive(Clone, Copy, Debug, Default, Eq, PartialEq)] /// A structure that stores the currently assigned value of a Boolean variable diff --git a/crates/huub/src/solver/value.rs b/crates/huub/src/solver/value.rs index f71a2ef..ea65b9e 100644 --- a/crates/huub/src/solver/value.rs +++ b/crates/huub/src/solver/value.rs @@ -6,9 +6,9 @@ use std::{fmt::Display, num::NonZeroI64}; use pindakaas::solver::FailedAssumtions; use rangelist::RangeList; -use crate::{ - solver::{view::BoolViewInner, SolverView}, - BoolView, +use crate::solver::{ + view::{BoolView, BoolViewInner}, + SolverView, }; /// Trait implemented by the object given to the callback on detecting failure diff --git a/crates/huub/src/solver/view.rs b/crates/huub/src/solver/view.rs index b4eac4e..066c5be 100644 --- a/crates/huub/src/solver/view.rs +++ b/crates/huub/src/solver/view.rs @@ -7,7 +7,7 @@ use std::{ ops::{Add, Mul, Neg, Not}, }; -use pindakaas::{solver::propagation::PropagatingSolver, Lit as RawLit, Var as RawVar}; +use pindakaas::{solver::propagation::PropagatingSolver, BoolVal, Lit as RawLit, Var as RawVar}; use crate::{ helpers::linear_transform::LinearTransform, @@ -106,6 +106,15 @@ impl From for BoolView { } } +impl Into for BoolView { + fn into(self) -> BoolVal { + match self.0 { + BoolViewInner::Lit(l) => l.into(), + BoolViewInner::Const(b) => b.into(), + } + } +} + impl Not for BoolView { type Output = Self; @@ -281,22 +290,13 @@ impl Neg for IntView { }) } } -impl From<&BoolView> for SolverView { - fn from(value: &BoolView) -> Self { - Self::Bool(*value) - } -} -impl From<&IntView> for SolverView { - fn from(value: &IntView) -> Self { - Self::Int(*value) - } -} impl From for SolverView { fn from(value: BoolView) -> Self { Self::Bool(value) } } + impl From for SolverView { fn from(value: IntView) -> Self { Self::Int(value) diff --git a/crates/huub/src/tests.rs b/crates/huub/src/tests.rs index 5ba1114..befb1b3 100644 --- a/crates/huub/src/tests.rs +++ b/crates/huub/src/tests.rs @@ -1,9 +1,8 @@ use expect_test::Expect; use itertools::Itertools; +use pindakaas::propositional_logic::Formula; -use crate::{ - BoolExpr, InitConfig, Model, ReformulationError, SolveResult, Solver, SolverView, Value, -}; +use crate::{InitConfig, Model, ReformulationError, SolveResult, Solver, SolverView, Value}; #[test] fn it_works() { @@ -11,12 +10,12 @@ fn it_works() { let a = prb.new_bool_var(); let b = prb.new_bool_var(); - prb += BoolExpr::Or(vec![(!a.clone()).into(), (!b.clone()).into()]); - prb += BoolExpr::Or(vec![a.clone().into(), b.clone().into()]); + prb += Formula::Or(vec![(!a).into(), (!b).into()]); + prb += Formula::Or(vec![a.into(), b.into()]); let (mut slv, map): (Solver, _) = prb.to_solver(&InitConfig::default()).unwrap(); - let a = map.get_bool(&mut slv, &a); - let b = map.get_bool(&mut slv, &b); + let a = map.get_bool(&mut slv, a); + let b = map.get_bool(&mut slv, b); assert_eq!( slv.solve(|value| {