diff --git a/Cargo.lock b/Cargo.lock index bc37899b4e..3e6fda83c6 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4,9 +4,9 @@ version = 3 [[package]] name = "addr2line" -version = "0.24.1" +version = "0.24.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f5fb1d8e4442bd405fdfd1dacb42792696b0cf9cb15882e5d097b742a676d375" +checksum = "dfbe277e56a376000877090da837660b4427aad530e3028d44e0bffe4f89a1c1" dependencies = [ "gimli", ] @@ -43,9 +43,9 @@ dependencies = [ [[package]] name = "anstream" -version = "0.6.15" +version = "0.6.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "64e15c1ab1f89faffbf04a634d5e1962e9074f2741eef6d97f3c4e322426d526" +checksum = "8acc5369981196006228e28809f761875c0327210a891e941f4c683b3a99529b" dependencies = [ "anstyle", "anstyle-parse", @@ -58,43 +58,43 @@ dependencies = [ [[package]] name = "anstyle" -version = "1.0.8" +version = "1.0.10" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1bec1de6f59aedf83baf9ff929c98f2ad654b97c9510f4e70cf6f661d49fd5b1" +checksum = "55cc3b69f167a1ef2e161439aa98aed94e6028e5f9a59be9a6ffb47aef1651f9" [[package]] name = "anstyle-parse" -version = "0.2.5" +version = "0.2.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eb47de1e80c2b463c735db5b217a0ddc39d612e7ac9e2e96a5aed1f57616c1cb" +checksum = "3b2d16507662817a6a20a9ea92df6652ee4f94f914589377d69f3b21bc5798a9" dependencies = [ "utf8parse", ] [[package]] name = "anstyle-query" -version = "1.1.1" +version = "1.1.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6d36fc52c7f6c869915e99412912f22093507da8d9e942ceaf66fe4b7c14422a" +checksum = "79947af37f4177cfead1110013d678905c37501914fba0efea834c3fe9a8d60c" dependencies = [ - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] name = "anstyle-wincon" -version = "3.0.4" +version = "3.0.6" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5bf74e1b6e971609db8ca7a9ce79fd5768ab6ae46441c572e46cf596f59e57f8" +checksum = "2109dbce0e72be3ec00bed26e6a7479ca384ad226efdd66db8fa2e3a38c83125" dependencies = [ "anstyle", - "windows-sys 0.52.0", + "windows-sys 0.59.0", ] [[package]] name = "anyhow" -version = "1.0.92" +version = "1.0.93" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "74f37166d7d48a0284b99dd824694c26119c700b53bf0d1540cdb147dbdaaf13" +checksum = "4c95c10ba0b00a02636238b814946408b1322d5ac4760326e6fb8ec956d85775" [[package]] name = "autocfg" @@ -138,7 +138,7 @@ dependencies = [ "proc-macro2", "quote", "regex", - "rustc-hash", + "rustc-hash 1.1.0", "shlex", "syn 2.0.87", ] @@ -187,15 +187,15 @@ checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" [[package]] name = "bytes" -version = "1.7.2" +version = "1.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "428d9aa8fbc0670b7b8d6030a7fadd0f86151cae55e4dbbece15f3780a3dfaf3" +checksum = "9ac0150caa2ae65ca5bd83f25c7de183dea78d4d366469f148435e2acfbad0da" [[package]] name = "cc" -version = "1.1.31" +version = "1.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2e7962b54006dcfcc61cb72735f4d89bb97061dd6a7ed882ec6b8ee53714c6f" +checksum = "1aeb932158bd710538c73702db6945cb68a8fb08c519e6e12706b94263b36db8" dependencies = [ "shlex", ] @@ -279,11 +279,20 @@ version = "0.7.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "1462739cb27611015575c0c11df5df7601141071f07518d56fcc1be504cbec97" +[[package]] +name = "cmake" +version = "0.1.51" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fb1e43aa7fd152b1f968787f7dbcdeb306d1867ff373c69955211876c053f91a" +dependencies = [ + "cc", +] + [[package]] name = "colorchoice" -version = "1.0.2" +version = "1.0.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d3fd119d74b830634cea2a0f58bbd0d54540518a14397557951e79340abc28c0" +checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990" [[package]] name = "conjure_core" @@ -301,6 +310,9 @@ dependencies = [ "minion_rs", "project-root", "regex", + "rustsat", + "rustsat-minisat", + "sat_rs", "schemars", "serde", "serde_json", @@ -336,6 +348,8 @@ dependencies = [ "pretty_assertions", "rand", "regex", + "rustsat", + "rustsat-minisat", "schemars", "serde", "serde_json", @@ -356,6 +370,16 @@ version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" +[[package]] +name = "cpu-time" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e9e393a7668fe1fad3075085b86c781883000b4ede868f43627b34a87c8b7ded" +dependencies = [ + "libc", + "winapi", +] + [[package]] name = "darling" version = "0.20.10" @@ -412,17 +436,6 @@ dependencies = [ "syn 1.0.109", ] -[[package]] -name = "derive-try-from-primitive" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "302ccf094df1151173bb6f5a2282fcd2f45accd5eae1bdf82dcbfefbc501ad5c" -dependencies = [ - "proc-macro2", - "quote", - "syn 1.0.109", -] - [[package]] name = "diff" version = "0.1.13" @@ -478,9 +491,9 @@ dependencies = [ [[package]] name = "fastrand" -version = "2.1.1" +version = "2.2.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8c02a5121d4ea3eb16a80748c74f5549a5665e4c21333c6098f283870fbdea6" +checksum = "486f806e73c5707928240ddc295403b1b93c96a02038563881c4a2fd84b81ac4" [[package]] name = "fnv" @@ -501,9 +514,9 @@ dependencies = [ [[package]] name = "gimli" -version = "0.31.0" +version = "0.31.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32085ea23f3234fc7846555e85283ba4de91e21016dc0455a16286d87a292d64" +checksum = "07e28edb80900c19c28f1072f2e8aeca7fa06b23cd4169cefe1af5aa3260783f" [[package]] name = "glob" @@ -519,9 +532,9 @@ checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" [[package]] name = "hashbrown" -version = "0.14.5" +version = "0.15.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5274423e17b7c9fc20b6e7e208532f9b19825d82dfd615708b70edd83df41f1" +checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" [[package]] name = "heck" @@ -592,12 +605,12 @@ dependencies = [ [[package]] name = "indexmap" -version = "2.5.0" +version = "2.6.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "68b900aa2f7301e21c36462b170ee99994de34dff39a4a6a528e80e7376d07e5" +checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" dependencies = [ "equivalent", - "hashbrown 0.14.5", + "hashbrown 0.15.1", "serde", ] @@ -633,39 +646,13 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b" [[package]] name = "js-sys" -version = "0.3.70" +version = "0.3.72" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1868808506b929d7b0cfa8f75951347aa71bb21144b7791bae35d9bccfcfe37a" +checksum = "6a88f1bda2bd75b0452a14784937d796722fdebfe50df998aeb3f0b7603019a9" dependencies = [ "wasm-bindgen", ] -[[package]] -name = "kissat-rs" -version = "0.1.3" -source = "git+https://github.com/firefighterduck/kissat-rs?branch=main#45cc75e369c8215c826647f100f4fd0eee3198e9" -dependencies = [ - "derive-try-from-primitive", - "kissat-sys", - "thiserror", -] - -[[package]] -name = "kissat-sys" -version = "0.1.3" -source = "git+https://github.com/firefighterduck/kissat-rs?branch=main#45cc75e369c8215c826647f100f4fd0eee3198e9" -dependencies = [ - "bindgen", -] - -[[package]] -name = "kissat_rs" -version = "0.1.0" -dependencies = [ - "kissat-rs", - "kissat-sys", -] - [[package]] name = "lazy_static" version = "1.5.0" @@ -674,9 +661,9 @@ checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" [[package]] name = "libc" -version = "0.2.161" +version = "0.2.162" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9489c2807c139ffd9c1794f4af0ebe86a828db53ecdc7fea2111d0fed085d1" +checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398" [[package]] name = "libloading" @@ -690,24 +677,24 @@ dependencies = [ [[package]] name = "libm" -version = "0.2.8" +version = "0.2.11" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ec2a862134d2a7d32d7983ddcdd1c4923530833c9f2ea1a44fc5fa473989058" +checksum = "8355be11b20d696c8f18f6cc018c4e372165b1fa8126cef092399c9951984ffa" [[package]] name = "linkme" -version = "0.3.29" +version = "0.3.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "70fe496a7af8c406f877635cbf3cd6a9fac9d6f443f58691cd8afe6ce0971af4" +checksum = "566336154b9e58a4f055f6dd4cbab62c7dc0826ce3c0a04e63b2d2ecd784cdae" dependencies = [ "linkme-impl", ] [[package]] name = "linkme-impl" -version = "0.3.29" +version = "0.3.31" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b01f197a15988fb5b2ec0a5a9800c97e70771499c456ad757d63b3c5e9b96e75" +checksum = "edbe595006d355eaf9ae11db92707d4338cd2384d16866131cc1afdbdd35d8d9" dependencies = [ "proc-macro2", "quote", @@ -800,18 +787,18 @@ dependencies = [ [[package]] name = "object" -version = "0.36.4" +version = "0.36.5" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "084f1a5821ac4c651660a94a7153d27ac9d8a53736203f58b31945ded098070a" +checksum = "aedf0a2d09c573ed1d8d85b30c119153926a2b36dce0ab28322c09a117a4683e" dependencies = [ "memchr", ] [[package]] name = "once_cell" -version = "1.19.0" +version = "1.20.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fdb12b2476b595f9358c5161aa467c2438859caa136dec86c26fdd2efe17b92" +checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" [[package]] name = "parking_lot" @@ -838,9 +825,9 @@ dependencies = [ [[package]] name = "pin-project-lite" -version = "0.2.14" +version = "0.2.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02" +checksum = "915a1e146535de9163f3987b8944ed8cf49a18bb0056bcebcdcece385cece4ff" [[package]] name = "powerfmt" @@ -869,9 +856,9 @@ dependencies = [ [[package]] name = "prettyplease" -version = "0.2.22" +version = "0.2.25" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "479cf940fbbb3426c32c5d5176f62ad57549a0bb84773423ba8be9d089f5faba" +checksum = "64d1ec885c64d0457d564db4ec299b2dae3f9c02808b8ad9c3a089c591b18033" dependencies = [ "proc-macro2", "syn 2.0.87", @@ -988,9 +975,9 @@ dependencies = [ [[package]] name = "redox_syscall" -version = "0.5.6" +version = "0.5.7" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "355ae415ccd3a04315d3f8246e86d67689ea74d88d915576e1589a351062a13b" +checksum = "9b6dfecf2c74bce2466cabf93f6664d6998a69eb21e39f4207930065b27b771f" dependencies = [ "bitflags", ] @@ -1009,9 +996,9 @@ dependencies = [ [[package]] name = "regex-automata" -version = "0.4.8" +version = "0.4.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "368758f23274712b504848e9d5a6f010445cc8b87a7cdb4d7cbee666c1288da3" +checksum = "809e8dc61f6de73b46c85f4c96486310fe304c434cfa43669d7b40f711150908" dependencies = [ "aho-corasick", "memchr", @@ -1036,11 +1023,17 @@ version = "1.1.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" +[[package]] +name = "rustc-hash" +version = "2.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "583034fd73374156e66797ed8e5b0d5690409c9226b22d87cb7f19821c05d152" + [[package]] name = "rustix" -version = "0.38.37" +version = "0.38.40" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8acb788b847c24f28525660c4d7758620a7210875711f79e7f663cc152726811" +checksum = "99e4ea3e1cdc4b559b8e5650f9c8e5998e3e5c1343b4eaf034565f32318d63c0" dependencies = [ "bitflags", "errno", @@ -1049,11 +1042,41 @@ dependencies = [ "windows-sys 0.52.0", ] +[[package]] +name = "rustsat" +version = "0.6.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a677c8c77e334fff543a436299ee565ae46d242fb5192b1bba0f7eb744ff3f84" +dependencies = [ + "anyhow", + "cpu-time", + "itertools 0.13.0", + "nom", + "rustc-hash 2.0.0", + "tempfile", + "thiserror", + "visibility", +] + +[[package]] +name = "rustsat-minisat" +version = "0.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8bd8d2c93bc7dd25707ebdab8e551cb76d2b66854cc8458f67df99abffea79f3" +dependencies = [ + "anyhow", + "bindgen", + "cmake", + "cpu-time", + "rustsat", + "thiserror", +] + [[package]] name = "rustversion" -version = "1.0.17" +version = "1.0.18" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "955d28af4278de8121b7ebeb796b6a45735dc01436d898801014aced2773a3d6" +checksum = "0e819f2bc632f285be6d7cd36e25940d45b2391dd6d9b939e79de557f7014248" [[package]] name = "rusty-fork" @@ -1082,6 +1105,15 @@ dependencies = [ "winapi-util", ] +[[package]] +name = "sat_rs" +version = "0.1.0" +dependencies = [ + "anyhow", + "rustsat", + "rustsat-minisat", +] + [[package]] name = "schemars" version = "0.8.21" @@ -1114,18 +1146,18 @@ checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49" [[package]] name = "serde" -version = "1.0.214" +version = "1.0.215" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f55c3193aca71c12ad7890f1785d2b73e1b9f63a0bbc353c08ef26fe03fc56b5" +checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.214" +version = "1.0.215" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "de523f781f095e28fa605cdce0f8307e451cc0fd14e2eb4cd2e98a355b147766" +checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" dependencies = [ "proc-macro2", "quote", @@ -1183,7 +1215,7 @@ dependencies = [ "chrono", "hex", "indexmap 1.9.3", - "indexmap 2.5.0", + "indexmap 2.6.0", "serde", "serde_derive", "serde_json", @@ -1265,15 +1297,15 @@ dependencies = [ [[package]] name = "sval" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "eaf38d1fa2ce984086ea42fb856a9f374d94680a4f796831a7fc868d7f2af1b9" +checksum = "f6dc0f9830c49db20e73273ffae9b5240f63c42e515af1da1fceefb69fceafd8" [[package]] name = "sval_buffer" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "81682ff859964ca1d7cf3d3d0f9ec7204ea04c2c32acb8cc2cf68ecbd3127354" +checksum = "429922f7ad43c0ef8fd7309e14d750e38899e32eb7e8da656ea169dd28ee212f" dependencies = [ "sval", "sval_ref", @@ -1281,18 +1313,18 @@ dependencies = [ [[package]] name = "sval_dynamic" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2a213b93bb4c6f4c9f9b17f2e740e077fd18746bbf7c80c72bbadcac68fa7ee4" +checksum = "68f16ff5d839396c11a30019b659b0976348f3803db0626f736764c473b50ff4" dependencies = [ "sval", ] [[package]] name = "sval_fmt" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6902c6d3fb52c89206fe0dc93546c0123f7d48b5997fd14e61c9e64ff0b63275" +checksum = "c01c27a80b6151b0557f9ccbe89c11db571dc5f68113690c1e028d7e974bae94" dependencies = [ "itoa", "ryu", @@ -1301,9 +1333,9 @@ dependencies = [ [[package]] name = "sval_json" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "11a28041ea78cdc394b930ae6b897d36246dc240a29a6edf82d76562487fb0b4" +checksum = "0deef63c70da622b2a8069d8600cf4b05396459e665862e7bdb290fd6cf3f155" dependencies = [ "itoa", "ryu", @@ -1312,9 +1344,9 @@ dependencies = [ [[package]] name = "sval_nested" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "850346e4b0742a7f2fd2697d703ff80084d0b658f0f2e336d71b8a06abf9b68e" +checksum = "a39ce5976ae1feb814c35d290cf7cf8cd4f045782fe1548d6bc32e21f6156e9f" dependencies = [ "sval", "sval_buffer", @@ -1323,18 +1355,18 @@ dependencies = [ [[package]] name = "sval_ref" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "824afd97a8919f28a35b0fdea979845cc2ae461a8a3aaa129455cb89c88bb77a" +checksum = "bb7c6ee3751795a728bc9316a092023529ffea1783499afbc5c66f5fabebb1fa" dependencies = [ "sval", ] [[package]] name = "sval_serde" -version = "2.13.1" +version = "2.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ada7520dd719ed672c786c7db7de4f5230f4d504b0821bd8305cd30ca442315" +checksum = "2a5572d0321b68109a343634e3a5d576bf131b82180c6c442dee06349dfc652a" dependencies = [ "serde", "sval", @@ -1365,9 +1397,9 @@ dependencies = [ [[package]] name = "tempfile" -version = "3.12.0" +version = "3.14.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "04cbcdd0c794ebb0d4cf35e88edd2f7d2c4c3e9a5a6dab322839b321c6a87a64" +checksum = "28cce251fcbc87fac86a866eeb0d6c2d536fc16d06f184bb61aeae11aa4cee0c" dependencies = [ "cfg-if", "fastrand", @@ -1378,18 +1410,18 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.67" +version = "1.0.69" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b3c6efbfc763e64eb85c11c25320f0737cb7364c4b6336db90aa9ebe27a0bbd" +checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.67" +version = "1.0.69" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b607164372e89797d78b8e23a6d67d5d1038c1c65efd52e1389ef8b77caba2a6" +checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" dependencies = [ "proc-macro2", "quote", @@ -1429,9 +1461,9 @@ dependencies = [ [[package]] name = "tokio" -version = "1.40.0" +version = "1.41.1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2b070231665d27ad9ec9b8df639893f46727666c6767db40317fbe920a5d998" +checksum = "22cfb5bee7a6a52939ca9224d6ac897bb669134078daa8735560897f69de4d33" dependencies = [ "backtrace", "bytes", @@ -1466,7 +1498,7 @@ version = "0.22.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "4ae48d6208a266e853d946088ed816055e556cc6028c5e8e2b84d9fa5dd7c7f5" dependencies = [ - "indexmap 2.5.0", + "indexmap 2.6.0", "serde", "serde_spanned", "toml_datetime", @@ -1532,9 +1564,9 @@ checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" [[package]] name = "value-bag" -version = "1.9.0" +version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5a84c137d37ab0142f0f2ddfe332651fdbf252e7b7dbb4e67b6c1f1b2e925101" +checksum = "3ef4c4aa54d5d05a279399bfa921ec387b7aba77caf7a682ae8d86785b8fdad2" dependencies = [ "value-bag-serde1", "value-bag-sval2", @@ -1542,9 +1574,9 @@ dependencies = [ [[package]] name = "value-bag-serde1" -version = "1.9.0" +version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ccacf50c5cb077a9abb723c5bcb5e0754c1a433f1e1de89edc328e2760b6328b" +checksum = "4bb773bd36fd59c7ca6e336c94454d9c66386416734817927ac93d81cb3c5b0b" dependencies = [ "erased-serde", "serde", @@ -1553,9 +1585,9 @@ dependencies = [ [[package]] name = "value-bag-sval2" -version = "1.9.0" +version = "1.10.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1785bae486022dfb9703915d42287dcb284c1ee37bd1080eeba78cc04721285b" +checksum = "53a916a702cac43a88694c97657d449775667bcd14b70419441d05b7fea4a83a" dependencies = [ "sval", "sval_buffer", @@ -1582,6 +1614,17 @@ dependencies = [ "nom", ] +[[package]] +name = "visibility" +version = "0.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d674d135b4a8c1d7e813e2f8d1c9a58308aee4a680323066025e53132218bd91" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.87", +] + [[package]] name = "wait-timeout" version = "0.2.0" @@ -1609,9 +1652,9 @@ checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" [[package]] name = "wasm-bindgen" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a82edfc16a6c469f5f44dc7b571814045d60404b55a0ee849f9bcfa2e63dd9b5" +checksum = "128d1e363af62632b8eb57219c8fd7877144af57558fb2ef0368d0087bddeb2e" dependencies = [ "cfg-if", "once_cell", @@ -1620,9 +1663,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-backend" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9de396da306523044d3302746f1208fa71d7532227f15e347e2d93e4145dd77b" +checksum = "cb6dd4d3ca0ddffd1dd1c9c04f94b868c37ff5fac97c30b97cff2d74fce3a358" dependencies = [ "bumpalo", "log", @@ -1635,9 +1678,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "585c4c91a46b072c92e908d99cb1dcdf95c5218eeb6f3bf1efa991ee7a68cccf" +checksum = "e79384be7f8f5a9dd5d7167216f022090cf1f9ec128e6e6a482a2cb5c5422c56" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -1645,9 +1688,9 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "afc340c74d9005395cf9dd098506f7f44e38f2b4a21c6aaacf9a105ea5e1e836" +checksum = "26c6ab57572f7a24a4985830b120de1594465e5d500f24afe89e16b4e833ef68" dependencies = [ "proc-macro2", "quote", @@ -1658,9 +1701,25 @@ dependencies = [ [[package]] name = "wasm-bindgen-shared" -version = "0.2.93" +version = "0.2.95" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c62a0a307cb4a311d3a07867860911ca130c3494e8c2719593806c08bc5d0484" +checksum = "65fc09f10666a9f147042251e0dda9c18f166ff7de300607007e96bdebc1068d" + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" [[package]] name = "winapi-util" @@ -1671,6 +1730,12 @@ dependencies = [ "windows-sys 0.59.0", ] +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" + [[package]] name = "windows-core" version = "0.52.0" diff --git a/Cargo.toml b/Cargo.toml index 84c799cf36..2a7d8f2cb4 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,7 +4,7 @@ resolver = "2" default-members = [ "conjure_oxide", "crates/conjure_core", - "solvers/kissat", + "solvers/sat_rs", "solvers/minion", ] @@ -13,8 +13,8 @@ members = [ "crates/conjure_core", "crates/enum_compatability_macro", "crates/conjure_macros", - "solvers/kissat", - "solvers/minion", + "solvers/minion", + "solvers/sat_rs", ] [workspace.lints.clippy] diff --git a/conjure_oxide/Cargo.toml b/conjure_oxide/Cargo.toml index 2ed3cf3787..7a61629cec 100644 --- a/conjure_oxide/Cargo.toml +++ b/conjure_oxide/Cargo.toml @@ -31,6 +31,8 @@ schemars = "0.8.21" toml = "0.8.19" glob = "0.3.1" rand = "0.8.5" +rustsat = "0.6.1" +rustsat-minisat = "0.4.1" [features] diff --git a/crates/conjure_core/Cargo.toml b/crates/conjure_core/Cargo.toml index 5b55bd458d..39bafeda66 100644 --- a/crates/conjure_core/Cargo.toml +++ b/crates/conjure_core/Cargo.toml @@ -26,6 +26,9 @@ schemars = "0.8.21" clap = { version = "4.5.20", features = ["derive"] } itertools = "0.13.0" im = "15.1.0" +sat_rs = { version = "0.1.0", path = "../../solvers/sat_rs" } +rustsat-minisat = "0.4.0" +rustsat = "0.6.1" [lints] workspace = true diff --git a/crates/conjure_core/src/solver/adaptors/kissat.rs b/crates/conjure_core/src/solver/adaptors/kissat.rs deleted file mode 100644 index 15023841eb..0000000000 --- a/crates/conjure_core/src/solver/adaptors/kissat.rs +++ /dev/null @@ -1,63 +0,0 @@ -use crate::solver::{SolveSuccess, SolverCallback, SolverFamily, SolverMutCallback}; -use crate::Model as ConjureModel; - -use super::super::model_modifier::NotModifiable; -use super::super::private; -use super::super::SearchComplete::*; -use super::super::SearchIncomplete::*; -use super::super::SearchStatus::*; -use super::super::SolverAdaptor; -use super::super::SolverError; -use super::super::SolverError::*; -use super::super::SolverError::*; -use super::sat_common::CNFModel; - -/// A [SolverAdaptor] for interacting with the Kissat SAT solver. -pub struct Kissat { - __non_constructable: private::Internal, - model: Option, -} - -impl private::Sealed for Kissat {} - -impl Kissat { - pub fn new() -> Self { - Kissat { - __non_constructable: private::Internal, - model: None, - } - } -} - -impl Default for Kissat { - fn default() -> Self { - Kissat::new() - } -} - -impl SolverAdaptor for Kissat { - fn solve( - &mut self, - callback: SolverCallback, - _: private::Internal, - ) -> Result { - Err(OpNotImplemented("solve(): todo!".to_owned())) - } - - fn solve_mut( - &mut self, - callback: SolverMutCallback, - _: private::Internal, - ) -> Result { - Err(OpNotSupported("solve_mut".to_owned())) - } - - fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> { - self.model = Some(CNFModel::from_conjure(model)?); - Ok(()) - } - - fn get_family(&self) -> SolverFamily { - SolverFamily::SAT - } -} diff --git a/crates/conjure_core/src/solver/adaptors/mod.rs b/crates/conjure_core/src/solver/adaptors/mod.rs index 9311122ddf..29526681f0 100644 --- a/crates/conjure_core/src/solver/adaptors/mod.rs +++ b/crates/conjure_core/src/solver/adaptors/mod.rs @@ -1,11 +1,6 @@ -//! Solver adaptors. -#[doc(inline)] -pub use kissat::Kissat; #[doc(inline)] pub use minion::Minion; - -mod sat_common; - -mod kissat; +pub use rustsat::SAT; mod minion; +pub mod rustsat; diff --git a/crates/conjure_core/src/solver/adaptors/rustsat.rs b/crates/conjure_core/src/solver/adaptors/rustsat.rs new file mode 100644 index 0000000000..5fd7bb1f75 --- /dev/null +++ b/crates/conjure_core/src/solver/adaptors/rustsat.rs @@ -0,0 +1,363 @@ +use std::any::type_name; +use std::fmt::format; +use std::iter::Inspect; +use std::ptr::null; +use std::vec; + +use clap::error; +use minion_rs::ast::Model; +use rustsat::encodings::am1::Def; +use rustsat::solvers::{Solve, SolverResult}; +use rustsat::types::Var as satVar; +use sat_rs::conversions::{self, conv_to_clause, conv_to_formula}; +use std::collections::HashMap; + +use rustsat_minisat::core::Minisat; + +use crate::ast::{Expression, Name}; +use crate::metadata::Metadata; +use crate::solver::{self, SearchStatus, SolveSuccess, SolverCallback, SolverFamily, SolverMutCallback}; +use crate::stats::SolverStats; +use crate::{ast as conjure_ast, model, Model as ConjureModel}; + +use super::super::model_modifier::NotModifiable; +use super::super::private; +use super::super::SearchComplete::*; +use super::super::SearchIncomplete::*; +use super::super::SearchStatus::*; +use super::super::SolverAdaptor; +use super::super::SolverError; +use super::super::SolverError::*; +use super::super::SolverError::*; + +use rustsat::instances::SatInstance; + +use thiserror::Error; + +/// A [SolverAdaptor] for interacting with the SatSolver generic and the types thereof. + +pub struct SAT { + __non_constructable: private::Internal, + model_inst: Option, + var_map: Option>, + solver_inst: Minisat, +} + +impl private::Sealed for SAT {} + +impl Default for SAT { + fn default() -> Self { + SAT { + __non_constructable: private::Internal, + model_inst: None, + var_map: None, + solver_inst: Minisat::default(), + } + } +} + +impl SAT { + pub fn new(model: ConjureModel) -> Self { + let model_to_use: Option = Some(SatInstance::new()); + SAT { + __non_constructable: private::Internal, + model_inst: model_to_use, + var_map: None, + solver_inst: Minisat::default(), + } + } + + pub fn add_clause_to_mod(&self, clause_vec: Vec) -> () {} +} + +pub fn instantiate_model_from_conjure( + conjure_model: ConjureModel, +) -> Result { + let mut inst: SatInstance = SatInstance::new(); + + for var_name_ref in conjure_model.variables.keys() { + let curr_decision_var = conjure_model + .variables + .get(var_name_ref) + .ok_or_else(|| ModelInvalid(format!("variable {:?} not found", var_name_ref)))?; + + { + // todo: the scope change may be unneeded + // check domain, err if bad domain + let cdom = &curr_decision_var.domain; + if cdom != &conjure_ast::Domain::BoolDomain { + return Err(ModelFeatureNotSupported(format!( + "variable {:?}: expected BoolDomain, found: {:?}", + curr_decision_var, curr_decision_var.domain + ))); + } + } + } + + let md = Metadata { + clean: false, + etype: None, + }; + + let constraints_vec: Vec = conjure_model.get_constraints_vec(); + let vec_cnf = handle_and(Expression::And(md, constraints_vec)); + conv_to_formula(&(vec_cnf.unwrap()), &mut inst); + + Ok(inst) +} + +impl SolverAdaptor for SAT { + fn solve( + &mut self, + callback: SolverCallback, + _: private::Internal, + ) -> Result { + // solver = self.solver + // handle + let cnf_func: rustsat::instances::Cnf = self.model_inst.clone().unwrap().into_cnf().0; + &self.solver_inst.add_cnf(cnf_func); + let res = &self.solver_inst.solve().unwrap(); + + let solver_res = match res { + SolverResult::Sat => true, + SolverResult::Unsat => false, + + // should not arise: + SolverResult::Interrupted => Err(SolverError::Runtime(format!("SatInstance may be invalid, Interrupted.")))?, + }; + + // error thrown always. impermanent + // will eventually have a SolveSucess instance being returned with Ok(), when the implementation is more permanent. + // Ok(SolveSuccess{ + // // stats tbd, fails + // stats:SolverStats::with_timings(10.0), + // status: SearchStatus::Complete(()) + // }); + print!("{}", solver_res); + + Err(OpNotImplemented("solve_mut".to_owned())) + // Ok(()) + } + + fn solve_mut( + &mut self, + callback: SolverMutCallback, + _: private::Internal, + ) -> Result { + Err(OpNotSupported("solve_mut".to_owned())) + } + + fn load_model(&mut self, model: ConjureModel, _: private::Internal) -> Result<(), SolverError> { + let inst_res = instantiate_model_from_conjure(model); + self.model_inst = Some(inst_res.unwrap()); + Ok(()) + } + + fn get_family(&self) -> SolverFamily { + SolverFamily::SAT + } +} + +pub fn handle_expr(e: Expression) -> Result<(Vec>), CNFError> { + match e { + Expression::And(_, _) => Ok(handle_and(e).unwrap()), + _ => Err(CNFError::UnexpectedExpression(e)), + } +} + +pub fn get_namevar_as_int(name: Name) -> Result { + match name { + Name::MachineName(val) => Ok(val), + _ => Err(CNFError::BadVariableType(name)), + } +} + +pub fn handle_lit(e: Expression) -> Result { + match e { + Expression::Not(_, heap_expr) => { + let expr = *heap_expr; + match expr { + Expression::Nothing => todo!(), // panic? + Expression::Not(_md, e) => handle_lit(*e), + // todo(ss504): decide + Expression::Reference(_md, name) => { + let check = get_namevar_as_int(name).unwrap(); + match check == 0 { + true => Ok(1), + false => Ok(0), + } + } + _ => Err(CNFError::UnexpectedExpressionInsideNot(expr)), + } + } + Expression::Reference(_md, name) => get_namevar_as_int(name), + _ => Err(CNFError::UnexpectedLiteralExpression(e)), + } +} + +pub fn handle_or(e: Expression) -> Result<(Vec), CNFError> { + let vec_clause = match e { + Expression::Or(_md, vec) => vec, + _ => Err(CNFError::UnexpectedExpression(e))?, + }; + + // if vec_clause.len() != 2 { + // panic!("Villain, What hast thou done?\nThat which thou canst not undo.") + // }; + + let mut ret_clause: Vec = Vec::new(); + + for expr in vec_clause { + match expr { + Expression::Reference(_, _) => ret_clause.push(handle_lit(expr).unwrap()), + Expression::Not(_, _) => ret_clause.push(handle_lit(expr).unwrap()), + _ => Err(CNFError::UnexpectedExpressionInsideOr(expr))?, + } + } + + Ok(ret_clause) +} + +pub fn handle_and(e: Expression) -> Result<(Vec>), CNFError> { + let vec_cnf = match e { + Expression::And(_md, vec_and) => vec_and, + _ => panic!("Villain, What hast thou done?\nThat which thou canst not undo."), + }; + + let mut ret_vec_of_vecs: Vec> = Vec::new(); + + for expr in vec_cnf { + match expr { + Expression::Or(_, _) => ret_vec_of_vecs.push(handle_or(expr).unwrap()), + _ => Err(CNFError::UnexpectedExpressionInsideOr(expr))?, + } + } + + Ok(ret_vec_of_vecs) +} +//CNF Error, may be replaced of integrated with error file +#[derive(Error, Debug)] +pub enum CNFError { + #[error("Variable with name `{0}` not found")] + VariableNameNotFound(conjure_ast::Name), + + #[error("Variable with name `{0}` not of right type")] + BadVariableType(Name), + + #[error("Unexpected Expression `{0}` inside Not(). Only Not(Reference) or Not(Not) allowed!")] + UnexpectedExpressionInsideNot(Expression), + + #[error("Unexpected Expression `{0}` as literal. Only Not() or Reference() allowed!")] + UnexpectedLiteralExpression(Expression), + + #[error("Unexpected Expression `{0}` inside And(). Only And(vec) allowed!")] + UnexpectedExpressionInsideAnd(Expression), + + #[error("Unexpected Expression `{0}` inside Or(). Only Or(lit, lit) allowed!")] + UnexpectedExpressionInsideOr(Expression), + + #[error("Unexpected Expression `{0}` found!")] + UnexpectedExpression(Expression) +} +#[cfg(test)] +mod tests { + use super::*; + use crate::ast::{Expression, Name}; + use crate::metadata::Metadata; + use crate::solver::{self, SearchStatus, SolveSuccess, SolverCallback, SolverFamily, SolverMutCallback}; + use crate::stats::SolverStats; + use crate::{ast as conjure_ast, model, Model as ConjureModel}; + + + #[test] + fn test_handle_expr_unexpected_expression() { + let expr = Expression::Not(Metadata::new(), Box::new(Expression::Reference(Metadata::new(), Name::MachineName(1)))); + let result = handle_expr(expr); + assert!(matches!(result, Err(CNFError::UnexpectedExpression(_)))); + } + + #[test] + fn test_handle_lit_unexpected_expression_inside_not() { + let expr = Expression::Not(Metadata::new(), Box::new(Expression::And(Metadata::new(), vec![]))); + let result = handle_lit(expr); + assert!(matches!(result, Err(CNFError::UnexpectedExpressionInsideNot(_)))); + } + + #[test] + fn test_handle_lit_unexpected_literal_expression() { + let expr = Expression::And(Metadata::new(), vec![]); + let result = handle_lit(expr); + assert!(matches!(result, Err(CNFError::UnexpectedLiteralExpression(_)))); + } + + #[test] + fn test_handle_or_unexpected_expression_inside_or() { + let expr = Expression::Or( + Metadata::new(), + vec![ + Expression::Reference(Metadata::new(), Name::MachineName(1)), + Expression::And(Metadata::new(), vec![]), + ], + ); + let result = handle_or(expr); + assert!(matches!(result, Err(CNFError::UnexpectedExpressionInsideOr(_)))); + } + + #[test] + fn test_handle_expr_success_badval() { + let expr = Expression::And( + Metadata::new(), + vec![ + Expression::Or(Metadata::new(), vec![ + Expression::Reference(Metadata::new(), Name::MachineName(1)), + Expression::Reference(Metadata::new(), Name::MachineName(2)), + ]), + ], + ); + let result = handle_expr(expr); + assert!(result.is_ok()); + let cnf_result = result.unwrap(); + assert_eq!(cnf_result.len(), 1); // Check that we have one clause + assert_eq!(cnf_result[0].len(), 2); // Check that the clause has two literals + } + + #[test] + fn test_handle_expr_success_goodval() { + let expr = Expression::And( + Metadata::new(), + vec![ + Expression::Or(Metadata::new(), vec![ + Expression::Reference(Metadata::new(), Name::MachineName(0)), + Expression::Reference(Metadata::new(), Name::MachineName(0)), + ]), + ], + ); + let result = handle_expr(expr); + assert!(result.is_ok()); + let cnf_result = result.unwrap(); + // Check number of clauses + assert_eq!(cnf_result.len(), 1); + + // Check number of literals in clause + assert_eq!(cnf_result[0].len(), 2); + + // check literals + assert_eq!(cnf_result[0][0], 0); + assert_eq!(cnf_result[0][1], 0); + } + + #[test] + fn test_handle_lit() { + let expr = Expression::Not( + Metadata::new(), + Box::new( + Expression::Reference(Metadata::new(), Name::MachineName(0)), + ) + ); + + let result = handle_lit(expr); + assert!(result.is_ok()); + let lit_result = result.unwrap(); + assert_eq!(lit_result, 1); // Check that we have one clause + } +} diff --git a/crates/conjure_core/src/solver/adaptors/sat_common.rs b/crates/conjure_core/src/solver/adaptors/sat_common.rs deleted file mode 100644 index 746286e39a..0000000000 --- a/crates/conjure_core/src/solver/adaptors/sat_common.rs +++ /dev/null @@ -1,324 +0,0 @@ -//! Common code for SAT adaptors. -//! Primarily, this is CNF related code. - -use std::collections::HashMap; - -use thiserror::Error; - -use crate::{ - ast as conjure_ast, solver::SolverError, solver::SolverError::*, Model as ConjureModel, -}; -// (nd60, march 24) - i basically copied all this from @gskorokod's SAT implemention for the old -// solver interface. -use crate::metadata::Metadata; - -/// A representation of a model in CNF. -/// -/// Expects Model to be in the Conjunctive Normal Form: -/// -/// - All variables must be boolean -/// - Expressions must be `Reference`, `Not(Reference)`, or `Or(Reference1, Not(Reference2), ...)` -/// - The top level And() may contain nested Or()s. Any other nested expressions are not allowed. -#[derive(Debug, Clone)] -pub struct CNFModel { - pub clauses: Vec>, - variables: HashMap, - next_ind: i32, -} -impl CNFModel { - pub fn new() -> CNFModel { - CNFModel { - clauses: Vec::new(), - variables: HashMap::new(), - next_ind: 1, - } - } - - pub fn from_conjure(conjure_model: ConjureModel) -> Result { - let mut ans: CNFModel = CNFModel::new(); - - for var in conjure_model.variables.keys() { - // Check that domain has the correct type - let decision_var = match conjure_model.variables.get(var) { - None => { - return Err(ModelInvalid(format!("variable {:?} not found", var))); - } - Some(var) => var, - }; - - if decision_var.domain != conjure_ast::Domain::BoolDomain { - return Err(ModelFeatureNotSupported(format!( - "variable {:?} is not BoolDomain", - decision_var - ))); - } - - ans.add_variable(var); - } - - for expr in conjure_model.get_constraints_vec() { - match ans.add_expression(&expr) { - Ok(_) => {} - Err(error) => { - let message = format!("{:?}", error); - return Err(ModelFeatureNotSupported(message)); - } - } - } - - Ok(ans) - } - - /// Gets all the Conjure variables in the CNF. - #[allow(dead_code)] // It will be used once we actually run kissat - pub fn get_variables(&self) -> Vec<&conjure_ast::Name> { - let mut ans: Vec<&conjure_ast::Name> = Vec::new(); - - for key in self.variables.keys() { - ans.push(key); - } - - ans - } - - /// Gets the index of a Conjure variable. - pub fn get_index(&self, var: &conjure_ast::Name) -> Option { - return self.variables.get(var).copied(); - } - - /// Gets a Conjure variable by index. - pub fn get_name(&self, ind: i32) -> Option<&conjure_ast::Name> { - for key in self.variables.keys() { - let idx = self.get_index(key)?; - if idx == ind { - return Some(key); - } - } - - None - } - - /// Adds a new Conjure variable to the CNF representation. - pub fn add_variable(&mut self, var: &conjure_ast::Name) { - self.variables.insert(var.clone(), self.next_ind); - self.next_ind += 1; - } - - /** - * Check if a Conjure variable or index is present in the CNF - */ - pub fn has_variable(&self, value: T) -> bool { - value.has_variable(self) - } - - /** - * Add a new clause to the CNF. Must be a vector of indices in CNF format - */ - pub fn add_clause(&mut self, vec: &Vec) -> Result<(), CNFError> { - for idx in vec { - if !self.has_variable(idx.abs()) { - return Err(CNFError::ClauseIndexNotFound(*idx)); - } - } - self.clauses.push(vec.clone()); - Ok(()) - } - - /** - * Add a new Conjure expression to the CNF. Must be a logical expression in CNF form - */ - pub fn add_expression(&mut self, expr: &conjure_ast::Expression) -> Result<(), CNFError> { - for row in self.handle_expression(expr)? { - self.add_clause(&row)?; - } - Ok(()) - } - - /** - * Convert the CNF to a Conjure expression - */ - #[allow(dead_code)] // It will be used once we actually run kissat - pub fn as_expression(&self) -> Result { - let mut expr_clauses: Vec = Vec::new(); - - for clause in &self.clauses { - expr_clauses.push(self.clause_to_expression(clause)?); - } - - Ok(conjure_ast::Expression::And(Metadata::new(), expr_clauses)) - } - - /** - * Convert a single clause to a Conjure expression - */ - fn clause_to_expression(&self, clause: &Vec) -> Result { - let mut ans: Vec = Vec::new(); - - for idx in clause { - match self.get_name(idx.abs()) { - None => return Err(CNFError::ClauseIndexNotFound(*idx)), - Some(name) => { - if *idx > 0 { - ans.push(conjure_ast::Expression::Reference( - Metadata::new(), - name.clone(), - )); - } else { - let expression: conjure_ast::Expression = - conjure_ast::Expression::Reference(Metadata::new(), name.clone()); - ans.push(conjure_ast::Expression::Not( - Metadata::new(), - Box::from(expression), - )) - } - } - } - } - - Ok(conjure_ast::Expression::Or(Metadata::new(), ans)) - } - - /** - * Get the index for a Conjure Reference or return an error - * @see get_index - * @see conjure_ast::Expression::Reference - */ - fn get_reference_index(&self, name: &conjure_ast::Name) -> Result { - match self.get_index(name) { - None => Err(CNFError::VariableNameNotFound(name.clone())), - Some(ind) => Ok(ind), - } - } - - /** - * Convert the contents of a single Reference to a row of the CNF format - * @see get_reference_index - * @see conjure_ast::Expression::Reference - */ - fn handle_reference(&self, name: &conjure_ast::Name) -> Result, CNFError> { - Ok(vec![self.get_reference_index(name)?]) - } - - /** - * Convert the contents of a single Not() to CNF - */ - fn handle_not(&self, expr: &conjure_ast::Expression) -> Result, CNFError> { - match expr { - // Expression inside the Not() - conjure_ast::Expression::Reference(_metadata, name) => { - Ok(vec![-self.get_reference_index(name)?]) - } - _ => Err(CNFError::UnexpectedExpressionInsideNot(expr.clone())), - } - } - - /** - * Convert the contents of a single Or() to a row of the CNF format - */ - fn handle_or(&self, expressions: &Vec) -> Result, CNFError> { - let mut ans: Vec = Vec::new(); - - for expr in expressions { - let ret = self.handle_flat_expression(expr)?; - for ind in ret { - ans.push(ind); - } - } - - Ok(ans) - } - - /** - * Convert a single Reference, `Not` or `Or` into a clause of the CNF format - */ - fn handle_flat_expression( - &self, - expression: &conjure_ast::Expression, - ) -> Result, CNFError> { - match expression { - conjure_ast::Expression::Reference(_metadata, name) => self.handle_reference(name), - conjure_ast::Expression::Not(_metadata, var_box) => self.handle_not(var_box), - conjure_ast::Expression::Or(_metadata, expressions) => self.handle_or(expressions), - _ => Err(CNFError::UnexpectedExpression(expression.clone())), - } - } - - /** - * Convert a single And() into a vector of clauses in the CNF format - */ - fn handle_and( - &self, - expressions: &Vec, - ) -> Result>, CNFError> { - let mut ans: Vec> = Vec::new(); - - for expression in expressions { - match expression { - conjure_ast::Expression::And(_metadata, _expressions) => { - return Err(CNFError::NestedAnd(expression.clone())); - } - _ => { - ans.push(self.handle_flat_expression(expression)?); - } - } - } - - Ok(ans) - } - - /** - * Convert a single Conjure expression into a vector of clauses of the CNF format - */ - fn handle_expression( - &self, - expression: &conjure_ast::Expression, - ) -> Result>, CNFError> { - match expression { - conjure_ast::Expression::And(_metadata, expressions) => self.handle_and(expressions), - _ => Ok(vec![self.handle_flat_expression(expression)?]), - } - } -} - -impl Default for CNFModel { - fn default() -> Self { - Self::new() - } -} - -#[derive(Error, Debug)] -pub enum CNFError { - #[error("Variable with name `{0}` not found")] - VariableNameNotFound(conjure_ast::Name), - - #[error("Clause with index `{0}` not found")] - ClauseIndexNotFound(i32), - - #[error("Unexpected Expression `{0}` inside Not(). Only Not(Reference) allowed!")] - UnexpectedExpressionInsideNot(conjure_ast::Expression), - - #[error( - "Unexpected Expression `{0}` found. Only Reference, Not(Reference) and Or(...) allowed!" - )] - UnexpectedExpression(conjure_ast::Expression), - - #[error("Unexpected nested And: {0}")] - NestedAnd(conjure_ast::Expression), -} - -/// Helper trait for checking if a variable is present in the CNF polymorphically (i32 or conjure_ast::Name) -pub trait HasVariable { - fn has_variable(self, cnf: &CNFModel) -> bool; -} - -impl HasVariable for i32 { - fn has_variable(self, cnf: &CNFModel) -> bool { - return cnf.get_name(self).is_some(); - } -} - -impl HasVariable for &conjure_ast::Name { - fn has_variable(self, cnf: &CNFModel) -> bool { - cnf.get_index(self).is_some() - } -} diff --git a/solvers/kissat/Cargo.toml b/solvers/kissat/Cargo.toml deleted file mode 100644 index 5d228436b9..0000000000 --- a/solvers/kissat/Cargo.toml +++ /dev/null @@ -1,10 +0,0 @@ -[package] -name = "kissat_rs" -version = "0.1.0" -edition = "2021" - -# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html - -[dependencies] -kissat-rs = { git = "https://github.com/firefighterduck/kissat-rs", branch = "main", version = "0.1" } -kissat-sys = { git = "https://github.com/firefighterduck/kissat-rs", branch = "main", version = "0.1" } diff --git a/solvers/kissat/src/lib.rs b/solvers/kissat/src/lib.rs deleted file mode 100644 index e7de73bf4a..0000000000 --- a/solvers/kissat/src/lib.rs +++ /dev/null @@ -1,31 +0,0 @@ -#[cfg(test)] -#[test] -fn test1() { - use kissat_rs::Assignment; - use kissat_rs::Solver; - - // Define three literals used in both formulae. - let x = 1; - let y = 2; - let z = 3; - - // Construct a formula from clauses (i.e. an iterator over literals). - // (~x || y) && (~y || z) && (x || ~z) && (x || y || z) - let formula1 = vec![vec![-x, y], vec![-y, z], vec![x, -z], vec![x, y, z]]; - let satisfying_assignment = Solver::solve_formula(formula1).unwrap(); - - // The formula from above is satisfied by the assignment: x -> True, y -> True, z -> True - if let Some(assignments) = satisfying_assignment { - assert_eq!(assignments.get(&x).unwrap(), &Some(Assignment::True)); - assert_eq!(assignments.get(&y).unwrap(), &Some(Assignment::True)); - assert_eq!(assignments.get(&z).unwrap(), &Some(Assignment::True)); - } - - // (x || y || ~z) && ~x && (x || y || z) && (x || ~y) - let formula2 = vec![vec![x, y, -z], vec![-x], vec![x, y, z], vec![x, -y]]; - let unsat_result = Solver::solve_formula(formula2).unwrap(); - - // The second formula is unsatisfiable. - // This can for example be proved by resolution. - assert_eq!(unsat_result, None); -} diff --git a/solvers/sat_rs/Cargo.toml b/solvers/sat_rs/Cargo.toml new file mode 100644 index 0000000000..49eeac13bd --- /dev/null +++ b/solvers/sat_rs/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "sat_rs" +version = "0.1.0" +edition = "2021" + +[dependencies] +anyhow = "1.0.93" +rustsat = "0.6.1" +rustsat-minisat = "0.4.1" + +[lints] +workspace = true diff --git a/solvers/sat_rs/src/conversions.rs b/solvers/sat_rs/src/conversions.rs new file mode 100644 index 0000000000..ac19a03a14 --- /dev/null +++ b/solvers/sat_rs/src/conversions.rs @@ -0,0 +1,50 @@ +use anyhow::{anyhow, Result}; +use rustsat::instances::SatInstance; +use rustsat::types::{Clause, Lit, Var}; +use std::collections::HashMap; + +pub fn conv_to_clause( + to_convert: &Vec, + instance_in_use: &mut SatInstance, + var_map: &mut HashMap, +) -> Result<()> { + let lits: Vec = to_convert + .iter() + .map(|&num| mk_lit(num, instance_in_use, var_map)) + .collect::, anyhow::Error>>()?; + let clause: Clause = lits.into_iter().collect(); + instance_in_use.add_clause(clause); + Ok(()) +} + +pub fn mk_lit( + num: i32, + instance_in_use: &mut SatInstance, + var_map: &mut HashMap, +) -> Result { + if num == 0 { + return Err(anyhow!("Variable index cannot be zero. Received: {}", num)); + } + + let var_index = num.abs(); + let var = if let Some(&v) = var_map.get(&var_index) { + v + } else { + let v = instance_in_use.new_var(); + var_map.insert(var_index, v); + v + }; + if num > 0 { + Ok(var.pos_lit()) + } else { + Ok(var.neg_lit()) + } +} + +pub fn conv_to_formula(vec_cnf: &Vec>, instance_in_use: &mut SatInstance) -> Result<()> { + let mut var_map: HashMap = HashMap::new(); + for clause in vec_cnf { + conv_to_clause(clause, instance_in_use, &mut var_map)?; + } + Ok(()) +} diff --git a/solvers/sat_rs/src/lib.rs b/solvers/sat_rs/src/lib.rs new file mode 100644 index 0000000000..88badee163 --- /dev/null +++ b/solvers/sat_rs/src/lib.rs @@ -0,0 +1,3 @@ +pub mod conversions; +pub mod solvers; +pub mod utils; diff --git a/solvers/sat_rs/src/solvers.rs b/solvers/sat_rs/src/solvers.rs new file mode 100644 index 0000000000..9b69e69887 --- /dev/null +++ b/solvers/sat_rs/src/solvers.rs @@ -0,0 +1,74 @@ +use anyhow::{Error, Result}; +use rustsat::instances::SatInstance; +use rustsat::solvers::{Solve, SolverResult}; +use rustsat_minisat::simp::Minisat; + +pub trait Solver { + fn solve(&self, instance: &SatInstance) -> Result; +} + +pub struct SatSolver { + solver: SolverType, +} + +impl SatSolver { + pub fn new(solver: SolverType) -> Self { + SatSolver { solver } + } + + pub fn solve(&self, inst: SatInstance) -> Result { + self.solver.solve(&inst) + } + + pub fn solver_instance(&self) -> &SolverType { + &self.solver + } +} + +impl Solver for Minisat { + fn solve(&self, instance: &SatInstance) -> Result { + let res: Result = self.solve(instance); + res + } +} + +#[cfg(test)] +mod tests { + use super::*; + use rustsat::instances::SatInstance; + use std::collections::HashMap; + + #[test] + fn test_minisat_solver_satisfiable() { + let mut instance = SatInstance::new(); + // Example: (1 OR -2) AND (-1 OR 2) + let clause1 = vec![1, -2]; + let clause2 = vec![-1, 2]; + let mut var_map = HashMap::new(); + crate::conversions::conv_to_clause(&clause1, &mut instance, &mut var_map).unwrap(); + crate::conversions::conv_to_clause(&clause2, &mut instance, &mut var_map).unwrap(); + + let solver = Minisat::default(); + let sat_solver = SatSolver::new(solver); + let result = sat_solver.solve(instance).unwrap(); + + assert_eq!(result, SolverResult::Sat); + } + + #[test] + fn test_minisat_solver_unsatisfiable() { + let mut instance = SatInstance::new(); + // Example: (1) AND (-1) + let clause1 = vec![1]; + let clause2 = vec![-1]; + let mut var_map = HashMap::new(); + crate::conversions::conv_to_clause(&clause1, &mut instance, &mut var_map).unwrap(); + crate::conversions::conv_to_clause(&clause2, &mut instance, &mut var_map).unwrap(); + + let solver = Minisat::default(); + let sat_solver = SatSolver::new(solver); + let result = sat_solver.solve(instance).unwrap(); + + assert_eq!(result, SolverResult::Unsat); + } +} diff --git a/solvers/sat_rs/src/utils.rs b/solvers/sat_rs/src/utils.rs new file mode 100644 index 0000000000..e0fe5f38c2 --- /dev/null +++ b/solvers/sat_rs/src/utils.rs @@ -0,0 +1,55 @@ +use crate::solvers::SatSolver; +use crate::conversions::conv_to_formula; +use anyhow::{Error, Result}; +use rustsat::instances::SatInstance; +use rustsat::solvers::SolverResult; +use rustsat_minisat::simp::Minisat; + +pub fn initialize_solver(vec_problem: &Vec>) -> Result<(SatSolver, SatInstance)> { + let mut inst: SatInstance = SatInstance::new(); + conv_to_formula(vec_problem, &mut inst)?; + let minisat_solver = Minisat::default(); + let sat_solver = SatSolver::new(minisat_solver); + Ok((sat_solver, inst)) +} + +pub fn solve_problem( + sat_solver: &SatSolver, + instance: SatInstance, +) -> Result { + let res = sat_solver.solve(instance)?; + Ok(res) +} + +#[cfg(test)] +mod tests { + use super::*; + use rustsat::{instances::SatInstance, solvers::SolverResult}; + use std::collections::HashMap; + + #[test] + fn test_initialize_and_solve_satisfiable() { + let problem = vec![ + vec![1, 2, -3], + vec![-1, 3], + vec![2, -3], + vec![-2, 3], + vec![1, -2], + ]; + + let (sat_solver, inst) = initialize_solver(&problem).unwrap(); + let result = solve_problem(&sat_solver, inst).unwrap(); + + assert_eq!(result, SolverResult::Sat); + } + + #[test] + fn test_initialize_and_solve_unsatisfiable() { + let problem = vec![vec![1], vec![-1]]; + + let (sat_solver, inst) = initialize_solver(&problem).unwrap(); + let result = solve_problem(&sat_solver, inst).unwrap(); + + assert_eq!(result, SolverResult::Unsat); + } +}