Initial commit

.gitignore

@@ -0,0 +1 @@
+target/

Cargo.toml

@@ -0,0 +1,7 @@
+[workspace]
+members = ["cadical", "cadical-sys"]
+
+[profile.release]
+opt-level = 3
+codegen-units = 1
+panic = "abort"

LICENSE

@@ -0,0 +1,29 @@
+BSD 3-Clause License
+
+Copyright (c) 2020, Jiang Zhu
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -0,0 +1,24 @@
+Rust bindings to state of art SAT solvers
+================================================================================
+
+Back to summer of 2015, when I first met SAT solver, it's picosat written by
+Armin Biere and used in BugScope, I'm impressed by the beauty of SAT solver.
+And I'm also intrigued by Rust, which brings fancy state of art features that
+come from recent programming language research to system programming world. I
+believe Rust will make SAT solvers better. This project is my attempt to bring
+state of art SAT solver to Rust ecosystem with safe API.
+
+Currently, Armin Biere's Cadical is supported. You can find high-level binding
+[here](cadical) and raw binding [here](cadical-sys).
+
+
+TODO
+--------------------------------------------------------------------------------
+- support for minisat
+- and other SAT solvers that derived from minisat
+- Tseitin transformation?
+
+License
+--------------------------------------------------------------------------------
+BSD 3-Clause
+

cadical-sys/Cargo.toml

@@ -0,0 +1,12 @@
+[package]
+name = "cadical-sys"
+version = "0.1.0"
+authors = ["Jiang Zhu <[email protected]>"]
+edition = "2018"
+build = "build.rs"
+
+[lib]
+crate-type = ["lib"]
+
+[build-dependencies]
+cc = { version = "1.0", features = ["parallel"] }

cadical-sys/build.rs

