summaryrefslogtreecommitdiffstats
path: root/vendor/varisat
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/varisat')
-rw-r--r--vendor/varisat/.cargo-checksum.json1
-rw-r--r--vendor/varisat/Cargo.toml85
-rw-r--r--vendor/varisat/LICENSE-APACHE201
-rw-r--r--vendor/varisat/LICENSE-MIT25
-rw-r--r--vendor/varisat/README.md51
-rw-r--r--vendor/varisat/build.rs48
-rw-r--r--vendor/varisat/proptest-regressions/solver.txt7
-rw-r--r--vendor/varisat/src/analyze_conflict.rs368
-rw-r--r--vendor/varisat/src/assumptions.rs376
-rw-r--r--vendor/varisat/src/binary.rs100
-rw-r--r--vendor/varisat/src/cdcl.rs264
-rw-r--r--vendor/varisat/src/clause.rs67
-rw-r--r--vendor/varisat/src/clause/activity.rs107
-rw-r--r--vendor/varisat/src/clause/alloc.rs262
-rw-r--r--vendor/varisat/src/clause/assess.rs69
-rw-r--r--vendor/varisat/src/clause/db.rs269
-rw-r--r--vendor/varisat/src/clause/gc.rs207
-rw-r--r--vendor/varisat/src/clause/header.rs148
-rw-r--r--vendor/varisat/src/clause/reduce.rs132
-rw-r--r--vendor/varisat/src/config.rs31
-rw-r--r--vendor/varisat/src/context.rs131
-rw-r--r--vendor/varisat/src/decision.rs58
-rw-r--r--vendor/varisat/src/decision/vsids.rs346
-rw-r--r--vendor/varisat/src/glue.rs36
-rw-r--r--vendor/varisat/src/lib.rs46
-rw-r--r--vendor/varisat/src/load.rs259
-rw-r--r--vendor/varisat/src/model.rs87
-rw-r--r--vendor/varisat/src/proof.rs434
-rw-r--r--vendor/varisat/src/proof/drat.rs85
-rw-r--r--vendor/varisat/src/proof/map_step.rs128
-rw-r--r--vendor/varisat/src/prop.rs261
-rw-r--r--vendor/varisat/src/prop/assignment.rs237
-rw-r--r--vendor/varisat/src/prop/binary.rs36
-rw-r--r--vendor/varisat/src/prop/graph.rs137
-rw-r--r--vendor/varisat/src/prop/long.rs164
-rw-r--r--vendor/varisat/src/prop/watch.rs135
-rw-r--r--vendor/varisat/src/schedule.rs101
-rw-r--r--vendor/varisat/src/schedule/luby.rs52
-rw-r--r--vendor/varisat/src/solver.rs512
-rw-r--r--vendor/varisat/src/state.rs42
-rw-r--r--vendor/varisat/src/tmp.rs35
-rw-r--r--vendor/varisat/src/unit_simplify.rs198
-rw-r--r--vendor/varisat/src/variables.rs669
-rw-r--r--vendor/varisat/src/variables/data.rs70
-rw-r--r--vendor/varisat/src/variables/var_map.rs124
-rw-r--r--vendor/varisat/tests/checker.rs193
-rw-r--r--vendor/varisat/tests/cnfs.rs27
-rw-r--r--vendor/varisat/tests/cnfs/sgen1_sat_90_0.cnf217
-rw-r--r--vendor/varisat/tests/cnfs/sgen1_unsat_57_0.cnf125
49 files changed, 7763 insertions, 0 deletions
diff --git a/vendor/varisat/.cargo-checksum.json b/vendor/varisat/.cargo-checksum.json
new file mode 100644
index 000000000..5a9da2546
--- /dev/null
+++ b/vendor/varisat/.cargo-checksum.json
@@ -0,0 +1 @@
+{"files":{"Cargo.toml":"21ce29b910fa74cb7bc2e46fa12466dbc22afca75a4398df05121f09ab07a220","LICENSE-APACHE":"a60eea817514531668d7e00765731449fe14d059d3249e0bc93b36de45f759f2","LICENSE-MIT":"2259cbb177661977dd5510c05a8670da3cb28aa7f4ff74c193798db496fe92d8","README.md":"ad1aca8172568a522d6e476f3245a44b8fed8097a2c4b353bc01989c8c8a4419","build.rs":"f02c2967a2265e95e0305d66adc164082634962db16d53f91f65baa81f06e0ae","proptest-regressions/solver.txt":"62f46e379e51cf2b2b207e2605a2462bdc92a7970df823ec4fd18683135a52c7","src/analyze_conflict.rs":"aad17da2ce3cc7902cff7b3a2fe419231e4ea4536f58213a644cfa25efcd433c","src/assumptions.rs":"0e0c0374c11b64d03daaca9c955b668890cc7a8911554e3772d71edb2c7a96cc","src/binary.rs":"5d9ad1e92799338d770389dfd0b48118f4ecfc559bd13e98c19c22d0b662e243","src/cdcl.rs":"0d9eb122cfab68eb02f3498a8a7a31c3c6444d9c87beb868f0b463cd885f0cef","src/clause.rs":"9b04487436875255143df5dc1cd07229c7a6578a0d52951e9a0cce2162ce6448","src/clause/activity.rs":"d4377517ceffc65eede5d7323d1fef9a9adaadad1d406f978f61de1d8941c5d3","src/clause/alloc.rs":"f0f30f17c3b8703e4147eae374b7fe0640276002718f44b73084c59cd029f8b3","src/clause/assess.rs":"239b9be0dd566bb7295fd2015ffa9e4bc24b542f106df642835305f8dac221a0","src/clause/db.rs":"58d50caa94db1015f83674bf2426438d87f799231cc85a77749ee3420a5730f3","src/clause/gc.rs":"981b25ec3eca4b84c51df6b912c487c9780055b91f8858ec3ab23b900dab5f1c","src/clause/header.rs":"a1d16bfac19ba7b3f2326a2296b4200ca5f1d2769e6d716d623ae595d41bb3e0","src/clause/reduce.rs":"7bd26e64afde13a77113cc919c56a049cf9b9dd5df137219f441a354f3b1326f","src/config.rs":"9c706c4e7e11a04a098409c9c70dd2bb2109f4649da4a5d54a0a628fd8a7638d","src/context.rs":"5533c6a2a14d8fe6d5b1ec37ae474d40dac8456697a0bb8e14eb5bd7ed0a1e19","src/decision.rs":"5f1e17b514c43ede94978c5dc4d74a9a1a20fb127f0c621439ffd78e6c90edef","src/decision/vsids.rs":"01a6c73f830162ccff3b8e741b3a75a761b21398319edc531dfba5edebaa62f8","src/glue.rs":"c20a45d317db29f7e192ee0b263d72ac4234d0a57faec835c0081024f9c29e71","src/lib.rs":"c840e41c370f06ef96d3bd8f6c3bcdad85a52b81c37b32bcf4f1d5440e236721","src/load.rs":"a78e4a9bc0806407ef1d47ab1089cb005749d743e7dbea7950983e710eb89ffe","src/model.rs":"5c2ca7da7afe414fdc7c51d759ee5a9d2178d30a3e667489d778b72b23da81a8","src/proof.rs":"06a5fcbe4c799a5882adeb250f97bcdfad832d6d7a041503cd89865727ad0513","src/proof/drat.rs":"c27f66a4bb27046bb152adbcd08cd555411623f524876763d8265dce5d8404c3","src/proof/map_step.rs":"9167b80d217019163ee52539c179b36b6f79999f5c2715e7459bed7116d0986b","src/prop.rs":"5fe93c2b5083bbb916e52ced937aca1c0f84cac5c039568fa4bdcf6f120cb34a","src/prop/assignment.rs":"6a208beb26d4e37a61e85bfec708b6cac0f48d01096a726f83e105a73deb941b","src/prop/binary.rs":"48b57ca120dcbcf68a5a35f9b45c665d8eee9ffe7070fad63e820a56aff1ed1b","src/prop/graph.rs":"8cc58f977a6d9cc878afbe5cb8d3bd6cf63555d8b015da989b995913832dd6c0","src/prop/long.rs":"8f6761010c8e5bf85297236fdd2af7bd6b229c1500542b475a257d8f2d7bfc57","src/prop/watch.rs":"cbe9ec16f2e983c0a9877fe63afd407b6109f0a482391ce0fca1e0e14176c441","src/schedule.rs":"bff34535fc65c1639da1699f59985c1728e81f2f7608d42328345b9f815ee6d2","src/schedule/luby.rs":"a16b68688dcb8fb3e98f05bb9383c0d9c1bad391231b7ff7e056c12d2ad4bdaa","src/solver.rs":"4b975f617e21b4fbf5aea47757c3f01ed38fc05d2fc8de61973da60a8bbcefd4","src/state.rs":"012dc415965f5c7a220aca707d8936bd1e2ad84e481e3a11dce34cf403cf90e8","src/tmp.rs":"715381a3cd8119d781582d972afb42463a252a76cf9f927807a9568f893b7527","src/unit_simplify.rs":"28606a72d7d8d0667b027f135b3ee62e61796e61971ccd4af5fd40c1b1697cb2","src/variables.rs":"d0e0d6f34212ddd8f1847ce4c4f6070294a5934e1143555f35a67e86b848679b","src/variables/data.rs":"0a4057da30251e476e40e37417d768755ca00add3e3f80992fccfec7da7f347d","src/variables/var_map.rs":"689de26a54a7c1bdb41a576faa398bcd6f83603306716ec88a000e0bb9b25783","tests/checker.rs":"102be4f4ad9fdb8e0177e266e87fad61ddbf6157c4ffe23ac0eaae89fea898dc","tests/cnfs.rs":"a32c9492cc115cf201704379c7966b1b710499cc01ec2d29a3699c1878a9ac79","tests/cnfs/sgen1_sat_90_0.cnf":"3aef3970087c0370c01ec159a2e462887cdb7519024b772a1dc9f54168ba4607","tests/cnfs/sgen1_unsat_57_0.cnf":"888c236d8a5bda36fc3df4a61bb841a0da6ae8a735eaf20fedff2479342687de"},"package":"ebe609851d1e9196674ac295f656bd8601200a1077343d22b345013497807caf"} \ No newline at end of file
diff --git a/vendor/varisat/Cargo.toml b/vendor/varisat/Cargo.toml
new file mode 100644
index 000000000..a8030e6d5
--- /dev/null
+++ b/vendor/varisat/Cargo.toml
@@ -0,0 +1,85 @@
+# THIS FILE IS AUTOMATICALLY GENERATED BY CARGO
+#
+# When uploading crates to the registry Cargo will automatically
+# "normalize" Cargo.toml files for maximal compatibility
+# with all versions of Cargo and also rewrite `path` dependencies
+# to registry (e.g., crates.io) dependencies
+#
+# If you believe there's an error in this file please file an
+# issue against the rust-lang/cargo repository. If you're
+# editing this file be aware that the upstream Cargo.toml
+# will likely look very different (and much more reasonable)
+
+[package]
+edition = "2018"
+name = "varisat"
+version = "0.2.2"
+authors = ["Jannis Harder <me@jix.one>"]
+build = "build.rs"
+description = "A CDCL based SAT solver (library)"
+homepage = "https://jix.one/project/varisat/"
+readme = "README.md"
+license = "MIT/Apache-2.0"
+repository = "https://github.com/jix/varisat"
+[dependencies.anyhow]
+version = "1.0.32"
+
+[dependencies.itoa]
+version = "0.4.4"
+
+[dependencies.leb128]
+version = "0.2.4"
+
+[dependencies.log]
+version = "0.4.6"
+
+[dependencies.ordered-float]
+version = "2.0.0"
+
+[dependencies.partial_ref]
+version = "0.3.1"
+
+[dependencies.rustc-hash]
+version = "1.1.0"
+
+[dependencies.serde]
+version = "1.0.91"
+features = ["derive"]
+
+[dependencies.thiserror]
+version = "1.0.20"
+
+[dependencies.varisat-checker]
+version = "=0.2.2"
+
+[dependencies.varisat-dimacs]
+version = "=0.2.2"
+
+[dependencies.varisat-formula]
+version = "=0.2.2"
+
+[dependencies.varisat-internal-macros]
+version = "=0.2.2"
+
+[dependencies.varisat-internal-proof]
+version = "=0.2.2"
+
+[dependencies.vec_mut_scan]
+version = "0.3.0"
+[dev-dependencies.env_logger]
+version = "0.7.1"
+
+[dev-dependencies.proptest]
+version = "0.10.1"
+
+[dev-dependencies.rand]
+version = "0.7.3"
+
+[dev-dependencies.tempfile]
+version = "3.0.8"
+
+[dev-dependencies.varisat-formula]
+version = "=0.2.2"
+features = ["proptest-strategies", "internal-testing"]
+[build-dependencies.anyhow]
+version = "1.0.32"
diff --git a/vendor/varisat/LICENSE-APACHE b/vendor/varisat/LICENSE-APACHE
new file mode 100644
index 000000000..16fe87b06
--- /dev/null
+++ b/vendor/varisat/LICENSE-APACHE
@@ -0,0 +1,201 @@
+ Apache License
+ Version 2.0, January 2004
+ http://www.apache.org/licenses/
+
+TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION
+
+1. Definitions.
+
+ "License" shall mean the terms and conditions for use, reproduction,
+ and distribution as defined by Sections 1 through 9 of this document.
+
+ "Licensor" shall mean the copyright owner or entity authorized by
+ the copyright owner that is granting the License.
+
+ "Legal Entity" shall mean the union of the acting entity and all
+ other entities that control, are controlled by, or are under common
+ control with that entity. For the purposes of this definition,
+ "control" means (i) the power, direct or indirect, to cause the
+ direction or management of such entity, whether by contract or
+ otherwise, or (ii) ownership of fifty percent (50%) or more of the
+ outstanding shares, or (iii) beneficial ownership of such entity.
+
+ "You" (or "Your") shall mean an individual or Legal Entity
+ exercising permissions granted by this License.
+
+ "Source" form shall mean the preferred form for making modifications,
+ including but not limited to software source code, documentation
+ source, and configuration files.
+
+ "Object" form shall mean any form resulting from mechanical
+ transformation or translation of a Source form, including but
+ not limited to compiled object code, generated documentation,
+ and conversions to other media types.
+
+ "Work" shall mean the work of authorship, whether in Source or
+ Object form, made available under the License, as indicated by a
+ copyright notice that is included in or attached to the work
+ (an example is provided in the Appendix below).
+
+ "Derivative Works" shall mean any work, whether in Source or Object
+ form, that is based on (or derived from) the Work and for which the
+ editorial revisions, annotations, elaborations, or other modifications
+ represent, as a whole, an original work of authorship. For the purposes
+ of this License, Derivative Works shall not include works that remain
+ separable from, or merely link (or bind by name) to the interfaces of,
+ the Work and Derivative Works thereof.
+
+ "Contribution" shall mean any work of authorship, including
+ the original version of the Work and any modifications or additions
+ to that Work or Derivative Works thereof, that is intentionally
+ submitted to Licensor for inclusion in the Work by the copyright owner
+ or by an individual or Legal Entity authorized to submit on behalf of
+ the copyright owner. For the purposes of this definition, "submitted"
+ means any form of electronic, verbal, or written communication sent
+ to the Licensor or its representatives, including but not limited to
+ communication on electronic mailing lists, source code control systems,
+ and issue tracking systems that are managed by, or on behalf of, the
+ Licensor for the purpose of discussing and improving the Work, but
+ excluding communication that is conspicuously marked or otherwise
+ designated in writing by the copyright owner as "Not a Contribution."
+
+ "Contributor" shall mean Licensor and any individual or Legal Entity
+ on behalf of whom a Contribution has been received by Licensor and
+ subsequently incorporated within the Work.
+
+2. Grant of Copyright License. Subject to the terms and conditions of
+ this License, each Contributor hereby grants to You a perpetual,
+ worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+ copyright license to reproduce, prepare Derivative Works of,
+ publicly display, publicly perform, sublicense, and distribute the
+ Work and such Derivative Works in Source or Object form.
+
+3. Grant of Patent License. Subject to the terms and conditions of
+ this License, each Contributor hereby grants to You a perpetual,
+ worldwide, non-exclusive, no-charge, royalty-free, irrevocable
+ (except as stated in this section) patent license to make, have made,
+ use, offer to sell, sell, import, and otherwise transfer the Work,
+ where such license applies only to those patent claims licensable
+ by such Contributor that are necessarily infringed by their
+ Contribution(s) alone or by combination of their Contribution(s)
+ with the Work to which such Contribution(s) was submitted. If You
+ institute patent litigation against any entity (including a
+ cross-claim or counterclaim in a lawsuit) alleging that the Work
+ or a Contribution incorporated within the Work constitutes direct
+ or contributory patent infringement, then any patent licenses
+ granted to You under this License for that Work shall terminate
+ as of the date such litigation is filed.
+
+4. Redistribution. You may reproduce and distribute copies of the
+ Work or Derivative Works thereof in any medium, with or without
+ modifications, and in Source or Object form, provided that You
+ meet the following conditions:
+
+ (a) You must give any other recipients of the Work or
+ Derivative Works a copy of this License; and
+
+ (b) You must cause any modified files to carry prominent notices
+ stating that You changed the files; and
+
+ (c) You must retain, in the Source form of any Derivative Works
+ that You distribute, all copyright, patent, trademark, and
+ attribution notices from the Source form of the Work,
+ excluding those notices that do not pertain to any part of
+ the Derivative Works; and
+
+ (d) If the Work includes a "NOTICE" text file as part of its
+ distribution, then any Derivative Works that You distribute must
+ include a readable copy of the attribution notices contained
+ within such NOTICE file, excluding those notices that do not
+ pertain to any part of the Derivative Works, in at least one
+ of the following places: within a NOTICE text file distributed
+ as part of the Derivative Works; within the Source form or
+ documentation, if provided along with the Derivative Works; or,
+ within a display generated by the Derivative Works, if and
+ wherever such third-party notices normally appear. The contents
+ of the NOTICE file are for informational purposes only and
+ do not modify the License. You may add Your own attribution
+ notices within Derivative Works that You distribute, alongside
+ or as an addendum to the NOTICE text from the Work, provided
+ that such additional attribution notices cannot be construed
+ as modifying the License.
+
+ You may add Your own copyright statement to Your modifications and
+ may provide additional or different license terms and conditions
+ for use, reproduction, or distribution of Your modifications, or
+ for any such Derivative Works as a whole, provided Your use,
+ reproduction, and distribution of the Work otherwise complies with
+ the conditions stated in this License.
+
+5. Submission of Contributions. Unless You explicitly state otherwise,
+ any Contribution intentionally submitted for inclusion in the Work
+ by You to the Licensor shall be under the terms and conditions of
+ this License, without any additional terms or conditions.
+ Notwithstanding the above, nothing herein shall supersede or modify
+ the terms of any separate license agreement you may have executed
+ with Licensor regarding such Contributions.
+
+6. Trademarks. This License does not grant permission to use the trade
+ names, trademarks, service marks, or product names of the Licensor,
+ except as required for reasonable and customary use in describing the
+ origin of the Work and reproducing the content of the NOTICE file.
+
+7. Disclaimer of Warranty. Unless required by applicable law or
+ agreed to in writing, Licensor provides the Work (and each
+ Contributor provides its Contributions) on an "AS IS" BASIS,
+ WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
+ implied, including, without limitation, any warranties or conditions
+ of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A
+ PARTICULAR PURPOSE. You are solely responsible for determining the
+ appropriateness of using or redistributing the Work and assume any
+ risks associated with Your exercise of permissions under this License.
+
+8. Limitation of Liability. In no event and under no legal theory,
+ whether in tort (including negligence), contract, or otherwise,
+ unless required by applicable law (such as deliberate and grossly
+ negligent acts) or agreed to in writing, shall any Contributor be
+ liable to You for damages, including any direct, indirect, special,
+ incidental, or consequential damages of any character arising as a
+ result of this License or out of the use or inability to use the
+ Work (including but not limited to damages for loss of goodwill,
+ work stoppage, computer failure or malfunction, or any and all
+ other commercial damages or losses), even if such Contributor
+ has been advised of the possibility of such damages.
+
+9. Accepting Warranty or Additional Liability. While redistributing
+ the Work or Derivative Works thereof, You may choose to offer,
+ and charge a fee for, acceptance of support, warranty, indemnity,
+ or other liability obligations and/or rights consistent with this
+ License. However, in accepting such obligations, You may act only
+ on Your own behalf and on Your sole responsibility, not on behalf
+ of any other Contributor, and only if You agree to indemnify,
+ defend, and hold each Contributor harmless for any liability
+ incurred by, or claims asserted against, such Contributor by reason
+ of your accepting any such warranty or additional liability.
+
+END OF TERMS AND CONDITIONS
+
+APPENDIX: How to apply the Apache License to your work.
+
+ To apply the Apache License to your work, attach the following
+ boilerplate notice, with the fields enclosed by brackets "[]"
+ replaced with your own identifying information. (Don't include
+ the brackets!) The text should be enclosed in the appropriate
+ comment syntax for the file format. We also recommend that a
+ file or class name and description of purpose be included on the
+ same "printed page" as the copyright notice for easier
+ identification within third-party archives.
+
+Copyright [yyyy] [name of copyright owner]
+
+Licensed under the Apache License, Version 2.0 (the "License");
+you may not use this file except in compliance with the License.
+You may obtain a copy of the License at
+
+ http://www.apache.org/licenses/LICENSE-2.0
+
+Unless required by applicable law or agreed to in writing, software
+distributed under the License is distributed on an "AS IS" BASIS,
+WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+See the License for the specific language governing permissions and
+limitations under the License.
diff --git a/vendor/varisat/LICENSE-MIT b/vendor/varisat/LICENSE-MIT
new file mode 100644
index 000000000..4fd1cb2ff
--- /dev/null
+++ b/vendor/varisat/LICENSE-MIT
@@ -0,0 +1,25 @@
+Copyright (c) 2017-2019 Jannis Harder
+
+Permission is hereby granted, free of charge, to any
+person obtaining a copy of this software and associated
+documentation files (the "Software"), to deal in the
+Software without restriction, including without
+limitation the rights to use, copy, modify, merge,
+publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software
+is furnished to do so, subject to the following
+conditions:
+
+The above copyright notice and this permission notice
+shall be included in all copies or substantial portions
+of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF
+ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED
+TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A
+PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT
+SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
+OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR
+IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER
+DEALINGS IN THE SOFTWARE.
diff --git a/vendor/varisat/README.md b/vendor/varisat/README.md
new file mode 100644
index 000000000..ae9783ca0
--- /dev/null
+++ b/vendor/varisat/README.md
@@ -0,0 +1,51 @@
+# Varisat
+
+Varisat is a [CDCL][cdcl] based SAT solver written in rust. Given a boolean
+formula in [conjunctive normal form][cnf], it either finds a variable
+assignment that makes the formula true or finds a proof that this is
+impossible.
+
+[cdcl]: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning
+[cnf]: https://en.wikipedia.org/wiki/Conjunctive_normal_form
+
+This is the library version. Varisat is also available as a command line solver
+([`varisat-cli` on crates.io][crate-varisat-cli]).
+
+## Documentation
+
+ * [User Manual](https://jix.github.io/varisat/manual/0.2.1/)
+ * [Library API Documentation](https://docs.rs/varisat/0.2.2/varisat/)
+
+## Developer Documentation
+
+The internal APIs are documented using rustdoc. It can be generated using
+`cargo doc --document-private-items --all --exclude varisat-cli` or [viewed
+online (master)][dev-docs].
+
+You can also read [a series of blog posts about the development of
+varisat][blog-series].
+
+## License
+
+The Varisat source code is licensed under either of
+
+ * Apache License, Version 2.0
+ ([LICENSE-APACHE](LICENSE-APACHE) or
+ http://www.apache.org/licenses/LICENSE-2.0)
+ * MIT license
+ ([LICENSE-MIT](LICENSE-MIT) or http://opensource.org/licenses/MIT)
+
+at your option.
+
+### Contribution
+
+Unless you explicitly state otherwise, any contribution intentionally submitted
+for inclusion in Varisat by you, as defined in the Apache-2.0 license, shall be
+dual licensed as above, without any additional terms or conditions.
+
+[cdcl]: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning
+[cnf]: https://en.wikipedia.org/wiki/Conjunctive_normal_form
+[dev-docs]: https://jix.github.io/varisat/dev/varisat/
+[blog-series]: https://jix.one/tags/refactoring-varisat/
+[crate-varisat]: https://crates.io/crates/varisat
+[crate-varisat-cli]: https://crates.io/crates/varisat-cli
diff --git a/vendor/varisat/build.rs b/vendor/varisat/build.rs
new file mode 100644
index 000000000..f709e9045
--- /dev/null
+++ b/vendor/varisat/build.rs
@@ -0,0 +1,48 @@
+use anyhow::{ensure, Error};
+use std::{env, process::Command, str::from_utf8};
+
+fn have_drat_trim() -> Result<(), Error> {
+ println!("rerun-if-env-changed=VARISAT_HAVE_DRAT_TRIM");
+ if env::var("VARISAT_HAVE_DRAT_TRIM").is_ok() {
+ return Ok(());
+ }
+
+ let output = Command::new("drat-trim").output()?;
+ let stdout = from_utf8(&output.stdout)?;
+
+ ensure!(
+ stdout.contains("force binary proof parse mode"),
+ "no force binary proof option found"
+ );
+
+ Ok(())
+}
+
+fn have_rate() -> Result<(), Error> {
+ println!("rerun-if-env-changed=VARISAT_HAVE_RATE");
+ if env::var("VARISAT_HAVE_RATE").is_ok() {
+ return Ok(());
+ }
+
+ let _ = Command::new("rate").arg("--version").output()?;
+
+ Ok(())
+}
+
+fn main() {
+ match have_drat_trim() {
+ Ok(_) => println!("cargo:rustc-cfg=test_drat_trim"),
+ Err(err) => println!(
+ "cargo:warning=drat-trim proof checker not found, some tests will be disabled: {}",
+ err
+ ),
+ }
+
+ match have_rate() {
+ Ok(_) => println!("cargo:rustc-cfg=test_rate"),
+ Err(err) => println!(
+ "cargo:warning=rate proof checker not found, some tests will be disabled: {}",
+ err
+ ),
+ }
+}
diff --git a/vendor/varisat/proptest-regressions/solver.txt b/vendor/varisat/proptest-regressions/solver.txt
new file mode 100644
index 000000000..b86cf27f4
--- /dev/null
+++ b/vendor/varisat/proptest-regressions/solver.txt
@@ -0,0 +1,7 @@
+# Seeds for failure cases proptest has generated in the past. It is
+# automatically read and these particular cases re-run before any
+# novel cases are generated.
+#
+# It is recommended to check this file in to source control so that
+# everyone who runs the test benefits from these saved cases.
+cc 26df7e6a68ee2be7d6d6f0229b3e7f96f86cb02069e508a3b62209ecde1eb5b7 # shrinks to (enable_row, columns, formula) = ([1, 2, 3, 4, 5, 6, 7, 8], 4, 40[[17, 18], [25, 32], [27, 32], [-17, -9, -25, -1, -33], [32, 31], [34, 33], [14, 10], [40, 33], [33, 38], [11, 14], [21, 24], [37, 36], [30, 29], [31, 26], [24, 22], [39, 36], [34, 35], [13, 12], [-16, 10], [32, 30], [-37, -29, -13, -21, -5], [9, 14], [26, 30], [-12, -4, -36, -28, -20], [13, 10], [37, 34], [9, 10], [37, 39], [18, 21], [9, 13], [27, 31], [27, 26], [37, 33], [11, -16], [20, 22], [17, 19], [23, 17], [28, 25], [22, 17], [17, 20], [15, -16], [35, 36], [15, 12], [27, 25], [11, 10], [39, 33], [17, 21], [18, 24], [9, -16], [28, 31], [15, 11], [31, 30], [26, 32], [40, 37], [21, 23], [18, 22], [20, 19], [34, 36], [31, 25], [12, 10], [12, 14], [26, 25], [28, 26], [23, 20], [21, 19], [25, 30], [36, 40], [13, -16], [21, 20], [34, 39], [12, 11], [29, 25], [18, 23], [23, 24], [40, 38], [-16, 12], [33, 35], [19, 18], [15, 13], [14, -16], [33, 36], [40, 34], [20, 24], [11, 13], [13, 14], [35, 40], [40, 39], [-14, -30, -6, -22, -38], [27, 28], [29, 26], [39, 38], [34, 38], [29, 31], [19, 22], [11, 9], [-24, -8, -40, -32, 16], [22, 23], [38, 35], [14, 15], [17, 24], [-18, -26, -34, -10, -2], [19, 23], [9, 12], [-15, -7, -23, -39, -31], [37, 35], [9, 15], [10, 15], [-35, -11, -19, -3, -27], [29, 28], [28, 30], [24, 19], [29, 27], [18, 20], [27, 30], [39, 35], [32, 29], [21, 22], [28, 32], [36, 38], [37, 38]])
diff --git a/vendor/varisat/src/analyze_conflict.rs b/vendor/varisat/src/analyze_conflict.rs
new file mode 100644
index 000000000..16f918782
--- /dev/null
+++ b/vendor/varisat/src/analyze_conflict.rs
@@ -0,0 +1,368 @@
+//! Learns a new clause by analyzing a conflict.
+use std::mem::swap;
+
+use partial_ref::{partial, split_borrow, PartialRef};
+
+use vec_mut_scan::VecMutScan;
+
+use varisat_formula::{lit::LitIdx, Lit, Var};
+use varisat_internal_proof::{clause_hash, lit_hash, ClauseHash};
+
+use crate::{
+ clause::ClauseRef,
+ context::{parts::*, Context},
+ prop::{Conflict, Reason},
+};
+
+/// Temporaries for conflict analysis
+#[derive(Default)]
+pub struct AnalyzeConflict {
+ /// This is the learned clause after analysis finishes.
+ clause: Vec<Lit>,
+ /// Number of literals in the current clause at the current level.
+ current_level_count: usize,
+ /// Variables in the current clause.
+ var_flags: Vec<bool>,
+ /// Entries to clean in `var_flags`.
+ to_clean: Vec<Var>,
+ /// Clauses to bump.
+ involved: Vec<ClauseRef>,
+ /// Hashes of all involved clauses needed to proof the minimized clause.
+ clause_hashes: Vec<ClauseHash>,
+ /// Clause hashes paired with the trail depth of the propagated lit.
+ unordered_clause_hashes: Vec<(LitIdx, ClauseHash)>,
+ /// Stack for recursive minimization.
+ stack: Vec<Lit>,
+}
+
+impl AnalyzeConflict {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.var_flags.resize(count, false);
+ }
+
+ /// The learned clause.
+ pub fn clause(&self) -> &[Lit] {
+ &self.clause
+ }
+
+ /// Long clauses involved in the conflict.
+ pub fn involved(&self) -> &[ClauseRef] {
+ &self.involved
+ }
+
+ /// Hashes of clauses involved in the proof of the learned clause.
+ ///
+ /// Hashes are in clause propagation order.
+ pub fn clause_hashes(&self) -> &[ClauseHash] {
+ &self.clause_hashes
+ }
+}
+
+/// Learns a new clause by analyzing a conflict.
+///
+/// Returns the lowest decision level that makes the learned clause asserting.
+pub fn analyze_conflict<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut VsidsP,
+ ClauseAllocP,
+ ImplGraphP,
+ ProofP<'a>,
+ TrailP,
+ ),
+ conflict: Conflict,
+) -> usize {
+ split_borrow!(lit_ctx = &(ClauseAllocP) ctx);
+
+ {
+ let analyze = ctx.part_mut(AnalyzeConflictP);
+
+ analyze.clause.clear();
+ analyze.involved.clear();
+ analyze.clause_hashes.clear();
+ analyze.unordered_clause_hashes.clear();
+ analyze.current_level_count = 0;
+ }
+
+ // We start with all the literals of the conflicted clause
+ let conflict_lits = conflict.lits(&lit_ctx);
+
+ if ctx.part(ProofP).clause_hashes_required() {
+ ctx.part_mut(AnalyzeConflictP)
+ .clause_hashes
+ .push(clause_hash(conflict_lits));
+ }
+
+ if ctx.part(TrailP).current_level() == 0 {
+ // Conflict with no decisions, generate empty clause
+ return 0;
+ }
+
+ for &lit in conflict_lits {
+ add_literal(ctx.borrow(), lit);
+ }
+
+ if let Conflict::Long(cref) = conflict {
+ ctx.part_mut(AnalyzeConflictP).involved.push(cref);
+ }
+
+ // To get rid of all but one literal of the current level, we resolve the clause with the reason
+ // for those literals. The correct order for this is reverse chronological.
+
+ split_borrow!(ctx_trail = &(TrailP) ctx);
+ // split_borrow!(ctx_analyze = &(mut AnalyzeConflictP) ctx);
+
+ for &lit in ctx_trail.part(TrailP).trail().iter().rev() {
+ let analyze = ctx.part_mut(AnalyzeConflictP);
+ let lit_present = &mut analyze.var_flags[lit.index()];
+ // Is the lit present in the current clause?
+ if *lit_present {
+ *lit_present = false;
+ analyze.current_level_count -= 1;
+ if analyze.current_level_count == 0 {
+ // lit is the last literal of the current level present in the current clause,
+ // therefore the resulting clause will assert !lit so we put in position 0
+ analyze.clause.push(!lit);
+ let end = analyze.clause.len() - 1;
+ analyze.clause.swap(0, end);
+
+ break;
+ } else {
+ // We removed the literal and now add its reason.
+ let (graph, mut ctx) = ctx.split_part(ImplGraphP);
+
+ let reason = graph.reason(lit.var());
+
+ let lits = reason.lits(&lit_ctx);
+
+ if ctx.part(ProofP).clause_hashes_required() && !reason.is_unit() {
+ let hash = clause_hash(lits) ^ lit_hash(lit);
+ ctx.part_mut(AnalyzeConflictP).clause_hashes.push(hash);
+ }
+
+ for &lit in lits {
+ add_literal(ctx.borrow(), lit);
+ }
+
+ if let Reason::Long(cref) = reason {
+ ctx.part_mut(AnalyzeConflictP).involved.push(*cref);
+ }
+ }
+ }
+ }
+
+ // This needs var_flags set and keeps some var_fags set.
+ minimize_clause(ctx.borrow());
+
+ let (analyze, mut ctx) = ctx.split_part_mut(AnalyzeConflictP);
+
+ if ctx.part(ProofP).clause_hashes_required() {
+ // Clause minimization cannot give us clause hashes in propagation order, so we need to sort
+ // them. Clauses used during minimization propagte before clauses used during initial
+ // analysis. The clauses during initial analysis are discovered in reverse propagation
+ // order. This means we can sort the minimization clauses in reverse order, append them to
+ // the initial clauses and then reverse the order of all clauses.
+ analyze
+ .unordered_clause_hashes
+ .sort_unstable_by_key(|&(depth, _)| !depth);
+
+ analyze
+ .unordered_clause_hashes
+ .dedup_by_key(|&mut (depth, _)| depth);
+
+ analyze.clause_hashes.extend(
+ analyze
+ .unordered_clause_hashes
+ .iter()
+ .map(|&(_, hash)| hash),
+ );
+ analyze.clause_hashes.reverse();
+ }
+
+ for var in analyze.to_clean.drain(..) {
+ analyze.var_flags[var.index()] = false;
+ }
+
+ // We find the highest level literal besides the asserted literal and move it into position 1.
+ // This is important to ensure the watchlist constraints are not violated on backtracking.
+ let mut backtrack_to = 0;
+
+ if analyze.clause.len() > 1 {
+ let (prefix, rest) = analyze.clause.split_at_mut(2);
+ let lit_1 = &mut prefix[1];
+ backtrack_to = ctx.part(ImplGraphP).level(lit_1.var());
+ for lit in rest.iter_mut() {
+ let lit_level = ctx.part(ImplGraphP).level(lit.var());
+ if lit_level > backtrack_to {
+ backtrack_to = lit_level;
+ swap(lit_1, lit);
+ }
+ }
+ }
+
+ ctx.part_mut(VsidsP).decay();
+
+ backtrack_to
+}
+
+/// Add a literal to the current clause.
+fn add_literal(
+ mut ctx: partial!(
+ Context,
+ mut AnalyzeConflictP,
+ mut VsidsP,
+ ImplGraphP,
+ TrailP
+ ),
+ lit: Lit,
+) {
+ let (analyze, mut ctx) = ctx.split_part_mut(AnalyzeConflictP);
+ let lit_level = ctx.part(ImplGraphP).level(lit.var());
+ // No need to add literals that are set by unit clauses or already present
+ if lit_level > 0 && !analyze.var_flags[lit.index()] {
+ ctx.part_mut(VsidsP).bump(lit.var());
+
+ analyze.var_flags[lit.index()] = true;
+ if lit_level == ctx.part(TrailP).current_level() {
+ analyze.current_level_count += 1;
+ } else {
+ analyze.clause.push(lit);
+ analyze.to_clean.push(lit.var());
+ }
+ }
+}
+
+/// A Bloom filter of levels.
+#[derive(Default)]
+struct LevelAbstraction {
+ bits: u64,
+}
+
+impl LevelAbstraction {
+ /// Add a level to the Bloom filter.
+ pub fn add(&mut self, level: usize) {
+ self.bits |= 1 << (level % 64)
+ }
+
+ /// Test whether a level could be in the Bloom filter.
+ pub fn test(&self, level: usize) -> bool {
+ self.bits & (1 << (level % 64)) != 0
+ }
+}
+
+/// Performs recursive clause minimization.
+///
+/// **Note:** Requires AnalyzeConflict's var_flags to be set for exactly the variables of the
+/// unminimized claused. This also sets some more var_flags, but lists them in to_clean.
+///
+/// This routine tries to remove some redundant literals of the learned clause. The idea is to
+/// detect literals of the learned clause that are already implied by other literals of the clause.
+///
+/// This is done by performing a DFS in the implication graph (following edges in reverse) for each
+/// literal (apart from the asserting one). The search doesn't expand literals already known to be
+/// implied by literals of the clause. When a decision literal that is not in the clause is found,
+/// it means that the literal is not redundant.
+///
+/// There are two optimizations used here: The first one is to stop the search as soon as a literal
+/// of a decision level not present in the clause is found. If the DFS would be continued it would
+/// at some point reach the decision of that level. That decision belongs to a level not in the
+/// clause and thus itself can't be in the clause. Checking whether the decision level is among the
+/// clause's decision levels is done approximately using a Bloom filter.
+///
+/// The other optimization is to avoid duplicating work during the DFS searches. When one literal is
+/// found to be redundant that means the whole search stayed within the implied literals. We
+/// remember this and will not expand any of these literals for the following DFS searches.
+///
+/// In this implementation the var_flags array here has two purposes. At the beginning it is set for
+/// all the literals of the clause. It is also used to mark the literals visited during the DFS.
+/// This allows us to combine the already-visited-check with the literal-present-in-clause check. It
+/// also allows for a neat implementation of the second optimization. When the search finds the
+/// literal to be non-redundant, we clear var_flags for the literals we visited, resetting it to the
+/// state at the beginning of the DFS. When the literal was redundant we keep it as is. This means
+/// the following DFS will not expand these literals.
+fn minimize_clause<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut VsidsP,
+ ClauseAllocP,
+ ImplGraphP,
+ ProofP<'a>,
+ TrailP,
+ ),
+) {
+ let (analyze, mut ctx) = ctx.split_part_mut(AnalyzeConflictP);
+ split_borrow!(lit_ctx = &(ClauseAllocP) ctx);
+ let impl_graph = ctx.part(ImplGraphP);
+
+ let mut involved_levels = LevelAbstraction::default();
+
+ for &lit in analyze.clause.iter() {
+ involved_levels.add(impl_graph.level(lit.var()));
+ }
+
+ let mut scan = VecMutScan::new(&mut analyze.clause);
+
+ // we always keep the first literal
+ scan.next();
+
+ 'next_lit: while let Some(lit) = scan.next() {
+ if impl_graph.reason(lit.var()) == &Reason::Unit {
+ continue;
+ }
+
+ // Start the DFS
+ analyze.stack.clear();
+ analyze.stack.push(!*lit);
+
+ // Used to remember which var_flags are set during this DFS
+ let top = analyze.to_clean.len();
+
+ // Used to remember which clause hashes were added during the DFS, so we can remove them in
+ // case the literal is not redundant.
+ let hashes_top = analyze.unordered_clause_hashes.len();
+
+ while let Some(lit) = analyze.stack.pop() {
+ let reason = impl_graph.reason(lit.var());
+ let lits = reason.lits(&lit_ctx);
+
+ if ctx.part(ProofP).clause_hashes_required() && !reason.is_unit() {
+ let depth = impl_graph.depth(lit.var()) as LitIdx;
+ let hash = clause_hash(lits) ^ lit_hash(lit);
+ analyze.unordered_clause_hashes.push((depth, hash));
+ }
+
+ for &reason_lit in lits {
+ let reason_level = impl_graph.level(reason_lit.var());
+
+ if !analyze.var_flags[reason_lit.index()] && reason_level > 0 {
+ // We haven't established reason_lit to be redundant, haven't visited it yet and
+ // it's not implied by unit clauses.
+
+ if impl_graph.reason(reason_lit.var()) == &Reason::Unit
+ || !involved_levels.test(reason_level)
+ {
+ // reason_lit is a decision not in the clause or in a decision level known
+ // not to be in the clause. Abort the search.
+
+ // Reset the var_flags set during _this_ DFS.
+ for lit in analyze.to_clean.drain(top..) {
+ analyze.var_flags[lit.index()] = false;
+ }
+ // Remove clauses not needed to justify the minimized clause.
+ analyze.unordered_clause_hashes.truncate(hashes_top);
+ continue 'next_lit;
+ } else {
+ analyze.var_flags[reason_lit.index()] = true;
+ analyze.to_clean.push(reason_lit.var());
+ analyze.stack.push(!reason_lit);
+ }
+ }
+ }
+ }
+
+ lit.remove();
+ }
+}
diff --git a/vendor/varisat/src/assumptions.rs b/vendor/varisat/src/assumptions.rs
new file mode 100644
index 000000000..c21d8cb7b
--- /dev/null
+++ b/vendor/varisat/src/assumptions.rs
@@ -0,0 +1,376 @@
+//! Incremental solving.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::{clause_hash, lit_hash, ClauseHash, ProofStep};
+
+use crate::{
+ context::{parts::*, Context},
+ proof,
+ prop::{enqueue_assignment, full_restart, Reason},
+ state::SatState,
+ variables,
+};
+
+/// Incremental solving.
+#[derive(Default)]
+pub struct Assumptions {
+ assumptions: Vec<Lit>,
+ failed_core: Vec<Lit>,
+ user_failed_core: Vec<Lit>,
+ assumption_levels: usize,
+ failed_propagation_hashes: Vec<ClauseHash>,
+}
+
+impl Assumptions {
+ /// Current number of decision levels used for assumptions.
+ pub fn assumption_levels(&self) -> usize {
+ self.assumption_levels
+ }
+
+ /// Resets assumption_levels to zero on a full restart.
+ pub fn full_restart(&mut self) {
+ self.assumption_levels = 0;
+ }
+
+ /// Subset of assumptions that made the formula unsatisfiable.
+ pub fn failed_core(&self) -> &[Lit] {
+ &self.failed_core
+ }
+
+ /// Subset of assumptions that made the formula unsatisfiable.
+ pub fn user_failed_core(&self) -> &[Lit] {
+ &self.user_failed_core
+ }
+
+ /// Current assumptions.
+ pub fn assumptions(&self) -> &[Lit] {
+ &self.assumptions
+ }
+}
+
+/// Return type of [`enqueue_assumption`].
+pub enum EnqueueAssumption {
+ Done,
+ Enqueued,
+ Conflict,
+}
+
+/// Change the currently active assumptions.
+///
+/// The input uses user variable names.
+pub fn set_assumptions<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut BinaryClausesP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ mut TrailP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+ user_assumptions: &[Lit],
+) {
+ full_restart(ctx.borrow());
+
+ let state = ctx.part_mut(SolverStateP);
+
+ state.sat_state = match state.sat_state {
+ SatState::Unsat => SatState::Unsat,
+ SatState::Sat | SatState::UnsatUnderAssumptions | SatState::Unknown => SatState::Unknown,
+ };
+
+ let (assumptions, mut ctx_2) = ctx.split_part_mut(AssumptionsP);
+
+ for lit in assumptions.assumptions.iter() {
+ ctx_2
+ .part_mut(VariablesP)
+ .var_data_solver_mut(lit.var())
+ .assumed = false;
+ }
+
+ variables::solver_from_user_lits(
+ ctx_2.borrow(),
+ &mut assumptions.assumptions,
+ user_assumptions,
+ true,
+ );
+
+ for lit in assumptions.assumptions.iter() {
+ ctx_2
+ .part_mut(VariablesP)
+ .var_data_solver_mut(lit.var())
+ .assumed = true;
+ }
+
+ proof::add_step(
+ ctx_2.borrow(),
+ true,
+ &ProofStep::Assumptions {
+ assumptions: &assumptions.assumptions,
+ },
+ );
+}
+
+/// Enqueue another assumption if possible.
+///
+/// Returns whether an assumption was enqueued, whether no assumptions are left or whether the
+/// assumptions result in a conflict.
+pub fn enqueue_assumption<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ mut TrailP,
+ ClauseAllocP,
+ VariablesP,
+ ),
+) -> EnqueueAssumption {
+ while let Some(&assumption) = ctx
+ .part(AssumptionsP)
+ .assumptions
+ .get(ctx.part(TrailP).current_level())
+ {
+ match ctx.part(AssignmentP).lit_value(assumption) {
+ Some(false) => {
+ analyze_assumption_conflict(ctx.borrow(), assumption);
+ return EnqueueAssumption::Conflict;
+ }
+ Some(true) => {
+ // The next assumption is already implied by other assumptions so we can remove it.
+ let level = ctx.part(TrailP).current_level();
+ let assumptions = ctx.part_mut(AssumptionsP);
+ assumptions.assumptions.swap_remove(level);
+ }
+ None => {
+ ctx.part_mut(TrailP).new_decision_level();
+ enqueue_assignment(ctx.borrow(), assumption, Reason::Unit);
+ let (assumptions, ctx) = ctx.split_part_mut(AssumptionsP);
+ assumptions.assumption_levels = ctx.part(TrailP).current_level();
+ return EnqueueAssumption::Enqueued;
+ }
+ }
+ }
+ EnqueueAssumption::Done
+}
+
+/// Analyze a conflicting set of assumptions.
+///
+/// Compute a set of incompatible assumptions given an assumption that is incompatible with the
+/// assumptions enqueued so far.
+fn analyze_assumption_conflict<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AssumptionsP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ ClauseAllocP,
+ ImplGraphP,
+ TrailP,
+ VariablesP,
+ ),
+ assumption: Lit,
+) {
+ let (assumptions, mut ctx) = ctx.split_part_mut(AssumptionsP);
+ let (tmp, mut ctx) = ctx.split_part_mut(TmpFlagsP);
+ let (trail, mut ctx) = ctx.split_part(TrailP);
+ let (impl_graph, mut ctx) = ctx.split_part(ImplGraphP);
+
+ let flags = &mut tmp.flags;
+
+ assumptions.failed_core.clear();
+ assumptions.failed_core.push(assumption);
+
+ assumptions.failed_propagation_hashes.clear();
+
+ flags[assumption.index()] = true;
+ let mut flag_count = 1;
+
+ for &lit in trail.trail().iter().rev() {
+ if flags[lit.index()] {
+ flags[lit.index()] = false;
+ flag_count -= 1;
+
+ match impl_graph.reason(lit.var()) {
+ Reason::Unit => {
+ if impl_graph.level(lit.var()) > 0 {
+ assumptions.failed_core.push(lit);
+ }
+ }
+ reason => {
+ let (ctx_lits, ctx) = ctx.split_borrow();
+ let reason_lits = reason.lits(&ctx_lits);
+
+ if ctx.part(ProofP).clause_hashes_required() {
+ let hash = clause_hash(reason_lits) ^ lit_hash(lit);
+ assumptions.failed_propagation_hashes.push(hash);
+ }
+
+ for &reason_lit in reason_lits {
+ if !flags[reason_lit.index()] {
+ flags[reason_lit.index()] = true;
+ flag_count += 1;
+ }
+ }
+ }
+ }
+
+ if flag_count == 0 {
+ break;
+ }
+ }
+ }
+
+ assumptions.failed_propagation_hashes.reverse();
+
+ assumptions.user_failed_core.clear();
+ assumptions
+ .user_failed_core
+ .extend(assumptions.failed_core.iter().map(|solver_lit| {
+ solver_lit
+ .map_var(|solver_var| ctx.part(VariablesP).existing_user_from_solver(solver_var))
+ }));
+
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::FailedAssumptions {
+ failed_core: &assumptions.failed_core,
+ propagation_hashes: &assumptions.failed_propagation_hashes,
+ },
+ );
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use proptest::{bool, prelude::*};
+
+ use partial_ref::IntoPartialRefMut;
+
+ use varisat_formula::{test::conditional_pigeon_hole, ExtendFormula, Var};
+
+ use crate::{cdcl::conflict_step, load::load_clause, solver::Solver, state::SatState};
+
+ proptest! {
+ #[test]
+ fn pigeon_hole_unsat_assumption_core_internal(
+ (enable_row, columns, formula) in conditional_pigeon_hole(1..5usize, 1..5usize),
+ chain in bool::ANY,
+ ) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ if chain {
+ for (&a, &b) in enable_row.iter().zip(enable_row.iter().skip(1)) {
+ load_clause(ctx.borrow(), &[!a, b]);
+ }
+ }
+
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Sat);
+
+ set_assumptions(ctx.borrow(), &enable_row);
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::UnsatUnderAssumptions);
+
+ let mut candidates = ctx.part(AssumptionsP).user_failed_core().to_owned();
+ let mut core: Vec<Lit> = vec![];
+
+ loop {
+ set_assumptions(ctx.borrow(), &candidates[0..candidates.len() - 1]);
+
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ match ctx.part(SolverStateP).sat_state {
+ SatState::Unknown => unreachable!(),
+ SatState::Unsat => break,
+ SatState::Sat => {
+ let skipped = *candidates.last().unwrap();
+ core.push(skipped);
+ load_clause(ctx.borrow(), &[skipped]);
+ },
+ SatState::UnsatUnderAssumptions => {
+ candidates = ctx.part(AssumptionsP).user_failed_core().to_owned();
+ }
+ }
+ }
+ if chain {
+ prop_assert_eq!(core.len(), 1);
+ } else {
+ prop_assert_eq!(core.len(), columns + 1);
+ }
+ }
+
+ #[test]
+ fn pigeon_hole_unsat_assumption_core_solver(
+ (enable_row, columns, formula) in conditional_pigeon_hole(1..5usize, 1..5usize),
+ ) {
+ let mut solver = Solver::new();
+ solver.add_formula(&formula);
+
+ prop_assert_eq!(solver.solve().ok(), Some(true));
+
+ let mut assumptions = enable_row;
+
+ assumptions.push(Lit::positive(Var::from_index(formula.var_count() + 10)));
+
+ solver.assume(&assumptions);
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+
+
+ let mut candidates = solver.failed_core().unwrap().to_owned();
+ let mut core: Vec<Lit> = vec![];
+
+ while !candidates.is_empty() {
+
+ solver.assume(&candidates[0..candidates.len() - 1]);
+
+ match solver.solve() {
+ Err(_) => unreachable!(),
+ Ok(true) => {
+ let skipped = *candidates.last().unwrap();
+ core.push(skipped);
+
+ solver.add_clause(&[skipped]);
+ solver.hide_var(skipped.var());
+ },
+ Ok(false) => {
+ candidates = solver.failed_core().unwrap().to_owned();
+ }
+ }
+ }
+
+ prop_assert_eq!(core.len(), columns + 1);
+ }
+ }
+}
diff --git a/vendor/varisat/src/binary.rs b/vendor/varisat/src/binary.rs
new file mode 100644
index 000000000..f39d04676
--- /dev/null
+++ b/vendor/varisat/src/binary.rs
@@ -0,0 +1,100 @@
+//! Binary clauses.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+use crate::{
+ context::{parts::*, Context},
+ proof,
+};
+
+/// Binary clauses.
+#[derive(Default)]
+pub struct BinaryClauses {
+ by_lit: Vec<Vec<Lit>>,
+ count: usize,
+}
+
+impl BinaryClauses {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.by_lit.resize(count * 2, vec![]);
+ }
+
+ /// Add a binary clause.
+ pub fn add_binary_clause(&mut self, lits: [Lit; 2]) {
+ for i in 0..2 {
+ self.by_lit[(!lits[i]).code()].push(lits[i ^ 1]);
+ }
+ self.count += 1;
+ }
+
+ /// Implications of a given literal
+ pub fn implied(&self, lit: Lit) -> &[Lit] {
+ &self.by_lit[lit.code()]
+ }
+
+ /// Number of binary clauses.
+ pub fn count(&self) -> usize {
+ self.count
+ }
+}
+
+/// Remove binary clauses that have an assigned literal.
+pub fn simplify_binary<'a>(
+ mut ctx: partial!(Context<'a>, mut BinaryClausesP, mut ProofP<'a>, mut SolverStateP, AssignmentP, VariablesP),
+) {
+ let (binary_clauses, mut ctx) = ctx.split_part_mut(BinaryClausesP);
+ let (assignment, mut ctx) = ctx.split_part(AssignmentP);
+
+ let mut double_count = 0;
+
+ for (code, implied) in binary_clauses.by_lit.iter_mut().enumerate() {
+ let lit = Lit::from_code(code);
+
+ if !assignment.lit_is_unk(lit) {
+ if ctx.part(ProofP).is_active() {
+ for &other_lit in implied.iter() {
+ // This check avoids deleting binary clauses twice if both literals are assigned.
+ if (!lit) < other_lit {
+ let lits = [!lit, other_lit];
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::DeleteClause {
+ clause: &lits[..],
+ proof: DeleteClauseProof::Satisfied,
+ },
+ );
+ }
+ }
+ }
+
+ implied.clear();
+ } else {
+ implied.retain(|&other_lit| {
+ let retain = assignment.lit_is_unk(other_lit);
+ // This check avoids deleting binary clauses twice if both literals are assigned.
+ if ctx.part(ProofP).is_active() && !retain && (!lit) < other_lit {
+ let lits = [!lit, other_lit];
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::DeleteClause {
+ clause: &lits[..],
+ proof: DeleteClauseProof::Satisfied,
+ },
+ );
+ }
+
+ retain
+ });
+
+ double_count += implied.len();
+ }
+ }
+
+ binary_clauses.count = double_count / 2;
+}
diff --git a/vendor/varisat/src/cdcl.rs b/vendor/varisat/src/cdcl.rs
new file mode 100644
index 000000000..88ee76d6a
--- /dev/null
+++ b/vendor/varisat/src/cdcl.rs
@@ -0,0 +1,264 @@
+//! Conflict driven clause learning.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_internal_proof::ProofStep;
+
+use crate::{
+ analyze_conflict::analyze_conflict,
+ assumptions::{enqueue_assumption, EnqueueAssumption},
+ clause::{assess_learned_clause, bump_clause, db, decay_clause_activities},
+ context::{parts::*, Context},
+ decision::make_decision,
+ model::reconstruct_global_model,
+ proof,
+ prop::{backtrack, enqueue_assignment, propagate, Conflict, Reason},
+ state::SatState,
+ unit_simplify::{prove_units, unit_simplify},
+};
+
+/// Find a conflict, learn a clause and backtrack.
+pub fn conflict_step<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut BinaryClausesP,
+ mut ClauseActivityP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ImplGraphP,
+ mut ModelP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpDataP,
+ mut TmpFlagsP,
+ mut TrailP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+) {
+ let conflict = find_conflict(ctx.borrow());
+
+ let conflict = match conflict {
+ Ok(()) => {
+ reconstruct_global_model(ctx.borrow());
+ return;
+ }
+ Err(FoundConflict::Assumption) => {
+ ctx.part_mut(SolverStateP).sat_state = SatState::UnsatUnderAssumptions;
+ return;
+ }
+ Err(FoundConflict::Conflict(conflict)) => conflict,
+ };
+
+ let backtrack_to = analyze_conflict(ctx.borrow(), conflict);
+
+ let (analyze, mut ctx) = ctx.split_part(AnalyzeConflictP);
+
+ for &cref in analyze.involved() {
+ bump_clause(ctx.borrow(), cref);
+ }
+
+ decay_clause_activities(ctx.borrow());
+
+ backtrack(ctx.borrow(), backtrack_to);
+
+ let clause = analyze.clause();
+
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::AtClause {
+ redundant: clause.len() > 2,
+ clause,
+ propagation_hashes: analyze.clause_hashes(),
+ },
+ );
+
+ let reason = match clause.len() {
+ 0 => {
+ ctx.part_mut(SolverStateP).sat_state = SatState::Unsat;
+ return;
+ }
+ 1 => Reason::Unit,
+ 2 => {
+ ctx.part_mut(BinaryClausesP)
+ .add_binary_clause([clause[0], clause[1]]);
+ Reason::Binary([clause[1]])
+ }
+ _ => {
+ let header = assess_learned_clause(ctx.borrow(), clause);
+ let cref = db::add_clause(ctx.borrow(), header, clause);
+ Reason::Long(cref)
+ }
+ };
+
+ enqueue_assignment(ctx.borrow(), clause[0], reason);
+}
+
+/// Return type of [`find_conflict`].
+///
+/// Specifies whether a conflict was found during propagation or while enqueuing assumptions.
+enum FoundConflict {
+ Conflict(Conflict),
+ Assumption,
+}
+
+impl From<Conflict> for FoundConflict {
+ fn from(conflict: Conflict) -> FoundConflict {
+ FoundConflict::Conflict(conflict)
+ }
+}
+
+/// Find a conflict.
+///
+/// Returns `Err` if a conflict was found and `Ok` if a satisfying assignment was found instead.
+fn find_conflict<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut BinaryClausesP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ mut TrailP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+) -> Result<(), FoundConflict> {
+ loop {
+ let propagation_result = propagate(ctx.borrow());
+
+ let new_unit = prove_units(ctx.borrow());
+
+ propagation_result?;
+
+ if new_unit {
+ unit_simplify(ctx.borrow());
+ }
+
+ match enqueue_assumption(ctx.borrow()) {
+ EnqueueAssumption::Enqueued => continue,
+ EnqueueAssumption::Conflict => return Err(FoundConflict::Assumption),
+ EnqueueAssumption::Done => (),
+ }
+
+ if !make_decision(ctx.borrow()) {
+ return Ok(());
+ }
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use proptest::prelude::*;
+
+ use partial_ref::IntoPartialRefMut;
+
+ use varisat_formula::{
+ cnf_formula,
+ test::{sat_formula, sgen_unsat_formula},
+ };
+
+ use crate::{load::load_clause, state::SatState};
+
+ #[test]
+ fn level_0_unsat() {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ let formula = cnf_formula![
+ 1, 2, 3;
+ -1;
+ 1, -2;
+ 2, -3;
+ ];
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+ }
+
+ proptest! {
+ #[test]
+ fn sgen_unsat(formula in sgen_unsat_formula(1..7usize)) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+ }
+
+ #[test]
+ fn sat(formula in sat_formula(4..20usize, 10..100usize, 0.05..0.2, 0.9..1.0)) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Sat);
+
+ for clause in formula.iter() {
+ prop_assert!(clause.iter().any(|&lit| ctx.part(ModelP).lit_is_true(
+ lit.map_var(|user_var| ctx
+ .part(VariablesP)
+ .global_from_user()
+ .get(user_var)
+ .expect("no existing global var for user var"))
+ )));
+ }
+ }
+
+ #[test]
+ fn sgen_unsat_incremetal_clauses(formula in sgen_unsat_formula(1..7usize)) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ let mut last_state = SatState::Sat;
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ while ctx.part(SolverStateP).sat_state == SatState::Unknown {
+ conflict_step(ctx.borrow());
+ }
+
+ if ctx.part(SolverStateP).sat_state != last_state {
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+ prop_assert_eq!(last_state, SatState::Sat);
+ last_state = ctx.part(SolverStateP).sat_state;
+ }
+ }
+
+ prop_assert_eq!(last_state, SatState::Unsat);
+ }
+ }
+}
diff --git a/vendor/varisat/src/clause.rs b/vendor/varisat/src/clause.rs
new file mode 100644
index 000000000..0d3591858
--- /dev/null
+++ b/vendor/varisat/src/clause.rs
@@ -0,0 +1,67 @@
+//! Clause storage.
+use std::slice;
+
+use varisat_formula::{lit::LitIdx, Lit};
+
+pub mod activity;
+pub mod alloc;
+pub mod assess;
+pub mod db;
+pub mod gc;
+pub mod header;
+pub mod reduce;
+
+pub use activity::{bump_clause_activity, decay_clause_activities, ClauseActivity};
+pub use alloc::{ClauseAlloc, ClauseRef};
+pub use assess::{assess_learned_clause, bump_clause};
+pub use db::{ClauseDb, Tier};
+pub use gc::collect_garbage;
+pub use header::ClauseHeader;
+
+use header::HEADER_LEN;
+
+/// A clause.
+///
+/// This is stoed in a [`ClauseAlloc`] and thus must have a representation compatible with slice of
+/// [`LitIdx`] values.
+///
+/// It would be nicer to use a DST struct with two members and `repr(C)`, but while that can be
+/// declared in stable rust, it's almost impossible to work with.
+#[repr(transparent)]
+pub struct Clause {
+ data: [LitIdx],
+}
+
+impl Clause {
+ /// The clause's header
+ pub fn header(&self) -> &ClauseHeader {
+ unsafe {
+ let header_ptr = self.data.as_ptr() as *const ClauseHeader;
+ &*header_ptr
+ }
+ }
+
+ /// Mutable reference to the clause's header
+ pub fn header_mut(&mut self) -> &mut ClauseHeader {
+ unsafe {
+ let header_ptr = self.data.as_mut_ptr() as *mut ClauseHeader;
+ &mut *header_ptr
+ }
+ }
+
+ /// The clause's literals
+ pub fn lits(&self) -> &[Lit] {
+ unsafe {
+ let lit_ptr = self.data.as_ptr().add(HEADER_LEN) as *const Lit;
+ slice::from_raw_parts(lit_ptr, self.data.len() - HEADER_LEN)
+ }
+ }
+
+ /// Mutable slice of the clause's literals
+ pub fn lits_mut(&mut self) -> &mut [Lit] {
+ unsafe {
+ let lit_ptr = self.data.as_mut_ptr().add(HEADER_LEN) as *mut Lit;
+ slice::from_raw_parts_mut(lit_ptr, self.data.len() - HEADER_LEN)
+ }
+ }
+}
diff --git a/vendor/varisat/src/clause/activity.rs b/vendor/varisat/src/clause/activity.rs
new file mode 100644
index 000000000..8404c7e75
--- /dev/null
+++ b/vendor/varisat/src/clause/activity.rs
@@ -0,0 +1,107 @@
+//! Clause activity.
+use partial_ref::{partial, PartialRef};
+
+use crate::{
+ config::SolverConfig,
+ context::{parts::*, Context},
+};
+
+use super::ClauseRef;
+
+/// Clause activity.
+///
+/// The individual clause activities are stored in the clause allocator. This stores global metadata
+/// used for bumping and decaying activities.
+pub struct ClauseActivity {
+ /// The value to add on bumping.
+ bump: f32,
+ /// The inverse of the decay factor.
+ inv_decay: f32,
+}
+
+impl Default for ClauseActivity {
+ fn default() -> ClauseActivity {
+ ClauseActivity {
+ bump: 1.0,
+ inv_decay: 1.0 / SolverConfig::default().clause_activity_decay,
+ }
+ }
+}
+
+impl ClauseActivity {
+ /// Change the decay factor.
+ pub fn set_decay(&mut self, decay: f32) {
+ assert!(decay < 1.0);
+ assert!(decay > 1.0 / 16.0);
+ self.inv_decay = 1.0 / decay;
+ }
+}
+
+/// Rescale activities if any value exceeds this value.
+fn rescale_limit() -> f32 {
+ std::f32::MAX / 16.0
+}
+
+/// Increase a clause's activity.
+pub fn bump_clause_activity(
+ mut ctx: partial!(
+ Context,
+ mut ClauseActivityP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ ),
+ cref: ClauseRef,
+) {
+ let bump = ctx.part(ClauseActivityP).bump;
+ let header = ctx.part_mut(ClauseAllocP).header_mut(cref);
+
+ let activity = header.activity() + bump;
+
+ header.set_activity(activity);
+
+ if activity > rescale_limit() {
+ rescale_clause_activities(ctx.borrow());
+ }
+}
+
+/// Rescale all values to avoid an overflow.
+fn rescale_clause_activities(
+ mut ctx: partial!(
+ Context,
+ mut ClauseActivityP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ ),
+) {
+ let rescale_factor = 1.0 / rescale_limit();
+
+ let (db, mut ctx) = ctx.split_part_mut(ClauseDbP);
+ let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+ db.clauses.retain(|&cref| {
+ let header = alloc.header_mut(cref);
+ if header.deleted() {
+ false
+ } else {
+ let activity = header.activity() * rescale_factor;
+ header.set_activity(activity);
+ true
+ }
+ });
+ ctx.part_mut(ClauseActivityP).bump *= rescale_factor;
+}
+
+/// Decay the clause activities.
+pub fn decay_clause_activities(
+ mut ctx: partial!(
+ Context,
+ mut ClauseActivityP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ ),
+) {
+ let activities = ctx.part_mut(ClauseActivityP);
+ activities.bump *= activities.inv_decay;
+ if activities.bump >= rescale_limit() {
+ rescale_clause_activities(ctx.borrow());
+ }
+}
diff --git a/vendor/varisat/src/clause/alloc.rs b/vendor/varisat/src/clause/alloc.rs
new file mode 100644
index 000000000..d39514040
--- /dev/null
+++ b/vendor/varisat/src/clause/alloc.rs
@@ -0,0 +1,262 @@
+//! Clause allocator.
+use std::{mem::transmute, slice};
+
+use varisat_formula::{lit::LitIdx, Lit};
+
+use super::{Clause, ClauseHeader, HEADER_LEN};
+
+/// Integer type used to store offsets into [`ClauseAlloc`]'s memory.
+type ClauseOffset = u32;
+
+/// Bump allocator for clause storage.
+///
+/// Clauses are allocated from a single continuous buffer. Clauses cannot be freed individually. To
+/// reclaim space from deleted clauses, a new `ClauseAlloc` is created and the remaining clauses are
+/// copied over.
+///
+/// When the `ClauseAlloc`'s buffer is full, it is reallocated using the growing strategy of
+/// [`Vec`]. External references ([`ClauseRef`]) store an offset into the `ClauseAlloc`'s memory and
+/// remaind valid when the buffer is grown. Clauses are aligned and the offset represents a multiple
+/// of the alignment size. This allows using 32-bit offsets while still supporting up to 16GB of
+/// clauses.
+#[derive(Default)]
+pub struct ClauseAlloc {
+ buffer: Vec<LitIdx>,
+}
+
+impl ClauseAlloc {
+ /// Create an emtpy clause allocator.
+ pub fn new() -> ClauseAlloc {
+ ClauseAlloc::default()
+ }
+
+ /// Create a clause allocator with preallocated capacity.
+ pub fn with_capacity(capacity: usize) -> ClauseAlloc {
+ ClauseAlloc {
+ buffer: Vec::with_capacity(capacity),
+ }
+ }
+
+ /// Allocate space for and add a new clause.
+ ///
+ /// Clauses have a minimal size of 3, as binary and unit clauses are handled separately. This is
+ /// enforced on the ClauseAlloc level to safely avoid extra bound checks when accessing the
+ /// initial literals of a clause.
+ ///
+ /// The size of the header will be set to the size of the given slice. The returned
+ /// [`ClauseRef`] can be used to access the new clause.
+ pub fn add_clause(&mut self, mut header: ClauseHeader, lits: &[Lit]) -> ClauseRef {
+ let offset = self.buffer.len();
+
+ assert!(
+ lits.len() >= 3,
+ "ClauseAlloc can only store ternary and larger clauses"
+ );
+
+ // TODO Maybe let the caller handle this?
+ assert!(
+ offset <= (ClauseRef::max_offset() as usize),
+ "Exceeded ClauseAlloc's maximal buffer size"
+ );
+
+ header.set_len(lits.len());
+
+ self.buffer.extend_from_slice(&header.data);
+
+ let lit_idx_slice = unsafe {
+ // This is safe as Lit and LitIdx have the same representation
+ slice::from_raw_parts(lits.as_ptr() as *const LitIdx, lits.len())
+ };
+
+ self.buffer.extend_from_slice(lit_idx_slice);
+
+ ClauseRef {
+ offset: offset as ClauseOffset,
+ }
+ }
+
+ /// Access the header of a clause.
+ pub fn header(&self, cref: ClauseRef) -> &ClauseHeader {
+ let offset = cref.offset as usize;
+ assert!(
+ offset as usize + HEADER_LEN <= self.buffer.len(),
+ "ClauseRef out of bounds"
+ );
+ unsafe { self.header_unchecked(cref) }
+ }
+
+ /// Mutate the header of a clause.
+ pub fn header_mut(&mut self, cref: ClauseRef) -> &mut ClauseHeader {
+ let offset = cref.offset as usize;
+ assert!(
+ offset as usize + HEADER_LEN <= self.buffer.len(),
+ "ClauseRef out of bounds"
+ );
+ unsafe { self.header_unchecked_mut(cref) }
+ }
+
+ unsafe fn header_unchecked(&self, cref: ClauseRef) -> &ClauseHeader {
+ let offset = cref.offset as usize;
+ let header_pointer = self.buffer.as_ptr().add(offset) as *const ClauseHeader;
+ &*header_pointer
+ }
+
+ /// Mutate the header of a clause without bound checks.
+ pub unsafe fn header_unchecked_mut(&mut self, cref: ClauseRef) -> &mut ClauseHeader {
+ let offset = cref.offset as usize;
+ let header_pointer = self.buffer.as_mut_ptr().add(offset) as *mut ClauseHeader;
+ &mut *header_pointer
+ }
+
+ /// Access a clause.
+ pub fn clause(&self, cref: ClauseRef) -> &Clause {
+ let header = self.header(cref);
+ let len = header.len();
+
+ // Even on 32 bit systems these additions can't overflow as we never create clause refs with
+ // an offset larger than ClauseRef::max_offset()
+
+ let lit_offset = cref.offset as usize + HEADER_LEN;
+ let lit_end = lit_offset + len;
+ assert!(lit_end <= self.buffer.len(), "ClauseRef out of bounds");
+ unsafe { self.clause_with_len_unchecked(cref, len) }
+ }
+
+ /// Mutate a clause.
+ pub fn clause_mut(&mut self, cref: ClauseRef) -> &mut Clause {
+ let header = self.header(cref);
+ let len = header.len();
+
+ // Even on 32 bit systems these additions can't overflow as we never create clause refs with
+ // an offset larger than ClauseRef::max_offset()
+
+ let lit_offset = cref.offset as usize + HEADER_LEN;
+ let lit_end = lit_offset + len;
+ assert!(lit_end <= self.buffer.len(), "ClauseRef out of bounds");
+ unsafe { self.clause_with_len_unchecked_mut(cref, len) }
+ }
+
+ /// Mutate the literals of a clause without bound checks.
+ pub unsafe fn lits_ptr_mut_unchecked(&mut self, cref: ClauseRef) -> *mut Lit {
+ let offset = cref.offset as usize;
+ self.buffer.as_ptr().add(offset + HEADER_LEN) as *mut Lit
+ }
+
+ /// Perform a manual bound check on a ClauseRef assuming a given clause length.
+ pub fn check_bounds(&self, cref: ClauseRef, len: usize) {
+ // Even on 32 bit systems these additions can't overflow as we never create clause refs with
+ // an offset larger than ClauseRef::max_offset()
+
+ let lit_offset = cref.offset as usize + HEADER_LEN;
+ let lit_end = lit_offset + len;
+ assert!(lit_end <= self.buffer.len(), "ClauseRef out of bounds");
+ }
+
+ unsafe fn clause_with_len_unchecked(&self, cref: ClauseRef, len: usize) -> &Clause {
+ let offset = cref.offset as usize;
+ #[allow(clippy::transmute_ptr_to_ptr)]
+ transmute::<&[LitIdx], &Clause>(slice::from_raw_parts(
+ self.buffer.as_ptr().add(offset),
+ len + HEADER_LEN,
+ ))
+ }
+
+ unsafe fn clause_with_len_unchecked_mut(&mut self, cref: ClauseRef, len: usize) -> &mut Clause {
+ let offset = cref.offset as usize;
+ #[allow(clippy::transmute_ptr_to_ptr)]
+ transmute::<&mut [LitIdx], &mut Clause>(slice::from_raw_parts_mut(
+ self.buffer.as_mut_ptr().add(offset),
+ len + HEADER_LEN,
+ ))
+ }
+
+ /// Current buffer size in multiples of [`LitIdx`].
+ pub fn buffer_size(&self) -> usize {
+ self.buffer.len()
+ }
+}
+
+/// Compact reference to a clause.
+///
+/// Used with [`ClauseAlloc`] to access the clause.
+#[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd, Debug)]
+pub struct ClauseRef {
+ offset: ClauseOffset,
+}
+
+impl ClauseRef {
+ /// The largest offset supported by the ClauseAlloc
+ const fn max_offset() -> ClauseOffset {
+ // Make sure we can savely add a length to an offset without overflowing usize
+ ((usize::max_value() >> 1) & (ClauseOffset::max_value() as usize)) as ClauseOffset
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use varisat_formula::{cnf::strategy::*, CnfFormula, ExtendFormula};
+
+ use proptest::*;
+
+ proptest! {
+ #[test]
+ fn roundtrip_from_cnf_formula(input in cnf_formula(1..100usize, 0..1000, 3..30)) {
+
+ let mut clause_alloc = ClauseAlloc::new();
+ let mut clause_refs = vec![];
+
+ for clause_lits in input.iter() {
+ let header = ClauseHeader::new();
+ clause_refs.push(clause_alloc.add_clause(header, clause_lits));
+ }
+
+ let mut recovered = CnfFormula::new();
+
+ for cref in clause_refs {
+ let clause = clause_alloc.clause(cref);
+ prop_assert_eq!(clause.header().len(), clause.lits().len());
+ recovered.add_clause(clause.lits());
+ }
+
+ // Ignore difference caused by unused vars
+ recovered.set_var_count(input.var_count());
+
+ prop_assert_eq!(input, recovered);
+ }
+
+ #[test]
+ fn clause_mutation(input in cnf_formula(1..100usize, 0..1000, 3..30)) {
+
+ let mut clause_alloc = ClauseAlloc::new();
+ let mut clause_refs = vec![];
+
+ for clause_lits in input.iter() {
+ let header = ClauseHeader::new();
+ clause_refs.push(clause_alloc.add_clause(header, clause_lits));
+ }
+
+ for &cref in clause_refs.iter() {
+ let clause = clause_alloc.clause_mut(cref);
+ clause.lits_mut().reverse();
+ }
+
+ for &cref in clause_refs.iter() {
+ let clause_len = clause_alloc.clause(cref).lits().len();
+ if clause_len > 3 {
+ clause_alloc.header_mut(cref).set_len(clause_len - 1);
+ }
+ }
+
+ for (&cref, lits) in clause_refs.iter().zip(input.iter()) {
+ let expected = if lits.len() > 3 {
+ lits[1..].iter().rev()
+ } else {
+ lits.iter().rev()
+ };
+ prop_assert!(clause_alloc.clause(cref).lits().iter().eq(expected));
+ }
+ }
+ }
+}
diff --git a/vendor/varisat/src/clause/assess.rs b/vendor/varisat/src/clause/assess.rs
new file mode 100644
index 000000000..a28dacb64
--- /dev/null
+++ b/vendor/varisat/src/clause/assess.rs
@@ -0,0 +1,69 @@
+//! Clause assessment.
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::{
+ clause::{db, ClauseRef},
+ context::{parts::*, Context},
+ glue::compute_glue,
+};
+
+use super::{bump_clause_activity, ClauseHeader, Tier};
+
+/// Assess the newly learned clause and generate a clause header.
+pub fn assess_learned_clause(
+ mut ctx: partial!(Context, mut TmpFlagsP, ImplGraphP),
+ lits: &[Lit],
+) -> ClauseHeader {
+ // This is called while the clause is still in conflict, thus the computed glue level is one
+ // higher than it'll be after backtracking when the clause becomes asserting.
+ let glue = compute_glue(ctx.borrow(), lits) - 1;
+
+ let mut header = ClauseHeader::new();
+
+ header.set_glue(glue);
+ header.set_tier(select_tier(glue));
+
+ header
+}
+
+/// Compute the tier for a redundant clause with a given glue level.
+fn select_tier(glue: usize) -> Tier {
+ if glue <= 2 {
+ Tier::Core
+ } else if glue <= 6 {
+ Tier::Mid
+ } else {
+ Tier::Local
+ }
+}
+
+/// Update stats for clauses involved in the conflict.
+pub fn bump_clause(
+ mut ctx: partial!(
+ Context,
+ mut ClauseActivityP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut TmpFlagsP,
+ ImplGraphP
+ ),
+ cref: ClauseRef,
+) {
+ bump_clause_activity(ctx.borrow(), cref);
+
+ let (alloc, mut ctx_2) = ctx.split_part_mut(ClauseAllocP);
+
+ let clause = alloc.clause_mut(cref);
+
+ let glue = compute_glue(ctx_2.borrow(), clause.lits());
+
+ clause.header_mut().set_active(true);
+
+ if glue < clause.header().glue() {
+ clause.header_mut().set_glue(glue);
+
+ db::set_clause_tier(ctx.borrow(), cref, select_tier(glue));
+ }
+}
diff --git a/vendor/varisat/src/clause/db.rs b/vendor/varisat/src/clause/db.rs
new file mode 100644
index 000000000..780e14557
--- /dev/null
+++ b/vendor/varisat/src/clause/db.rs
@@ -0,0 +1,269 @@
+//! Database for long clauses.
+use std::mem::transmute;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::{
+ context::{parts::*, Context},
+ prop::Reason,
+};
+
+use super::{header::HEADER_LEN, ClauseAlloc, ClauseHeader, ClauseRef};
+
+/// Partitions of the clause database.
+///
+/// The long clauses are partitioned into 4 [`Tier`]s. This follows the approach described by
+/// Chanseok Oh in ["Between SAT and UNSAT: The Fundamental Difference in CDCL
+/// SAT"](https://doi.org/10.1007/978-3-319-24318-4_23), section 4.
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+#[repr(u8)]
+pub enum Tier {
+ Irred = 0,
+ Core = 1,
+ Mid = 2,
+ Local = 3,
+}
+
+impl Tier {
+ /// Total number of tiers.
+ pub const fn count() -> usize {
+ 4
+ }
+
+ /// Cast an index into the corresponding tier.
+ pub unsafe fn from_index(index: usize) -> Tier {
+ debug_assert!(index < Tier::count());
+ transmute(index as u8)
+ }
+}
+
+/// Database for long clauses.
+///
+/// Removal of clauses from the `clauses` and the `by_tier` fields can be delayed. The clause
+/// header's deleted and tier fields need to be checked when iterating over these. `by_tier` may
+/// also contain duplicate entries.
+#[derive(Default)]
+pub struct ClauseDb {
+ /// May contain deleted clauses, see above
+ pub(super) clauses: Vec<ClauseRef>,
+ /// May contain deleted and moved clauses, see above
+ pub(super) by_tier: [Vec<ClauseRef>; Tier::count()],
+ /// These counts should always be up to date
+ pub(super) count_by_tier: [usize; Tier::count()],
+ /// Size of deleted but not collected clauses
+ pub(super) garbage_size: usize,
+}
+
+impl ClauseDb {
+ /// The number of long clauses of a given tier.
+ pub fn count_by_tier(&self, tier: Tier) -> usize {
+ self.count_by_tier[tier as usize]
+ }
+}
+
+/// Add a long clause to the database.
+pub fn add_clause(
+ mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP, mut WatchlistsP),
+ header: ClauseHeader,
+ lits: &[Lit],
+) -> ClauseRef {
+ let tier = header.tier();
+
+ let cref = ctx.part_mut(ClauseAllocP).add_clause(header, lits);
+
+ ctx.part_mut(WatchlistsP)
+ .watch_clause(cref, [lits[0], lits[1]]);
+
+ let db = ctx.part_mut(ClauseDbP);
+
+ db.clauses.push(cref);
+ db.by_tier[tier as usize].push(cref);
+ db.count_by_tier[tier as usize] += 1;
+
+ cref
+}
+
+/// Change the tier of a long clause.
+///
+/// This is a noop for a clause already of the specified tier.
+pub fn set_clause_tier(
+ mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP),
+ cref: ClauseRef,
+ tier: Tier,
+) {
+ let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+ let db = ctx.part_mut(ClauseDbP);
+
+ let old_tier = alloc.header(cref).tier();
+ if old_tier != tier {
+ db.count_by_tier[old_tier as usize] -= 1;
+ db.count_by_tier[tier as usize] += 1;
+
+ alloc.header_mut(cref).set_tier(tier);
+ db.by_tier[tier as usize].push(cref);
+ }
+}
+
+/// Delete a long clause from the database.
+pub fn delete_clause(
+ mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP, mut WatchlistsP),
+ cref: ClauseRef,
+) {
+ // TODO Don't force a rebuild of all watchlists here
+ ctx.part_mut(WatchlistsP).disable();
+
+ let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+ let db = ctx.part_mut(ClauseDbP);
+
+ let header = alloc.header_mut(cref);
+
+ debug_assert!(
+ !header.deleted(),
+ "delete_clause for already deleted clause"
+ );
+
+ header.set_deleted(true);
+
+ db.count_by_tier[header.tier() as usize] -= 1;
+
+ db.garbage_size += header.len() + HEADER_LEN;
+}
+
+/// Delete a long clause from the database unless it is asserting.
+///
+/// Returns true if the clause was deleted.
+pub fn try_delete_clause(
+ mut ctx: partial!(
+ Context,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut WatchlistsP,
+ ImplGraphP,
+ AssignmentP,
+ ),
+ cref: ClauseRef,
+) -> bool {
+ let initial_lit = ctx.part(ClauseAllocP).clause(cref).lits()[0];
+ let asserting = ctx.part(AssignmentP).lit_is_true(initial_lit)
+ && ctx.part(ImplGraphP).reason(initial_lit.var()) == &Reason::Long(cref);
+
+ if !asserting {
+ delete_clause(ctx.borrow(), cref);
+ }
+ !asserting
+}
+
+/// Iterator over all long clauses.
+///
+/// This filters deleted (but uncollected) clauses on the fly.
+pub fn clauses_iter<'a>(
+ ctx: &'a partial!('a Context, ClauseAllocP, ClauseDbP),
+) -> impl Iterator<Item = ClauseRef> + 'a {
+ let alloc = ctx.part(ClauseAllocP);
+ ctx.part(ClauseDbP)
+ .clauses
+ .iter()
+ .cloned()
+ .filter(move |&cref| !alloc.header(cref).deleted())
+}
+
+/// Iterate over all and remove some long clauses.
+///
+/// Takes a closure that returns true for each clause that should be kept and false for each that
+/// should be deleted.
+pub fn filter_clauses<F>(
+ mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP, mut WatchlistsP),
+ mut filter: F,
+) where
+ F: FnMut(&mut ClauseAlloc, ClauseRef) -> bool,
+{
+ ctx.part_mut(WatchlistsP).disable();
+
+ let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+ let db = ctx.part_mut(ClauseDbP);
+
+ let count_by_tier = &mut db.count_by_tier;
+ let garbage_size = &mut db.garbage_size;
+
+ db.clauses.retain(|&cref| {
+ if alloc.header(cref).deleted() {
+ false
+ } else if filter(alloc, cref) {
+ true
+ } else {
+ let header = alloc.header_mut(cref);
+
+ header.set_deleted(true);
+
+ count_by_tier[header.tier() as usize] -= 1;
+
+ *garbage_size += header.len() + HEADER_LEN;
+
+ false
+ }
+ })
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use partial_ref::IntoPartialRefMut;
+
+ use varisat_formula::cnf_formula;
+
+ use crate::context::set_var_count;
+
+ #[test]
+ fn set_tiers_and_deletes() {
+ let mut ctx = Context::default();
+
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ let clauses = cnf_formula![
+ 1, 2, 3;
+ 4, -5, 6;
+ -2, 3, -4;
+ -3, 5, 2, 7, 5;
+ ];
+
+ set_var_count(ctx.borrow(), clauses.var_count());
+
+ let tiers = vec![Tier::Irred, Tier::Core, Tier::Mid, Tier::Local];
+ let new_tiers = vec![Tier::Irred, Tier::Local, Tier::Local, Tier::Core];
+
+ let mut crefs = vec![];
+
+ for (clause, &tier) in clauses.iter().zip(tiers.iter()) {
+ let mut header = ClauseHeader::new();
+ header.set_tier(tier);
+ let cref = add_clause(ctx.borrow(), header, clause);
+ crefs.push(cref);
+ }
+
+ for (&cref, &tier) in crefs.iter().rev().zip(new_tiers.iter().rev()) {
+ set_clause_tier(ctx.borrow(), cref, tier);
+ }
+
+ // We only check presence, as deletion from these lists is delayed
+ assert!(ctx.part(ClauseDbP).by_tier[Tier::Irred as usize].contains(&crefs[0]));
+ assert!(ctx.part(ClauseDbP).by_tier[Tier::Core as usize].contains(&crefs[3]));
+ assert!(ctx.part(ClauseDbP).by_tier[Tier::Local as usize].contains(&crefs[1]));
+ assert!(ctx.part(ClauseDbP).by_tier[Tier::Local as usize].contains(&crefs[2]));
+
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 1);
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Core), 1);
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Mid), 0);
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Local), 2);
+
+ delete_clause(ctx.borrow(), crefs[0]);
+ delete_clause(ctx.borrow(), crefs[2]);
+
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 0);
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Core), 1);
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Mid), 0);
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Local), 1);
+ }
+}
diff --git a/vendor/varisat/src/clause/gc.rs b/vendor/varisat/src/clause/gc.rs
new file mode 100644
index 000000000..0ad116660
--- /dev/null
+++ b/vendor/varisat/src/clause/gc.rs
@@ -0,0 +1,207 @@
+//! Garbage collection of long clauses.
+use partial_ref::{partial, PartialRef};
+
+use crate::{
+ context::{parts::*, Context},
+ prop::Reason,
+};
+
+use super::{ClauseAlloc, Tier};
+
+/// Perform a garbage collection of long clauses if necessary.
+pub fn collect_garbage(
+ mut ctx: partial!(
+ Context,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ImplGraphP,
+ mut WatchlistsP,
+ TrailP,
+ ),
+) {
+ let alloc = ctx.part(ClauseAllocP);
+ let db = ctx.part(ClauseDbP);
+
+ // Collecting when a fixed fraction of the allocation is garbage amortizes collection costs.
+ if db.garbage_size * 2 > alloc.buffer_size() {
+ collect_garbage_now(ctx.borrow());
+ }
+}
+
+/// Unconditionally perform a garbage collection of long clauses.
+///
+/// This needs to invalidate or update any other data structure containing references to
+/// clauses.
+fn collect_garbage_now(
+ mut ctx: partial!(
+ Context,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ImplGraphP,
+ mut WatchlistsP,
+ TrailP,
+ ),
+) {
+ ctx.part_mut(WatchlistsP).disable();
+
+ mark_asserting_clauses(ctx.borrow());
+
+ let (db, mut ctx) = ctx.split_part_mut(ClauseDbP);
+ let (impl_graph, mut ctx) = ctx.split_part_mut(ImplGraphP);
+ let alloc = ctx.part_mut(ClauseAllocP);
+
+ assert!(
+ db.garbage_size <= alloc.buffer_size(),
+ "Inconsistent garbage tracking in ClauseDb"
+ );
+ let current_size = alloc.buffer_size() - db.garbage_size;
+
+ // Allocating just the current size would lead to an immediate growing when new clauses are
+ // learned, overallocating here avoids that.
+ let mut new_alloc = ClauseAlloc::with_capacity(current_size * 2);
+
+ let mut new_clauses = vec![];
+ let mut new_by_tier: [Vec<_>; Tier::count()] = Default::default();
+
+ // TODO Optimize order of clauses (benchmark this)
+
+ db.clauses.retain(|&cref| {
+ let clause = alloc.clause(cref);
+ let mut header = *clause.header();
+ if header.deleted() {
+ false
+ } else {
+ let clause_is_asserting = header.mark();
+ header.set_mark(false);
+
+ let new_cref = new_alloc.add_clause(header, clause.lits());
+
+ new_clauses.push(new_cref);
+ new_by_tier[header.tier() as usize].push(new_cref);
+
+ if clause_is_asserting {
+ let asserted_lit = clause.lits()[0];
+
+ debug_assert_eq!(impl_graph.reason(asserted_lit.var()), &Reason::Long(cref));
+ impl_graph.update_reason(asserted_lit.var(), Reason::Long(new_cref));
+ }
+ true
+ }
+ });
+
+ *ctx.part_mut(ClauseAllocP) = new_alloc;
+ db.clauses = new_clauses;
+ db.by_tier = new_by_tier;
+ db.garbage_size = 0;
+}
+
+/// Mark asserting clauses to track them through GC.
+fn mark_asserting_clauses(mut ctx: partial!(Context, mut ClauseAllocP, ImplGraphP, TrailP,)) {
+ let (trail, mut ctx) = ctx.split_part(TrailP);
+ let (alloc, ctx) = ctx.split_part_mut(ClauseAllocP);
+ let impl_graph = ctx.part(ImplGraphP);
+
+ for &lit in trail.trail().iter() {
+ if let Reason::Long(cref) = impl_graph.reason(lit.var()) {
+ alloc.header_mut(*cref).set_mark(true);
+ }
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use std::cmp::max;
+
+ use partial_ref::IntoPartialRefMut;
+ use proptest::*;
+
+ use varisat_formula::{cnf::strategy::*, Lit};
+
+ use crate::{
+ clause::{db, ClauseHeader},
+ context::set_var_count,
+ prop::enqueue_assignment,
+ };
+
+ proptest! {
+ #[test]
+ fn garbage_collection(
+ input_a in cnf_formula(2..100usize, 500..1000, 3..30),
+ input_b in cnf_formula(2..100usize, 10..500, 4..20),
+ ) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ set_var_count(ctx.borrow(), max(input_a.var_count(), input_b.var_count()));
+
+ let mut crefs_a = vec![];
+ let mut crefs_b = vec![];
+
+ for lits in input_a.iter() {
+ let header = ClauseHeader::new();
+ let cref = db::add_clause(ctx.borrow(), header, lits);
+ crefs_a.push(cref);
+ }
+
+ for lits in input_b.iter() {
+ let header = ClauseHeader::new();
+ let cref = db::add_clause(ctx.borrow(), header, lits);
+ crefs_b.push(cref);
+
+ if ctx.part(AssignmentP).lit_value(lits[0]) == None {
+ // This isn't consistent, as the clause isn't actually propagating, but that
+ // isn't checked during garbage collection
+ enqueue_assignment(ctx.borrow(), lits[0], Reason::Long(cref));
+ }
+ }
+
+ for cref in crefs_a {
+ db::delete_clause(ctx.borrow(), cref);
+ prop_assert!(ctx.part(ClauseDbP).garbage_size > 0);
+ }
+
+ let old_buffer_size = ctx.part(ClauseAllocP).buffer_size();
+
+ collect_garbage(ctx.borrow());
+
+ prop_assert!(
+ ctx.part(ClauseDbP).garbage_size * 2 < ctx.part(ClauseAllocP).buffer_size()
+ );
+
+ prop_assert!(
+ old_buffer_size > ctx.part(ClauseAllocP).buffer_size()
+ );
+
+ prop_assert!(!ctx.part(WatchlistsP).enabled());
+
+ let mut output_clauses: Vec<Vec<Lit>> = vec![];
+
+ for &cref in ctx.part(ClauseDbP).clauses.iter() {
+ let clause = ctx.part(ClauseAllocP).clause(cref);
+ if clause.header().deleted() {
+ continue;
+ }
+ prop_assert!(!clause.header().mark());
+ output_clauses.push(clause.lits().to_vec());
+ }
+
+ let mut input_clauses: Vec<Vec<Lit>> = input_b
+ .iter()
+ .map(|c| c.to_vec())
+ .collect();
+
+ output_clauses.sort();
+ input_clauses.sort();
+
+ prop_assert_eq!(input_clauses, output_clauses);
+
+ for &lit in ctx.part(TrailP).trail() {
+ if let Reason::Long(cref) = ctx.part(ImplGraphP).reason(lit.var()) {
+ prop_assert_eq!(ctx.part(ClauseAllocP).clause(*cref).lits()[0], lit)
+ }
+ }
+ }
+ }
+}
diff --git a/vendor/varisat/src/clause/header.rs b/vendor/varisat/src/clause/header.rs
new file mode 100644
index 000000000..74656e8c1
--- /dev/null
+++ b/vendor/varisat/src/clause/header.rs
@@ -0,0 +1,148 @@
+//! Metadata stored in the header of each long clause.
+use std::cmp::min;
+
+use varisat_formula::{lit::LitIdx, Var};
+
+use super::Tier;
+
+/// Length of a [`ClauseHeader`] in multiples of [`LitIdx`]
+pub(super) const HEADER_LEN: usize = 3;
+
+const TIER_WORD: usize = HEADER_LEN - 2;
+const TIER_OFFSET: usize = 0;
+const TIER_MASK: LitIdx = 0b11;
+
+const DELETED_WORD: usize = HEADER_LEN - 2;
+const DELETED_OFFSET: usize = 2;
+
+const MARK_WORD: usize = HEADER_LEN - 2;
+const MARK_OFFSET: usize = 3;
+
+const GLUE_WORD: usize = HEADER_LEN - 2;
+const GLUE_OFFSET: usize = 4;
+const GLUE_MASK: LitIdx = (1 << 6) - 1;
+
+const ACTIVE_WORD: usize = HEADER_LEN - 2;
+const ACTIVE_OFFSET: usize = 10;
+
+const ACTIVITY_WORD: usize = HEADER_LEN - 3;
+
+/// Metadata for a clause.
+///
+/// This is stored in a [`ClauseAlloc`](super::ClauseAlloc) and thus must have a representation
+/// compatible with slice of [`LitIdx`] values.
+#[repr(transparent)]
+#[derive(Copy, Clone, Default)]
+pub struct ClauseHeader {
+ pub(super) data: [LitIdx; HEADER_LEN],
+}
+
+impl ClauseHeader {
+ /// Create a new clause header with default entries.
+ pub fn new() -> ClauseHeader {
+ Self::default()
+ }
+
+ /// Length of the clause.
+ pub fn len(&self) -> usize {
+ self.data[HEADER_LEN - 1] as usize
+ }
+
+ /// Set the length of the clause.
+ ///
+ /// Must be `<= Var::max_count()` as each variable may only be present once per clause.
+ pub fn set_len(&mut self, length: usize) {
+ debug_assert!(length <= Var::max_count());
+
+ self.data[HEADER_LEN - 1] = length as LitIdx;
+ }
+
+ /// Whether the clause is marked as deleted.
+ pub fn deleted(&self) -> bool {
+ (self.data[DELETED_WORD] >> DELETED_OFFSET) & 1 != 0
+ }
+
+ /// Mark the clause as deleted.
+ pub fn set_deleted(&mut self, deleted: bool) {
+ let word = &mut self.data[DELETED_WORD];
+ *word = (*word & !(1 << DELETED_OFFSET)) | ((deleted as LitIdx) << DELETED_OFFSET);
+ }
+
+ /// Current [`Tier`] of the clause.
+ pub fn tier(&self) -> Tier {
+ unsafe { Tier::from_index(((self.data[TIER_WORD] >> TIER_OFFSET) & TIER_MASK) as usize) }
+ }
+
+ /// Set the current [`Tier`] of the clause.
+ pub fn set_tier(&mut self, tier: Tier) {
+ let word = &mut self.data[TIER_WORD];
+ *word = (*word & !(TIER_MASK << TIER_OFFSET)) | ((tier as LitIdx) << TIER_OFFSET);
+ }
+
+ /// Whether the clause is redundant.
+ pub fn redundant(&self) -> bool {
+ self.tier() != Tier::Irred
+ }
+
+ /// Whether the clause is marked.
+ ///
+ /// The mark is a temporary bit that can be set by various routines, but should always be reset
+ /// to false.
+ pub fn mark(&self) -> bool {
+ (self.data[MARK_WORD] >> MARK_OFFSET) & 1 != 0
+ }
+
+ /// Mark or unmark the clause.
+ ///
+ /// Make sure to clear the mark after use.
+ pub fn set_mark(&mut self, mark: bool) {
+ let word = &mut self.data[MARK_WORD];
+ *word = (*word & !(1 << MARK_OFFSET)) | ((mark as LitIdx) << MARK_OFFSET);
+ }
+
+ /// The clause's active flag
+ ///
+ /// This is set when a clause was involved in conflict analysis and periodically reset.
+ pub fn active(&self) -> bool {
+ (self.data[ACTIVE_WORD] >> ACTIVE_OFFSET) & 1 != 0
+ }
+
+ /// Set or reset the clause's active flag.
+ pub fn set_active(&mut self, active: bool) {
+ let word = &mut self.data[ACTIVE_WORD];
+ *word = (*word & !(1 << ACTIVE_OFFSET)) | ((active as LitIdx) << ACTIVE_OFFSET);
+ }
+
+ /// The [glue][crate::glue] level.
+ pub fn glue(&self) -> usize {
+ ((self.data[GLUE_WORD] >> GLUE_OFFSET) & GLUE_MASK) as usize
+ }
+
+ /// Update the [glue][crate::glue] level.
+ pub fn set_glue(&mut self, glue: usize) {
+ let glue = min(glue, GLUE_MASK as usize) as LitIdx;
+ let word = &mut self.data[GLUE_WORD];
+
+ *word = (*word & !(GLUE_MASK << GLUE_OFFSET)) | (glue << GLUE_OFFSET);
+ }
+
+ /// Clause [activity][crate::clause::activity].
+ pub fn activity(&self) -> f32 {
+ f32::from_bits(self.data[ACTIVITY_WORD] as u32)
+ }
+
+ /// Update clause [activity][crate::clause::activity].
+ pub fn set_activity(&mut self, activity: f32) {
+ self.data[ACTIVITY_WORD] = activity.to_bits() as LitIdx;
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ #[test]
+ fn tier_mask() {
+ assert!(Tier::count() <= TIER_MASK as usize + 1);
+ }
+}
diff --git a/vendor/varisat/src/clause/reduce.rs b/vendor/varisat/src/clause/reduce.rs
new file mode 100644
index 000000000..1252ca50b
--- /dev/null
+++ b/vendor/varisat/src/clause/reduce.rs
@@ -0,0 +1,132 @@
+//! Clause database reduction.
+use std::mem::replace;
+
+use ordered_float::OrderedFloat;
+use vec_mut_scan::VecMutScan;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+use crate::{
+ context::{parts::*, Context},
+ proof,
+};
+
+use super::db::{set_clause_tier, try_delete_clause, Tier};
+
+/// Remove deleted and duplicate entries from the by_tier clause lists.
+///
+/// This has the side effect of setting the mark bit on all clauses of the tier.
+pub fn dedup_and_mark_by_tier(
+ mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP),
+ tier: Tier,
+) {
+ let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+ let by_tier = &mut ctx.part_mut(ClauseDbP).by_tier[tier as usize];
+
+ by_tier.retain(|&cref| {
+ let header = alloc.header_mut(cref);
+ let retain = !header.deleted() && !header.mark() && header.tier() == tier;
+ if retain {
+ header.set_mark(true);
+ }
+ retain
+ })
+}
+
+/// Reduce the number of local tier clauses by deleting half of them.
+pub fn reduce_locals<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut WatchlistsP,
+ AssignmentP,
+ ImplGraphP,
+ VariablesP,
+ ),
+) {
+ dedup_and_mark_by_tier(ctx.borrow(), Tier::Local);
+
+ let mut locals = replace(
+ &mut ctx.part_mut(ClauseDbP).by_tier[Tier::Local as usize],
+ vec![],
+ );
+
+ locals.sort_unstable_by_key(|&cref| {
+ (
+ OrderedFloat(ctx.part(ClauseAllocP).header(cref).activity()),
+ cref,
+ )
+ });
+
+ let mut to_delete = locals.len() / 2;
+
+ let mut scan = VecMutScan::new(&mut locals);
+
+ if to_delete > 0 {
+ while let Some(cref) = scan.next() {
+ ctx.part_mut(ClauseAllocP).header_mut(*cref).set_mark(false);
+
+ if try_delete_clause(ctx.borrow(), *cref) {
+ if ctx.part(ProofP).is_active() {
+ let (alloc, mut ctx) = ctx.split_part(ClauseAllocP);
+ let lits = alloc.clause(*cref).lits();
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::DeleteClause {
+ clause: lits,
+ proof: DeleteClauseProof::Redundant,
+ },
+ );
+ }
+
+ cref.remove();
+ to_delete -= 1;
+ if to_delete == 0 {
+ break;
+ }
+ }
+ }
+ }
+
+ // Make sure to clear all marks
+ while let Some(cref) = scan.next() {
+ ctx.part_mut(ClauseAllocP).header_mut(*cref).set_mark(false);
+ }
+
+ drop(scan);
+
+ ctx.part_mut(ClauseDbP).count_by_tier[Tier::Local as usize] = locals.len();
+ ctx.part_mut(ClauseDbP).by_tier[Tier::Local as usize] = locals;
+}
+
+/// Reduce the number of mid tier clauses by moving inactive ones to the local tier.
+pub fn reduce_mids(mut ctx: partial!(Context, mut ClauseAllocP, mut ClauseDbP)) {
+ dedup_and_mark_by_tier(ctx.borrow(), Tier::Mid);
+
+ let mut mids = replace(
+ &mut ctx.part_mut(ClauseDbP).by_tier[Tier::Mid as usize],
+ vec![],
+ );
+
+ mids.retain(|&cref| {
+ let header = ctx.part_mut(ClauseAllocP).header_mut(cref);
+ header.set_mark(false);
+
+ if header.active() {
+ header.set_active(false);
+ true
+ } else {
+ set_clause_tier(ctx.borrow(), cref, Tier::Local);
+ false
+ }
+ });
+
+ ctx.part_mut(ClauseDbP).count_by_tier[Tier::Mid as usize] = mids.len();
+ ctx.part_mut(ClauseDbP).by_tier[Tier::Mid as usize] = mids;
+}
diff --git a/vendor/varisat/src/config.rs b/vendor/varisat/src/config.rs
new file mode 100644
index 000000000..433b91ccf
--- /dev/null
+++ b/vendor/varisat/src/config.rs
@@ -0,0 +1,31 @@
+//! Solver configuration.
+use varisat_internal_macros::{ConfigUpdate, DocDefault};
+
+/// Configurable parameters used during solving.
+#[derive(DocDefault, ConfigUpdate)]
+pub struct SolverConfig {
+ /// Multiplicative decay for the VSIDS decision heuristic.
+ ///
+ /// [default: 0.95] [range: 0.5..1.0]
+ pub vsids_decay: f32,
+
+ /// Multiplicative decay for clause activities.
+ ///
+ /// [default: 0.999] [range: 0.5..1.0]
+ pub clause_activity_decay: f32,
+
+ /// Number of conflicts between local clause reductions.
+ ///
+ /// [default: 15000] [range: 1..]
+ pub reduce_locals_interval: u64,
+
+ /// Number of conflicts between mid clause reductions.
+ ///
+ /// [default: 10000] [range: 1..]
+ pub reduce_mids_interval: u64,
+
+ /// Scaling factor for luby sequence based restarts (number of conflicts).
+ ///
+ /// [default: 128] [range: 1..]
+ pub luby_restart_interval_scale: u64,
+}
diff --git a/vendor/varisat/src/context.rs b/vendor/varisat/src/context.rs
new file mode 100644
index 000000000..47a83c2e3
--- /dev/null
+++ b/vendor/varisat/src/context.rs
@@ -0,0 +1,131 @@
+//! Central solver data structure.
+//!
+//! This module defines the `Context` data structure which holds all data used by the solver. It
+//! also contains global notification functions that likely need to be extended when new parts are
+//! added to the solver.
+use partial_ref::{part, partial, PartialRef, PartialRefTarget};
+
+use crate::{
+ analyze_conflict::AnalyzeConflict,
+ assumptions::Assumptions,
+ binary::BinaryClauses,
+ clause::{ClauseActivity, ClauseAlloc, ClauseDb},
+ config::{SolverConfig, SolverConfigUpdate},
+ decision::vsids::Vsids,
+ model::Model,
+ proof::Proof,
+ prop::{Assignment, ImplGraph, Trail, Watchlists},
+ schedule::Schedule,
+ state::SolverState,
+ tmp::{TmpData, TmpFlags},
+ variables::Variables,
+};
+
+/// Part declarations for the [`Context`] struct.
+pub mod parts {
+ use super::*;
+
+ part!(pub AnalyzeConflictP: AnalyzeConflict);
+ part!(pub AssignmentP: Assignment);
+ part!(pub BinaryClausesP: BinaryClauses);
+ part!(pub ClauseActivityP: ClauseActivity);
+ part!(pub ClauseAllocP: ClauseAlloc);
+ part!(pub ClauseDbP: ClauseDb);
+ part!(pub ImplGraphP: ImplGraph);
+ part!(pub AssumptionsP: Assumptions);
+ part!(pub ModelP: Model);
+ part!(pub ProofP<'a>: Proof<'a>);
+ part!(pub ScheduleP: Schedule);
+ part!(pub SolverConfigP: SolverConfig);
+ part!(pub SolverStateP: SolverState);
+ part!(pub TmpDataP: TmpData);
+ part!(pub TmpFlagsP: TmpFlags);
+ part!(pub TrailP: Trail);
+ part!(pub VariablesP: Variables);
+ part!(pub VsidsP: Vsids);
+ part!(pub WatchlistsP: Watchlists);
+}
+
+use parts::*;
+
+/// Central solver data structure.
+///
+/// This struct contains all data kept by the solver. Most functions operating on multiple fields of
+/// the context use partial references provided by the `partial_ref` crate. This documents the data
+/// dependencies and makes the borrow checker happy without the overhead of passing individual
+/// references.
+#[derive(PartialRefTarget, Default)]
+pub struct Context<'a> {
+ #[part(AnalyzeConflictP)]
+ pub analyze_conflict: AnalyzeConflict,
+ #[part(AssignmentP)]
+ pub assignment: Assignment,
+ #[part(BinaryClausesP)]
+ pub binary_clauses: BinaryClauses,
+ #[part(ClauseActivityP)]
+ pub clause_activity: ClauseActivity,
+ #[part(ClauseAllocP)]
+ pub clause_alloc: ClauseAlloc,
+ #[part(ClauseDbP)]
+ pub clause_db: ClauseDb,
+ #[part(ImplGraphP)]
+ pub impl_graph: ImplGraph,
+ #[part(AssumptionsP)]
+ pub assumptions: Assumptions,
+ #[part(ModelP)]
+ pub model: Model,
+ #[part(ProofP<'a>)]
+ pub proof: Proof<'a>,
+ #[part(ScheduleP)]
+ pub schedule: Schedule,
+ #[part(SolverConfigP)]
+ pub solver_config: SolverConfig,
+ #[part(SolverStateP)]
+ pub solver_state: SolverState,
+ #[part(TmpDataP)]
+ pub tmp_data: TmpData,
+ #[part(TmpFlagsP)]
+ pub tmp_flags: TmpFlags,
+ #[part(TrailP)]
+ pub trail: Trail,
+ #[part(VariablesP)]
+ pub variables: Variables,
+ #[part(VsidsP)]
+ pub vsids: Vsids,
+ #[part(WatchlistsP)]
+ pub watchlists: Watchlists,
+}
+
+/// Update structures for a new variable count.
+pub fn set_var_count(
+ mut ctx: partial!(
+ Context,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut BinaryClausesP,
+ mut ImplGraphP,
+ mut TmpFlagsP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+ count: usize,
+) {
+ ctx.part_mut(AnalyzeConflictP).set_var_count(count);
+ ctx.part_mut(AssignmentP).set_var_count(count);
+ ctx.part_mut(BinaryClausesP).set_var_count(count);
+ ctx.part_mut(ImplGraphP).set_var_count(count);
+ ctx.part_mut(TmpFlagsP).set_var_count(count);
+ ctx.part_mut(VsidsP).set_var_count(count);
+ ctx.part_mut(WatchlistsP).set_var_count(count);
+}
+
+/// The solver configuration has changed.
+pub fn config_changed(
+ mut ctx: partial!(Context, mut VsidsP, mut ClauseActivityP, SolverConfigP),
+ _update: &SolverConfigUpdate,
+) {
+ let (config, mut ctx) = ctx.split_part(SolverConfigP);
+ ctx.part_mut(VsidsP).set_decay(config.vsids_decay);
+ ctx.part_mut(ClauseActivityP)
+ .set_decay(config.clause_activity_decay);
+}
diff --git a/vendor/varisat/src/decision.rs b/vendor/varisat/src/decision.rs
new file mode 100644
index 000000000..a8c8ed267
--- /dev/null
+++ b/vendor/varisat/src/decision.rs
@@ -0,0 +1,58 @@
+//! Decision heuristics.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Var;
+
+use crate::{
+ context::{parts::*, Context},
+ prop::{enqueue_assignment, Reason},
+};
+
+pub mod vsids;
+
+/// Make a decision and enqueue it.
+///
+/// Returns `false` if no decision was made because all variables are assigned.
+pub fn make_decision(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut ImplGraphP,
+ mut TrailP,
+ mut VsidsP
+ ),
+) -> bool {
+ let (vsids, mut ctx) = ctx.split_part_mut(VsidsP);
+
+ if let Some(decision_var) = vsids.find(|&var| ctx.part(AssignmentP).var_value(var).is_none()) {
+ let decision = decision_var.lit(ctx.part(AssignmentP).last_var_value(decision_var));
+
+ ctx.part_mut(TrailP).new_decision_level();
+
+ enqueue_assignment(ctx.borrow(), decision, Reason::Unit);
+
+ true
+ } else {
+ false
+ }
+}
+
+/// Make a variable available for decisions.
+pub fn make_available(mut ctx: partial!(Context, mut VsidsP), var: Var) {
+ ctx.part_mut(VsidsP).make_available(var);
+}
+
+/// Initialize decision heuristics for a new variable.
+pub fn initialize_var(mut ctx: partial!(Context, mut VsidsP), var: Var, available: bool) {
+ ctx.part_mut(VsidsP).reset(var);
+
+ if available {
+ make_available(ctx.borrow(), var);
+ }
+}
+
+/// Remove a variable from the decision heuristics.
+pub fn remove_var(mut ctx: partial!(Context, mut VsidsP), var: Var) {
+ ctx.part_mut(VsidsP).make_unavailable(var);
+}
diff --git a/vendor/varisat/src/decision/vsids.rs b/vendor/varisat/src/decision/vsids.rs
new file mode 100644
index 000000000..e59656d1b
--- /dev/null
+++ b/vendor/varisat/src/decision/vsids.rs
@@ -0,0 +1,346 @@
+//! The VSIDS branching heuristic.
+//!
+//! The VSIDS (Variable State Independent Decaying Sum) branching heuristic keeps an activity value
+//! for each variable. For each conflict some variables are bumped, which means that their activity
+//! is increased by a constant. After bumping some variables, the activity of all variables is
+//! decayed by multiplying it with a constant below 1.
+//!
+//! When a decision is made, it branches on the vairable with the highest activity among the
+//! unassigned variables.
+//!
+//! There are a few variants that differ in which variables are bumped. Varisat follows Minisat (and
+//! others) by bumping all variables in the conflict clause and all variables resolved on during
+//! conflict analysis.
+
+use ordered_float::OrderedFloat;
+
+use varisat_formula::Var;
+
+use crate::config::SolverConfig;
+
+/// The VSIDS branching heuristic.
+///
+/// As an optimization instead of decaying all activities each conflict, the bump value is divided
+/// by the decay factor each conflict. When this would cause a value to overflow all activities and
+/// the bump value are scaled down. Apart from a scaling factor that is the same for all involved
+/// values, this is equivalent to the naive implementation. As we only care about the order of
+/// activities we can ignore the scaling factor.
+pub struct Vsids {
+ /// The activity of each variable.
+ activity: Vec<OrderedFloat<f32>>,
+ /// A binary heap of the variables.
+ heap: Vec<Var>,
+ /// The position in the binary heap for each variable.
+ position: Vec<Option<usize>>,
+ /// The value to add on bumping.
+ bump: f32,
+ /// The inverse of the decay factor.
+ inv_decay: f32,
+}
+
+impl Default for Vsids {
+ fn default() -> Vsids {
+ Vsids {
+ activity: vec![],
+ heap: vec![],
+ position: vec![],
+ bump: 1.0,
+ inv_decay: 1.0 / SolverConfig::default().vsids_decay,
+ }
+ }
+}
+
+impl Vsids {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.activity.resize(count, OrderedFloat(0.0));
+ self.position.resize(count, None);
+ }
+
+ /// Rescale activities if any value exceeds this value.
+ fn rescale_limit() -> f32 {
+ std::f32::MAX / 16.0
+ }
+
+ /// Change the decay factor.
+ pub fn set_decay(&mut self, decay: f32) {
+ assert!(decay < 1.0);
+ assert!(decay > 1.0 / 16.0);
+ self.inv_decay = 1.0 / decay;
+ }
+
+ /// Bump a variable by increasing its activity.
+ pub fn bump(&mut self, var: Var) {
+ let rescale = {
+ let value = &mut self.activity[var.index()];
+ value.0 += self.bump;
+ value.0 >= Self::rescale_limit()
+ };
+ if rescale {
+ self.rescale();
+ }
+ if let Some(pos) = self.position[var.index()] {
+ self.sift_up(pos);
+ }
+ }
+
+ /// Decay all variable activities.
+ pub fn decay(&mut self) {
+ self.bump *= self.inv_decay;
+ if self.bump >= Self::rescale_limit() {
+ self.rescale();
+ }
+ }
+
+ /// Rescale all values to avoid an overflow.
+ fn rescale(&mut self) {
+ let rescale_factor = 1.0 / Self::rescale_limit();
+ for activity in &mut self.activity {
+ activity.0 *= rescale_factor;
+ }
+ self.bump *= rescale_factor;
+ }
+
+ /// Reset the activity of an unavailable variable to zero.
+ ///
+ /// Panics if the variable is still available.
+ pub fn reset(&mut self, var: Var) {
+ assert!(self.position[var.index()].is_none());
+ self.activity[var.index()] = OrderedFloat(0.0);
+ }
+
+ /// Remove a variable from the heap if present.
+ pub fn make_unavailable(&mut self, var: Var) {
+ if let Some(position) = self.position[var.index()] {
+ self.heap.swap_remove(position);
+ if self.heap.len() > position {
+ let moved_var = self.heap[position];
+ self.position[moved_var.index()] = Some(position);
+ self.sift_down(position);
+ }
+ self.position[var.index()] = None;
+ }
+ }
+
+ /// Insert a variable into the heap if not already present.
+ pub fn make_available(&mut self, var: Var) {
+ if self.position[var.index()].is_none() {
+ let position = self.heap.len();
+ self.position[var.index()] = Some(position);
+ self.heap.push(var);
+ self.sift_up(position);
+ }
+ }
+
+ /// Move a variable closer to the root until the heap property is satisfied.
+ fn sift_up(&mut self, mut pos: usize) {
+ let var = self.heap[pos];
+ loop {
+ if pos == 0 {
+ return;
+ }
+ let parent_pos = (pos - 1) / 2;
+ let parent_var = self.heap[parent_pos];
+ if self.activity[parent_var.index()] >= self.activity[var.index()] {
+ return;
+ }
+ self.position[var.index()] = Some(parent_pos);
+ self.heap[parent_pos] = var;
+ self.position[parent_var.index()] = Some(pos);
+ self.heap[pos] = parent_var;
+ pos = parent_pos;
+ }
+ }
+
+ /// Move a variable away from the root until the heap property is satisfied.
+ fn sift_down(&mut self, mut pos: usize) {
+ let var = self.heap[pos];
+ loop {
+ let mut largest_pos = pos;
+ let mut largest_var = var;
+
+ let left_pos = pos * 2 + 1;
+ if left_pos < self.heap.len() {
+ let left_var = self.heap[left_pos];
+
+ if self.activity[largest_var.index()] < self.activity[left_var.index()] {
+ largest_pos = left_pos;
+ largest_var = left_var;
+ }
+ }
+
+ let right_pos = pos * 2 + 2;
+ if right_pos < self.heap.len() {
+ let right_var = self.heap[right_pos];
+
+ if self.activity[largest_var.index()] < self.activity[right_var.index()] {
+ largest_pos = right_pos;
+ largest_var = right_var;
+ }
+ }
+
+ if largest_pos == pos {
+ return;
+ }
+
+ self.position[var.index()] = Some(largest_pos);
+ self.heap[largest_pos] = var;
+ self.position[largest_var.index()] = Some(pos);
+ self.heap[pos] = largest_var;
+ pos = largest_pos;
+ }
+ }
+}
+
+impl Iterator for Vsids {
+ type Item = Var;
+
+ fn next(&mut self) -> Option<Var> {
+ if self.heap.is_empty() {
+ None
+ } else {
+ let var = self.heap.swap_remove(0);
+ if !self.heap.is_empty() {
+ let top_var = self.heap[0];
+ self.position[top_var.index()] = Some(0);
+ self.sift_down(0);
+ }
+ self.position[var.index()] = None;
+ Some(var)
+ }
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use varisat_formula::var;
+
+ #[test]
+ fn rescale_bump() {
+ let mut vsids = Vsids::default();
+ vsids.set_var_count(4);
+ vsids.set_decay(1.0 / 8.0);
+
+ for _ in 0..4 {
+ vsids.next();
+ }
+
+ for i in 0..4 {
+ for _ in 0..i {
+ vsids.bump(Var::from_index(i));
+ }
+ }
+
+ for _ in 0..41 {
+ vsids.decay();
+ }
+
+ for _ in 0..30 {
+ vsids.bump(var!(4));
+ }
+
+ // Decay is a power of two so these values are exact
+ #[allow(clippy::float_cmp)]
+ {
+ assert_eq!(vsids.activity[0].0, 0.0);
+ assert_eq!(vsids.activity[2].0, vsids.activity[1].0 * 2.0);
+ assert!(vsids.activity[3] > vsids.activity[2]);
+ }
+ }
+
+ #[test]
+ fn rescale_decay() {
+ let mut vsids = Vsids::default();
+ vsids.set_var_count(4);
+ vsids.set_decay(1.0 / 8.0);
+
+ for _ in 0..4 {
+ vsids.next();
+ }
+
+ for i in 0..4 {
+ for _ in 0..i {
+ vsids.bump(Var::from_index(i));
+ }
+ }
+
+ for _ in 0..60 {
+ vsids.decay();
+ }
+
+ // Decay is a power of two so these values are exact
+ #[allow(clippy::float_cmp)]
+ {
+ assert_eq!(vsids.activity[0].0, 0.0);
+ assert_eq!(vsids.activity[2].0, vsids.activity[1].0 * 2.0);
+ assert_eq!(vsids.activity[3].0, vsids.activity[1].0 * 3.0);
+ }
+ }
+
+ #[test]
+ fn heap_sorts() {
+ let mut vsids = Vsids::default();
+ vsids.set_var_count(8);
+
+ for _ in 0..8 {
+ vsids.next();
+ }
+
+ for i in 0..8 {
+ for _ in 0..i {
+ vsids.bump(Var::from_index(i));
+ }
+ }
+
+ for i in 0..8 {
+ vsids.make_available(Var::from_index((i * 5) % 8));
+ }
+
+ for i in (0..8).rev() {
+ assert_eq!(vsids.next(), Some(Var::from_index(i)));
+ }
+ assert_eq!(vsids.next(), None);
+ }
+
+ #[test]
+ fn heap_bump() {
+ let mut vsids = Vsids::default();
+ vsids.set_var_count(8);
+ vsids.set_decay(1.0 / 8.0);
+
+ for _ in 0..8 {
+ vsids.next();
+ }
+
+ for i in 0..8 {
+ for _ in 0..i {
+ vsids.bump(Var::from_index(i));
+ }
+ }
+
+ for i in 0..8 {
+ vsids.make_available(Var::from_index((i * 5) % 8));
+ }
+
+ for i in (0..4).rev() {
+ assert_eq!(vsids.next(), Some(Var::from_index(i + 4)));
+ }
+
+ vsids.decay();
+ vsids.decay();
+
+ for i in 0..8 {
+ for _ in 0..(8 - i) {
+ vsids.bump(Var::from_index(i));
+ }
+ }
+
+ for i in 0..4 {
+ assert_eq!(vsids.next(), Some(Var::from_index(i)));
+ }
+
+ assert_eq!(vsids.next(), None);
+ }
+}
diff --git a/vendor/varisat/src/glue.rs b/vendor/varisat/src/glue.rs
new file mode 100644
index 000000000..2036cdd99
--- /dev/null
+++ b/vendor/varisat/src/glue.rs
@@ -0,0 +1,36 @@
+//! Compute glue levels of clauses.
+//!
+//! The glue level of a propagating clause is the number of distinct decision levels of the clause's
+//! variables. This is also called the literal block distance (LBD). For each clause the smallest
+//! glue level observed is used as an indicator of how useful that clause is.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::context::{parts::*, Context};
+
+/// Compute the glue level of a clause.
+pub fn compute_glue(mut ctx: partial!(Context, mut TmpFlagsP, ImplGraphP), lits: &[Lit]) -> usize {
+ let (tmp_flags, ctx) = ctx.split_part_mut(TmpFlagsP);
+ let impl_graph = ctx.part(ImplGraphP);
+ let flags = &mut tmp_flags.flags;
+
+ let mut glue = 0;
+
+ for &lit in lits {
+ let level = impl_graph.level(lit.var());
+ let flag = &mut flags[level];
+ if !*flag {
+ *flag = true;
+ glue += 1
+ }
+ }
+
+ for &lit in lits {
+ let level = impl_graph.level(lit.var());
+ flags[level] = false;
+ }
+
+ glue
+}
diff --git a/vendor/varisat/src/lib.rs b/vendor/varisat/src/lib.rs
new file mode 100644
index 000000000..340b57b6f
--- /dev/null
+++ b/vendor/varisat/src/lib.rs
@@ -0,0 +1,46 @@
+//! Varisat is a [CDCL][cdcl] based SAT solver written in rust. Given a boolean formula in
+//! [conjunctive normal form][cnf], it either finds a variable assignment that makes the formula
+//! true or finds a proof that this is impossible.
+//!
+//! In addition to this API documentation, Varisat comes with a [user manual].
+//!
+//! [cdcl]: https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning
+//! [cnf]: https://en.wikipedia.org/wiki/Conjunctive_normal_form
+//! [user manual]: https://jix.github.io/varisat/manual/0.2.1/
+
+pub mod config;
+pub mod solver;
+
+mod analyze_conflict;
+mod assumptions;
+mod binary;
+mod cdcl;
+mod clause;
+mod context;
+mod decision;
+mod glue;
+mod load;
+mod model;
+mod proof;
+mod prop;
+mod schedule;
+mod state;
+mod tmp;
+mod unit_simplify;
+mod variables;
+
+pub use solver::{ProofFormat, Solver};
+pub use varisat_formula::{cnf, lit, CnfFormula, ExtendFormula, Lit, Var};
+
+pub mod dimacs {
+ //! DIMCAS CNF parser and writer.
+ pub use varisat_dimacs::*;
+}
+
+pub mod checker {
+ //! Proof checker for Varisat proofs.
+ pub use varisat_checker::{
+ CheckedProofStep, Checker, CheckerData, CheckerError, ProofProcessor,
+ ProofTranscriptProcessor, ProofTranscriptStep,
+ };
+}
diff --git a/vendor/varisat/src/load.rs b/vendor/varisat/src/load.rs
new file mode 100644
index 000000000..43415dbfb
--- /dev/null
+++ b/vendor/varisat/src/load.rs
@@ -0,0 +1,259 @@
+//! Loading a formula into the solver.
+use vec_mut_scan::VecMutScan;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::{DeleteClauseProof, ProofStep};
+
+use crate::{
+ clause::{db, ClauseHeader, Tier},
+ context::{parts::*, Context},
+ proof,
+ prop::{assignment, full_restart, Reason},
+ state::SatState,
+ unit_simplify::resurrect_unit,
+ variables,
+};
+
+/// Adds a clause to the current formula.
+///
+/// The input uses user variable names.
+///
+/// Removes duplicated literals, ignores tautological clauses (eg. x v -x v y), handles empty
+/// clauses and dispatches among unit, binary and long clauses.
+pub fn load_clause<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut BinaryClausesP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpDataP,
+ mut TmpFlagsP,
+ mut TrailP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+ user_lits: &[Lit],
+) {
+ match ctx.part(SolverStateP).sat_state {
+ SatState::Unsat => return,
+ SatState::Sat => {
+ ctx.part_mut(SolverStateP).sat_state = SatState::Unknown;
+ }
+ _ => {}
+ }
+
+ ctx.part_mut(SolverStateP).formula_is_empty = false;
+
+ // Restart the search when the user adds new clauses.
+ full_restart(ctx.borrow());
+
+ // Convert the clause from user to solver literals.
+ let (tmp_data, mut ctx_variables) = ctx.split_part_mut(TmpDataP);
+ variables::solver_from_user_lits(ctx_variables.borrow(), &mut tmp_data.lits, user_lits, true);
+
+ let (tmp_data, mut ctx) = ctx.split_part_mut(TmpDataP);
+
+ let lits = &mut tmp_data.lits;
+ let false_lits = &mut tmp_data.lits_2;
+
+ lits.sort_unstable();
+ lits.dedup();
+
+ proof::add_clause(ctx.borrow(), &lits);
+
+ // Detect tautological clauses
+ let mut last = None;
+
+ for &lit in lits.iter() {
+ if last == Some(!lit) {
+ return;
+ }
+ last = Some(lit);
+ }
+
+ // If we're not a unit clause the contained variables are not isolated anymore.
+ if lits.len() > 1 {
+ for &lit in lits.iter() {
+ ctx.part_mut(VariablesP)
+ .var_data_solver_mut(lit.var())
+ .isolated = false;
+ }
+ }
+
+ // Remove satisfied clauses and handle false literals.
+ //
+ // Proof generation expects us to start with the actual input clauses. If we would remove false
+ // literals we would have to generate proof steps for that. This would result in derived clauses
+ // being added during loading. If we're running proof processors on the fly, they'd see those
+ // derived clauses interspersed with the input clauses.
+ //
+ // We don't want to require each proof processor to handle dervied clause additions during
+ // loading of the initial formula. Thus we need to handle clauses with false literals here.
+ false_lits.clear();
+
+ let mut lits_scan = VecMutScan::new(lits);
+
+ let mut clause_is_true = false;
+
+ // We move unassigned literals to the beginning to make sure we're going to watch unassigned
+ // literals.
+ while let Some(lit) = lits_scan.next() {
+ match ctx.part(AssignmentP).lit_value(*lit) {
+ Some(true) => {
+ clause_is_true = true;
+ break;
+ }
+ Some(false) => {
+ false_lits.push(lit.remove());
+ }
+ None => (),
+ }
+ }
+
+ drop(lits_scan);
+
+ let will_conflict = lits.is_empty();
+
+ // We resurrect any removed false literals to ensure propagation by this new clause. This is
+ // also required to eventually simplify this clause.
+ for &lit in false_lits.iter() {
+ resurrect_unit(ctx.borrow(), !lit);
+ }
+
+ lits.extend_from_slice(&false_lits);
+
+ if clause_is_true {
+ if lits.len() > 1 {
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::DeleteClause {
+ clause: lits,
+ proof: DeleteClauseProof::Satisfied,
+ },
+ );
+ }
+ return;
+ }
+
+ match lits[..] {
+ [] => ctx.part_mut(SolverStateP).sat_state = SatState::Unsat,
+ [lit] => {
+ if will_conflict {
+ ctx.part_mut(SolverStateP).sat_state = SatState::Unsat
+ } else {
+ assignment::enqueue_assignment(ctx.borrow(), lit, Reason::Unit)
+ }
+ }
+ [lit_0, lit_1] => {
+ ctx.part_mut(BinaryClausesP)
+ .add_binary_clause([lit_0, lit_1]);
+ }
+ _ => {
+ let mut header = ClauseHeader::new();
+ header.set_tier(Tier::Irred);
+
+ db::add_clause(ctx.borrow(), header, lits);
+ }
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use partial_ref::IntoPartialRefMut;
+
+ use varisat_formula::lits;
+
+ use crate::clause::Tier;
+
+ #[test]
+ fn unsat_on_empty_clause() {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ load_clause(ctx.borrow(), &[]);
+
+ assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+ }
+
+ #[test]
+ fn unit_clauses() {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ load_clause(ctx.borrow(), &lits![1]);
+
+ assert_eq!(ctx.part(TrailP).trail().len(), 1);
+
+ load_clause(ctx.borrow(), &lits![3, -3]);
+
+ assert_eq!(ctx.part(TrailP).trail().len(), 1);
+
+ load_clause(ctx.borrow(), &lits![-2]);
+
+ assert_eq!(ctx.part(TrailP).trail().len(), 2);
+
+ load_clause(ctx.borrow(), &lits![1, 1]);
+
+ assert_eq!(ctx.part(TrailP).trail().len(), 2);
+
+ assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+
+ load_clause(ctx.borrow(), &lits![2]);
+
+ assert_eq!(ctx.part(TrailP).trail().len(), 2);
+
+ assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unsat);
+ }
+
+ #[test]
+ fn binary_clauses() {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ load_clause(ctx.borrow(), &lits![1, 2]);
+
+ assert_eq!(ctx.part(BinaryClausesP).count(), 1);
+
+ load_clause(ctx.borrow(), &lits![-1, 3, 3]);
+
+ assert_eq!(ctx.part(BinaryClausesP).count(), 2);
+
+ load_clause(ctx.borrow(), &lits![4, -4]);
+
+ assert_eq!(ctx.part(BinaryClausesP).count(), 2);
+
+ assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+ }
+
+ #[test]
+ fn long_clauses() {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ load_clause(ctx.borrow(), &lits![1, 2, 3]);
+
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 1);
+
+ load_clause(ctx.borrow(), &lits![-2, 3, 3, 4]);
+
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 2);
+
+ load_clause(ctx.borrow(), &lits![4, -5, 5, 2]);
+
+ assert_eq!(ctx.part(ClauseDbP).count_by_tier(Tier::Irred), 2);
+
+ assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+ }
+}
diff --git a/vendor/varisat/src/model.rs b/vendor/varisat/src/model.rs
new file mode 100644
index 000000000..d4f269f6f
--- /dev/null
+++ b/vendor/varisat/src/model.rs
@@ -0,0 +1,87 @@
+//! Global model reconstruction
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::ProofStep;
+
+use crate::{
+ context::{parts::*, Context},
+ proof,
+ state::SatState,
+};
+
+/// Global model reconstruction
+#[derive(Default)]
+pub struct Model {
+ /// Assignment of the global model.
+ ///
+ /// Whenever the solver state is SAT this must be up to date.
+ assignment: Vec<Option<bool>>,
+}
+
+impl Model {
+ /// Assignment of the global model.
+ ///
+ /// Only valid if the solver state is SAT.
+ pub fn assignment(&self) -> &[Option<bool>] {
+ &self.assignment
+ }
+
+ /// Whether a given global literal is true in the model assignment.
+ ///
+ /// Only valid if the solver state is SAT.
+ pub fn lit_is_true(&self, global_lit: Lit) -> bool {
+ self.assignment[global_lit.index()] == Some(global_lit.is_positive())
+ }
+}
+
+pub fn reconstruct_global_model<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut ModelP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpDataP,
+ AssignmentP,
+ VariablesP
+ ),
+) {
+ let (variables, mut ctx) = ctx.split_part(VariablesP);
+ let (model, mut ctx) = ctx.split_part_mut(ModelP);
+ let (tmp, mut ctx) = ctx.split_part_mut(TmpDataP);
+
+ let models_in_proof = ctx.part(ProofP).models_in_proof();
+
+ tmp.lits.clear();
+
+ model.assignment.clear();
+ model.assignment.resize(variables.global_watermark(), None);
+
+ for global_var in variables.global_var_iter() {
+ let value = if let Some(solver_var) = variables.solver_from_global().get(global_var) {
+ ctx.part(AssignmentP).var_value(solver_var)
+ } else {
+ Some(variables.var_data_global(global_var).unit.unwrap_or(false))
+ };
+
+ model.assignment[global_var.index()] = value;
+
+ if models_in_proof {
+ if let Some(value) = value {
+ tmp.lits.push(global_var.lit(value))
+ }
+ }
+ }
+
+ if models_in_proof {
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::Model {
+ assignment: &tmp.lits,
+ },
+ );
+ }
+ ctx.part_mut(SolverStateP).sat_state = SatState::Sat;
+}
diff --git a/vendor/varisat/src/proof.rs b/vendor/varisat/src/proof.rs
new file mode 100644
index 000000000..336f7fbc2
--- /dev/null
+++ b/vendor/varisat/src/proof.rs
@@ -0,0 +1,434 @@
+//! Proof generation.
+
+use std::io::{self, sink, BufWriter, Write};
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_checker::{internal::SelfChecker, Checker, CheckerError, ProofProcessor};
+use varisat_formula::{Lit, Var};
+use varisat_internal_proof::{ClauseHash, ProofStep};
+
+use crate::{
+ context::{parts::*, Context},
+ solver::SolverError,
+};
+
+mod drat;
+mod map_step;
+
+/// Proof formats that can be generated during solving.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum ProofFormat {
+ Varisat,
+ Drat,
+ BinaryDrat,
+}
+
+/// Number of added or removed clauses.
+pub fn clause_count_delta(step: &ProofStep) -> isize {
+ match step {
+ ProofStep::AddClause { clause } | ProofStep::AtClause { clause, .. } => {
+ if clause.len() > 1 {
+ 1
+ } else {
+ 0
+ }
+ }
+ ProofStep::DeleteClause { clause, .. } => {
+ if clause.len() > 1 {
+ -1
+ } else {
+ 0
+ }
+ }
+ ProofStep::SolverVarName { .. }
+ | ProofStep::UserVarName { .. }
+ | ProofStep::DeleteVar { .. }
+ | ProofStep::ChangeSamplingMode { .. }
+ | ProofStep::UnitClauses { .. }
+ | ProofStep::ChangeHashBits { .. }
+ | ProofStep::Model { .. }
+ | ProofStep::Assumptions { .. }
+ | ProofStep::FailedAssumptions { .. }
+ | ProofStep::End => 0,
+ }
+}
+
+/// Proof generation.
+pub struct Proof<'a> {
+ format: Option<ProofFormat>,
+ target: BufWriter<Box<dyn Write + 'a>>,
+ checker: Option<Checker<'a>>,
+ map_step: map_step::MapStep,
+ /// How many bits are used for storing clause hashes.
+ hash_bits: u32,
+ /// How many clauses are currently in the db.
+ ///
+ /// This is used to pick a good number of hash_bits
+ clause_count: isize,
+}
+
+impl<'a> Default for Proof<'a> {
+ fn default() -> Proof<'a> {
+ Proof {
+ format: None,
+ target: BufWriter::new(Box::new(sink())),
+ checker: None,
+ map_step: Default::default(),
+ hash_bits: 64,
+ clause_count: 0,
+ }
+ }
+}
+
+impl<'a> Proof<'a> {
+ /// Start writing proof steps to the given target with the given format.
+ pub fn write_proof(&mut self, target: impl Write + 'a, format: ProofFormat) {
+ self.format = Some(format);
+ self.target = BufWriter::new(Box::new(target))
+ }
+
+ /// Begin checking proof steps.
+ pub fn begin_checking(&mut self) {
+ if self.checker.is_none() {
+ self.checker = Some(Checker::new())
+ }
+ }
+
+ /// Add a [`ProofProcessor`].
+ ///
+ /// See also [`Checker::add_processor`].
+ pub fn add_processor(&mut self, processor: &'a mut dyn ProofProcessor) {
+ self.begin_checking();
+ self.checker.as_mut().unwrap().add_processor(processor);
+ }
+
+ /// Whether proof generation is active.
+ pub fn is_active(&self) -> bool {
+ self.checker.is_some() || self.format.is_some()
+ }
+
+ /// Are we emitting or checking our native format.
+ pub fn native_format(&self) -> bool {
+ self.checker.is_some()
+ || match self.format {
+ Some(ProofFormat::Varisat) => true,
+ _ => false,
+ }
+ }
+
+ /// Whether clause hashes are required for steps that support them.
+ pub fn clause_hashes_required(&self) -> bool {
+ self.native_format()
+ }
+
+ /// Whether found models are included in the proof.
+ pub fn models_in_proof(&self) -> bool {
+ self.native_format()
+ }
+}
+
+/// Call when adding an external clause.
+///
+/// This is required for on the fly checking and checking of incremental solving.
+///
+/// *Note:* this function expects the clause to use solver var names.
+pub fn add_clause<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, VariablesP),
+ clause: &[Lit],
+) {
+ if ctx.part(SolverStateP).solver_invoked {
+ add_step(ctx.borrow(), true, &ProofStep::AddClause { clause })
+ } else {
+ let (variables, mut ctx) = ctx.split_part(VariablesP);
+ let proof = ctx.part_mut(ProofP);
+ if let Some(checker) = &mut proof.checker {
+ let clause = proof.map_step.map_lits(clause, |var| {
+ variables
+ .global_from_solver()
+ .get(var)
+ .expect("no existing global var for solver var")
+ });
+
+ let result = checker.add_clause(clause);
+ handle_self_check_result(ctx.borrow(), result);
+ }
+ if clause.len() > 1 {
+ ctx.part_mut(ProofP).clause_count += 1;
+ }
+ }
+}
+
+/// Add a step to the proof.
+///
+/// Ignored when proof generation is disabled.
+///
+/// When `solver_vars` is true, all variables and literals will be converted from solver to global
+/// vars. Otherwise the proof step needs to use global vars.
+pub fn add_step<'a, 's>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, VariablesP),
+ solver_vars: bool,
+ step: &'s ProofStep<'s>,
+) {
+ if ctx.part(SolverStateP).solver_error.is_some() {
+ return;
+ }
+
+ if ctx.part(SolverStateP).solver_error.is_some() {
+ return;
+ }
+
+ let (variables, mut ctx) = ctx.split_part(VariablesP);
+ let proof = ctx.part_mut(ProofP);
+
+ let map_vars = |var| {
+ if solver_vars {
+ variables
+ .global_from_solver()
+ .get(var)
+ .expect("no existing global var for solver var")
+ } else {
+ var
+ }
+ };
+
+ let io_result = match proof.format {
+ Some(ProofFormat::Varisat) => write_varisat_step(ctx.borrow(), map_vars, step),
+ Some(ProofFormat::Drat) => {
+ let step = proof.map_step.map(step, map_vars, |hash| hash);
+ drat::write_step(&mut proof.target, &step)
+ }
+ Some(ProofFormat::BinaryDrat) => {
+ let step = proof.map_step.map(step, map_vars, |hash| hash);
+ drat::write_binary_step(&mut proof.target, &step)
+ }
+ None => Ok(()),
+ };
+
+ if io_result.is_ok() {
+ let proof = ctx.part_mut(ProofP);
+ if let Some(checker) = &mut proof.checker {
+ let step = proof.map_step.map(step, map_vars, |hash| hash);
+ let result = checker.self_check_step(step);
+ handle_self_check_result(ctx.borrow(), result);
+ }
+ }
+
+ handle_io_errors(ctx.borrow(), io_result);
+}
+
+/// Write a step using our native format
+fn write_varisat_step<'a, 's>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, SolverStateP),
+ map_vars: impl Fn(Var) -> Var,
+ step: &'s ProofStep<'s>,
+) -> io::Result<()> {
+ let (proof, ctx) = ctx.split_part_mut(ProofP);
+
+ proof.clause_count += clause_count_delta(step);
+
+ let mut rehash = false;
+ // Should we change the hash size?
+ while proof.clause_count > (1 << (proof.hash_bits / 2)) {
+ proof.hash_bits += 2;
+ rehash = true;
+ }
+ if ctx.part(SolverStateP).solver_invoked {
+ while proof.hash_bits > 6 && proof.clause_count * 4 < (1 << (proof.hash_bits / 2)) {
+ proof.hash_bits -= 2;
+ rehash = true;
+ }
+ }
+
+ if rehash {
+ varisat_internal_proof::binary_format::write_step(
+ &mut proof.target,
+ &ProofStep::ChangeHashBits {
+ bits: proof.hash_bits,
+ },
+ )?;
+ }
+
+ let shift_bits = ClauseHash::max_value().count_ones() - proof.hash_bits;
+
+ let map_hash = |hash| hash >> shift_bits;
+ let step = proof.map_step.map(step, map_vars, map_hash);
+
+ if proof.format == Some(ProofFormat::Varisat) {
+ varisat_internal_proof::binary_format::write_step(&mut proof.target, &step)?;
+ }
+
+ Ok(())
+}
+
+/// Flush buffers used for writing proof steps.
+pub fn flush_proof<'a>(mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP)) {
+ // We need to explicitly flush to handle IO errors.
+ let result = ctx.part_mut(ProofP).target.flush();
+ handle_io_errors(ctx.borrow(), result);
+}
+
+/// Stop writing proof steps.
+pub fn close_proof<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, VariablesP),
+) {
+ add_step(ctx.borrow(), true, &ProofStep::End);
+ flush_proof(ctx.borrow());
+ ctx.part_mut(ProofP).format = None;
+ ctx.part_mut(ProofP).target = BufWriter::new(Box::new(sink()));
+}
+
+/// Called before solve returns to flush buffers and to trigger delayed unit conflict processing.
+///
+/// We flush buffers before solve returns to ensure that we can pass IO errors to the user.
+pub fn solve_finished<'a>(mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP)) {
+ flush_proof(ctx.borrow());
+ if let Some(checker) = &mut ctx.part_mut(ProofP).checker {
+ let result = checker.self_check_delayed_steps();
+ handle_self_check_result(ctx.borrow(), result);
+ }
+}
+
+/// Handle results of on the fly checking.
+///
+/// Panics when the proof is incorrect and aborts solving when a proof processor produced an error.
+fn handle_self_check_result<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP),
+ result: Result<(), CheckerError>,
+) {
+ match result {
+ Err(CheckerError::ProofProcessorError { cause }) => {
+ ctx.part_mut(SolverStateP).solver_error =
+ Some(SolverError::ProofProcessorError { cause });
+ *ctx.part_mut(ProofP) = Proof::default();
+ }
+ Err(err) => {
+ log::error!("{}", err);
+ if let CheckerError::CheckFailed { debug_step, .. } = err {
+ if !debug_step.is_empty() {
+ log::error!("failed step was {}", debug_step)
+ }
+ }
+ panic!("self check failure");
+ }
+ Ok(()) => (),
+ }
+}
+
+/// Handle io errors during proof writing.
+fn handle_io_errors<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP),
+ result: io::Result<()>,
+) {
+ if let Err(io_err) = result {
+ ctx.part_mut(SolverStateP).solver_error = Some(SolverError::ProofIoError { cause: io_err });
+ *ctx.part_mut(ProofP) = Proof::default();
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use proptest::prelude::*;
+
+ use std::{fs::File, process::Command};
+
+ use tempfile::TempDir;
+
+ use varisat_dimacs::write_dimacs;
+ use varisat_formula::{test::sgen_unsat_formula, CnfFormula};
+
+ use crate::solver::Solver;
+
+ enum Checker {
+ DratTrim,
+ Rate,
+ }
+
+ fn test_drat(checker: Checker, formula: CnfFormula, binary: bool) -> Result<(), TestCaseError> {
+ let mut solver = Solver::new();
+
+ let tmp = TempDir::new()?;
+
+ let drat_proof = tmp.path().join("proof.drat");
+ let cnf_file = tmp.path().join("input.cnf");
+
+ write_dimacs(&mut File::create(&cnf_file)?, &formula)?;
+
+ let format = if binary {
+ ProofFormat::BinaryDrat
+ } else {
+ ProofFormat::Drat
+ };
+
+ solver.write_proof(File::create(&drat_proof)?, format);
+
+ solver.add_formula(&formula);
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+
+ solver
+ .close_proof()
+ .map_err(|e| TestCaseError::fail(e.to_string()))?;
+
+ let output = match checker {
+ Checker::DratTrim => {
+ if binary {
+ Command::new("drat-trim")
+ .arg(&cnf_file)
+ .arg(&drat_proof)
+ .arg("-i")
+ .output()?
+ } else {
+ Command::new("drat-trim")
+ .arg(&cnf_file)
+ .arg(&drat_proof)
+ .output()?
+ }
+ }
+ Checker::Rate => Command::new("rate")
+ .arg(&cnf_file)
+ .arg(&drat_proof)
+ .output()?,
+ };
+
+ prop_assert!(std::str::from_utf8(&output.stdout)?.contains("s VERIFIED"));
+
+ Ok(())
+ }
+
+ proptest! {
+ #[cfg_attr(not(test_drat_trim), ignore)]
+ #[test]
+ fn sgen_unsat_drat_trim(
+ formula in sgen_unsat_formula(1..7usize),
+ ) {
+ test_drat(Checker::DratTrim, formula, false)?;
+ }
+
+ #[cfg_attr(not(test_drat_trim), ignore)]
+ #[test]
+ fn sgen_unsat_binary_drat_trim(
+ formula in sgen_unsat_formula(1..7usize),
+ ) {
+ test_drat(Checker::DratTrim, formula, true)?;
+ }
+
+ #[cfg_attr(not(test_rate), ignore)]
+ #[test]
+ fn sgen_unsat_rate(
+ formula in sgen_unsat_formula(1..7usize),
+ ) {
+ test_drat(Checker::Rate, formula, false)?;
+ }
+
+ #[cfg_attr(not(test_rate), ignore)]
+ #[test]
+ fn sgen_unsat_binary_rate(
+ formula in sgen_unsat_formula(1..7usize),
+ ) {
+ test_drat(Checker::Rate, formula, true)?;
+ }
+ }
+}
diff --git a/vendor/varisat/src/proof/drat.rs b/vendor/varisat/src/proof/drat.rs
new file mode 100644
index 000000000..76382fab3
--- /dev/null
+++ b/vendor/varisat/src/proof/drat.rs
@@ -0,0 +1,85 @@
+use std::io::{self, Write};
+
+use varisat_formula::Lit;
+use varisat_internal_proof::ProofStep;
+
+/// Prepares a proof step for DRAT writing
+fn drat_step(
+ step: &ProofStep,
+ mut emit_drat_step: impl FnMut(bool, &[Lit]) -> io::Result<()>,
+) -> io::Result<()> {
+ match step {
+ ProofStep::AtClause { clause, .. } => {
+ emit_drat_step(true, &clause)?;
+ }
+ ProofStep::UnitClauses { units } => {
+ for &(unit, _hash) in units.iter() {
+ emit_drat_step(true, &[unit])?;
+ }
+ }
+ ProofStep::DeleteClause { clause, .. } => {
+ emit_drat_step(false, &clause[..])?;
+ }
+ ProofStep::SolverVarName { .. }
+ | ProofStep::UserVarName { .. }
+ | ProofStep::DeleteVar { .. }
+ | ProofStep::ChangeSamplingMode { .. }
+ | ProofStep::ChangeHashBits { .. }
+ | ProofStep::Model { .. }
+ | ProofStep::End => (),
+ ProofStep::AddClause { .. } => {
+ // TODO allow error handling here?
+ panic!("incremental clause additions not supported by DRAT proofs");
+ }
+ ProofStep::Assumptions { .. } | ProofStep::FailedAssumptions { .. } => {
+ // TODO allow error handling here?
+ panic!("assumptions not supported by DRAT proofs");
+ }
+ }
+
+ Ok(())
+}
+
+/// Writes a proof step in DRAT format
+pub fn write_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> {
+ drat_step(step, |add, clause| {
+ if !add {
+ target.write_all(b"d ")?;
+ }
+ write_literals(target, &clause[..])?;
+ Ok(())
+ })
+}
+
+/// Writes a proof step in binary DRAT format
+pub fn write_binary_step<'s>(target: &mut impl Write, step: &'s ProofStep<'s>) -> io::Result<()> {
+ drat_step(step, |add, clause| {
+ if add {
+ target.write_all(b"a")?;
+ } else {
+ target.write_all(b"d")?;
+ }
+ write_binary_literals(target, &clause[..])?;
+ Ok(())
+ })
+}
+
+/// Writes the literals of a clause for a step in a DRAT proof.
+fn write_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> {
+ for &lit in literals {
+ itoa::write(&mut *target, lit.to_dimacs())?;
+ target.write_all(b" ")?;
+ }
+ target.write_all(b"0\n")?;
+ Ok(())
+}
+
+/// Writes the literals of a clause for a step in a binary DRAT proof.
+fn write_binary_literals(target: &mut impl Write, literals: &[Lit]) -> io::Result<()> {
+ for &lit in literals {
+ let drat_code = lit.code() as u64 + 2;
+ leb128::write::unsigned(target, drat_code)?;
+ }
+ target.write_all(&[0])?;
+ Ok(())
+}
diff --git a/vendor/varisat/src/proof/map_step.rs b/vendor/varisat/src/proof/map_step.rs
new file mode 100644
index 000000000..0c08e6510
--- /dev/null
+++ b/vendor/varisat/src/proof/map_step.rs
@@ -0,0 +1,128 @@
+//! Maps literals and hashes of clause steps between the solver and the checker.
+
+use varisat_formula::{Lit, Var};
+
+use super::{ClauseHash, ProofStep};
+
+/// Maps literals and hashes of clause steps between the solver and the checker.
+#[derive(Default)]
+pub struct MapStep {
+ lit_buf: Vec<Lit>,
+ hash_buf: Vec<ClauseHash>,
+ unit_buf: Vec<(Lit, ClauseHash)>,
+}
+
+impl MapStep {
+ pub fn map_lits(&mut self, lits: &[Lit], map_var: impl Fn(Var) -> Var) -> &[Lit] {
+ let map_var_ref = &map_var;
+ self.lit_buf.clear();
+ self.lit_buf
+ .extend(lits.iter().map(|lit| lit.map_var(map_var_ref)));
+ &self.lit_buf
+ }
+
+ pub fn map<'s, 'a, 'b>(
+ &'a mut self,
+ step: &ProofStep<'b>,
+ map_var: impl Fn(Var) -> Var,
+ map_hash: impl Fn(ClauseHash) -> ClauseHash,
+ ) -> ProofStep<'s>
+ where
+ 'a: 's,
+ 'b: 's,
+ {
+ let map_var_ref = &map_var;
+ let map_lit = |lit: Lit| lit.map_var(map_var_ref);
+ match *step {
+ ProofStep::AddClause { clause } => {
+ self.lit_buf.clear();
+ self.lit_buf.extend(clause.iter().cloned().map(map_lit));
+ ProofStep::AddClause {
+ clause: &self.lit_buf,
+ }
+ }
+
+ ProofStep::AtClause {
+ redundant,
+ clause,
+ propagation_hashes,
+ } => {
+ self.lit_buf.clear();
+ self.lit_buf.extend(clause.iter().cloned().map(map_lit));
+ self.hash_buf.clear();
+ self.hash_buf
+ .extend(propagation_hashes.iter().cloned().map(map_hash));
+ ProofStep::AtClause {
+ redundant,
+ clause: &self.lit_buf,
+ propagation_hashes: &self.hash_buf,
+ }
+ }
+
+ ProofStep::UnitClauses { units } => {
+ self.unit_buf.clear();
+ self.unit_buf.extend(
+ units
+ .iter()
+ .map(|&(lit, hash)| (map_lit(lit), map_hash(hash))),
+ );
+ ProofStep::UnitClauses {
+ units: &self.unit_buf,
+ }
+ }
+
+ ProofStep::DeleteClause { clause, proof } => {
+ self.lit_buf.clear();
+ self.lit_buf.extend(clause.iter().cloned().map(map_lit));
+ ProofStep::DeleteClause {
+ clause: &self.lit_buf,
+ proof,
+ }
+ }
+
+ ProofStep::Model { assignment } => {
+ self.lit_buf.clear();
+ self.lit_buf.extend(assignment.iter().cloned().map(map_lit));
+ ProofStep::Model {
+ assignment: &self.lit_buf,
+ }
+ }
+
+ ProofStep::Assumptions { assumptions } => {
+ self.lit_buf.clear();
+ self.lit_buf
+ .extend(assumptions.iter().cloned().map(map_lit));
+ ProofStep::Assumptions {
+ assumptions: &self.lit_buf,
+ }
+ }
+
+ ProofStep::FailedAssumptions {
+ failed_core,
+ propagation_hashes,
+ } => {
+ self.lit_buf.clear();
+ self.lit_buf
+ .extend(failed_core.iter().cloned().map(map_lit));
+ self.hash_buf.clear();
+ self.hash_buf
+ .extend(propagation_hashes.iter().cloned().map(map_hash));
+ ProofStep::FailedAssumptions {
+ failed_core: &self.lit_buf,
+ propagation_hashes: &self.hash_buf,
+ }
+ }
+
+ ProofStep::ChangeHashBits { .. } | ProofStep::End => *step,
+
+ ProofStep::SolverVarName { .. }
+ | ProofStep::UserVarName { .. }
+ | ProofStep::DeleteVar { .. }
+ | ProofStep::ChangeSamplingMode { .. } => {
+ // while these steps do contain variables, they are used to update the mapping, so
+ // they shouldn't be mapped themselves.
+ *step
+ }
+ }
+ }
+}
diff --git a/vendor/varisat/src/prop.rs b/vendor/varisat/src/prop.rs
new file mode 100644
index 000000000..517f03be2
--- /dev/null
+++ b/vendor/varisat/src/prop.rs
@@ -0,0 +1,261 @@
+//! Unit propagation.
+use partial_ref::{partial, PartialRef};
+
+use crate::context::{parts::*, Context};
+
+pub mod assignment;
+pub mod binary;
+pub mod graph;
+pub mod long;
+pub mod watch;
+
+pub use assignment::{backtrack, enqueue_assignment, full_restart, restart, Assignment, Trail};
+pub use graph::{Conflict, ImplGraph, ImplNode, Reason};
+pub use watch::{enable_watchlists, Watch, Watchlists};
+
+/// Propagate enqueued assignments.
+///
+/// Returns when all enqueued assignments are propagated, including newly propagated assignemnts, or
+/// if there is a conflict.
+///
+/// On conflict the first propagation that would assign the opposite value to an already assigned
+/// literal is returned.
+pub fn propagate(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut ClauseAllocP,
+ mut ImplGraphP,
+ mut TrailP,
+ mut WatchlistsP,
+ BinaryClausesP,
+ ClauseDbP,
+ ),
+) -> Result<(), Conflict> {
+ enable_watchlists(ctx.borrow());
+
+ while let Some(lit) = ctx.part_mut(TrailP).pop_queue() {
+ binary::propagate_binary(ctx.borrow(), lit)?;
+ long::propagate_long(ctx.borrow(), lit)?;
+ }
+ Ok(())
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use proptest::{prelude::*, *};
+
+ use rand::{distributions::Bernoulli, seq::SliceRandom};
+
+ use partial_ref::IntoPartialRefMut;
+
+ use varisat_formula::{cnf::strategy::*, CnfFormula, Lit};
+
+ use crate::{
+ clause::{db, gc},
+ load::load_clause,
+ state::SatState,
+ };
+
+ /// Generate a random formula and list of implied literals.
+ pub fn prop_formula(
+ vars: impl Strategy<Value = usize>,
+ extra_vars: impl Strategy<Value = usize>,
+ extra_clauses: impl Strategy<Value = usize>,
+ density: impl Strategy<Value = f64>,
+ ) -> impl Strategy<Value = (Vec<Lit>, CnfFormula)> {
+ (vars, extra_vars, extra_clauses, density).prop_flat_map(
+ |(vars, extra_vars, extra_clauses, density)| {
+ let polarity = collection::vec(bool::ANY, vars + extra_vars);
+
+ let dist = Bernoulli::new(density).unwrap();
+
+ let lits = polarity
+ .prop_map(|polarity| {
+ polarity
+ .into_iter()
+ .enumerate()
+ .map(|(index, polarity)| Lit::from_index(index, polarity))
+ .collect::<Vec<_>>()
+ })
+ .prop_shuffle();
+
+ lits.prop_perturb(move |mut lits, mut rng| {
+ let assigned_lits = &lits[..vars];
+
+ let mut clauses: Vec<Vec<Lit>> = vec![];
+ for (i, &lit) in assigned_lits.iter().enumerate() {
+ // Build a clause that implies lit
+ let mut clause = vec![lit];
+ for &reason_lit in assigned_lits[..i].iter() {
+ if rng.sample(dist) {
+ clause.push(!reason_lit);
+ }
+ }
+ clause.shuffle(&mut rng);
+ clauses.push(clause);
+ }
+
+ for _ in 0..extra_clauses {
+ // Build a clause that is satisfied
+ let &true_lit = assigned_lits.choose(&mut rng).unwrap();
+ let mut clause = vec![true_lit];
+ for &other_lit in lits.iter() {
+ if other_lit != true_lit && rng.sample(dist) {
+ clause.push(other_lit ^ rng.gen::<bool>());
+ }
+ }
+ clause.shuffle(&mut rng);
+ clauses.push(clause);
+ }
+
+ clauses.shuffle(&mut rng);
+
+ // Only return implied lits
+ lits.drain(vars..);
+
+ (lits, CnfFormula::from(clauses))
+ })
+ },
+ )
+ }
+
+ proptest! {
+ #[test]
+ fn propagation_no_conflict(
+ (mut lits, formula) in prop_formula(
+ 2..30usize,
+ 0..10usize,
+ 0..20usize,
+ 0.1..0.9
+ ),
+ ) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+
+ let prop_result = propagate(ctx.borrow());
+
+ prop_assert_eq!(prop_result, Ok(()));
+
+ lits.sort();
+
+ let mut prop_lits = ctx.part(TrailP).trail().to_owned();
+
+ // Remap vars
+ for lit in prop_lits.iter_mut() {
+ *lit = lit.map_var(|solver_var| {
+ ctx.part(VariablesP).existing_user_from_solver(solver_var)
+ });
+ }
+
+ prop_lits.sort();
+
+ prop_assert_eq!(prop_lits, lits);
+ }
+
+ #[test]
+ fn propagation_conflict(
+ (lits, formula) in prop_formula(
+ 2..30usize,
+ 0..10usize,
+ 0..20usize,
+ 0.1..0.9
+ ),
+ conflict_size in any::<sample::Index>(),
+ ) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ // We add the conflict clause first to make sure that it isn't simplified during loading
+
+ let conflict_size = conflict_size.index(lits.len() - 1) + 2;
+
+ let conflict_clause: Vec<_> = lits[..conflict_size].iter().map(|&lit| !lit).collect();
+
+ load_clause(ctx.borrow(), &conflict_clause);
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+
+ let prop_result = propagate(ctx.borrow());
+
+ prop_assert!(prop_result.is_err());
+
+ let conflict = prop_result.unwrap_err();
+
+ let conflict_lits = conflict.lits(&ctx.borrow()).to_owned();
+
+ for &lit in conflict_lits.iter() {
+ prop_assert!(ctx.part(AssignmentP).lit_is_false(lit));
+ }
+ }
+
+ #[test]
+ fn propagation_no_conflict_after_gc(
+ tmp_formula in cnf_formula(3..30usize, 30..100, 3..30),
+ (mut lits, formula) in prop_formula(
+ 2..30usize,
+ 0..10usize,
+ 0..20usize,
+ 0.1..0.9
+ ),
+ ) {
+ let mut ctx = Context::default();
+ let mut ctx = ctx.into_partial_ref_mut();
+
+ for clause in tmp_formula.iter() {
+ // Only add long clauses here
+ let mut lits = clause.to_owned();
+ lits.sort();
+ lits.dedup();
+ if lits.len() >= 3 {
+ load_clause(ctx.borrow(), clause);
+ }
+ }
+
+ let tmp_crefs: Vec<_> = db::clauses_iter(&ctx.borrow()).collect();
+
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+
+ for cref in tmp_crefs {
+ db::delete_clause(ctx.borrow(), cref);
+ }
+
+ gc::collect_garbage(ctx.borrow());
+
+ prop_assert_eq!(ctx.part(SolverStateP).sat_state, SatState::Unknown);
+
+ let prop_result = propagate(ctx.borrow());
+
+ prop_assert_eq!(prop_result, Ok(()));
+
+ lits.sort();
+
+ let mut prop_lits = ctx.part(TrailP).trail().to_owned();
+
+ // Remap vars
+ for lit in prop_lits.iter_mut() {
+ *lit = lit.map_var(|solver_var| {
+ ctx.part(VariablesP).existing_user_from_solver(solver_var)
+ });
+ }
+
+ prop_lits.sort();
+
+ prop_assert_eq!(prop_lits, lits);
+ }
+ }
+}
diff --git a/vendor/varisat/src/prop/assignment.rs b/vendor/varisat/src/prop/assignment.rs
new file mode 100644
index 000000000..a87f60485
--- /dev/null
+++ b/vendor/varisat/src/prop/assignment.rs
@@ -0,0 +1,237 @@
+//! Partial assignment and backtracking.
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::{lit::LitIdx, Lit, Var};
+
+use crate::{
+ context::{parts::*, Context},
+ decision::make_available,
+};
+
+use super::Reason;
+
+/// Current partial assignment.
+#[derive(Default)]
+pub struct Assignment {
+ assignment: Vec<Option<bool>>,
+ last_value: Vec<bool>,
+}
+
+/// This compares two `Option<bool>` values as bytes. Workaround for bad code generation.
+pub fn fast_option_eq(a: Option<bool>, b: Option<bool>) -> bool {
+ unsafe { std::mem::transmute::<_, u8>(a) == std::mem::transmute::<_, u8>(b) }
+}
+
+impl Assignment {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.assignment.resize(count, None);
+ self.last_value.resize(count, false);
+ }
+
+ /// Current partial assignment as slice.
+ pub fn assignment(&self) -> &[Option<bool>] {
+ &self.assignment
+ }
+
+ /// Value assigned to a variable.
+ pub fn var_value(&self, var: Var) -> Option<bool> {
+ self.assignment[var.index()]
+ }
+
+ /// Value last assigned to a variable.
+ ///
+ /// If the variable is currently assigned this returns the previously assigned value. If the
+ /// variable was never assigned this returns false.
+ pub fn last_var_value(&self, var: Var) -> bool {
+ self.last_value[var.index()]
+ }
+
+ /// Value assigned to a literal.
+ pub fn lit_value(&self, lit: Lit) -> Option<bool> {
+ self.assignment[lit.index()].map(|b| b ^ lit.is_negative())
+ }
+
+ pub fn lit_is_true(&self, lit: Lit) -> bool {
+ fast_option_eq(self.assignment[lit.index()], Some(lit.is_positive()))
+ }
+
+ pub fn lit_is_false(&self, lit: Lit) -> bool {
+ fast_option_eq(self.assignment[lit.index()], Some(lit.is_negative()))
+ }
+
+ pub fn lit_is_unk(&self, lit: Lit) -> bool {
+ fast_option_eq(self.assignment[lit.index()], None)
+ }
+
+ pub fn assign_lit(&mut self, lit: Lit) {
+ self.assignment[lit.index()] = lit.is_positive().into()
+ }
+
+ pub fn unassign_var(&mut self, var: Var) {
+ self.assignment[var.index()] = None;
+ }
+
+ /// Set the assigned/unassigned value of a variable.
+ pub fn set_var(&mut self, var: Var, assignment: Option<bool>) {
+ self.assignment[var.index()] = assignment;
+ }
+}
+
+/// Decision and propagation history.
+#[derive(Default)]
+pub struct Trail {
+ /// Stack of all propagated and all enqueued assignments
+ trail: Vec<Lit>,
+ /// Next assignment in trail to propagate
+ queue_head_pos: usize,
+ /// Decision levels as trail indices.
+ decisions: Vec<LitIdx>,
+ /// Number of unit clauses removed from the trail.
+ units_removed: usize,
+}
+
+impl Trail {
+ /// Return the next assigned literal to propagate.
+ pub fn queue_head(&self) -> Option<Lit> {
+ self.trail.get(self.queue_head_pos).cloned()
+ }
+
+ /// Return the next assigned literal to propagate and remove it from the queue.
+ pub fn pop_queue(&mut self) -> Option<Lit> {
+ let head = self.queue_head();
+ if head.is_some() {
+ self.queue_head_pos += 1;
+ }
+ head
+ }
+
+ /// Re-enqueue all assigned literals.
+ pub fn reset_queue(&mut self) {
+ self.queue_head_pos = 0;
+ }
+
+ /// Assigned literals in assignment order.
+ pub fn trail(&self) -> &[Lit] {
+ &self.trail
+ }
+
+ /// Clear the trail.
+ ///
+ /// This simply removes all entries without performing any backtracking. Can only be called with
+ /// no active decisions.
+ pub fn clear(&mut self) {
+ assert!(self.decisions.is_empty());
+ self.units_removed += self.trail.len();
+ self.trail.clear();
+ self.queue_head_pos = 0;
+ }
+
+ /// Start a new decision level.
+ ///
+ /// Does not enqueue the decision itself.
+ pub fn new_decision_level(&mut self) {
+ self.decisions.push(self.trail.len() as LitIdx)
+ }
+
+ /// Current decision level.
+ pub fn current_level(&self) -> usize {
+ self.decisions.len()
+ }
+
+ /// The number of assignments at level 0.
+ pub fn top_level_assignment_count(&self) -> usize {
+ self.decisions
+ .get(0)
+ .map(|&len| len as usize)
+ .unwrap_or(self.trail.len())
+ + self.units_removed
+ }
+
+ /// Whether all assignments are processed.
+ pub fn fully_propagated(&self) -> bool {
+ self.queue_head_pos == self.trail.len()
+ }
+}
+
+/// Enqueues the assignment of true to a literal.
+///
+/// This updates the assignment and trail, but does not perform any propagation. The literal has to
+/// be unassigned when calling this.
+pub fn enqueue_assignment(
+ mut ctx: partial!(Context, mut AssignmentP, mut ImplGraphP, mut TrailP),
+ lit: Lit,
+ reason: Reason,
+) {
+ let assignment = ctx.part_mut(AssignmentP);
+ debug_assert!(assignment.lit_value(lit) == None);
+
+ assignment.assign_lit(lit);
+
+ let (trail, mut ctx) = ctx.split_part_mut(TrailP);
+
+ trail.trail.push(lit);
+
+ let node = &mut ctx.part_mut(ImplGraphP).nodes[lit.index()];
+ node.reason = reason;
+ node.level = trail.decisions.len() as LitIdx;
+ node.depth = trail.trail.len() as LitIdx;
+}
+
+/// Undo all assignments in decision levels deeper than the given level.
+pub fn backtrack(
+ mut ctx: partial!(Context, mut AssignmentP, mut TrailP, mut VsidsP),
+ level: usize,
+) {
+ let (assignment, mut ctx) = ctx.split_part_mut(AssignmentP);
+ let (trail, mut ctx) = ctx.split_part_mut(TrailP);
+
+ // level can actually be greater than the current level. This happens when restart is called
+ // after a conflict backtracked into the assumptions, but before any assumption was reenqueued.
+ // TODO should we update assumption_levels on backtracking instead of allowing this here?
+ if level >= trail.decisions.len() {
+ return;
+ }
+
+ let new_trail_len = trail.decisions[level] as usize;
+
+ trail.queue_head_pos = new_trail_len;
+ trail.decisions.truncate(level);
+
+ let trail_end = &trail.trail[new_trail_len..];
+ for &lit in trail_end {
+ make_available(ctx.borrow(), lit.var());
+ let var_assignment = &mut assignment.assignment[lit.index()];
+ assignment.last_value[lit.index()] = *var_assignment == Some(true);
+ *var_assignment = None;
+ }
+ trail.trail.truncate(new_trail_len);
+}
+
+/// Undo all decisions and assumptions.
+pub fn full_restart(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut TrailP,
+ mut VsidsP,
+ ),
+) {
+ ctx.part_mut(AssumptionsP).full_restart();
+ backtrack(ctx.borrow(), 0);
+}
+
+/// Undo all decisions.
+pub fn restart(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut TrailP,
+ mut VsidsP,
+ AssumptionsP
+ ),
+) {
+ let level = ctx.part(AssumptionsP).assumption_levels();
+ backtrack(ctx.borrow(), level);
+}
diff --git a/vendor/varisat/src/prop/binary.rs b/vendor/varisat/src/prop/binary.rs
new file mode 100644
index 000000000..d89347c8a
--- /dev/null
+++ b/vendor/varisat/src/prop/binary.rs
@@ -0,0 +1,36 @@
+//! Propagation of binary clauses.
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::context::{parts::*, Context};
+
+use super::{enqueue_assignment, Conflict, Reason};
+
+/// Propagate all literals implied by the given literal via binary clauses.
+///
+/// On conflict return the binary clause propgating the conflicting assignment.
+pub fn propagate_binary(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut ImplGraphP,
+ mut TrailP,
+ BinaryClausesP,
+ ),
+ lit: Lit,
+) -> Result<(), Conflict> {
+ let (binary_clauses, mut ctx) = ctx.split_part(BinaryClausesP);
+
+ for &implied in binary_clauses.implied(lit) {
+ let assignment = ctx.part(AssignmentP);
+
+ if assignment.lit_is_false(implied) {
+ return Err(Conflict::Binary([implied, !lit]));
+ } else if !assignment.lit_is_true(implied) {
+ enqueue_assignment(ctx.borrow(), implied, Reason::Binary([!lit]));
+ }
+ }
+
+ Ok(())
+}
diff --git a/vendor/varisat/src/prop/graph.rs b/vendor/varisat/src/prop/graph.rs
new file mode 100644
index 000000000..3a0e3a42d
--- /dev/null
+++ b/vendor/varisat/src/prop/graph.rs
@@ -0,0 +1,137 @@
+//! The implication graph.
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::{lit::LitIdx, Lit, Var};
+
+use crate::{
+ clause::ClauseRef,
+ context::{parts::*, Context},
+};
+
+/// Assignments that caused a propagation.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum Reason {
+ Unit,
+ Binary([Lit; 1]),
+ Long(ClauseRef),
+}
+
+impl Reason {
+ /// The literals that caused the propagation.
+ pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit]
+ where
+ 'a: 'out,
+ 'b: 'out,
+ {
+ match self {
+ Reason::Unit => &[],
+ Reason::Binary(lit) => lit,
+ // The propagated literal is always kept at position 0
+ Reason::Long(cref) => &ctx.part(ClauseAllocP).clause(*cref).lits()[1..],
+ }
+ }
+
+ /// True if a unit clause or assumption and not a propagation.
+ pub fn is_unit(&self) -> bool {
+ match self {
+ Reason::Unit => true,
+ _ => false,
+ }
+ }
+}
+
+/// Propagation that resulted in a conflict.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum Conflict {
+ Binary([Lit; 2]),
+ Long(ClauseRef),
+}
+
+impl Conflict {
+ /// The literals that caused the conflict.
+ pub fn lits<'out, 'a, 'b>(&'a self, ctx: &'b partial!('b Context, ClauseAllocP)) -> &'out [Lit]
+ where
+ 'a: 'out,
+ 'b: 'out,
+ {
+ match self {
+ Conflict::Binary(lits) => lits,
+ Conflict::Long(cref) => ctx.part(ClauseAllocP).clause(*cref).lits(),
+ }
+ }
+}
+
+/// Node and incoming edges of the implication graph.
+#[derive(Copy, Clone)]
+pub struct ImplNode {
+ pub reason: Reason,
+ pub level: LitIdx,
+ /// Position in trail when assigned, `LitIdx::max_value()` is used as sentinel for removed
+ /// units.
+ pub depth: LitIdx,
+}
+
+/// The implication graph.
+///
+/// This is a DAG having all assigned variables as nodes. It has unit clauses, assumptions and
+/// decisions as sources. For each propagated assignment it has incomming edges from the literals
+/// whose assignment caused the propagation to happen.
+#[derive(Default)]
+pub struct ImplGraph {
+ /// Contains only valid data for indices of assigned variables.
+ pub nodes: Vec<ImplNode>,
+}
+
+impl ImplGraph {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.nodes.resize(
+ count,
+ ImplNode {
+ reason: Reason::Unit,
+ level: 0,
+ depth: 0,
+ },
+ );
+ }
+
+ /// Get the reason for an assigned variable.
+ ///
+ /// Returns stale data if the variable isn't assigned.
+ pub fn reason(&self, var: Var) -> &Reason {
+ &self.nodes[var.index()].reason
+ }
+
+ /// Get the decision level of an assigned variable.
+ ///
+ /// Returns stale data if the variable isn't assigned.
+ pub fn level(&self, var: Var) -> usize {
+ self.nodes[var.index()].level as usize
+ }
+
+ /// Get the trail depth of an assigned variable.
+ ///
+ /// Returns stale data if the variable isn't assigned.
+ pub fn depth(&self, var: Var) -> usize {
+ self.nodes[var.index()].depth as usize
+ }
+
+ /// Updates the reason for an assigned variable.
+ ///
+ /// Make sure the reason vars are in front of the assigned variable in the trail.
+ pub fn update_reason(&mut self, var: Var, reason: Reason) {
+ self.nodes[var.index()].reason = reason
+ }
+
+ /// Updates the reason and depth of a unit clause removed from the trail.
+ pub fn update_removed_unit(&mut self, var: Var) {
+ let node = &mut self.nodes[var.index()];
+ node.reason = Reason::Unit;
+ node.depth = LitIdx::max_value();
+ }
+
+ pub fn is_removed_unit(&self, var: Var) -> bool {
+ self.nodes[var.index()].depth == LitIdx::max_value()
+ }
+}
diff --git a/vendor/varisat/src/prop/long.rs b/vendor/varisat/src/prop/long.rs
new file mode 100644
index 000000000..8fde47ec7
--- /dev/null
+++ b/vendor/varisat/src/prop/long.rs
@@ -0,0 +1,164 @@
+//! Propagation of long clauses.
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::context::{parts::*, Context};
+
+use super::{assignment::fast_option_eq, enqueue_assignment, Conflict, Reason, Watch};
+
+/// Propagate all literals implied by long clauses watched by the given literal.
+///
+/// On conflict return the clause propgating the conflicting assignment.
+///
+/// See [`prop::watch`](crate::prop::watch) for the invariants that this has to uphold.
+pub fn propagate_long(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut ImplGraphP,
+ mut TrailP,
+ mut WatchlistsP,
+ mut ClauseAllocP,
+ ),
+ lit: Lit,
+) -> Result<(), Conflict> {
+ // The code below is heavily optimized and replaces a much nicer but sadly slower version.
+ // Nevertheless it still performs full bound checks. Therefore this function is safe to call
+ // even when some other code violated invariants of for example the clause db.
+ unsafe {
+ let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP);
+ let (alloc, mut ctx) = ctx.split_part_mut(ClauseAllocP);
+
+ let watch_begin;
+ let watch_end;
+ {
+ let watch_list = &mut watchlists.watched_by_mut(lit);
+ watch_begin = watch_list.as_mut_ptr();
+ watch_end = watch_begin.add(watch_list.len());
+ }
+ let mut watch_ptr = watch_begin;
+
+ let false_lit = !lit;
+
+ let mut watch_write = watch_ptr;
+
+ let assignment_limit = ctx.part(AssignmentP).assignment().len();
+ let assignment_ptr = ctx.part(AssignmentP).assignment().as_ptr();
+
+ let is_true = |lit: Lit| {
+ assert!(lit.index() < assignment_limit);
+ fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_positive()))
+ };
+
+ let is_false = |lit: Lit| {
+ assert!(lit.index() < assignment_limit);
+ fast_option_eq(*assignment_ptr.add(lit.index()), Some(lit.is_negative()))
+ };
+
+ 'watchers: while watch_ptr != watch_end {
+ let watch = *watch_ptr;
+ watch_ptr = watch_ptr.add(1);
+
+ // If the blocking literal (which is part of the watched clause) is already true, the
+ // watched clause is satisfied and we don't even have to look at it.
+ if is_true(watch.blocking) {
+ *watch_write = watch;
+ watch_write = watch_write.add(1);
+ continue;
+ }
+
+ let cref = watch.cref;
+
+ // Make sure we can access at least 3 lits
+ alloc.check_bounds(cref, 3);
+
+ let clause_ptr = alloc.lits_ptr_mut_unchecked(cref);
+ let &mut header = alloc.header_unchecked_mut(cref);
+
+ // First we ensure that the literal we're currently propagating is at index 1. This
+ // prepares the literal order for further propagations, as the propagating literal has
+ // to be at index 0. Doing this here also avoids a similar check later should the clause
+ // be satisfied by a non-watched literal, as we can just move it to index 1.
+ let mut first = *clause_ptr.add(0);
+ if first == false_lit {
+ let c1 = *clause_ptr.add(1);
+ first = c1;
+ *clause_ptr.add(0) = c1;
+ *clause_ptr.add(1) = false_lit;
+ }
+
+ // We create a new watch with the other watched literal as blocking literal. This will
+ // either replace the currently processed watch or be added to another literals watch
+ // list.
+ let new_watch = Watch {
+ cref,
+ blocking: first,
+ };
+
+ // If the other watched literal (now the first) isn't the blocking literal, check
+ // whether that one is true. If so nothing else needs to be done.
+ if first != watch.blocking && is_true(first) {
+ *watch_write = new_watch;
+ watch_write = watch_write.add(1);
+ continue;
+ }
+
+ // At this point we try to find a non-false unwatched literal to replace our current
+ // literal as the watched literal.
+
+ let clause_len = header.len();
+ let mut lit_ptr = clause_ptr.add(2);
+ let lit_end = clause_ptr.add(clause_len);
+
+ // Make sure we can access all clause literals.
+ alloc.check_bounds(cref, clause_len);
+
+ while lit_ptr != lit_end {
+ let rest_lit = *lit_ptr;
+ if !is_false(rest_lit) {
+ // We found a non-false literal and make it a watched literal by reordering the
+ // literals and adding the watch to the corresponding watchlist.
+ *clause_ptr.offset(1) = rest_lit;
+ *lit_ptr = false_lit;
+
+ // We're currently using unsafe to modify the watchlist of lit, so make extra
+ // sure we're not aliasing.
+ assert_ne!(!rest_lit, lit);
+ watchlists.add_watch(!rest_lit, new_watch);
+ continue 'watchers;
+ }
+ lit_ptr = lit_ptr.add(1);
+ }
+
+ // We didn't find a non-false unwatched literal, so either we're propagating or we have
+ // a conflict.
+ *watch_write = new_watch;
+ watch_write = watch_write.add(1);
+
+ // If the other watched literal is false we have a conflict.
+ if is_false(first) {
+ // We move all unprocessed watches and resize the currentl watchlist.
+ while watch_ptr != watch_end {
+ *watch_write = *watch_ptr;
+ watch_write = watch_write.add(1);
+ watch_ptr = watch_ptr.add(1);
+ }
+ let out_size = ((watch_write as usize) - (watch_begin as usize))
+ / std::mem::size_of::<Watch>();
+
+ watchlists.watched_by_mut(lit).truncate(out_size as usize);
+
+ return Err(Conflict::Long(cref));
+ }
+
+ // Otherwise we enqueue a new propagation.
+ enqueue_assignment(ctx.borrow(), first, Reason::Long(cref));
+ }
+
+ let out_size =
+ ((watch_write as usize) - (watch_begin as usize)) / std::mem::size_of::<Watch>();
+ watchlists.watched_by_mut(lit).truncate(out_size as usize);
+ }
+ Ok(())
+}
diff --git a/vendor/varisat/src/prop/watch.rs b/vendor/varisat/src/prop/watch.rs
new file mode 100644
index 000000000..095ac86a9
--- /dev/null
+++ b/vendor/varisat/src/prop/watch.rs
@@ -0,0 +1,135 @@
+//! Watchlists to detect clauses that became unit.
+//!
+//! Each (long) clause has always two watches pointing to it. The watches are kept in the watchlists
+//! of two different literals of the clause. Whenever the watches are moved to different literals
+//! the litereals of the clause are permuted so the watched literals are in position 0 and 1.
+//!
+//! When a clause is not unit under the current assignment, the watched literals point at two
+//! non-false literals. When a clause is unit and thus propagating, the true literal is watched and
+//! in position 0, the other watched literal is the one with the largest decision level and kept in
+//! position 1. When a clause becomes satisfied before becoming unit the watches can be kept as they
+//! were.
+//!
+//! When a literal is assigned false that invariant can be invalidated. This can be detected by
+//! scanning the watches of the assigned literal. When the assignment is processed the watches are
+//! moved to restore that invariant. Unless there is a conflict, i.e. a clause with no non-false
+//! literals, this can always be done. This also finds all clauses that became unit. The new unit
+//! clauses are exactly those clauses where no two non-false literals can be found.
+//!
+//! There is no need to update watchlists on backtracking, as unassigning variables cannot
+//! invalidate the invariant.
+//!
+//! See [Section 4.5.1 of the "Handbook of Satisfiability"][handbook-ch4] for more details and
+//! references.
+//!
+//! As a further optimization we use blocking literals. This means that each watch stores a literal
+//! of the clause that is different from the watched literal. It can be the other watched literal or
+//! any unwatched literal. When that literal is true, the clause is already satisfied, meaning that
+//! no watches need to be updated. This can be detected by just looking at the watch, avoiding
+//! access of the clause database. This variant was introduced by [Niklas Sörensson and Niklas Eén
+//! in "MINISAT 2.1 and MINISAT++1.0 — SAT Race 2008 Editions"][minisat-2.1].
+//!
+//! [handbook-ch4]: https://www.satassociation.org/articles/FAIA185-0131.pdf
+//! [minisat-2.1]: https://www.cril.univ-artois.fr/SAT09/solvers/booklet.pdf
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::Lit;
+
+use crate::{
+ clause::{db, ClauseRef},
+ context::{parts::*, Context},
+};
+
+/// A watch on a long clause.
+#[derive(Copy, Clone)]
+pub struct Watch {
+ /// Clause which has the referring lit in position 0 or 1.
+ pub cref: ClauseRef,
+ /// A lit of the clause, different from the referring lit.
+ pub blocking: Lit,
+}
+
+/// Watchlists to detect clauses that became unit.
+pub struct Watchlists {
+ /// Contains only valid data for indices of assigned variables.
+ watches: Vec<Vec<Watch>>,
+ /// Whether watchlists are present
+ enabled: bool,
+}
+
+impl Default for Watchlists {
+ fn default() -> Watchlists {
+ Watchlists {
+ watches: vec![],
+ enabled: true,
+ }
+ }
+}
+
+impl Watchlists {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.watches.resize(count * 2, vec![]);
+ }
+
+ /// Start watching a clause.
+ ///
+ /// `lits` have to be the first two literals of the given clause.
+ pub fn watch_clause(&mut self, cref: ClauseRef, lits: [Lit; 2]) {
+ if !self.enabled {
+ return;
+ }
+
+ for i in 0..2 {
+ let watch = Watch {
+ cref,
+ blocking: lits[i ^ 1],
+ };
+ self.add_watch(!lits[i], watch);
+ }
+ }
+
+ /// Return watches for a given literal.
+ pub fn watched_by_mut(&mut self, lit: Lit) -> &mut Vec<Watch> {
+ &mut self.watches[lit.code()]
+ }
+
+ /// Make a literal watch a clause.
+ pub fn add_watch(&mut self, lit: Lit, watch: Watch) {
+ self.watches[lit.code()].push(watch)
+ }
+
+ /// Are watchlists enabled.
+ pub fn enabled(&self) -> bool {
+ self.enabled
+ }
+
+ /// Clear and disable watchlists.
+ ///
+ /// Actual clearing of the watchlists is done on re-enabling of the watchlists.
+ pub fn disable(&mut self) {
+ self.enabled = false;
+ }
+}
+
+/// Enable and rebuild watchlists.
+pub fn enable_watchlists(mut ctx: partial!(Context, mut WatchlistsP, ClauseAllocP, ClauseDbP)) {
+ let (watchlists, mut ctx) = ctx.split_part_mut(WatchlistsP);
+ if watchlists.enabled {
+ return;
+ }
+
+ for watchlist in watchlists.watches.iter_mut() {
+ watchlist.clear();
+ }
+
+ watchlists.enabled = true;
+
+ let (alloc, mut ctx) = ctx.split_part(ClauseAllocP);
+
+ for cref in db::clauses_iter(&ctx.borrow()) {
+ let lits = alloc.clause(cref).lits();
+ watchlists.watch_clause(cref, [lits[0], lits[1]]);
+ }
+}
diff --git a/vendor/varisat/src/schedule.rs b/vendor/varisat/src/schedule.rs
new file mode 100644
index 000000000..1e1b04e57
--- /dev/null
+++ b/vendor/varisat/src/schedule.rs
@@ -0,0 +1,101 @@
+//! Scheduling of processing and solving steps.
+//!
+//! The current implementation is temporary and will be replaced with something more flexible.
+use log::info;
+
+use partial_ref::{partial, PartialRef};
+
+use crate::{
+ cdcl::conflict_step,
+ clause::{
+ collect_garbage,
+ reduce::{reduce_locals, reduce_mids},
+ Tier,
+ },
+ context::{parts::*, Context},
+ prop::restart,
+ state::SatState,
+};
+
+mod luby;
+
+use luby::LubySequence;
+
+/// Scheduling of processing and solving steps.
+#[derive(Default)]
+pub struct Schedule {
+ conflicts: u64,
+ next_restart: u64,
+ restarts: u64,
+ luby: LubySequence,
+}
+
+/// Perform one step of the schedule.
+pub fn schedule_step<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut AssumptionsP,
+ mut BinaryClausesP,
+ mut ClauseActivityP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ImplGraphP,
+ mut ModelP,
+ mut ProofP<'a>,
+ mut ScheduleP,
+ mut SolverStateP,
+ mut TmpDataP,
+ mut TmpFlagsP,
+ mut TrailP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ SolverConfigP,
+ ),
+) -> bool {
+ let (schedule, mut ctx) = ctx.split_part_mut(ScheduleP);
+ let (config, mut ctx) = ctx.split_part(SolverConfigP);
+
+ if ctx.part(SolverStateP).sat_state != SatState::Unknown
+ || ctx.part(SolverStateP).solver_error.is_some()
+ {
+ false
+ } else {
+ if schedule.conflicts > 0 && schedule.conflicts % 5000 == 0 {
+ let db = ctx.part(ClauseDbP);
+ let units = ctx.part(TrailP).top_level_assignment_count();
+ info!(
+ "confl: {}k rest: {} vars: {} bin: {} irred: {} core: {} mid: {} local: {}",
+ schedule.conflicts / 1000,
+ schedule.restarts,
+ ctx.part(AssignmentP).assignment().len() - units,
+ ctx.part(BinaryClausesP).count(),
+ db.count_by_tier(Tier::Irred),
+ db.count_by_tier(Tier::Core),
+ db.count_by_tier(Tier::Mid),
+ db.count_by_tier(Tier::Local)
+ );
+ }
+
+ if schedule.next_restart == schedule.conflicts {
+ restart(ctx.borrow());
+ schedule.restarts += 1;
+ schedule.next_restart += config.luby_restart_interval_scale * schedule.luby.advance();
+ }
+
+ if schedule.conflicts % config.reduce_locals_interval == 0 {
+ reduce_locals(ctx.borrow());
+ }
+ if schedule.conflicts % config.reduce_mids_interval == 0 {
+ reduce_mids(ctx.borrow());
+ }
+
+ collect_garbage(ctx.borrow());
+
+ conflict_step(ctx.borrow());
+ schedule.conflicts += 1;
+ true
+ }
+}
diff --git a/vendor/varisat/src/schedule/luby.rs b/vendor/varisat/src/schedule/luby.rs
new file mode 100644
index 000000000..9b44f7646
--- /dev/null
+++ b/vendor/varisat/src/schedule/luby.rs
@@ -0,0 +1,52 @@
+//! The reluctant doubling Luby sequence.
+//!
+//! This sequence is [A182105](https://oeis.org/A182105).
+
+/// Infinite iterator yielding the Luby sequence.
+pub struct LubySequence {
+ u: u64,
+ v: u64,
+}
+
+impl Default for LubySequence {
+ fn default() -> LubySequence {
+ LubySequence { u: 1, v: 1 }
+ }
+}
+
+impl LubySequence {
+ /// Yields the next number of hte Luby sequence.
+ pub fn advance(&mut self) -> u64 {
+ let result = self.v;
+
+ // Method by Knuth 2012
+ if (self.u & self.u.wrapping_neg()) == self.v {
+ self.u += 1;
+ self.v = 1;
+ } else {
+ self.v <<= 1;
+ }
+
+ result
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ #[test]
+ fn luby_sequence() {
+ let mut luby = LubySequence::default();
+ let initial_terms: Vec<_> = std::iter::repeat_with(|| luby.advance()).take(64).collect();
+
+ assert_eq!(
+ initial_terms,
+ vec![
+ 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2,
+ 4, 8, 16, 1, 1, 2, 1, 1, 2, 4, 1, 1, 2, 1, 1, 2, 4, 8, 1, 1, 2, 1, 1, 2, 4, 1, 1,
+ 2, 1, 1, 2, 4, 8, 16, 32, 1,
+ ]
+ )
+ }
+}
diff --git a/vendor/varisat/src/solver.rs b/vendor/varisat/src/solver.rs
new file mode 100644
index 000000000..d347fafd2
--- /dev/null
+++ b/vendor/varisat/src/solver.rs
@@ -0,0 +1,512 @@
+//! Boolean satisfiability solver.
+use std::io;
+
+use partial_ref::{IntoPartialRef, IntoPartialRefMut, PartialRef};
+
+use anyhow::Error;
+use thiserror::Error;
+
+use varisat_checker::ProofProcessor;
+use varisat_dimacs::DimacsParser;
+use varisat_formula::{CnfFormula, ExtendFormula, Lit, Var};
+
+use crate::{
+ assumptions::set_assumptions,
+ config::SolverConfigUpdate,
+ context::{config_changed, parts::*, Context},
+ load::load_clause,
+ proof,
+ schedule::schedule_step,
+ state::SatState,
+ variables,
+};
+
+pub use crate::proof::ProofFormat;
+
+/// Possible errors while solving a formula.
+#[derive(Debug, Error)]
+#[non_exhaustive]
+pub enum SolverError {
+ #[error("The solver was interrupted")]
+ Interrupted,
+ #[error("Error in proof processor: {}", cause)]
+ ProofProcessorError {
+ #[source]
+ cause: Error,
+ },
+ #[error("Error writing proof file: {}", cause)]
+ ProofIoError {
+ #[source]
+ cause: io::Error,
+ },
+}
+
+impl SolverError {
+ /// Whether a Solver instance can be used after producing such an error.
+ pub fn is_recoverable(&self) -> bool {
+ match self {
+ SolverError::Interrupted => true,
+ _ => false,
+ }
+ }
+}
+
+/// A boolean satisfiability solver.
+#[derive(Default)]
+pub struct Solver<'a> {
+ ctx: Box<Context<'a>>,
+}
+
+impl<'a> Solver<'a> {
+ /// Create a new solver.
+ pub fn new() -> Solver<'a> {
+ Solver::default()
+ }
+
+ /// Change the solver configuration.
+ pub fn config(&mut self, config_update: &SolverConfigUpdate) -> Result<(), Error> {
+ config_update.apply(&mut self.ctx.solver_config)?;
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ config_changed(ctx.borrow(), config_update);
+ Ok(())
+ }
+
+ /// Add a formula to the solver.
+ pub fn add_formula(&mut self, formula: &CnfFormula) {
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ for clause in formula.iter() {
+ load_clause(ctx.borrow(), clause);
+ }
+ }
+
+ /// Reads and adds a formula in DIMACS CNF format.
+ ///
+ /// Using this avoids creating a temporary [`CnfFormula`].
+ pub fn add_dimacs_cnf(&mut self, input: impl io::Read) -> Result<(), Error> {
+ let parser = DimacsParser::parse_incremental(input, |parser| {
+ self.add_formula(&parser.take_formula());
+ Ok(())
+ })?;
+
+ log::info!(
+ "Parsed formula with {} variables and {} clauses",
+ parser.var_count(),
+ parser.clause_count()
+ );
+
+ Ok(())
+ }
+
+ /// Sets the "witness" sampling mode for a variable.
+ pub fn witness_var(&mut self, var: Var) {
+ // TODO add link to sampling mode section of the manual when written
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ let global = variables::global_from_user(ctx.borrow(), var, false);
+ variables::set_sampling_mode(ctx.borrow(), global, variables::data::SamplingMode::Witness);
+ }
+
+ /// Sets the "sample" sampling mode for a variable.
+ pub fn sample_var(&mut self, var: Var) {
+ // TODO add link to sampling mode section of the manual when written
+ // TODO add warning about constrainig variables that previously were witness variables
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ let global = variables::global_from_user(ctx.borrow(), var, false);
+ variables::set_sampling_mode(ctx.borrow(), global, variables::data::SamplingMode::Sample);
+ }
+
+ /// Hide a variable.
+ ///
+ /// Turns a free variable into an existentially quantified variable. If the passed `Var` is used
+ /// again after this call, it refers to a new variable not the previously hidden variable.
+ pub fn hide_var(&mut self, var: Var) {
+ // TODO add link to sampling mode section of the manual when written
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ let global = variables::global_from_user(ctx.borrow(), var, false);
+ variables::set_sampling_mode(ctx.borrow(), global, variables::data::SamplingMode::Hide);
+ }
+
+ /// Observe solver internal variables.
+ ///
+ /// This turns solver internal variables into witness variables. There is no guarantee that the
+ /// newly visible variables correspond to previously hidden variables.
+ ///
+ /// Returns a list of newly visible variables.
+ pub fn observe_internal_vars(&mut self) -> Vec<Var> {
+ // TODO add link to sampling mode section of the manual when written
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ variables::observe_internal_vars(ctx.borrow())
+ }
+
+ /// Check the satisfiability of the current formula.
+ pub fn solve(&mut self) -> Result<bool, SolverError> {
+ self.ctx.solver_state.solver_invoked = true;
+
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ assert!(
+ !ctx.part_mut(SolverStateP).state_is_invalid,
+ "solve() called after encountering an unrecoverable error"
+ );
+
+ while schedule_step(ctx.borrow()) {}
+
+ proof::solve_finished(ctx.borrow());
+
+ self.check_for_solver_error()?;
+
+ match self.ctx.solver_state.sat_state {
+ SatState::Unknown => Err(SolverError::Interrupted),
+ SatState::Sat => Ok(true),
+ SatState::Unsat | SatState::UnsatUnderAssumptions => Ok(false),
+ }
+ }
+
+ /// Check for asynchronously generated errors.
+ ///
+ /// To avoid threading errors out of deep call stacks, we have a solver_error field in the
+ /// SolverState. This function takes and returns that error if present.
+ fn check_for_solver_error(&mut self) -> Result<(), SolverError> {
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ let error = ctx.part_mut(SolverStateP).solver_error.take();
+
+ if let Some(error) = error {
+ if !error.is_recoverable() {
+ ctx.part_mut(SolverStateP).state_is_invalid = true;
+ }
+ Err(error)
+ } else {
+ Ok(())
+ }
+ }
+
+ /// Assume given literals for future calls to solve.
+ ///
+ /// This replaces the current set of assumed literals.
+ pub fn assume(&mut self, assumptions: &[Lit]) {
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ set_assumptions(ctx.borrow(), assumptions);
+ }
+
+ /// Set of literals that satisfy the formula.
+ pub fn model(&self) -> Option<Vec<Lit>> {
+ let ctx = self.ctx.into_partial_ref();
+ if ctx.part(SolverStateP).sat_state == SatState::Sat {
+ Some(
+ ctx.part(VariablesP)
+ .user_var_iter()
+ .flat_map(|user_var| {
+ let global_var = ctx
+ .part(VariablesP)
+ .global_from_user()
+ .get(user_var)
+ .expect("no existing global var for user var");
+ ctx.part(ModelP).assignment()[global_var.index()]
+ .map(|value| user_var.lit(value))
+ })
+ .collect(),
+ )
+ } else {
+ None
+ }
+ }
+
+ /// Subset of the assumptions that made the formula unsatisfiable.
+ ///
+ /// This is not guaranteed to be minimal and may just return all assumptions every time.
+ pub fn failed_core(&self) -> Option<&[Lit]> {
+ match self.ctx.solver_state.sat_state {
+ SatState::UnsatUnderAssumptions => Some(self.ctx.assumptions.user_failed_core()),
+ SatState::Unsat => Some(&[]),
+ SatState::Unknown | SatState::Sat => None,
+ }
+ }
+
+ /// Generate a proof of unsatisfiability during solving.
+ ///
+ /// This needs to be called before any clauses are added.
+ pub fn write_proof(&mut self, target: impl io::Write + 'a, format: ProofFormat) {
+ assert!(
+ self.ctx.solver_state.formula_is_empty,
+ "called after clauses were added"
+ );
+ self.ctx.proof.write_proof(target, format);
+ }
+
+ /// Stop generating a proof of unsatisfiability.
+ ///
+ /// This also flushes internal buffers and closes the target file.
+ pub fn close_proof(&mut self) -> Result<(), SolverError> {
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ proof::close_proof(ctx.borrow());
+ self.check_for_solver_error()
+ }
+
+ /// Generate and check a proof on the fly.
+ ///
+ /// This needs to be called before any clauses are added.
+ pub fn enable_self_checking(&mut self) {
+ assert!(
+ self.ctx.solver_state.formula_is_empty,
+ "called after clauses were added"
+ );
+ self.ctx.proof.begin_checking();
+ }
+
+ /// Generate a proof and process it using a [`ProofProcessor`].
+ ///
+ /// This implicitly enables self checking.
+ ///
+ /// This needs to be called before any clauses are added.
+ pub fn add_proof_processor(&mut self, processor: &'a mut dyn ProofProcessor) {
+ assert!(
+ self.ctx.solver_state.formula_is_empty,
+ "called after clauses were added"
+ );
+ self.ctx.proof.add_processor(processor);
+ }
+}
+
+impl<'a> Drop for Solver<'a> {
+ fn drop(&mut self) {
+ let _ = self.close_proof();
+ }
+}
+
+impl<'a> ExtendFormula for Solver<'a> {
+ /// Add a clause to the solver.
+ fn add_clause(&mut self, clause: &[Lit]) {
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ load_clause(ctx.borrow(), clause);
+ }
+
+ /// Add a new variable to the solver.
+ fn new_var(&mut self) -> Var {
+ self.ctx.solver_state.formula_is_empty = false;
+ let mut ctx = self.ctx.into_partial_ref_mut();
+ variables::new_user_var(ctx.borrow())
+ }
+}
+
+#[cfg(test)]
+mod tests {
+ use super::*;
+
+ use proptest::prelude::*;
+
+ use varisat_checker::{CheckedProofStep, CheckerData};
+ use varisat_formula::{
+ cnf_formula, lits,
+ test::{sat_formula, sgen_unsat_formula},
+ };
+
+ use varisat_dimacs::write_dimacs;
+
+ fn enable_test_schedule(solver: &mut Solver) {
+ let mut config = SolverConfigUpdate::new();
+ config.reduce_locals_interval = Some(150);
+ config.reduce_mids_interval = Some(100);
+
+ solver.config(&config).unwrap();
+ }
+
+ #[test]
+ #[should_panic(expected = "solve() called after encountering an unrecoverable error")]
+ fn error_handling_proof_writing() {
+ let mut output_buffer = [0u8; 4];
+ let mut solver = Solver::new();
+ let proof_output = std::io::Cursor::new(&mut output_buffer[..]);
+
+ solver.write_proof(proof_output, ProofFormat::Varisat);
+
+ solver.add_formula(&cnf_formula![
+ -1, -2, -3; -1, -2, -4; -1, -2, -5; -1, -3, -4; -1, -3, -5; -1, -4, -5; -2, -3, -4;
+ -2, -3, -5; -2, -4, -5; -3, -4, -5; 1, 2, 5; 1, 2, 3; 1, 2, 4; 1, 5, 3; 1, 5, 4;
+ 1, 3, 4; 2, 5, 3; 2, 5, 4; 2, 3, 4; 5, 3, 4;
+ ]);
+
+ let result = solver.solve();
+
+ assert!(match result {
+ Err(SolverError::ProofIoError { .. }) => true,
+ _ => false,
+ });
+
+ let _ = solver.solve();
+ }
+
+ struct FailingProcessor;
+
+ impl ProofProcessor for FailingProcessor {
+ fn process_step(
+ &mut self,
+ _step: &CheckedProofStep,
+ _data: CheckerData,
+ ) -> Result<(), Error> {
+ anyhow::bail!("failing processor");
+ }
+ }
+ #[test]
+ #[should_panic(expected = "solve() called after encountering an unrecoverable error")]
+ fn error_handling_proof_processing() {
+ let mut processor = FailingProcessor;
+
+ let mut solver = Solver::new();
+
+ solver.add_proof_processor(&mut processor);
+
+ solver.add_formula(&cnf_formula![
+ -1, -2, -3; -1, -2, -4; -1, -2, -5; -1, -3, -4; -1, -3, -5; -1, -4, -5; -2, -3, -4;
+ -2, -3, -5; -2, -4, -5; -3, -4, -5; 1, 2, 5; 1, 2, 3; 1, 2, 4; 1, 5, 3; 1, 5, 4;
+ 1, 3, 4; 2, 5, 3; 2, 5, 4; 2, 3, 4; 5, 3, 4;
+ ]);
+
+ let result = solver.solve();
+
+ assert!(match result {
+ Err(SolverError::ProofProcessorError { cause }) => {
+ format!("{}", cause) == "failing processor"
+ }
+ _ => false,
+ });
+
+ let _ = solver.solve();
+ }
+
+ #[test]
+ #[should_panic(expected = "called after clauses were added")]
+ fn write_proof_too_late() {
+ let mut solver = Solver::new();
+ solver.add_clause(&lits![1, 2, 3]);
+ solver.write_proof(std::io::sink(), ProofFormat::Varisat);
+ }
+
+ #[test]
+ #[should_panic(expected = "called after clauses were added")]
+ fn add_proof_processor_too_late() {
+ let mut processor = FailingProcessor;
+
+ let mut solver = Solver::new();
+ solver.add_clause(&lits![1, 2, 3]);
+
+ solver.add_proof_processor(&mut processor);
+ }
+
+ #[test]
+ #[should_panic(expected = "called after clauses were added")]
+ fn enable_self_checking_too_late() {
+ let mut solver = Solver::new();
+ solver.add_clause(&lits![1, 2, 3]);
+
+ solver.enable_self_checking();
+ }
+
+ #[test]
+ fn self_check_duplicated_unit_clauses() {
+ let mut solver = Solver::new();
+
+ solver.enable_self_checking();
+
+ solver.add_formula(&cnf_formula![
+ 4;
+ 4;
+ ]);
+
+ assert_eq!(solver.solve().ok(), Some(true));
+ }
+
+ proptest! {
+ #[test]
+ fn sgen_unsat(
+ formula in sgen_unsat_formula(1..7usize),
+ test_schedule in proptest::bool::ANY,
+ ) {
+ let mut solver = Solver::new();
+
+ solver.add_formula(&formula);
+
+ if test_schedule {
+ enable_test_schedule(&mut solver);
+ }
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+ }
+
+ #[test]
+ fn sgen_unsat_checked(
+ formula in sgen_unsat_formula(1..7usize),
+ test_schedule in proptest::bool::ANY,
+ ) {
+ let mut solver = Solver::new();
+
+ solver.enable_self_checking();
+
+ solver.add_formula(&formula);
+
+ if test_schedule {
+ enable_test_schedule(&mut solver);
+ }
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+ }
+
+ #[test]
+ fn sat(
+ formula in sat_formula(4..20usize, 10..100usize, 0.05..0.2, 0.9..1.0),
+ test_schedule in proptest::bool::ANY,
+ ) {
+ let mut solver = Solver::new();
+
+ solver.add_formula(&formula);
+
+ if test_schedule {
+ enable_test_schedule(&mut solver);
+ }
+
+ prop_assert_eq!(solver.solve().ok(), Some(true));
+
+ let model = solver.model().unwrap();
+
+ for clause in formula.iter() {
+ prop_assert!(clause.iter().any(|lit| model.contains(lit)));
+ }
+ }
+
+ #[test]
+ fn sat_via_dimacs(formula in sat_formula(4..20usize, 10..100usize, 0.05..0.2, 0.9..1.0)) {
+ let mut solver = Solver::new();
+
+ let mut dimacs = vec![];
+
+ write_dimacs(&mut dimacs, &formula).unwrap();
+
+ solver.add_dimacs_cnf(&mut &dimacs[..]).unwrap();
+
+ prop_assert_eq!(solver.solve().ok(), Some(true));
+
+ let model = solver.model().unwrap();
+
+ for clause in formula.iter() {
+ prop_assert!(clause.iter().any(|lit| model.contains(lit)));
+ }
+ }
+
+ #[test]
+ fn sgen_unsat_incremental_clauses(formula in sgen_unsat_formula(1..7usize)) {
+ let mut solver = Solver::new();
+
+ let mut last_state = Some(true);
+
+ for clause in formula.iter() {
+ solver.add_clause(clause);
+
+ let state = solver.solve().ok();
+ if state != last_state {
+ prop_assert_eq!(state, Some(false));
+ prop_assert_eq!(last_state, Some(true));
+ last_state = state;
+ }
+ }
+
+ prop_assert_eq!(last_state, Some(false));
+ }
+ }
+}
diff --git a/vendor/varisat/src/state.rs b/vendor/varisat/src/state.rs
new file mode 100644
index 000000000..4fb636e66
--- /dev/null
+++ b/vendor/varisat/src/state.rs
@@ -0,0 +1,42 @@
+//! Miscellaneous solver state.
+use crate::solver::SolverError;
+
+/// Satisfiability state.
+#[derive(Copy, Clone, Eq, PartialEq, Debug)]
+pub enum SatState {
+ Unknown,
+ Sat,
+ Unsat,
+ UnsatUnderAssumptions,
+}
+
+impl Default for SatState {
+ fn default() -> SatState {
+ SatState::Unknown
+ }
+}
+
+/// Miscellaneous solver state.
+///
+/// Anything larger or any larger group of related state variables should be moved into a separate
+/// part of [`Context`](crate::context::Context).
+pub struct SolverState {
+ pub sat_state: SatState,
+ pub formula_is_empty: bool,
+ /// Whether solve was called at least once.
+ pub solver_invoked: bool,
+ pub state_is_invalid: bool,
+ pub solver_error: Option<SolverError>,
+}
+
+impl Default for SolverState {
+ fn default() -> SolverState {
+ SolverState {
+ sat_state: SatState::Unknown,
+ formula_is_empty: true,
+ solver_invoked: false,
+ state_is_invalid: false,
+ solver_error: None,
+ }
+ }
+}
diff --git a/vendor/varisat/src/tmp.rs b/vendor/varisat/src/tmp.rs
new file mode 100644
index 000000000..a822d7fe8
--- /dev/null
+++ b/vendor/varisat/src/tmp.rs
@@ -0,0 +1,35 @@
+//! Temporary data.
+use varisat_formula::Lit;
+
+/// Temporary data used by various parts of the solver.
+///
+/// Make sure to check any documented invariants when using this. Also make sure to check all
+/// existing users when adding invariants.
+#[derive(Default)]
+pub struct TmpData {
+ pub lits: Vec<Lit>,
+ pub lits_2: Vec<Lit>,
+}
+
+/// Temporary data that is automatically resized.
+///
+/// This contains buffers that are automatically resized when the variable count of the solver
+/// changes. They are also always kept in a clean state, so using them doesn't come with costs
+/// proportional to the number of variables.
+///
+/// Make sure to check any documented invariants when using this. Also make sure to check all
+/// existing users when adding invariants.
+#[derive(Default)]
+pub struct TmpFlags {
+ /// A boolean for each literal.
+ ///
+ /// Reset to all-false, keep size.
+ pub flags: Vec<bool>,
+}
+
+impl TmpFlags {
+ /// Update structures for a new variable count.
+ pub fn set_var_count(&mut self, count: usize) {
+ self.flags.resize(count * 2, false);
+ }
+}
diff --git a/vendor/varisat/src/unit_simplify.rs b/vendor/varisat/src/unit_simplify.rs
new file mode 100644
index 000000000..d70130b58
--- /dev/null
+++ b/vendor/varisat/src/unit_simplify.rs
@@ -0,0 +1,198 @@
+//! Simplification using unit clauses.
+
+use partial_ref::{partial, split_borrow, PartialRef};
+
+use varisat_formula::{Lit, Var};
+use varisat_internal_proof::{clause_hash, lit_hash, DeleteClauseProof, ProofStep};
+
+use crate::{
+ binary::simplify_binary,
+ clause::db::filter_clauses,
+ context::{parts::*, Context},
+ proof,
+ prop::{enqueue_assignment, Reason},
+ variables,
+};
+
+/// Remove satisfied clauses and false literals.
+pub fn prove_units<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TrailP,
+ AssignmentP,
+ ClauseAllocP,
+ VariablesP,
+ ),
+) -> bool {
+ let mut new_unit = false;
+
+ if ctx.part(TrailP).current_level() == 0 {
+ let (impl_graph, mut ctx) = ctx.split_part_mut(ImplGraphP);
+
+ let mut unit_proofs = vec![];
+
+ let (trail, mut ctx) = ctx.split_part_mut(TrailP);
+
+ for &lit in trail.trail() {
+ new_unit = true;
+ let ctx_lits = ctx.borrow();
+ let reason = impl_graph.reason(lit.var());
+ if !reason.is_unit() {
+ let lits = impl_graph.reason(lit.var()).lits(&ctx_lits);
+ let hash = clause_hash(lits) ^ lit_hash(lit);
+
+ unit_proofs.push((lit, hash));
+ }
+
+ impl_graph.update_removed_unit(lit.var());
+ }
+
+ trail.clear();
+
+ if !unit_proofs.is_empty() {
+ proof::add_step(
+ ctx.borrow(),
+ true,
+ &ProofStep::UnitClauses {
+ units: &unit_proofs,
+ },
+ );
+ }
+ }
+
+ new_unit
+}
+
+/// Put a removed unit back onto the trail.
+pub fn resurrect_unit<'a>(
+ mut ctx: partial!(Context<'a>, mut AssignmentP, mut ImplGraphP, mut TrailP),
+ lit: Lit,
+) {
+ if ctx.part(ImplGraphP).is_removed_unit(lit.var()) {
+ debug_assert!(ctx.part(AssignmentP).lit_is_true(lit));
+ ctx.part_mut(AssignmentP).unassign_var(lit.var());
+
+ // Because we always enqueue with Reason::Unit this will not cause a unit clause to be
+ // proven in `prove_units`.
+ enqueue_assignment(ctx.borrow(), lit, Reason::Unit);
+ }
+}
+
+/// Remove satisfied clauses and false literals.
+pub fn unit_simplify<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AssignmentP,
+ mut BinaryClausesP,
+ mut ClauseAllocP,
+ mut ClauseDbP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut VariablesP,
+ mut WatchlistsP,
+ mut VsidsP,
+ AssumptionsP,
+ ),
+) {
+ simplify_binary(ctx.borrow());
+
+ let (assignment, mut ctx) = ctx.split_part(AssignmentP);
+
+ let mut new_lits = vec![];
+ {
+ split_borrow!(proof_ctx = &(mut ProofP, mut SolverStateP, VariablesP) ctx);
+ let (ctx_2, mut ctx) = ctx.split_borrow();
+
+ filter_clauses(ctx_2, |alloc, cref| {
+ let clause = alloc.clause_mut(cref);
+ let redundant = clause.header().redundant();
+ new_lits.clear();
+ for &lit in clause.lits() {
+ match assignment.lit_value(lit) {
+ None => new_lits.push(lit),
+ Some(true) => {
+ proof::add_step(
+ proof_ctx.borrow(),
+ true,
+ &ProofStep::DeleteClause {
+ clause: clause.lits(),
+ proof: if redundant {
+ DeleteClauseProof::Redundant
+ } else {
+ DeleteClauseProof::Satisfied
+ },
+ },
+ );
+ return false;
+ }
+ Some(false) => (),
+ }
+ }
+ if new_lits.len() < clause.lits().len() {
+ if proof_ctx.part(ProofP).is_active() {
+ let hash = [clause_hash(clause.lits())];
+ proof::add_step(
+ proof_ctx.borrow(),
+ true,
+ &ProofStep::AtClause {
+ redundant: redundant && new_lits.len() > 2,
+ clause: &new_lits,
+ propagation_hashes: &hash[..],
+ },
+ );
+ proof::add_step(
+ proof_ctx.borrow(),
+ true,
+ &ProofStep::DeleteClause {
+ clause: clause.lits(),
+ proof: if redundant {
+ DeleteClauseProof::Redundant
+ } else {
+ DeleteClauseProof::Simplified
+ },
+ },
+ );
+ }
+
+ match new_lits[..] {
+ // Cannot have empty or unit clauses after full propagation. An empty clause would
+ // have been a conflict and a unit clause must be satisfied and thus would have been
+ // dropped above.
+ [] | [_] => unreachable!(),
+ [lit_0, lit_1] => {
+ ctx.part_mut(BinaryClausesP)
+ .add_binary_clause([lit_0, lit_1]);
+ false
+ }
+ ref lits => {
+ clause.lits_mut()[..lits.len()].copy_from_slice(lits);
+ clause.header_mut().set_len(lits.len());
+ true
+ }
+ }
+ } else {
+ true
+ }
+ });
+ }
+
+ // TODO detect vars that became isolated without being having a unit clause
+
+ for (var_index, &value) in assignment.assignment().iter().enumerate() {
+ let var = Var::from_index(var_index);
+ if !ctx.part(VariablesP).solver_var_present(var) {
+ continue;
+ }
+ let var_data = ctx.part_mut(VariablesP).var_data_solver_mut(var);
+ if let Some(value) = value {
+ var_data.unit = Some(value);
+ var_data.isolated = true;
+ }
+ if var_data.isolated && !var_data.assumed {
+ variables::remove_solver_var(ctx.borrow(), var);
+ }
+ }
+}
diff --git a/vendor/varisat/src/variables.rs b/vendor/varisat/src/variables.rs
new file mode 100644
index 000000000..ec997430e
--- /dev/null
+++ b/vendor/varisat/src/variables.rs
@@ -0,0 +1,669 @@
+//! Variable mapping and metadata.
+
+use rustc_hash::FxHashSet as HashSet;
+
+use partial_ref::{partial, PartialRef};
+
+use varisat_formula::{Lit, Var};
+use varisat_internal_proof::ProofStep;
+
+use crate::{
+ context::{parts::*, set_var_count, Context},
+ decision, proof,
+};
+
+pub mod data;
+pub mod var_map;
+
+use data::{SamplingMode, VarData};
+use var_map::{VarBiMap, VarBiMapMut, VarMap};
+
+/// Variable mapping and metadata.
+pub struct Variables {
+ /// Bidirectional mapping from user variables to global variables.
+ ///
+ /// Initially this is the identity mapping. This ensures that in the non-assumptions setting the
+ /// map from used user variables to global variables is the identity. This is a requirement for
+ /// generating proofs in non-native formats. Those proofs are not aware of variable renaming,
+ /// but are restricted to the non-incremental setting, so this works out.
+ ///
+ /// This is also requried for native proofs, as they assume that the mapping during the initial
+ /// load is the identity.
+ global_from_user: VarBiMap,
+ /// Bidirectional mapping from global variables to user variables.
+ ///
+ /// This starts with the empty mapping, so only used variables are allocated.
+ solver_from_global: VarBiMap,
+ /// User variables that were explicitly hidden by the user.
+ user_freelist: HashSet<Var>,
+ /// Global variables that can be recycled without increasing the global_watermark.
+ global_freelist: HashSet<Var>,
+ /// Solver variables that are unused and can be recycled.
+ solver_freelist: HashSet<Var>,
+
+ /// Variable metadata.
+ ///
+ /// Indexed by global variable indices.
+ var_data: Vec<VarData>,
+}
+
+impl Default for Variables {
+ fn default() -> Variables {
+ Variables {
+ global_from_user: VarBiMap::default(),
+ solver_from_global: VarBiMap::default(),
+ user_freelist: Default::default(),
+ global_freelist: Default::default(),
+ solver_freelist: Default::default(),
+
+ var_data: vec![],
+ }
+ }
+}
+
+impl Variables {
+ /// Number of allocated solver variables.
+ pub fn solver_watermark(&self) -> usize {
+ self.global_from_solver().watermark()
+ }
+
+ /// Number of allocated global variables.
+ pub fn global_watermark(&self) -> usize {
+ self.var_data.len()
+ }
+
+ /// Number of allocated global variables.
+ pub fn user_watermark(&self) -> usize {
+ self.global_from_user().watermark()
+ }
+
+ /// Iterator over all user variables that are in use.
+ pub fn user_var_iter<'a>(&'a self) -> impl Iterator<Item = Var> + 'a {
+ let global_from_user = self.global_from_user.fwd();
+ (0..self.global_from_user().watermark())
+ .map(Var::from_index)
+ .filter(move |&user_var| global_from_user.get(user_var).is_some())
+ }
+
+ /// Iterator over all global variables that are in use.
+ pub fn global_var_iter<'a>(&'a self) -> impl Iterator<Item = Var> + 'a {
+ (0..self.global_watermark())
+ .map(Var::from_index)
+ .filter(move |&global_var| !self.var_data[global_var.index()].deleted)
+ }
+
+ /// The user to global mapping.
+ pub fn global_from_user(&self) -> &VarMap {
+ &self.global_from_user.fwd()
+ }
+
+ /// Mutable user to global mapping.
+ pub fn global_from_user_mut(&mut self) -> VarBiMapMut {
+ self.global_from_user.fwd_mut()
+ }
+
+ /// The global to solver mapping.
+ pub fn solver_from_global(&self) -> &VarMap {
+ &self.solver_from_global.fwd()
+ }
+
+ /// Mutable global to solver mapping.
+ pub fn solver_from_global_mut(&mut self) -> VarBiMapMut {
+ self.solver_from_global.fwd_mut()
+ }
+
+ /// The global to user mapping.
+ pub fn user_from_global(&self) -> &VarMap {
+ &self.global_from_user.bwd()
+ }
+
+ /// Mutable global to user mapping.
+ pub fn user_from_global_mut(&mut self) -> VarBiMapMut {
+ self.global_from_user.bwd_mut()
+ }
+
+ /// The solver to global mapping.
+ pub fn global_from_solver(&self) -> &VarMap {
+ &self.solver_from_global.bwd()
+ }
+
+ /// Mutable solver to global mapping.
+ pub fn global_from_solver_mut(&mut self) -> VarBiMapMut {
+ self.solver_from_global.bwd_mut()
+ }
+
+ /// Get an existing solver var for a user var.
+ pub fn existing_solver_from_user(&self, user: Var) -> Var {
+ let global = self
+ .global_from_user()
+ .get(user)
+ .expect("no existing global var for user var");
+ let solver = self
+ .solver_from_global()
+ .get(global)
+ .expect("no existing solver var for global var");
+ solver
+ }
+
+ /// Get an existing user var from a solver var.
+ pub fn existing_user_from_solver(&self, solver: Var) -> Var {
+ let global = self
+ .global_from_solver()
+ .get(solver)
+ .expect("no existing global var for solver var");
+ let user = self
+ .user_from_global()
+ .get(global)
+ .expect("no existing user var for global var");
+ user
+ }
+
+ /// Mutable reference to the var data for a global variable.
+ pub fn var_data_global_mut(&mut self, global: Var) -> &mut VarData {
+ if self.var_data.len() <= global.index() {
+ self.var_data.resize(global.index() + 1, VarData::default());
+ }
+ &mut self.var_data[global.index()]
+ }
+
+ /// Mutable reference to the var data for a solver variable.
+ pub fn var_data_solver_mut(&mut self, solver: Var) -> &mut VarData {
+ let global = self
+ .global_from_solver()
+ .get(solver)
+ .expect("no existing global var for solver var");
+ &mut self.var_data[global.index()]
+ }
+
+ /// Var data for a global variable.
+ pub fn var_data_global(&self, global: Var) -> &VarData {
+ &self.var_data[global.index()]
+ }
+
+ /// Check if a solver var is mapped to a global var
+ pub fn solver_var_present(&self, solver: Var) -> bool {
+ self.global_from_solver().get(solver).is_some()
+ }
+
+ /// Get an unmapped global variable.
+ pub fn next_unmapped_global(&self) -> Var {
+ self.global_freelist
+ .iter()
+ .next()
+ .cloned()
+ .unwrap_or_else(|| Var::from_index(self.global_watermark()))
+ }
+
+ /// Get an unmapped global variable.
+ pub fn next_unmapped_solver(&self) -> Var {
+ self.solver_freelist
+ .iter()
+ .next()
+ .cloned()
+ .unwrap_or_else(|| Var::from_index(self.solver_watermark()))
+ }
+
+ /// Get an unmapped user variable.
+ pub fn next_unmapped_user(&self) -> Var {
+ self.user_freelist
+ .iter()
+ .next()
+ .cloned()
+ .unwrap_or_else(|| Var::from_index(self.user_watermark()))
+ }
+}
+
+/// Maps a user variable into a global variable.
+///
+/// If no matching global variable exists a new global variable is allocated.
+pub fn global_from_user<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, mut VariablesP),
+ user: Var,
+ require_sampling: bool,
+) -> Var {
+ let variables = ctx.part_mut(VariablesP);
+
+ if user.index() > variables.user_watermark() {
+ // TODO use a batch proof step for this?
+ for index in variables.user_watermark()..user.index() {
+ global_from_user(ctx.borrow(), Var::from_index(index), false);
+ }
+ }
+
+ let variables = ctx.part_mut(VariablesP);
+
+ match variables.global_from_user().get(user) {
+ Some(global) => {
+ if require_sampling
+ && variables.var_data[global.index()].sampling_mode != SamplingMode::Sample
+ {
+ panic!("witness variables cannot be constrained");
+ }
+ global
+ }
+ None => {
+ // Can we add an identity mapping?
+ let global = match variables.var_data.get(user.index()) {
+ Some(var_data) if var_data.deleted => user,
+ None => user,
+ _ => variables.next_unmapped_global(),
+ };
+
+ *variables.var_data_global_mut(global) = VarData::user_default();
+
+ variables.global_from_user_mut().insert(global, user);
+ variables.global_freelist.remove(&global);
+ variables.user_freelist.remove(&user);
+
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::UserVarName {
+ global,
+ user: Some(user),
+ },
+ );
+
+ global
+ }
+ }
+}
+
+/// Maps an existing global variable to a solver variable.
+///
+/// If no matching solver variable exists a new one is allocated.
+pub fn solver_from_global<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut BinaryClausesP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+ global: Var,
+) -> Var {
+ let variables = ctx.part_mut(VariablesP);
+
+ debug_assert!(!variables.var_data[global.index()].deleted);
+
+ match variables.solver_from_global().get(global) {
+ Some(solver) => solver,
+ None => {
+ let solver = variables.next_unmapped_solver();
+
+ let old_watermark = variables.global_from_solver().watermark();
+
+ variables.solver_from_global_mut().insert(solver, global);
+ variables.solver_freelist.remove(&solver);
+
+ let new_watermark = variables.global_from_solver().watermark();
+
+ if new_watermark > old_watermark {
+ set_var_count(ctx.borrow(), new_watermark);
+ }
+
+ initialize_solver_var(ctx.borrow(), solver, global);
+
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::SolverVarName {
+ global,
+ solver: Some(solver),
+ },
+ );
+
+ solver
+ }
+ }
+}
+
+/// Maps a user variable to a solver variable.
+///
+/// Allocates global and solver variables as requried.
+pub fn solver_from_user<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut BinaryClausesP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+ user: Var,
+ require_sampling: bool,
+) -> Var {
+ let global = global_from_user(ctx.borrow(), user, require_sampling);
+ solver_from_global(ctx.borrow(), global)
+}
+
+/// Allocates a currently unused user variable.
+///
+/// This is either a user variable above any user variable used so far, or a user variable that was
+/// previously hidden by the user.
+pub fn new_user_var<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, mut VariablesP),
+) -> Var {
+ let variables = ctx.part_mut(VariablesP);
+ let user_var = variables.next_unmapped_user();
+ global_from_user(ctx.borrow(), user_var, false);
+ user_var
+}
+
+/// Maps a slice of user lits to solver lits using [`solver_from_user`].
+pub fn solver_from_user_lits<'a>(
+ mut ctx: partial!(
+ Context<'a>,
+ mut AnalyzeConflictP,
+ mut AssignmentP,
+ mut BinaryClausesP,
+ mut ImplGraphP,
+ mut ProofP<'a>,
+ mut SolverStateP,
+ mut TmpFlagsP,
+ mut VariablesP,
+ mut VsidsP,
+ mut WatchlistsP,
+ ),
+ solver_lits: &mut Vec<Lit>,
+ user_lits: &[Lit],
+ require_sampling: bool,
+) {
+ solver_lits.clear();
+ solver_lits.extend(user_lits.iter().map(|user_lit| {
+ user_lit.map_var(|user_var| solver_from_user(ctx.borrow(), user_var, require_sampling))
+ }))
+}
+
+/// Changes the sampling mode of a global variable.
+///
+/// If the mode is changed to hidden, an existing user mapping is automatically removed.
+///
+/// If the mode is changed from hidden, a new user mapping is allocated and the user variable is
+/// returned.
+pub fn set_sampling_mode<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, mut VariablesP),
+ global: Var,
+ mode: SamplingMode,
+) -> Option<Var> {
+ let variables = ctx.part_mut(VariablesP);
+
+ let var_data = &mut variables.var_data[global.index()];
+
+ assert!(!var_data.deleted);
+
+ if var_data.assumed {
+ panic!("cannot change sampling mode of assumption variable")
+ }
+
+ let previous_mode = var_data.sampling_mode;
+
+ if previous_mode == mode {
+ return None;
+ }
+
+ var_data.sampling_mode = mode;
+
+ let mut result = None;
+
+ if mode != SamplingMode::Hide {
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::ChangeSamplingMode {
+ var: global,
+ sample: mode == SamplingMode::Sample,
+ },
+ );
+ }
+ let variables = ctx.part_mut(VariablesP);
+
+ if previous_mode == SamplingMode::Hide {
+ let user = variables.next_unmapped_user();
+ variables.user_from_global_mut().insert(user, global);
+ variables.user_freelist.remove(&user);
+
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::UserVarName {
+ global,
+ user: Some(user),
+ },
+ );
+
+ result = Some(user);
+ } else if mode == SamplingMode::Hide {
+ if let Some(user) = variables.user_from_global_mut().remove(global) {
+ variables.user_freelist.insert(user);
+ }
+
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::UserVarName { global, user: None },
+ );
+
+ delete_global_if_unused(ctx.borrow(), global);
+ }
+
+ result
+}
+
+/// Turns all hidden vars into witness vars and returns them.
+pub fn observe_internal_vars<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, mut VariablesP),
+) -> Vec<Var> {
+ let mut result = vec![];
+ let mut variables = ctx.part_mut(VariablesP);
+ for global_index in 0..variables.global_watermark() {
+ let global = Var::from_index(global_index);
+ let var_data = &variables.var_data[global.index()];
+ if !var_data.deleted && var_data.sampling_mode == SamplingMode::Hide {
+ let user = set_sampling_mode(ctx.borrow(), global, SamplingMode::Witness).unwrap();
+ result.push(user);
+ variables = ctx.part_mut(VariablesP);
+ }
+ }
+ result
+}
+
+/// Initialize a newly allocated solver variable
+pub fn initialize_solver_var(
+ mut ctx: partial!(
+ Context,
+ mut AssignmentP,
+ mut ImplGraphP,
+ mut VsidsP,
+ VariablesP
+ ),
+ solver: Var,
+ global: Var,
+) {
+ let (variables, mut ctx) = ctx.split_part(VariablesP);
+ let data = &variables.var_data[global.index()];
+
+ // This recovers the state of a variable that has a known value and was already propagated. This
+ // is important so that when new clauses containing this variable are added, load_clause knows
+ // to reenqueue the assignment.
+ ctx.part_mut(AssignmentP).set_var(solver, data.unit);
+ if data.unit.is_some() {
+ ctx.part_mut(ImplGraphP).update_removed_unit(solver);
+ }
+ decision::initialize_var(ctx.borrow(), solver, data.unit.is_none());
+
+ // TODO unhiding beyond unit clauses
+}
+
+/// Remove a solver var.
+///
+/// If the variable is isolated and hidden, the global variable is also removed.
+pub fn remove_solver_var<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, mut VariablesP, mut VsidsP),
+ solver: Var,
+) {
+ decision::remove_var(ctx.borrow(), solver);
+
+ let variables = ctx.part_mut(VariablesP);
+
+ let global = variables
+ .global_from_solver_mut()
+ .remove(solver)
+ .expect("no existing global var for solver var");
+
+ variables.solver_freelist.insert(solver);
+
+ proof::add_step(
+ ctx.borrow(),
+ false,
+ &ProofStep::SolverVarName {
+ global,
+ solver: None,
+ },
+ );
+
+ delete_global_if_unused(ctx.borrow(), global);
+}
+
+/// Delete a global variable if it is unused
+fn delete_global_if_unused<'a>(
+ mut ctx: partial!(Context<'a>, mut ProofP<'a>, mut SolverStateP, mut VariablesP),
+ global: Var,
+) {
+ let variables = ctx.part_mut(VariablesP);
+
+ if variables.user_from_global().get(global).is_some() {
+ return;
+ }
+
+ if variables.solver_from_global().get(global).is_some() {
+ return;
+ }
+
+ let data = &mut variables.var_data[global.index()];
+
+ assert!(data.sampling_mode == SamplingMode::Hide);
+
+ if !data.isolated {
+ return;
+ }
+
+ data.deleted = true;
+
+ proof::add_step(ctx.borrow(), false, &ProofStep::DeleteVar { var: global });
+
+ // TODO deletion of unit clauses isn't supported by most DRAT checkers, needs an extra
+ // variable mapping instead.
+
+ ctx.part_mut(VariablesP).global_freelist.insert(global);
+}
+
+#[cfg(test)]
+mod tests {
+ use proptest::{collection, prelude::*};
+
+ use varisat_formula::{
+ test::{sat_formula, sgen_unsat_formula},
+ ExtendFormula, Var,
+ };
+
+ use crate::solver::Solver;
+
+ #[test]
+ #[should_panic(expected = "cannot change sampling mode of assumption variable")]
+ fn cannot_hide_assumed_vars() {
+ let mut solver = Solver::new();
+
+ let (x, y, z) = solver.new_lits();
+
+ solver.assume(&[x, y, z]);
+ solver.hide_var(x.var());
+ }
+
+ #[test]
+ #[should_panic(expected = "cannot change sampling mode of assumption variable")]
+ fn cannot_witness_assumed_vars() {
+ let mut solver = Solver::new();
+
+ let (x, y, z) = solver.new_lits();
+
+ solver.assume(&[x, y, z]);
+ solver.witness_var(x.var());
+ }
+
+ proptest! {
+ #[test]
+ fn sgen_unsat_hidden_with_sat(
+ unsat_formula in sgen_unsat_formula(1..7usize),
+ sat_formula in sat_formula(4..20usize, 10..100usize, 0.05..0.2, 0.9..1.0),
+ ) {
+ use std::cmp::max;
+
+ let mut solver = Solver::new();
+
+ solver.enable_self_checking();
+
+ let cond = Var::from_index(max(unsat_formula.var_count(), sat_formula.var_count()));
+
+ let mut tmp = vec![];
+
+ for clause in unsat_formula.iter() {
+ tmp.clear();
+ tmp.extend_from_slice(&clause);
+ tmp.push(cond.negative());
+ solver.add_clause(&tmp);
+ }
+
+ for i in 0..unsat_formula.var_count() {
+ solver.hide_var(Var::from_index(i));
+ }
+
+ solver.add_formula(&sat_formula);
+
+ prop_assert_eq!(solver.solve().ok(), Some(true));
+
+ solver.add_clause(&[cond.positive()]);
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+ }
+
+ #[test]
+ fn sgen_sat_many_hidden_observe_internal(
+ sat_formulas in collection::vec(
+ sat_formula(4..20usize, 10..100usize, 0.05..0.2, 0.9..1.0),
+ 1..10,
+ )
+ ) {
+ let mut solver = Solver::new();
+
+ solver.enable_self_checking();
+
+ for formula in sat_formulas {
+ solver.add_formula(&formula);
+
+ let new_vars = solver.observe_internal_vars();
+
+ for i in 0..formula.var_count() {
+ solver.hide_var(Var::from_index(i));
+ }
+
+ for var in new_vars {
+ solver.hide_var(var);
+ }
+ }
+
+ prop_assert_eq!(solver.solve().ok(), Some(true));
+ }
+ }
+}
diff --git a/vendor/varisat/src/variables/data.rs b/vendor/varisat/src/variables/data.rs
new file mode 100644
index 000000000..ea29e6280
--- /dev/null
+++ b/vendor/varisat/src/variables/data.rs
@@ -0,0 +1,70 @@
+//! Data associated with variables.
+
+/// Variable sampling mode.
+///
+/// This partitions all variables into three sets. Using these partitions it is possible to specify
+/// equivalence vs. equisatisfiability per variable. Let V be the set of all variables, S, W and H
+/// the sets of Sampling, Witness and Hidden variables. Let F be the input formula and G be the
+/// current formula. The following invariants are upheld:
+///
+/// * The formulas are always equisatisfiable:
+/// (∃ V) G ⇔ (∃ V) F
+/// * Restricted to the sampling variables they are equivalent:
+/// (∀ S) ((∃ V∖S) G ⇔ (∃ V∖S) F)
+/// * Restricted to the non-hidden variables the input formula is implied:
+/// (∀ V∖H) ((∃ H) G ⇒ (∃ H) F)
+///
+/// This ensures that the solver will be able to find and extend each satisfiable assignment of the
+/// sampling variables to an assignment that covers the witness variables.
+
+#[derive(Copy, Clone, PartialEq, Eq, Debug)]
+pub enum SamplingMode {
+ Sample,
+ Witness,
+ Hide,
+}
+
+/// Data associated with variables.
+///
+/// This is available for each _global_ variable, even if eliminated within the solver.
+#[derive(Clone)]
+pub struct VarData {
+ /// The variable's sampling mode.
+ pub sampling_mode: SamplingMode,
+ /// Whether the variable is forced by a unit clause.
+ ///
+ /// This is used to remember unit clauses after they are removed from the solver.
+ pub unit: Option<bool>,
+ /// True if there are no clauses containing this variable and other variables.
+ ///
+ /// This is the case if there are no clauses containing this variable or just a unit clause with
+ /// this variable.
+ pub isolated: bool,
+ /// True if this variable is part of the current assumptions.
+ pub assumed: bool,
+ /// Whether the global variable was deleted.
+ pub deleted: bool,
+}
+
+impl Default for VarData {
+ fn default() -> VarData {
+ VarData {
+ sampling_mode: SamplingMode::Hide,
+ unit: None,
+ isolated: true,
+ assumed: false,
+ deleted: true,
+ }
+ }
+}
+
+impl VarData {
+ /// Default variable data for a new user variable.
+ pub fn user_default() -> VarData {
+ VarData {
+ sampling_mode: SamplingMode::Sample,
+ deleted: false,
+ ..VarData::default()
+ }
+ }
+}
diff --git a/vendor/varisat/src/variables/var_map.rs b/vendor/varisat/src/variables/var_map.rs
new file mode 100644
index 000000000..730a6bf52
--- /dev/null
+++ b/vendor/varisat/src/variables/var_map.rs
@@ -0,0 +1,124 @@
+//! Mappings between variable names
+
+use varisat_formula::{lit::LitIdx, Var};
+
+const NO_VAR_IDX: LitIdx = Var::max_count() as LitIdx;
+
+/// A mapping from variables to variables.
+#[derive(Default)]
+pub struct VarMap {
+ mapping: Vec<LitIdx>,
+}
+
+impl VarMap {
+ /// Look up a variable in the mapping
+ pub fn get(&self, from: Var) -> Option<Var> {
+ match self.mapping.get(from.index()).cloned() {
+ Some(index) if index == NO_VAR_IDX => None,
+ Some(index) => Some(Var::from_index(index as usize)),
+ None => None,
+ }
+ }
+
+ /// Insert a new mapping.
+ ///
+ /// Note that the parameters are reversed from the usual order, to match the naming convention
+ /// used for maps.
+ ///
+ /// This has the precondition that `from` is not mapped.
+ pub fn insert(&mut self, into: Var, from: Var) {
+ if self.mapping.len() <= from.index() {
+ self.mapping.resize(from.index() + 1, NO_VAR_IDX);
+ }
+ debug_assert_eq!(self.mapping[from.index()], NO_VAR_IDX);
+ self.mapping[from.index()] = into.index() as LitIdx;
+ }
+
+ /// Remove a mapping.
+ ///
+ /// Does nothing if `from` is not mapped.
+ pub fn remove(&mut self, from: Var) {
+ if self.mapping.len() > from.index() {
+ self.mapping[from.index()] = NO_VAR_IDX;
+ }
+ }
+
+ /// One above the largest index that is mapped.
+ pub fn watermark(&self) -> usize {
+ self.mapping.len()
+ }
+}
+
+/// A bidirectional mapping between variables.
+///
+/// This is initialized with the identity mapping over all variables. It is possible to remove
+/// variables from this mapping on both sides.
+#[derive(Default)]
+pub struct VarBiMap {
+ fwd: VarMap,
+ bwd: VarMap,
+}
+
+impl VarBiMap {
+ /// Access the forward mapping.
+ pub fn fwd(&self) -> &VarMap {
+ &self.fwd
+ }
+
+ /// Access the backward mapping.
+ pub fn bwd(&self) -> &VarMap {
+ &self.bwd
+ }
+
+ /// Mutate the mapping in forward direction.
+ pub fn fwd_mut(&mut self) -> VarBiMapMut {
+ VarBiMapMut {
+ fwd: &mut self.fwd,
+ bwd: &mut self.bwd,
+ }
+ }
+
+ /// Mutate the mapping in backward direction.
+ pub fn bwd_mut(&mut self) -> VarBiMapMut {
+ VarBiMapMut {
+ fwd: &mut self.bwd,
+ bwd: &mut self.fwd,
+ }
+ }
+}
+
+/// Mutable view of a [`VarBiMap`].
+///
+/// Helper so `VarBiMap` mutating routines can work in both directions.
+pub struct VarBiMapMut<'a> {
+ fwd: &'a mut VarMap,
+ bwd: &'a mut VarMap,
+}
+
+impl<'a> VarBiMapMut<'a> {
+ /// Insert a new mapping.
+ ///
+ /// Note that the parameters are reversed from the usual order, to match the naming convention
+ /// used for maps.
+ ///
+ /// This has the precondition that `into` and `from` are not mapped.
+ pub fn insert(&mut self, into: Var, from: Var) {
+ self.fwd.insert(into, from);
+ self.bwd.insert(from, into);
+ }
+
+ /// Remove a mapping.
+ ///
+ /// Does nothing if `from` is not mapped.
+ ///
+ /// Returns the existing mapping if it was present.
+ pub fn remove(&mut self, from: Var) -> Option<Var> {
+ if let Some(into) = self.fwd.get(from) {
+ self.fwd.remove(from);
+ self.bwd.remove(into);
+ Some(into)
+ } else {
+ None
+ }
+ }
+}
diff --git a/vendor/varisat/tests/checker.rs b/vendor/varisat/tests/checker.rs
new file mode 100644
index 000000000..1a7fd428f
--- /dev/null
+++ b/vendor/varisat/tests/checker.rs
@@ -0,0 +1,193 @@
+//! Checker tests, that require a Solver instance, so they cannot be unit tests of the
+//! varisat-checker crate.
+
+use anyhow::Error;
+
+use proptest::prelude::*;
+
+use varisat::{
+ checker::{Checker, ProofTranscriptProcessor, ProofTranscriptStep},
+ dimacs::write_dimacs,
+ CnfFormula, ExtendFormula, Lit, ProofFormat, Solver, Var,
+};
+use varisat_formula::test::{conditional_pigeon_hole, sgen_unsat_formula};
+
+proptest! {
+ #[test]
+ fn checked_unsat_via_dimacs(formula in sgen_unsat_formula(1..7usize)) {
+ let mut dimacs = vec![];
+ let mut proof = vec![];
+
+ let mut solver = Solver::new();
+
+ write_dimacs(&mut dimacs, &formula).unwrap();
+
+ solver.write_proof(&mut proof, ProofFormat::Varisat);
+
+ solver.add_dimacs_cnf(&mut &dimacs[..]).unwrap();
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+
+ solver.close_proof().map_err(|e| TestCaseError::fail(e.to_string()))?;
+
+ drop(solver);
+
+ let mut checker = Checker::new();
+
+ checker.add_dimacs_cnf(&mut &dimacs[..]).unwrap();
+
+ checker.check_proof(&mut &proof[..]).unwrap();
+ }
+
+ #[test]
+ fn sgen_checked_unsat_incremental_clauses(formula in sgen_unsat_formula(1..7usize)) {
+ let mut proof = vec![];
+
+ let mut solver = Solver::new();
+ solver.write_proof(&mut proof, ProofFormat::Varisat);
+
+ let mut expected_models = 0;
+
+ // Add all clauses incrementally so they are recorded in the proof
+ solver.solve().unwrap();
+ expected_models += 1;
+
+ let mut last_state = Some(true);
+
+ for clause in formula.iter() {
+ solver.add_clause(clause);
+
+ let state = solver.solve().ok();
+ if state != last_state {
+ prop_assert_eq!(state, Some(false));
+ prop_assert_eq!(last_state, Some(true));
+ last_state = state;
+ }
+ if state == Some(true) {
+ expected_models += 1;
+ }
+ }
+
+ prop_assert_eq!(last_state, Some(false));
+
+ drop(solver);
+
+ #[derive(Default)]
+ struct FoundModels {
+ counter: usize,
+ unsat: bool,
+ }
+
+ impl ProofTranscriptProcessor for FoundModels {
+ fn process_step(
+ &mut self,
+ step: &ProofTranscriptStep,
+ ) -> Result<(), Error> {
+ if let ProofTranscriptStep::Model { .. } = step {
+ self.counter += 1;
+ } else if let ProofTranscriptStep::Unsat = step {
+ self.unsat = true;
+ }
+ Ok(())
+ }
+ }
+
+ let mut found_models = FoundModels::default();
+ let mut checker = Checker::new();
+ checker.add_transcript(&mut found_models);
+ checker.check_proof(&mut &proof[..]).unwrap();
+
+ prop_assert_eq!(found_models.counter, expected_models);
+ prop_assert!(found_models.unsat);
+ }
+
+ #[test]
+ fn pigeon_hole_checked_unsat_assumption_core(
+ (enable_row, columns, formula) in conditional_pigeon_hole(1..5usize, 1..5usize),
+ ) {
+ let mut proof = vec![];
+
+ let mut solver = Solver::new();
+ solver.write_proof(&mut proof, ProofFormat::Varisat);
+
+ let mut expected_sat = 0;
+ let mut expected_unsat = 0;
+
+ solver.solve().unwrap();
+ expected_sat += 1;
+ solver.add_formula(&formula);
+
+ prop_assert_eq!(solver.solve().ok(), Some(true));
+ expected_sat += 1;
+
+ let mut assumptions = enable_row;
+
+ assumptions.push(Lit::positive(Var::from_index(formula.var_count() + 10)));
+
+ solver.assume(&assumptions);
+
+ prop_assert_eq!(solver.solve().ok(), Some(false));
+ expected_unsat += 1;
+
+ let mut candidates = solver.failed_core().unwrap().to_owned();
+ let mut core: Vec<Lit> = vec![];
+
+ while !candidates.is_empty() {
+
+ solver.assume(&candidates[0..candidates.len() - 1]);
+
+ match solver.solve() {
+ Err(_) => unreachable!(),
+ Ok(true) => {
+ expected_sat += 1;
+ let skipped = *candidates.last().unwrap();
+ core.push(skipped);
+
+ let single_clause = CnfFormula::from(Some([skipped]));
+ solver.add_formula(&single_clause);
+ },
+ Ok(false) => {
+ expected_unsat += 1;
+ candidates = solver.failed_core().unwrap().to_owned();
+ }
+ }
+ }
+
+ prop_assert_eq!(core.len(), columns + 1);
+
+ drop(solver);
+
+ #[derive(Default)]
+ struct CountResults {
+ sat: usize,
+ unsat: usize,
+ }
+
+ impl ProofTranscriptProcessor for CountResults {
+ fn process_step(
+ &mut self,
+ step: &ProofTranscriptStep,
+ ) -> Result<(), Error> {
+ match step {
+ ProofTranscriptStep::Model { .. } => {
+ self.sat += 1;
+ }
+ ProofTranscriptStep::Unsat
+ | ProofTranscriptStep::FailedAssumptions { .. } => {
+ self.unsat += 1;
+ }
+ _ => (),
+ }
+ Ok(())
+ }
+ }
+
+ let mut count_results = CountResults::default();
+ let mut checker = Checker::new();
+ checker.add_transcript(&mut count_results);
+ checker.check_proof(&mut &proof[..]).unwrap();
+
+ prop_assert_eq!(count_results.sat, expected_sat);
+ prop_assert_eq!(count_results.unsat, expected_unsat);
+ }
+}
diff --git a/vendor/varisat/tests/cnfs.rs b/vendor/varisat/tests/cnfs.rs
new file mode 100644
index 000000000..8797c6596
--- /dev/null
+++ b/vendor/varisat/tests/cnfs.rs
@@ -0,0 +1,27 @@
+use std::collections::HashSet;
+
+use varisat::{solver::Solver, Lit};
+
+macro_rules! test_cnf {
+ ($name:ident, $result:expr) => {
+ #[test]
+ fn $name() {
+ let cnf = include_bytes!(concat!("cnfs/", stringify!($name), ".cnf"));
+ let mut solver = Solver::new();
+ solver.enable_self_checking();
+ let formula = varisat_dimacs::DimacsParser::parse(&cnf[..]).expect("parsing failed");
+ solver.add_formula(&formula);
+ let result = $result;
+ assert_eq!(solver.solve().expect("solve failed"), result);
+ if result {
+ let model: HashSet<Lit> = solver.model().unwrap().into_iter().collect();
+ for clause in formula.iter() {
+ assert!(clause.iter().any(|&lit| model.contains(&lit)));
+ }
+ }
+ }
+ };
+}
+
+test_cnf!(sgen1_unsat_57_0, false);
+test_cnf!(sgen1_sat_90_0, true);
diff --git a/vendor/varisat/tests/cnfs/sgen1_sat_90_0.cnf b/vendor/varisat/tests/cnfs/sgen1_sat_90_0.cnf
new file mode 100644
index 000000000..a465a7283
--- /dev/null
+++ b/vendor/varisat/tests/cnfs/sgen1_sat_90_0.cnf
@@ -0,0 +1,217 @@
+p cnf 90 216
+-1 -2 0
+-1 -3 0
+-1 -4 0
+-1 -5 0
+-2 -3 0
+-2 -4 0
+-2 -5 0
+-3 -4 0
+-3 -5 0
+-4 -5 0
+-6 -7 0
+-6 -8 0
+-6 -9 0
+-6 -10 0
+-7 -8 0
+-7 -9 0
+-7 -10 0
+-8 -9 0
+-8 -10 0
+-9 -10 0
+-11 -12 0
+-11 -13 0
+-11 -14 0
+-11 -15 0
+-12 -13 0
+-12 -14 0
+-12 -15 0
+-13 -14 0
+-13 -15 0
+-14 -15 0
+-16 -17 0
+-16 -18 0
+-16 -19 0
+-16 -20 0
+-17 -18 0
+-17 -19 0
+-17 -20 0
+-18 -19 0
+-18 -20 0
+-19 -20 0
+-21 -22 0
+-21 -23 0
+-21 -24 0
+-21 -25 0
+-22 -23 0
+-22 -24 0
+-22 -25 0
+-23 -24 0
+-23 -25 0
+-24 -25 0
+-26 -27 0
+-26 -28 0
+-26 -29 0
+-26 -30 0
+-27 -28 0
+-27 -29 0
+-27 -30 0
+-28 -29 0
+-28 -30 0
+-29 -30 0
+-31 -32 0
+-31 -33 0
+-31 -34 0
+-31 -35 0
+-32 -33 0
+-32 -34 0
+-32 -35 0
+-33 -34 0
+-33 -35 0
+-34 -35 0
+-36 -37 0
+-36 -38 0
+-36 -39 0
+-36 -40 0
+-37 -38 0
+-37 -39 0
+-37 -40 0
+-38 -39 0
+-38 -40 0
+-39 -40 0
+-41 -42 0
+-41 -43 0
+-41 -44 0
+-41 -45 0
+-42 -43 0
+-42 -44 0
+-42 -45 0
+-43 -44 0
+-43 -45 0
+-44 -45 0
+-46 -47 0
+-46 -48 0
+-46 -49 0
+-46 -50 0
+-47 -48 0
+-47 -49 0
+-47 -50 0
+-48 -49 0
+-48 -50 0
+-49 -50 0
+-51 -52 0
+-51 -53 0
+-51 -54 0
+-51 -55 0
+-52 -53 0
+-52 -54 0
+-52 -55 0
+-53 -54 0
+-53 -55 0
+-54 -55 0
+-56 -57 0
+-56 -58 0
+-56 -59 0
+-56 -60 0
+-57 -58 0
+-57 -59 0
+-57 -60 0
+-58 -59 0
+-58 -60 0
+-59 -60 0
+-61 -62 0
+-61 -63 0
+-61 -64 0
+-61 -65 0
+-62 -63 0
+-62 -64 0
+-62 -65 0
+-63 -64 0
+-63 -65 0
+-64 -65 0
+-66 -67 0
+-66 -68 0
+-66 -69 0
+-66 -70 0
+-67 -68 0
+-67 -69 0
+-67 -70 0
+-68 -69 0
+-68 -70 0
+-69 -70 0
+-71 -72 0
+-71 -73 0
+-71 -74 0
+-71 -75 0
+-72 -73 0
+-72 -74 0
+-72 -75 0
+-73 -74 0
+-73 -75 0
+-74 -75 0
+-76 -77 0
+-76 -78 0
+-76 -79 0
+-76 -80 0
+-77 -78 0
+-77 -79 0
+-77 -80 0
+-78 -79 0
+-78 -80 0
+-79 -80 0
+-81 -82 0
+-81 -83 0
+-81 -84 0
+-81 -85 0
+-82 -83 0
+-82 -84 0
+-82 -85 0
+-83 -84 0
+-83 -85 0
+-84 -85 0
+-86 -87 0
+-86 -88 0
+-86 -89 0
+-86 -90 0
+-87 -88 0
+-87 -89 0
+-87 -90 0
+-88 -89 0
+-88 -90 0
+-89 -90 0
+1 85 34 20 9 0
+6 46 59 82 30 0
+11 80 28 33 70 0
+47 17 36 41 35 0
+84 15 23 39 51 0
+21 42 54 29 77 0
+58 32 71 50 53 0
+7 37 55 78 88 0
+83 73 43 2 76 0
+89 25 48 18 67 0
+72 52 5 27 16 0
+56 8 44 63 69 0
+90 40 31 64 26 0
+24 3 68 38 57 0
+22 10 65 74 14 0
+62 49 4 79 13 0
+81 66 75 61 86 0
+60 87 19 45 12 0
+1 90 14 24 59 0
+6 78 53 57 72 0
+11 9 65 86 18 0
+82 17 13 35 38 0
+66 89 23 54 83 0
+69 50 15 29 71 0
+42 32 10 85 3 0
+2 37 70 8 63 0
+5 55 43 20 76 0
+36 88 48 45 75 0
+47 52 61 21 31 0
+56 67 46 19 39 0
+60 73 80 64 34 0
+77 25 68 12 41 0
+22 4 16 74 30 0
+27 84 49 79 7 0
+81 44 62 28 58 0
+26 87 51 40 33 0
diff --git a/vendor/varisat/tests/cnfs/sgen1_unsat_57_0.cnf b/vendor/varisat/tests/cnfs/sgen1_unsat_57_0.cnf
new file mode 100644
index 000000000..045a3c5da
--- /dev/null
+++ b/vendor/varisat/tests/cnfs/sgen1_unsat_57_0.cnf
@@ -0,0 +1,125 @@
+p cnf 57 124
+-2 -3 -4 0
+-1 -3 -4 0
+-1 -2 -4 0
+-1 -2 -3 0
+-6 -7 -8 0
+-5 -7 -8 0
+-5 -6 -8 0
+-5 -6 -7 0
+-10 -11 -12 0
+-9 -11 -12 0
+-9 -10 -12 0
+-9 -10 -11 0
+-14 -15 -16 0
+-13 -15 -16 0
+-13 -14 -16 0
+-13 -14 -15 0
+-18 -19 -20 0
+-17 -19 -20 0
+-17 -18 -20 0
+-17 -18 -19 0
+-22 -23 -24 0
+-21 -23 -24 0
+-21 -22 -24 0
+-21 -22 -23 0
+-26 -27 -28 0
+-25 -27 -28 0
+-25 -26 -28 0
+-25 -26 -27 0
+-30 -31 -32 0
+-29 -31 -32 0
+-29 -30 -32 0
+-29 -30 -31 0
+-34 -35 -36 0
+-33 -35 -36 0
+-33 -34 -36 0
+-33 -34 -35 0
+-38 -39 -40 0
+-37 -39 -40 0
+-37 -38 -40 0
+-37 -38 -39 0
+-42 -43 -44 0
+-41 -43 -44 0
+-41 -42 -44 0
+-41 -42 -43 0
+-46 -47 -48 0
+-45 -47 -48 0
+-45 -46 -48 0
+-45 -46 -47 0
+-50 -51 -52 0
+-49 -51 -52 0
+-49 -50 -52 0
+-49 -50 -51 0
+-53 -54 -55 0
+-53 -54 -56 0
+-53 -54 -57 0
+-53 -55 -56 0
+-53 -55 -57 0
+-53 -56 -57 0
+-54 -55 -56 0
+-54 -55 -57 0
+-54 -56 -57 0
+-55 -56 -57 0
+5 13 43 0
+32 13 43 0
+32 5 43 0
+32 5 13 0
+51 39 19 0
+10 39 19 0
+10 51 19 0
+10 51 39 0
+26 1 16 0
+11 1 16 0
+11 26 16 0
+11 26 1 0
+30 4 20 0
+34 4 20 0
+34 30 20 0
+34 30 4 0
+24 18 28 0
+8 18 28 0
+8 24 28 0
+8 24 18 0
+50 46 3 0
+41 46 3 0
+41 50 3 0
+41 50 46 0
+56 40 2 0
+6 40 2 0
+6 56 2 0
+6 56 40 0
+37 45 31 0
+27 45 31 0
+27 37 31 0
+27 37 45 0
+33 38 42 0
+22 38 42 0
+22 33 42 0
+22 33 38 0
+21 9 29 0
+55 9 29 0
+55 21 29 0
+55 21 9 0
+52 44 25 0
+54 44 25 0
+54 52 25 0
+54 52 44 0
+17 14 47 0
+57 14 47 0
+57 17 47 0
+57 17 14 0
+49 15 36 0
+23 15 36 0
+23 49 36 0
+23 49 15 0
+35 7 48 0
+35 7 53 0
+35 7 12 0
+35 48 53 0
+35 48 12 0
+35 53 12 0
+7 48 53 0
+7 48 12 0
+7 53 12 0
+48 53 12 0