diff --git a/cadical/Cargo.toml b/cadical/Cargo.toml index d0f70274..636733ef 100644 --- a/cadical/Cargo.toml +++ b/cadical/Cargo.toml @@ -16,6 +16,10 @@ include = [ "/patches/", "/examples/", "/cpp-extension/", + "/cppsrc/src/", + "/cppsrc/README.md", + "/cppsrc/LICENSE", + "/cppsrc/VERSION", ] build = "build.rs" diff --git a/cadical/README.md b/cadical/README.md index a976758e..6ef0515a 100644 --- a/cadical/README.md +++ b/cadical/README.md @@ -21,12 +21,20 @@ Armin Biere's SAT solver [CaDiCaL](https://github.com/arminbiere/cadical) to be ## CaDiCaL Versions CaDiCaL versions can be selected via cargo crate features. -All CaDiCaL versions up to [Version 2.1.3](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.3) are available. -For the full list of versions and the changelog see [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases). +All CaDiCaL versions from +[Version 1.5.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.0) +up to +[Version 2.1.3](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.3) +are available. For the full list of versions and the changelog see +[the CaDiCaL releases](https://github.com/arminbiere/cadical/releases). Without any features selected, the newest version will be used. If conflicting CaDiCaL versions are requested, the newest requested version will be selected. +If the determined version is _not_ the newest available, and no custom source directory is +specified (see customization below), the CaDiCaL source code is downloaded at compile time, +which requires network access. + ## Customization In order to build a custom version of CaDiCaL, this crate supports two environment variables to diff --git a/cadical/build.rs b/cadical/build.rs index ec6a1039..85090442 100644 --- a/cadical/build.rs +++ b/cadical/build.rs @@ -44,6 +44,40 @@ enum Version { // Don't forget to update the crate documentation when adding a newer version } +/// Checks if the version was set manually via a feature +macro_rules! version_set_manually { + () => { + cfg!(any( + feature = "v2-1-3", + feature = "v2-1-2", + feature = "v2-1-1", + feature = "v2-1-0", + feature = "v2-0-0", + feature = "v1-9-5", + feature = "v1-9-4", + feature = "v1-9-3", + feature = "v1-9-2", + feature = "v1-9-1", + feature = "v1-9-0", + feature = "v1-8-0", + feature = "v1-7-5", + feature = "v1-7-4", + feature = "v1-7-3", + feature = "v1-7-2", + feature = "v1-7-1", + feature = "v1-7-0", + feature = "v1-6-0", + feature = "v1-5-6", + feature = "v1-5-5", + feature = "v1-5-4", + feature = "v1-5-3", + feature = "v1-5-2", + feature = "v1-5-1", + feature = "v1-5-0", + )) + }; +} + impl Version { fn determine() -> Self { if cfg!(feature = "v2-1-3") { @@ -181,13 +215,6 @@ fn main() { let version = Version::determine(); - if std::env::var("DOCS_RS").is_ok() { - // don't build c++ library on docs.rs due to network restrictions - // instead, only generate bindings from included header file - generate_bindings("cpp-extension/dummy-ccadical.h", version, &out_dir); - return; - } - #[cfg(all(feature = "quiet", feature = "logging"))] compile_error!("cannot combine cadical features quiet and logging"); @@ -216,7 +243,7 @@ fn main() { } } - let cadical_dir = get_cadical_dir(None); + let cadical_dir = get_cadical_dir(version, None); generate_bindings(&format!("{cadical_dir}/src/ccadical.h"), version, &out_dir); @@ -269,26 +296,36 @@ fn generate_bindings(header_path: &str, version: Version, out_dir: &str) { .expect("Could not write ffi bindings"); } -fn get_cadical_dir(remote: Option<(&str, &str, Version)>) -> String { - std::env::var("CADICAL_SRC_DIR").unwrap_or_else(|_| { - let out_dir = env::var("OUT_DIR").unwrap(); - let mut tmp = out_dir.clone(); - tmp.push_str("/cadical"); - if let Some((repo, branch, version)) = remote { - update_repo( - Path::new(&tmp), - repo, - branch, - version.reference(), - Path::new("patches").join(version.patch()), - ); +fn get_cadical_dir(version: Version, remote: Option<(&str, &str)>) -> String { + if let Ok(src_dir) = std::env::var("CADICAL_SRC_DIR") { + if version_set_manually!() { + println!("cargo:warning=Both version feature and CADICAL_SRC_DIR. It is your responsibility to ensure that they make sense together."); } - tmp - }) + return src_dir; + } + + if version == Version::default() { + // the sources for the default version are included with the crate and do not need to be + // cloned + return String::from("cppsrc"); + } + + let mut src_dir = env::var("OUT_DIR").unwrap(); + src_dir.push_str("/cadical"); + if let Some((repo, branch)) = remote { + update_repo( + Path::new(&src_dir), + repo, + branch, + version.reference(), + Path::new("patches").join(version.patch()), + ); + } + src_dir } fn build(repo: &str, branch: &str, version: Version) { - let cadical_dir_str = get_cadical_dir(Some((repo, branch, version))); + let cadical_dir_str = get_cadical_dir(version, Some((repo, branch))); let cadical_dir = Path::new(&cadical_dir_str); // We specify the build manually here instead of calling make for better portability let src_files = glob(&format!("{cadical_dir_str}/src/*.cpp")) @@ -313,13 +350,13 @@ fn build(repo: &str, branch: &str, version: Version) { .opt_level(0) .define("DEBUG", None) .warnings(true) - .debug(true) - .define("NCONTRACTS", None) // --no-contracts - .define("NTRACING", None); // --no-tracing + .debug(true); } else { cadical_build .opt_level(3) .define("NDEBUG", None) + .define("NCONTRACTS", None) // --no-contracts + .define("NTRACING", None) // --no-tracing .warnings(false); } #[cfg(feature = "quiet")] diff --git a/cadical/cpp-extension/dummy-ccadical.h b/cadical/cpp-extension/dummy-ccadical.h deleted file mode 100644 index 7a82f4cd..00000000 --- a/cadical/cpp-extension/dummy-ccadical.h +++ /dev/null @@ -1,72 +0,0 @@ -// This is a copy of the `ccadical.h` file of CaDiCaL, included to enable -// building the crate without network access, mainly on docs.rs - -#ifndef _ccadical_h_INCLUDED -#define _ccadical_h_INCLUDED - -/*------------------------------------------------------------------------*/ -#ifdef __cplusplus -extern "C" { -#endif -/*------------------------------------------------------------------------*/ - -#include -#include - -// C wrapper for CaDiCaL's C++ API following IPASIR. - -typedef struct CCaDiCaL CCaDiCaL; - -const char *ccadical_signature(void); -CCaDiCaL *ccadical_init(void); -void ccadical_release(CCaDiCaL *); - -void ccadical_add(CCaDiCaL *, int lit); -void ccadical_assume(CCaDiCaL *, int lit); -int ccadical_solve(CCaDiCaL *); -int ccadical_val(CCaDiCaL *, int lit); -int ccadical_failed(CCaDiCaL *, int lit); - -void ccadical_set_terminate(CCaDiCaL *, void *state, - int (*terminate)(void *state)); - -void ccadical_set_learn(CCaDiCaL *, void *state, int max_length, - void (*learn)(void *state, int *clause)); - -/*------------------------------------------------------------------------*/ - -// Non-IPASIR conformant 'C' functions. - -void ccadical_constrain(CCaDiCaL *, int lit); -int ccadical_constraint_failed(CCaDiCaL *); -void ccadical_set_option(CCaDiCaL *, const char *name, int val); -void ccadical_limit(CCaDiCaL *, const char *name, int limit); -int ccadical_get_option(CCaDiCaL *, const char *name); -void ccadical_print_statistics(CCaDiCaL *); -int64_t ccadical_active(CCaDiCaL *); -int64_t ccadical_irredundant(CCaDiCaL *); -int ccadical_fixed(CCaDiCaL *, int lit); -int ccadical_trace_proof(CCaDiCaL *, FILE *, const char *); -void ccadical_close_proof(CCaDiCaL *); -void ccadical_conclude(CCaDiCaL *); -void ccadical_terminate(CCaDiCaL *); -void ccadical_freeze(CCaDiCaL *, int lit); -int ccadical_frozen(CCaDiCaL *, int lit); -void ccadical_melt(CCaDiCaL *, int lit); -int ccadical_simplify(CCaDiCaL *); - -/*------------------------------------------------------------------------*/ - -// Support legacy names used before moving to more IPASIR conforming names. - -#define ccadical_reset ccadical_release -#define ccadical_sat ccadical_solve -#define ccadical_deref ccadical_val - -/*------------------------------------------------------------------------*/ -#ifdef __cplusplus -} -#endif -/*------------------------------------------------------------------------*/ - -#endif diff --git a/cadical/src/lib.rs b/cadical/src/lib.rs index f2fd6fd5..51f020bc 100644 --- a/cadical/src/lib.rs +++ b/cadical/src/lib.rs @@ -14,12 +14,20 @@ //! ## CaDiCaL Versions //! //! CaDiCaL versions can be selected via cargo crate features. -//! All CaDiCaL versions up to [Version 2.1.3](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.3) are available. -//! For the full list of versions and the changelog see [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases). +//! All CaDiCaL versions from +//! [Version 1.5.0](https://github.com/arminbiere/cadical/releases/tag/rel-1.5.0) +//! up to +//! [Version 2.1.3](https://github.com/arminbiere/cadical/releases/tag/rel-2.1.3) +//! are available. For the full list of versions and the changelog see +//! [the CaDiCaL releases](https://github.com/arminbiere/cadical/releases). //! //! Without any features selected, the newest version will be used. //! If conflicting CaDiCaL versions are requested, the newest requested version will be selected. //! +//! If the determined version is _not_ the newest available, and no custom source directory is +//! specified (see customization below), the CaDiCaL source code is downloaded at compile time, +//! which requires network access. +//! //! ## Customization //! //! In order to build a custom version of CaDiCaL, this crate supports two environment variables to diff --git a/cadical/test-all.sh b/cadical/test-all.sh index a5974360..d1adbbb3 100755 --- a/cadical/test-all.sh +++ b/cadical/test-all.sh @@ -2,145 +2,145 @@ echo "Testing default (newest) version" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test &> def-test.log +cargo nextest run &> def-test.log echo "Default (newest) test returned: $?" echo "Testing v1.5.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-0 &> v150-test.log +cargo nextest run --features=v1-5-0 &> v150-test.log echo "v1.5.0 test returned: $?" echo "Testing v1.5.1" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-1 &> v151-test.log +cargo nextest run --features=v1-5-1 &> v151-test.log echo "v1.5.1 test returned: $?" echo "Testing v1.5.2" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-2 &> v152-test.log +cargo nextest run --features=v1-5-2 &> v152-test.log echo "v1.5.2 test returned: $?" echo "Testing v1.5.3" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-3 &> v153-test.log +cargo nextest run --features=v1-5-3 &> v153-test.log echo "v1.5.3 test returned: $?" echo "Testing v1.5.4" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-4 &> v154-test.log +cargo nextest run --features=v1-5-4 &> v154-test.log echo "v1.5.4 test returned: $?" echo "Testing v1.5.5" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-5 &> v155-test.log +cargo nextest run --features=v1-5-5 &> v155-test.log echo "v1.5.5 test returned: $?" echo "Testing v1.5.6" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-5-6 &> v156-test.log +cargo nextest run --features=v1-5-6 &> v156-test.log echo "v1.5.6 test returned: $?" echo "Testing v1.6.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-6-0 &> v160-test.log +cargo nextest run --features=v1-6-0 &> v160-test.log echo "v1.6.0 test returned: $?" echo "Testing v1.7.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-7-0 &> v170-test.log +cargo nextest run --features=v1-7-0 &> v170-test.log echo "v1.7.0 test returned: $?" echo "Testing v1.7.1" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-7-1 &> v171-test.log +cargo nextest run --features=v1-7-1 &> v171-test.log echo "v1.7.1 test returned: $?" echo "Testing v1.7.2" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-7-2 &> v172-test.log +cargo nextest run --features=v1-7-2 &> v172-test.log echo "v1.7.2 test returned: $?" echo "Testing v1.7.3" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-7-3 &> v173-test.log +cargo nextest run --features=v1-7-3 &> v173-test.log echo "v1.7.3 test returned: $?" echo "Testing v1.7.4" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-7-4 &> v174-test.log +cargo nextest run --features=v1-7-4 &> v174-test.log echo "v1.7.4 test returned: $?" echo "Testing v1.7.5" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-7-5 &> v175-test.log +cargo nextest run --features=v1-7-5 &> v175-test.log echo "v1.7.5 test returned: $?" echo "Testing v1.8.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-8-0 &> v180-test.log +cargo nextest run --features=v1-8-0 &> v180-test.log echo "v1.8.0 test returned: $?" echo "Testing v1.9.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-9-0 &> v190-test.log +cargo nextest run --features=v1-9-0 &> v190-test.log echo "v1.9.0 test returned: $?" echo "Testing v1.9.1" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-9-1 &> v191-test.log +cargo nextest run --features=v1-9-1 &> v191-test.log echo "v1.9.1 test returned: $?" echo "Testing v1.9.2" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-9-2 &> v192-test.log +cargo nextest run --features=v1-9-2 &> v192-test.log echo "v1.9.2 test returned: $?" echo "Testing v1.9.3" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-9-3 &> v193-test.log +cargo nextest run --features=v1-9-3 &> v193-test.log echo "v1.9.3 test returned: $?" echo "Testing v1.9.4" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-9-4 &> v194-test.log +cargo nextest run --features=v1-9-4 &> v194-test.log echo "v1.9.4 test returned: $?" echo "Testing v1.9.5" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v1-9-5 &> v195-test.log +cargo nextest run --features=v1-9-5 &> v195-test.log echo "v1.9.5 test returned: $?" echo "Testing v2.0.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v2-0-0 &> v200-test.log +cargo nextest run --features=v2-0-0 &> v200-test.log echo "v2.0.0 test returned: $?" echo "Testing v2.1.0" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v2-1-0 &> v210-test.log +cargo nextest run --features=v2-1-0 &> v210-test.log echo "v2.1.0 test returned: $?" echo "Testing v2.1.1" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v2-1-1 &> v211-test.log +cargo nextest run --features=v2-1-1 &> v211-test.log echo "v2.1.1 test returned: $?" echo "Testing v2.1.2" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v2-1-2 &> v212-test.log +cargo nextest run --features=v2-1-2 &> v212-test.log echo "v2.1.2 test returned: $?" echo "Testing v2.1.3" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=v2-1-3 &> v213-test.log +cargo nextest run --features=v2-1-3 &> v213-test.log echo "v2.1.3 test returned: $?" echo "Testing quiet" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=quiet &> quiet-test.log +cargo nextest run --features=quiet &> quiet-test.log echo "quiet test returned: $?" echo "Testing logging" if [ "$1" == "--clean" ]; then cargo clean -p rustsat-cadical > /dev/null; fi -cargo test --features=logging &> logging-test.log +cargo nextest run --no-default-features --features=logging &> logging-test.log echo "logging test returned: $?"