@@ -0,0 +1,81 @@
+const LIB_PATH: &str = "cadical-rel-1.2.1/src";
+
+fn main() {
+    // delete ipasir.cpp cadical.cpp mobical.cpp
+    let src_files = [
+        "cadical-rel-1.2.1/src/analyze.cpp",
+        "cadical-rel-1.2.1/src/arena.cpp",
+        "cadical-rel-1.2.1/src/assume.cpp",
+        "cadical-rel-1.2.1/src/averages.cpp",
+        "cadical-rel-1.2.1/src/backtrack.cpp",
+        "cadical-rel-1.2.1/src/backward.cpp",
+        "cadical-rel-1.2.1/src/bins.cpp",
+        "cadical-rel-1.2.1/src/block.cpp",
+        "cadical-rel-1.2.1/src/ccadical.cpp",
+        "cadical-rel-1.2.1/src/checker.cpp",
+        "cadical-rel-1.2.1/src/clause.cpp",
+        "cadical-rel-1.2.1/src/collect.cpp",
+        "cadical-rel-1.2.1/src/compact.cpp",
+        "cadical-rel-1.2.1/src/condition.cpp",
+        "cadical-rel-1.2.1/src/config.cpp",
+        "cadical-rel-1.2.1/src/cover.cpp",
+        "cadical-rel-1.2.1/src/decide.cpp",
+        "cadical-rel-1.2.1/src/decompose.cpp",
+        "cadical-rel-1.2.1/src/deduplicate.cpp",
+        "cadical-rel-1.2.1/src/elim.cpp",
+        "cadical-rel-1.2.1/src/ema.cpp",
+        "cadical-rel-1.2.1/src/extend.cpp",
+        "cadical-rel-1.2.1/src/external.cpp",
+        "cadical-rel-1.2.1/src/file.cpp",
+        "cadical-rel-1.2.1/src/flags.cpp",
+        "cadical-rel-1.2.1/src/format.cpp",
+        "cadical-rel-1.2.1/src/gates.cpp",
+        "cadical-rel-1.2.1/src/instantiate.cpp",
+        "cadical-rel-1.2.1/src/internal.cpp",
+        "cadical-rel-1.2.1/src/limit.cpp",
+        "cadical-rel-1.2.1/src/logging.cpp",
+        "cadical-rel-1.2.1/src/lucky.cpp",
+        "cadical-rel-1.2.1/src/message.cpp",
+        "cadical-rel-1.2.1/src/minimize.cpp",
+        "cadical-rel-1.2.1/src/occs.cpp",
+        "cadical-rel-1.2.1/src/options.cpp",
+        "cadical-rel-1.2.1/src/parse.cpp",
+        "cadical-rel-1.2.1/src/phases.cpp",
+        "cadical-rel-1.2.1/src/probe.cpp",
+        "cadical-rel-1.2.1/src/profile.cpp",
+        "cadical-rel-1.2.1/src/proof.cpp",
+        "cadical-rel-1.2.1/src/propagate.cpp",
+        "cadical-rel-1.2.1/src/queue.cpp",
+        "cadical-rel-1.2.1/src/random.cpp",
+        "cadical-rel-1.2.1/src/reduce.cpp",
+        "cadical-rel-1.2.1/src/rephase.cpp",
+        "cadical-rel-1.2.1/src/report.cpp",
+        "cadical-rel-1.2.1/src/resources.cpp",
+        "cadical-rel-1.2.1/src/restart.cpp",
+        "cadical-rel-1.2.1/src/restore.cpp",
+        "cadical-rel-1.2.1/src/score.cpp",
+        "cadical-rel-1.2.1/src/signal.cpp",
+        "cadical-rel-1.2.1/src/solution.cpp",
+        "cadical-rel-1.2.1/src/solver.cpp",
+        "cadical-rel-1.2.1/src/stats.cpp",
+        "cadical-rel-1.2.1/src/subsume.cpp",
+        "cadical-rel-1.2.1/src/terminal.cpp",
+        "cadical-rel-1.2.1/src/ternary.cpp",
+        "cadical-rel-1.2.1/src/tracer.cpp",
+        "cadical-rel-1.2.1/src/transred.cpp",
+        "cadical-rel-1.2.1/src/util.cpp",
+        "cadical-rel-1.2.1/src/var.cpp",
+        "cadical-rel-1.2.1/src/version.cpp",
+        "cadical-rel-1.2.1/src/vivify.cpp",
+        "cadical-rel-1.2.1/src/walk.cpp",
+        "cadical-rel-1.2.1/src/watch.cpp",
+    ];
+    cc::Build::new()
+        .cpp(true)
+        .include(LIB_PATH)
+        .define("NDEBUG", None)
+        .define("NBUILD", None)
+        // .define("QUIET", None)
+        .files(src_files.iter())
+        .compile("cadical");
+}

cadical-sys/cadical-rel-1.2.1/BUILD.md

@@ -0,0 +1,72 @@
+# CaDiCaL Build
+
+Use `./configure && make` to configure and build `cadical` in the default
+`build` sub-directory.
+
+This will also build the library `libcadical.a` as well as the model based
+tester `mobical`:
+
+    build/cadical
+    build/mobical
+    build/libcadical.a
+
+The header file of the library is in
+
+    src/cadical.hpp
+
+The build process requires GNU make.  Using the generated `makefile` with
+GNU make compiles separate object files, which can be cached (for instance
+with `ccache`).  In order to force parallel build you can use the '-j'
+option either for 'configure' or with 'make'.  If the environment variable
+'MAKEFLAGS' is set, e.g., 'MAKEFLAGS=-j ./configure', the same effect
+is achieved and the generated makefile will use those flags.
+
+You might want to check out options of `./configure -h`, such as
+
+    ./configure -c # include assertion checking code
+
+    ./configure -l # include code to really see what the solver is doing
+
+    ./configure -a # both above and in addition `-g` for debugging.
+
+You can easily use multiple build directories, e.g.,
+
+    mkdir debug; cd debug; ../configure -g; make
+
+which compiles and builds a debugging version in the sub-directory `debug`,
+since `-g` was specified as parameter to `configure`.  The object files,
+the library and the binaries are all independent of those in the default
+build directory `build`.
+
+All source files reside in the `src` directory.  The library `libcadical.a`
+is compiled from all the `.cpp` files except `cadical.cpp` and
+`mobical.cpp`, which provide the applications, i.e., the stand alone solver
+`cadical` and the model based tester `mobical`.
+
+If you can not or do not want to rely on our `configure` script nor on our
+build system based on GNU `make`, then this is easily doable as follows.
+
+    mkdir build
+    cd build
+    for f in ../src/*.cpp; do g++ -O3 -DNDEBUG -DNBUILD -c $f; done
+    ar rc libcadical.a `ls *.o | grep -v ical.o`
+    g++ -O3 -DNDEBUG -DNBUILD -o cadical cadical.o -L. -lcadical
+    g++ -O3 -DNDEBUG -DNBUILD -o mobical mobical.o -L. -lcadical
+
+Note that application object files are excluded from the library.
+Of course you can use different compilation options as well.
+
+Since `build.hpp` is not generated in this flow the `-DNBUILD` flag is
+necessary though, which avoids dependency of `version.cpp` on `build.hpp`.
+Consequently you will only get very basic version information compiled into
+the library and binaries (guaranteed is in essence just the version number
+of the library).
+
+Further note that the `configure` script provides some feature checks and
+might generate additional compiler flags necessary for compilation.  You
+might need to set those yourself or just use a modern C++11 compiler.
+
+This manual build process using object files is fast enough in combination
+with caching solutions such as `ccache`.  But it lacks the ability of our
+GNU make solution to run compilation in parallel without additional parallel
+process scheduling solutions.

cadical-sys/cadical-rel-1.2.1/CONTRIBUTING

@@ -0,0 +1,4 @@
+At this point we want to keep complete ownership in one hand
+to particularly avoid any additional co-authorship claims.
+Thus please refrain from generating pull requests.  Use the issue
+tracker or send email to '[email protected]' instead.

cadical-sys/cadical-rel-1.2.1/LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2016-2019 Armin Biere, Johannes Kepler University Linz, Austria
+
+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.

cadical-sys/cadical-rel-1.2.1/README.md

@@ -0,0 +1,34 @@
+[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
+[![Build Status](https://travis-ci.org/arminbiere/cadical.svg?branch=master)](https://travis-ci.org/arminbiere/cadical)
+
+
+CaDiCaL Simplified Satisfiability Solver
+===============================================================================
+
+The original goal of the development of CaDiCaL was to obtain a CDCL solver,
+which is easy to understand and change, while at the same time not being
+much slower than other state-of-the-art CDCL solvers.  Originally we wanted
+to also radically simplify the design and internal data structures, but that
+goal was only achieved partially, at least for instance compared to
+Lingeling.
+
+However, the code is much better documented and on the other hand CaDiCaL
+actually became in general faster than Lingeling even though it is missing
+some preprocessors (mostly parity and cardinality constraint reasoning),
+which would be crucial to solve certain instances.
+
+Use `./configure && make` to configure and build `cadical` and the library
+`libcadical.a` in the default `build` sub-directory.  The header file of
+the library is [`src/cadical.hpp`](src/cadical.hpp) and includes an example
+for API usage.
+
+See [`BUILD.md`](BUILD.md) for options and more details related to the build
+process and [`test/README.md`](test/README.md) for testing the library and
+the solver.
+
+The solver has the following usage `cadical [ dimacs [ proof ] ]`.
+See `cadical -h` for more options.
+
+The latest version can be found at <http://fmv.jku.at/cadical>.
+
+Armin Biere

cadical-sys/cadical-rel-1.2.1/VERSION

@@ -0,0 +1 @@
+1.2.1